Galois Announces Formal Specifications for Post-Quantum Cryptographic Algorithms

Galois has formally specified new algorithms recommended by the National Security Agency (NSA) for the Commercial National Security Algorithm Suite (CNSA 2.0). These post-quantum (PQ) cryptographic algorithms were previously approved by the National Institute of Standards and Technology (NIST).  

This work was part of the Quantum Secure Architectures Fit for Embedded devices (QSAFE) project, funded by DARPA’s Cryptography for Hyper-scale Architectures in a Robust Internet Of Things (CHARIOT) program. QSAFE’s overall goal is to secure Internet of Things (IoT) devices used for government and military applications. 

For the project, Galois partnered with PQSecure Technologies, a security solutions company in Florida specializing in quantum-safe cryptography solutions for small IoT devices. PQSecure implemented several “flavors” of low resource, side channel-free software and hardware implementations of the algorithms, such as AES, SHA-3, DILITHIUM, and XMMS. Galois complemented PQSecure’s efforts by spearheading research in the formal specification of the post-quantum algorithms, and demonstrating how those specifications can be used to assure implementations. Galois obtained the source documents from the algorithms’s authors to make the specifications as close to the original source as possible, then “wove” into them formal specifications written in Cryptol, turning them into “Literal Cryptol” specifications. 

Work based upon QSAFE will continue into the future. Many companies are implementing PQ algorithms now, and need to demonstrate to NIST, the NSA, and many branches of the DoD, that their implementations are correct. Galois will likely be involved in some of these efforts, and we hope that NIST uses our work to strengthen its CAVP and CMVP programs in the future.