E

ec-cryptobox

An EasyCrypt proof of security for NaCl's cryptobox construction (abstracting over the DH group and AE scheme), guided by the state-separating proof methodology.

A recipe book for turning SSPs into machine-checked proofs.