CSDL Home IEEE Transactions on Dependable and Secure Computing 2008 vol.5 Issue No.04 - October-December

Subscribe

Issue No.04 - October-December (2008 vol.5)

pp: 193-207

ABSTRACT

We present a new mechanized prover for secrecy properties of security protocols. In contrast to most previous provers, our tool does not rely on the Dolev-Yao model, but on the computational model. It produces proofs presented as sequences of games; these games are formalized in a probabilistic polynomial-time process calculus. Our tool provides a generic method for specifying security properties of the cryptographic primitives, which can handle shared-key and public-key encryption, signatures, message authentication codes, and hash functions. Our tool produces proofs valid for a number of sessions polynomial in the security parameter, in the presence of an active adversary. We have implemented our tool and tested it on a number of examples of protocols from the literature.

INDEX TERMS

C.2.2.c Protocol verification, F.3.1.d Mechanical verification, D.2.4.d Formal methods

CITATION

Bruno Blanchet, "A Computationally Sound Mechanized Prover for Security Protocols",

*IEEE Transactions on Dependable and Secure Computing*, vol.5, no. 4, pp. 193-207, October-December 2008, doi:10.1109/TDSC.2007.1005REFERENCES

- [1] M. Abadi and P. Rogaway, “Reconciling Two Views of Cryptography (The Computational Soundness of Formal Encryption),”
J.Cryptology, vol. 15, no. 2, pp. 103-127, 2002.- [2] M. Abadi and J. Jürjens, “Formal Eavesdropping and its Computational Interpretation,”
Proc. Fourth Int'l Symp. Theoretical Aspects of Computer Software (TACS '01), pp. 82-94, Oct. 2001.- [5] D. Micciancio and B. Warinschi, “Completeness Theorems for the Abadi-Rogaway Logic of Encrypted Expressions,”
J. Computer Security, vol. 12, no. 1, pp. 99-129, 2004.- [6] D. Micciancio and B. Warinschi, “Soundness of Formal Encryption in the Presence of Active Adversaries,”
Proc. First Theory of Cryptography Conf. (TCC '04), pp. 133-151, Feb. 2004.- [7] V. Cortier and B. Warinschi, “Computationally Sound Automated Proofs for Security Protocols,”
Proc. 14th European Symp. Programming (ESOP '05), pp. 157-171, Apr. 2005.- [8] R. Janvier, Y. Lakhnech, and L. Mazaré, “Completing the Picture: Soundness of Formal Encryption in the Presence of Active Adversaries,”
Proc. 14th European Symp. Programming (ESOP '05), pp. 172-185, Apr. 2005.- [9] M. Baudet, V. Cortier, and S. Kremer, “Computationally Sound Implementations of Equational Theories against Passive Adversaries,”
Proc. 32nd Int'l Colloquium Automata, Languages and Programming (ICALP '05), pp. 652-663, July 2005.- [10] P. Adão, G. Bana, J. Herzog, and A. Scedrov, “Soundness of Formal Encryption in the Presence of Key-Cycles,”
Proc. 10th European Symp. Research in Computer Security (ESORICS '05), pp.374-396, Sept. 2005.- [11] V. Shoup, “A Proposal for an ISO Standard for Public-Key Encryption,” ISO/IEC JTC 1/SC27, Dec. 2001.
- [14] P.D. Lincoln, J.C. Mitchell, M. Mitchell, and A. Scedrov, “A Probabilistic Poly-Time Framework for Protocol Analysis,”
Proc. Fifth ACM Conf. Computer and Comm. Security (CCS '98), pp. 112-121, Nov. 1998.- [15] P.D. Lincoln, J.C. Mitchell, M. Mitchell, and A. Scedrov, “Probabilistic Polynomial-Time Equivalence and Security Protocols,”
Proc. World Congress on Formal Methods in the Development of Computing Systems (FM '99), pp. 776-793, Sept. 1999.- [20] D.E. Knuth and P.B. Bendix, “Simple Word Problems in Universal Algebras,”
Computational Problems in Abstract Algebra, pp. 263-297, 1970.- [24] M. Bellare, A. Desai, D. Pointcheval, and P. Rogaway, “Relations among Notions of Security for Public-Key Encryption Schemes,”
Advances in Cryptology—Proc. 18th Ann. Int'l Cryptology Conf. (CRYPTO '98), pp. 26-45, Aug. 1998.- [26] M. Burrows, M. Abadi, and R. Needham, “A Logic of Authentication,”
Proc. Royal Soc. of London A, vol. 426, pp. 233-271, 1989.- [31] G. Lowe, “Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR,”
Proc. Second Int'l Workshop Tools and Algorithms for the Construction and Analysis of Systems (TACAS '96), pp. 147-166, 1996.- [32] M. Backes, B. Pfitzmann, and M. Waidner, “Symmetric Authentication Within a Simulatable Cryptographic Library,”
Computer Security—Proc. Eighth European Symp. Research in Computer Security (ESORICS '03), pp. 271-290, Oct. 2003.- [33] M. Backes and B. Pfitzmann, “Symmetric Encryption in a Simulatable Dolev-Yao Style Cryptographic Library,”
Proc. 17th IEEE Computer Security Foundations Workshop (CSFW-17), June 2004.- [37] R. Canetti and J. Herzog, “Universally Composable Symbolic Analysis of Mutual Authentication and Key Exchange Protocols,”
Proc. Third Theory of Cryptography Conf. (TCC '06), Mar. 2006.- [39] P. Mateus, J. Mitchell, and A. Scedrov, “Composition of Cryptographic Protocols in a Probabilistic Polynomial-Time Process Calculus,”
Proc. 14th Int'l Conf. Concurrency Theory (CONCUR '03), pp. 327-349, Sept. 2003.- [40] A. Ramanathan, J. Mitchell, A. Scedrov, and V. Teague, “Probabilistic Bisimulation and Equivalence for Security Analysis of Network Protocols,”
Proc. Seventh Int'l Conf. Foundations of Software Science and Computation Structures (FOSSACS '04), pp.468-483, Mar. 2004.- [41] A. Datta, A. Derek, J.C. Mitchell, V. Shmatikov, and M. Turuani, “Probabilistic Polynomial-Time Semantics for a Protocol Security Logic,”
Proc. 32nd Int'l Colloquium Automata, Languages and Programming (ICALP '05), pp. 16-29, July 2005.- [42] P. Laud, “Handling Encryption in an Analysis for Secure Information Flow,”
Programming Languages and Systems—Proc. 12th European Symp. Programming (ESOP '03), pp. 159-173, Apr. 2003.- [45] G. Barthe, J. Cederquist, and S. Tarento, “A Machine-Checked Formalization of the Generic Model and the Random Oracle Model,”
Proc. Second Int'l Joint Conf. Automated Reasoning (IJCAR '04), pp. 385-399, July 2004.- [46] S. Tarento, “Machine-Checked Security Proofs of Cryptographic Signature Schemes,”
Proc. 10th European Symp. Research in Computer Security (ESORICS '05), pp. 140-158, Sept. 2005.- [47] S. Halevi, “A Plausible Approach to Computer-Aided Cryptographic Proofs,”
Cryptology ePrint Archive, Report 2005/181, http://eprint.iacr.org/2005181, June 2005.- [48] B. Blanchet and D. Pointcheval, “Automated Security Proofs with Sequences of Games,”
Advances in Cryptology—Proc. 26th Ann. Int'l Cryptology Conf. (CRYPTO '06), pp. 537-554, Aug. 2006. |