Cryptol: The Language of Cryptography

What is Cryptol?

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.

View on GitHub Download

Core Features, Capabilities, and Applications

  • 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.

  • Formal Verification: Cryptol allows users to test and verify specifications, while SAW extends this capability to verify implementations written in C, Java, and Cryptol.

  • 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.

How Does It Work?

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.

READ OUR DOCUMENTATION

Impact

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.

Open Source

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.

View the Cryptol Specs Repository on Github

Last updated