Modular Code-Based Cryptographic Verification

CCS'11 paper (.pdf); Extended draft (.pdf); F#/F7 files (.tar); Coq/SSReflect proofs (.tar).

Related work on symbolic cryptographic verification