The Community for Technology Leaders
RSS Icon
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.1005
REFERENCES
[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.
24 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool