Intro to Cryptol and High Assurance Crypto Engineering
summary
Introduces Cryptol, a Haskell-like, pure functional language for bit-precise cryptographic code with size-polymorphic types and arithmetic predicates. Demonstrates implementing a classical cryptosystem, using QuickCheck-style fuzz testing and SMT/SAT solvers to express and verify correctness properties, and shows a Cryptol spec of the ZUC LTE stream cipher that revealed a real bug.
AI-written summary · about
related talks
39mKeynote: Towards High-Assurance Cryptographic Software
58mFast Cryptographic Code via Partial Evaluation
58mModern, Functional Cryptography (Part 6)
41mFormally Verifying Everybody's Cryptography
59mModern, Functional Cryptography (Part 3)
28mScalaZ and Cryptography
58mModern, Functional Cryptography (Part 1)
20mFixing the rusty core of the internet with functional prog.