Loading...
Loading...
Loading...
Loading...
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.
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 join here
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 GitHub, or send email to cryptol@galois.com.
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.
Read the Cryptol Blog
Read the latest articles about Cryptol
Cryptographic Specifications
Access the Cryptographic Library
Github
Explore the Github repository
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.
Cryptol binaries for Mac OS X, Linux, and Windows are available from the GitHub releases page. Binaries are distributed as tarballs which you can extract to a location of your choice. The 3.0.0 release also includes optional downloads including supported versions of several solvers.
GPG signatures are available for each release, and we encourage you to check the signature against our public key 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):
Cryptol currently depends on the Z3 SMT solver 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 releases page.
Cryptol generally requires the most recent version of Z3, but you can see the specific version tested in CI by looking here.
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 the solvers we use in CI and the SBV versions page.
Cryptol is licensed under a standard 3-clause BSD license.
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.
Browning, S. and Weaver, P. Designing Tunable, Verifiable Cryptographic Hardware Using Cryptol. In Design and Verification of Microprocessor Systems for High-Assurance, 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.
Levent Erkök, John Matthews. High assurance programming in Cryptol. In CSIIRW’09: Proceedings of the 5th Annual Workshop on Cyber Security and Information Intelligence Research, Oak Ridge, TN, April 2009, ACM.
Levent Erkök and John Matthews. Pragmatic Equivalence and Safety Checking in Cryptol. PLPV 2009: 73-81.
Lee Pike, Mark Shields, John Matthews: A verifying core for a cryptographic language compiler. ACL2 2006: 1-10.
Browse the Cryptol Reference Manual ->
Read our Programming Cryptol guide ->
Access the web-based Cryptol course ->