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.
