Information Security Seminar 

28/06/2010, 16:15 — 17:15 — Room P3.10, Mathematics Building
Gergei Bana, LSV and ENS-Cachan

Secrecy-Oriented, Computationally Sound First-Order LogicalAnalysis of Cryptographic Protocols

We present a computationally sound first-order system for security-analysis of protocols that places secrecy of nonces and keys in its center. Even trace properties such as agreement and authentication are proven via proving a non-trace property, namely, secrecy first with an inductive method. These security properties are derived directly from a set of computationally sound axioms, without the need to formalize adversarial capabilities explicitly. This results a very powerful system, the working of which we illustrate on the agreement and authentication proofs for the Needham-Schroeder-Lowe public-key and the amended Needham-Schroeder shared-key protocols in case of unlimited sessions. Unlike other available formal verification techniques, computational soundness of our approach does not require any idealizations about parsing of bitstrings or unnecessary tagging. In particular, we have control over detecting and eliminating the possibility of type-flaw attacks.