CTL
20 mai 2010 - 14h00
Secrecy-Oriented, Computationally Sound First-Order Logical Analysis of Cryptographic Protocols
par Gregei Bana de LSV ENS Cachan
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.
Les tranparents de la presentation.
