Cryptol: The Language of Cryptography
Last updated
Last updated
Cryptol is a mathematically-focused programming language for creating, analyzing, and verifying complex cryptographic algorithms. Intuitive, expressive, and precise, Cryptol and its associated software tools allow you to describe algorithms in the language of mathematics and prove key security and other properties.
Expressive Syntax: Cryptol’s high-level abstraction and intuitive syntax make it exceptionally expressive and ideal for rapid prototyping, refining, and analyzing cryptographic algorithms.
Executable Specifications: With Cryptol, users can create specifications that aren’t just theoretical models, but can be run as executable code.
Scalable Security: Cryptol and SAW automate much of the most time-consuming parts of formal verification, enabling the process to scale to complex systems
Open Source Library: Access specs for traditional and post-quantum cryptographic algorithms in our open source repository of Cryptol specifications.
Bridging the Gap: Cryptographic algorithms are typically represented in two forms: a non-executable mathematical notation for theoretical understanding (the “specification"), and a “reference implementation” for practical use. However, this approach presents a significant challenge: there isn’t an easy way to check the implementation against the mathematical specification to verify the correlation between the two and ensure it is correct and secure.
A New Paradigm: Cryptol revolutionizes this process in two key ways. First, it enables engineers to create specifications of cryptographic algorithms (e.g., to generate cryptographic keys, encryption/decryption algorithms, hashing functions, etc.) that are executable, testable, and verifiable. From those specifications, users can generate their own test vectors, prove theorems, and more. Second, using Galois’s Software Analysis Workbench (SAW), it’s possible to prove the equivalence of performant, manually-written implementations to specifications.
Cryptol and SAW have been used in national security, fintech, and cloud computing applications to keep citizens, systems, and data safe; secure financial transactions; and protect the privacy of millions of people across the globe. The high assurance approach they represent forms the backbone—both technologically and philosophically—of Galois’s larger effort to create trustworthiness in the most critical systems on the planet, and to maximize impact through sharing these powerful tools with the open source community.
The R&D community, industry, and the public at large can benefit when tools like Cryptol are open sourced. In addition, open-source tools can themselves benefit from and be independently verified by a broad, diverse user community. With this in mind, the U.S. Government and Galois agreed to open source Cryptol for broad application and public benefit, releasing the first fully public version in 2014. Now, Cryptol is open for anyone to use and explore, as is our open-source cryptographic library that includes specs for both traditional and post-quantum cryptographic algorithms.
Formal Verification: Cryptol allows users to test and verify specifications, while extends this capability to verify implementations written in C, Java, and Cryptol.
