We are pleased to announce the release of Cryptol 2.13.0. Cryptol is a language for writing and specifying cryptographic algorithms. This release brings a variety of improvements, including: The sortBy function is now implemented using merge sort instead of insertion sort. This improves both asymptotic and observed performance on sorting tasks. “Type mismatch” errors now […]

Field arithmetic code is important and has edge cases lurking everywhere. Cryptol is a tool that can guarantee you’ve got the edge cases right! In this post, we continue reproducing an NCC Group Post about programming in z3. In our last post, we checked the implementation of part of the QUIC protocol. Now we’ll explore […]

At Galois, we’ve run into NCC’s Cryptography Group numerous times, because Galois’ services and NCC’s complement each other extremely well. For example in the ‘blst’ cryptographic library project from Supranational, Ethereum Foundation, and Protocol Labs, NCC provided a public audit and report, while we at Galois have verified much of the core library. When I […]

This is the second in a series of three blog posts detailing the use of SAW and Cryptol to prove the correctness of the HMAC implementation in Amazon’s s2n TLS library. Part one: Verifying s2n HMAC with SAW. Part three: Proving Program Equivalence with SAW. In the first post, we described how we proved equivalence between a mathematical description […]

To commemorate the public release of the Software Analysis Workbench (SAW), it seemed fitting to blog about some recent work specifying algorithms in Cryptol and proving properties, leveraging SAW along the way. Cryptol, Galois’s domain specific language for describing cryptographic algorithms, has frequently been demonstrated over individual algorithms and toy problems. Our blog is covered […]

We are pleased to announce the open source release of Cryptol version 2.  Bugs in crypto code have been in the news lately – Cryptol helps developers detect (or avoid) correctness errors in cryptographic code. What Cryptol does is reduce the gap between the reference specification of a cryptographic algorithm and an executable version which […]

Last week, the NSA published two families of lightweight block ciphers, SIMON and SPECK: http://eprint.iacr.org/2013/404 We’ve formally specified both ciphers in Cryptol: https://github.com/GaloisInc/cryptol/blob/master/examples/contrib/simon.cry https://github.com/GaloisInc/cryptol/blob/master/examples/contrib/speck.cry The following sections explore some applications of our specifications. Parameters SIMON and SPECK are cipher families: each algorithm in the family offers different security and performance based on parameters such as […]

ZUC is a stream cipher that is proposed for inclusion in the “4G” mobile standard named LTE (Long Term Evolution), the future of secure GSM. The proposal is actually comprised several different algorithms: A stream cipher named ZUC, LTEencryption algorithm (128-EEA3), based on ZUC, LTEintegrity algorithm (128-EIA3), which is a hash function using ZUC as […]

During BelHac, the Ghent Haskell Hackathon in November, we took an afternoon session for a “Functional Programming in Industry” impromptu workshop. The following are slides I presented on Galois’ experience building a business using our functional programming expertise, in particular, Haskell. The talk describes three case studies where “functional thinking” helped shape the solution to […]

Galois is offering a four‐day Cryptol course for those interested in exploring the capabilities of the Cryptol workbench.The course is highly participatory: we will work on a series of exercises for each new topic, using the Cryptol toolset interactively. Prospective participants should have experience writing programs and some knowledge of cryptography. Those who complete the course will have the skills necessary to develop high‐assurance, high‐performance cryptographic algorithms in Cryptol. A tentative outline and further information can be found in the course flyer. Interested parties should contact Dr. Sally Browning via e-mail at sally@galois.com, or call her at (503) 808 7151.