Computational Soundness of Formal Security Protocol Analysis

Steve Kremer
CNRS, ENS Cachan, France
Friday, 15 February, 2008 (All day)

Formal verification of security protocols in so-called Dolev-Yao models has become common practice and recent tools are able to analyze complex, real-life case studies such as SSL and Kerberos. These methods have however been criticised because they make strong hypotheses on the underlying cryptgraphic primitives (often refered to as the perfect cryptography assumption).

In an influential paper, Abadi and Rogaway have shown that under standard cryptographic assumptions the abstractions on cryptographic primitives made in Dolev-Yao models are sound: formal security proofs imply security proofs in a detailed, computational model where adversaries are arbitrary probabilistic poly-time Turing Machines. In this talk I will first present the seminal result by Abadi and Rogaway. Then, I will present a general setting for reasoning about the soundness of abstract models where cryptographic primitives are specified by the means of equational theories. While the Abadi-Rogaway result only considers encryption and pairing, we are able to show soundness results for many more primitives including different encryption functions, exclusive or and modular exponentiation.

This talk covers material from:

  • [AR02] Martín Abadi and Phillip Rogaway. Reconciling Two Views of Cryptography (The Computational Soundness of Formal Encryption). J. Cryptology 15(2): 103-127, 2002.
  • [BCK05] Mathieu Baudet, Véronique Cortier and Steve Kremer. Computationally Sound Implementations of Equational Theories against Passive Adversaries. In Proceedings of the 32nd International Colloquium on Automata, Languages and Programming (ICALP'05), LNCS 3580, Springer, 2005.
  • [ABW06] Martín Abadi, Mathieu Baudet and Bogdan Warinschi. Guessing Attacks and the Computational Soundness of Static Equivalence. In Proceedings of the 9th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'06), LNCS 3921, Springer, 2006.
  • [KM07] Steve Kremer and Laurent Mazaré. Adaptive Soundness of Static Equivalence. In Proceedings of the 12th European Symposium on Research in Computer Security (ESORICS'07), LNCS 4734, Springer, 2007.