« Tech Talk: OpenTheory: Package Management for Higher Order Logic Theories | Main | Formal Methods in Use at Galois »

Cryptol, the language of cryptography, now available

Galois is pleased to announce that Cryptol, the language of cryptography, is now available to the public!Cryptol is a domain specific language for the design, implementation and verification of cryptographic algorithms, developed over the past decade by Galois for the United States National Security Agency. It has been used successfully in a number of projects, and is also in use at Rockwell Collins, Inc.

Domain-specific languages (DSLs) allow subject-matter experts to design solutions in using familiar concepts and constructs. Cryptol, as a DSL, allows domain experts in cryptography to design and implement cryptographic algorithms with a high degree of assurance in the correctness of their design, and at the same time, producing a high performance implementation of their algorithms.Cryptol allows a cryptographer to:

  • Create a reference specification and associated formal model.
  • Test the specification against published test vectors and formal assertions about state.
  • Quickly refine the specification, in Cryptol, to one or more implementations, trading off space, time, and other performance metrics.
  • Compile the implementation for multiple targets, including: C/C++, Haskell, and VHDL/Verilog.
  • Equivalence check an implementation against the reference specification, including implementations not produced by Cryptol.

The Cryptol site has further documentation and the full language specification. In this release, Galois has made a implementation of the Cryptol language available free of charge for non-commercial uses.

The trial version is available for Linux, MacOS, and Windows installations and can be downloaded at the Cryptol site. The trial version is meant for language exploration. It includes a Cryptol interpreter with QuickCheck capabilities, documentation, and examples. The open version does not compile to VHDL, C/C++, or Haskell, and does not produce the formal models used for equivalence checking.Cryptol is implemented in Haskell.

Contact Galois to obtain a full-featured version for evaluation.

Reader Comments (16)

Good job guys!

December 24, 2008 | Unregistered Commenteryav

If you want to run the cryptol interpreter, you might have to install some extra libraries. For Linux, libedit.so and libgmp.so.3, for example. And/or tweak the LD_LIBRARY_PATH, and/or create symbolic links... This needs to be documented or improved better, of course!

Feedback is welcome!

December 24, 2008 | Unregistered Commentermagnus

Certainly intriguing... is Cryptol 'plastic' enough to expand to cover the specification of quantum cryptographic protocols?

December 24, 2008 | Unregistered CommenterMeredith Gregory

Is it possible to get in pdf file ?

December 25, 2008 | Unregistered CommenterRobert

is it possible to get pdf file with Cryptol ?

December 25, 2008 | Unregistered CommenterRobert

If this was designed for the NSA don't you think there might be a back door for them. I would be cautious when using proprietary software. But what do I know.

December 26, 2008 | Unregistered CommenterThe Outlaw

Hi, Even when Cryptol looks interesting, to be a true cryptography language, there are many functions that are missing and there are limitations that should not be there. Just to name a few; There is no modular exponentiation (hey, there is not even an implementation of arbitrary length numbers). There are no built-in F(2^n) and F(p) functions/libraries needed for ECC.

December 26, 2008 | Unregistered CommenterLucas

Obviously, Lucas has no idea what he's talking about. He hasn't presented ANY factual evidence to support his claim.

December 26, 2008 | Unregistered CommenterHate Lucas

yes, clearly lucas is an idiot who hasn't a clue what he's talking about. why can't people resist the urge to talk about stuff they clearly don't understand.

December 26, 2008 | Unregistered Commentergaylucas

[...] Galois › Blog › Blog » Cryptol, the language of cryptography, now available Blogged with the Flock Browser [...]

December 26, 2008 | Unregistered Commenternetworkreading.com » Gal

What, no GPL??!

December 26, 2008 | Unregistered Commenterfoo

Wow! this certianly is a breakthrough for the community. if only they made a python version :)

anyway, check this out if you would like to see the problem here:


December 26, 2008 | Unregistered CommenterKenneth Reitz

Please use darker and clear fonts, somehow this light grey font strains my eyes.

December 26, 2008 | Unregistered CommenterAdisabledReader

[...] voor het publiek dat vroeger werd gebruikt door de NSA ( National Security Agency). Op een andere blog kan je een duidelijke uitleg vinden over die bepaalde taal, [...]

[...] Cryptol, the language of cryptography, now available [...]

[...] specific language for the design, implementation and verification of cryptographic algorithms, is now available to the public. Cryptol was originally designed for the NSA. It allows for a quick evaluation and continued [...]

PostPost a New Comment

Enter your information below to add a new comment.

My response is on my own website »
Author Email (optional):
Author URL (optional):
Some HTML allowed: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <code> <em> <i> <strike> <strong>