CCIS Seminar - Thursday 20 May 2010 - CTL
14:00:00 - Salle de CTL

Gregei Bana, LSV ENS Cachan

Secrecy-Oriented, Computationally Sound First-Order Logical Analysis of Cryptographic Protocols

Abstract: 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 pars- ing of bitstrings or unnecessary tagging. In particular, we have control over detecting and eliminating the possibility of type-flaw attacks.

Home page CCIS Seminars
How to come to CTL -