Cryptol is an open source project, hosted on GitHub, licensed under the three-clause BSD license. We believe that anyone who uses Cryptol is making an important contribution toward making Cryptol better. There are many ways to get involved.

Explore

How to Contribute

Users

If you write Cryptol programs that you think would benefit the community, fork the GitHub repository, and add them to the examples/contrib directory and submit a pull request.

We host a Cryptol mailing list, which you can

If you run into a bug in Cryptol, if something doesn’t make sense in the documentation, if you think something could be better, or if you just have a cool use of Cryptol that you’d like to share with us, use the issues page on , or send email to [email protected].

Developers

If you plan to do development work on the Cryptol interpreter, please make a fork of the GitHub repository and send along pull requests. This makes it easier for us to track development and to incorporate your changes.

Reference Materials

Publications

Some of the material below was created for an earlier version of Cryptol. While the core ideas still apply to the current version, there have been some syntactic changes to the language, so some of the examples need to be translated to the current version.

Case Studies and White Papers

Research Publications

• Browning, S. and Weaver, P. Designing Tunable, Verifiable Cryptographic Hardware Using Cryptol. In , David S. Hardin, Editor. Springer 2010.

• Colby Hoffman, Jeff Lewis, Brad Martin, Sally Browning, A Complete Design Flow for MILS in a Single High Assurance FPGA, European Reconfigurable Radio Technologies Workshop, 2010.

• Levent Erkök, Magnus Carlsson, and Adam Wick. Hardware/Software Co-verification of Cryptographic Algorithms using Cryptol. In Formal Methods in Computer Aided Design Conference, FMCAD’09, Austin, TX, November 2009, IEEE.

Download a Binary

• Linux (Ubuntu 22.04) (GPG Signature)

• ()

• ()

• ()

• ()

Cryptol binaries for Mac OS X, Linux, and Windows are available from the . Binaries are distributed as tarballs which you can extract to a location of your choice. The 3.x releases also include including supported versions of several solvers.

GPG signatures are available for each release, and we encourage you to against our before installing to ensure the integrity of the release you downloaded.

Cryptol is also packaged using Docker and can be fetched using one of the following commands (for the REPL and RPC server, respectively):

Getting Z3

Cryptol currently depends on the to solve constraints during typechecking, and as the default solver for the :sat and :prove commands. You can download Z3 binaries for a variety of platforms from their .

Cryptol generally requires the most recent version of Z3, but you can see the specific version tested in CI by looking .

Getting other SMT Solvers

Cryptol also integrates with the Yices, Boolector, CVC4, CVC5, and other SMT solvers. If you download and install them, you can select which one Cryptol uses as follows: :set prover=cvc4, :set prover=yices, etc. For a list of currently-supported solvers, see and the .

Licensing Terms

Cryptol is licensed under a standard .

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 extends this capability to verify implementations written in C, Java, and Cryptol.

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.

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.