Galois and our partners have been using Cryptol as a platform for active research for over a decade.
Download Programming Cryptol Book PDF
Our goal in Programming Cryptol is to both teach you the Cryptol language and provide a reference text for the use of the Cryptol system.
We demonstrate Cryptol in action via normal programming problems, traditional cryptographic techniques (such as substitution ciphers), historical cryptographic mechanisms (such as the Enigma), and modern algorithms (such as DES, SHA, and AES), focusing on how they are elegantly modeled using the Cryptol language.
Since our emphasis is on programming, we introduce some of the techniques that are useful for the working programmer, including the use of Cryptol’s validation and verification tools that directly support high-assurance programming.
A summary of the changes made in Cryptol version 2.
Some of the material below refers to details and capabilities of Cryptol version 1 that are not yet available in Cryptol version 2.
Empowering the Experts: High-Assurance, High-Performance, High-Level Design with Cryptol
Domain Specific Languages: A path to high assurance solutions
CRYPTOL: High Assurance, Retargetable Crypto Development and Validation
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.