This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
A Computationally Sound Mechanized Prover for Security Protocols
October-December 2008 (vol. 5 no. 4)
pp. 193-207
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.

[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.
[3] M. Backes, B. Pfitzmann, and M. Waidner, “A Composable Cryptographic Library with Nested Operations,” Proc. 10th ACM Conf. Computer and Comm. Security (CCS '03), pp. 220-230, Oct. 2003.
[4] J. Herzog, “A Computational Interpretation of Dolev-Yao Adversaries,” Theoretical Computer Science, vol. 340, pp. 57-81, June 2005.
[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.
[12] V. Shoup, “OAEP Reconsidered,” J. Cryptology, vol. 15, no. 4, pp.223-249, Sept. 2002.
[13] M. Bellare and P. Rogaway, “The Security of Triple Encryption and a Framework for Code-Based Game-Playing Proofs,” Advances in Cryptology—Proc. 25th Int'l Conf. Theory and Applications of Cryptographic Techniques (EUROCRYPT '06), pp. 409-426, May 2006.
[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.
[16] J.C. Mitchell, A. Ramanathan, A. Scedrov, and V. Teague, “A Probabilistic Polynomial-Time Calculus for the Analysis of Cryptographic Protocols,” Theoretical Computer Science, vol. 353, nos. 1-3, pp. 118-164, Mar. 2006.
[17] P. Laud, “Secrecy Types for a Simulatable Cryptographic Library,” Proc. 12th ACM Conf. Computer and Comm. Security (CCS '05), pp. 26-35, Nov. 2005.
[18] M. Bellare, J. Kilian, and P. Rogaway, “The Security of the Cipher Block Chaining Message Authentication Code,” J. Computer and System Sciences, vol. 61, no. 3, pp. 362-399, Dec. 2000.
[19] M. Bellare, A. Desai, E. Jokipii, and P. Rogaway, “A Concrete Security Treatment of Symmetric Encryption,” Proc. 38th Symp. Foundations of Computer Science (FOCS '97), pp. 394-403, Oct. 1997.
[20] D.E. Knuth and P.B. Bendix, “Simple Word Problems in Universal Algebras,” Computational Problems in Abstract Algebra, pp. 263-297, 1970.
[21] M. Abdalla, P.-A. Fouque, and D. Pointcheval, “Password-Based Authenticated Key Exchange in the Three-Party Setting,” Proc. IEE Information Security, vol. 153, no. 1, pp. 27-39, Mar. 2006.
[22] B. Blanchet, “Computationally Sound Mechanized Proofs of Correspondence Assertions,” Proc. 20th IEEE Computer Security Foundations Symp. (CSF '07), pp. 97-111, July 2007.
[23] T.Y.C. Woo and S.S. Lam, “A Semantic Model for Authentication Protocols,” Proc. 14th IEEE Symp. Security and Privacy (SP '93), pp.178-194, May 1993.
[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.
[25] D. Otway and O. Rees, “Efficient and Timely Mutual Authentication,” Operating Systems Rev., vol. 21, no. 1, pp. 8-10, 1987.
[26] M. Burrows, M. Abadi, and R. Needham, “A Logic of Authentication,” Proc. Royal Soc. of London A, vol. 426, pp. 233-271, 1989.
[27] R.M. Needham and M.D. Schroeder, “Using Encryption for Authentication in Large Networks of Computers,” Comm. ACM, vol. 21, no. 12, pp. 993-999, Dec. 1978.
[28] R.M. Needham and M.D. Schroeder, “Authentication Revisited,” Operating Systems Rev., vol. 21, no. 1, p. 7, 1987.
[29] D.E. Denning and G.M. Sacco, “Timestamps in Key Distribution Protocols,” Comm. ACM, vol. 24, no. 8, pp. 533-536, Aug. 1981.
[30] M. Abadi and R. Needham, “Prudent Engineering Practice for Cryptographic Protocols,” IEEE Trans. Software Eng., vol. 22, no. 1, pp. 6-15, Jan. 1996.
[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.
[34] M. Backes and B. Pfitzmann, “Relating Symbolic and Cryptographic Secrecy,” IEEE Trans. Dependable and Secure Computing, vol. 2, no. 2, pp. 109-123, Apr.-June 2005.
[35] C. Sprenger, M. Backes, D. Basin, B. Pfitzmann, and M. Waidner, “Cryptographically Sound Theorem Proving,” Proc. 19th IEEE Computer Security Foundations Workshop (CSFW-19), pp. 153-166, July 2006.
[36] R. Canetti, “Universally Composable Security: A New Paradigm for Cryptographic Protocols,” Proc. 42nd Ann. Symp. Foundations of Computer Science (FOCS '01), pp. 136-145, Oct. 2001.
[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.
[38] B. Blanchet, “Automatic Proof of Strong Secrecy for Security Protocols,” Proc. 25th IEEE Symp. Security and Privacy (SP '04), pp.86-100, May 2004.
[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.
[43] P. Laud, “Symmetric Encryption in Automatic Analyses for Confidentiality against Active Adversaries,” Proc. 25th IEEE Symp. Security and Privacy (SP '04), pp. 71-85, May 2004.
[44] M. Backes and P. Laud, “Computationally Sound Secrecy Proofs by Mechanized Flow Analysis,” Proc. 13th ACM Conf. Computer and Comm. Security (CCS '06), pp. 370-379, Nov. 2006.
[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.

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, Oct.-Dec. 2008, doi:10.1109/TDSC.2007.1005
Usage of this product signifies your acceptance of the Terms of Use.