Real World Crypto 2021 - Session 10: Formal Analysis
Session video
Kevin Liao (MIT) / SoK: Computer-Aided Cryptography / paper video
HACLxN - verified generic SIMD crypto: used to prove functional correctness for OpenSSL
Formal models != real world: design-level security, functional correctness, implementation-level security all differ, due to simplicfications, unaccounted side-channels, difference between what was verified and final machine code…
Computer-aided crypto aims to close those gaps.
Nadim Kobeissi (NGIzero/nlnet) / Verifpal: Cryptographic Protocol Analysis for the Real World / verifpal.com paper video slides
F* has been used to prove e.g. Signal protocol to be functionally correct
ProVerif, Tamarin, CryptoVerif: these approaches make models of protocols
Symbolic Model (idealised black boxes, fully automated) v.s. Computational Model (more nuanced, manually assisted).
Seems Legit: Automated Analysis of subtle attacks on protocols that use signatures (Katriel Cohn-Gordon, Cas Cremers)
ProVerif and Tamarin both require very opaque looking code, hard to get into. Do they have to be that hard? Author says, yes, they do really. But maybe a new language could be easier to read and write ==> Verifpal. It is intended for students or engineers to use, to be accessible, but is not as formally proven as the other two tools.
VerifPal makes modeling protocols very readable, and generates readable diagrams. You have to use primitives out of the box, can’t define new ones (use the more ‘pro’ tools if you have to do that). It’s great for getting meaningful feedback early in a design phase, for little investment. It’s also great for teaching.
There’s VerifPal for VS Code!
See also: VerifPal Heroes: a book and online guide to protocal verification