Output details
11 - Computer Science and Informatics
University of Edinburgh
Modular verification of security protocol code by typing
<10> Originality: Paper introduces modular technique of invariants for cryptographic structures for verifying cryptographic code.
Significance: Analyzes richer range of cryptographic primitives (including hybrid encryption) than previous work with F7, hence allowing F7 to beat close competitor in area (fs2pv plus ProVerif). Associated software, download site, and users:
F7 (version 2.0)
http://research.microsoft.com/en-us/downloads/c0c4ed53-cfd8-4b9c-b780-74946bd1337e/
1120 downloads (version 2.0)
Rigour: The paper includes formal correctness proofs, and also evaluation of the method on over 5000 LOC, and shows an order of magnitude performance improvement over closest competitor. Acceptance rate of POPL 2010 is 19%.