Relating cryptography and formal methods: a panel

ABSTRACT

Bridging the gap between formal methods and cryptography has recently received a lot of interest, i.e., investigating to what extent proofs of cryptographic protocols made with abstracted cryptographic operations are valid for real implementations. This led to the notion of cryptographically faithful (sound) abstractions. These abstractions allow for a provably secure cryptographic implementation; however their incorporation into machine-aided verification of security protocols has not been properly adressed yet. The panel should serve as an opportunity to discuss the current state-of-the-art in this area of research as well as the suitability of these abstractions for tool-supported verification of cryptographic protocols. We hope that the discussion will shed light on how far both communities are still apart.

REFERENCES

• 1: Martín Abadi , Andrew D. Gordon, A calculus for cryptographic protocols, Information and Computation, v.148 n.1, p.1-70, Jan. 10, 1999 [doi>10.1006/inco.1998.2740]
• 2: Martín Abadi , Jan Jürjens, Formal Eavesdropping and Its Computational Interpretation, Proceedings of the 4th International Symposium on Theoretical Aspects of Computer Software, p.82-94, October 29-31, 2001
• 3: M. Abadi and P. Rogaway. Reconciling two views of cryptography (the computational soundness of formal encryption). J. Cryptology, 15(2):103-127, 2002.
• 4: G. Ateniese, M. Steiner, and G. Tsudik. New multiparty authentication services and agreement protocols. IEEE Journal on Selected Areas in Communications, 18(4), April 2000.
• 5: M. Backes. Unifying simulatability definitions under different timing assumptions (extended abstract). In Proc. 14th International Conference on Concurrency Theory (CONCUR), Springer, 2003. Extended version in Cryptology ePrint Archive, Report 2003/114, http://eprint.iacr.org/.
• 6: Michael Backes , Christian Jacobi, II, Cryptographically Sound and Machine-Assisted Verification of Security Protocols, Proceedings of the 20th Annual Symposium on Theoretical Aspects of Computer Science, p.675-686, February 27-March 01, 2003
• 7: Michael Backes , Birgit Pfitzmann, Computational Probabilistic Non-interference, Proceedings of the 7th European Symposium on Research in Computer Security, p.1-23, October 14-16, 2002
• 8: M. Backes and B. Pfitzmann. A cryptographically sound security proof of the Needham-Schroeder-Lowe public-key protocol. In Proc. 23rd Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS), 2003.
• 9: Michael Backes , Birgit Pfitzmann, Intransitive Non-Interference for Cryptographic Purposes, Proceedings of the 2003 IEEE Symposium on Security and Privacy, p.140, May 11-14, 2003
• 10: Michael Backes , Birgit Pfitzmann , Michael Steiner , Michael Waidner, Polynomial Fairness and Liveness, Proceedings of the 15th IEEE Computer Security Foundations Workshop (CSFW'02), p.160, June 24-26, 2002
• 11: M. Backes, B. Pfitzmann, and M. Waidner. Symmetric authentication within a simulatable cryptographic library. In Proc. 8th European Symposium on Research in Computer Security (ESORICS), Springer, 2003. Extended version in Cryptology ePrint Archive, Report 2003/145, http://eprint.iacr.org/.
• 12: Michael Backes , Birgit Pfitzmann , Michael Waidner, A composable cryptographic library with nested operations, Proceedings of the 10th ACM conference on Computer and communications security, October 27-30, 2003, Washington D.C., USA [doi>10.1145/948109.948140]
• 13: Mihir Bellare , Phillip Rogaway, Provably secure session key distribution: the three party case, Proceedings of the twenty-seventh annual ACM symposium on Theory of computing, p.57-66, May 29-June 01, 1995, Las Vegas, Nevada, United States [doi>10.1145/225058.225084]
• 14: R. Canetti, Universally Composable Security: A New Paradigm for Cryptographic Protocols, Proceedings of the 42nd IEEE symposium on Foundations of Computer Science, p.136, October 14-17, 2001
• 15: Ran Canetti , Hugo Krawczyk, Universally Composable Notions of Key Exchange and Secure Channels, Proceedings of the International Conference on the Theory and Applications of Cryptographic Techniques: Advances in Cryptology, p.337-351, May 02, 2002
• 16: R. Canetti and T. Rabin. Universal composition with joint state. In Crypto, 2003.
• 17: I. Cervesato , N. A. Durgin , P. D. Lincoln , J. C. Mitchell , A. Scedrov, A Meta-Notation for Protocol Analysis, Proceedings of the 1999 IEEE Computer Security Foundations Workshop, p.55, June 28-30, 1999
• 18: Y. Chevalier, R. Küsters, M. Rusinowitch, and M. Turuani. Deciding the security of protocols with Diffie-Hellman exponentiation and products in exponents. In 23rd Conf. Foundations of Software Technology and Theoretical Computer Science, 2003.
• 19: Yannick Chevalier , Ralf Küsters , Michaël Rusinowitch , Mathieu Turuani, An NP Decision Procedure for Protocol Insecurity with XOR, Proceedings of the 18th Annual IEEE Symposium on Logic in Computer Science, p.261, June 22-25, 2003
• 20: H. Comon-Lundh , V. Shmatikov, Intruder Deductions, Constraint Solving and Insecurity Decision in Presence of Exclusive or, Proceedings of the 18th Annual IEEE Symposium on Logic in Computer Science, p.271, June 22-25, 2003
• 21: Danny Dolev , Cynthia Dwork , Moni Naor, Non-malleable cryptography, Proceedings of the twenty-third annual ACM symposium on Theory of computing, p.542-552, May 05-08, 1991, New Orleans, Louisiana, United States [doi>10.1145/103418.103474]
• 22: D. Dolev, S. Even, and R. Karp. On the security of ping-pong protocols. Information and Control, 55:57-68, 1982.
• 23: D. Dolev and A. Yao. On the security of public-key protocols. IEEE Transactions on Information Theory, 2(29):198-208, 1983.
• 24: F. J. T. Fábrega, J. C. Herzog, and J. D. Guttman. Strand spaces: Why is a security protocol correct? In Proceedings of the 1998 IEEE Symposium on Security and Privacy, pages 160-171, 1998.
• 25: R. Gennaro and S. Micali. Verifiable secret sharing as secure computation. In Advances in Cryptology: EUROCRYPT '95, volume 921 of Lecture Notes in Computer Science, pages 168-182. Springer, 1995.
• 26: James Heather , Gavin Lowe , Steve Schneider, How to Prevent Type Flaw Attacks on Security Protocols, Proceedings of the 13th IEEE Computer Security Foundations Workshop (CSFW'00), p.255, July 03-05, 2000
• 27: J. Herzog. The Diffie-Hellman key-agreement scheme in the strand-space model. In Proc. IEEE Computer Security Foundations Workshop (CFSW), Pacific Grove, California, pages 234-247, 2003.
• 28: R. Impagliazzo and B. Kapron. Logics for reasoning about cryptographic constructions, 2003. See http://www.csr.uvic.ca/~bmkapron/bibl.html.
• 29: P. Lincoln , J. Mitchell , M. Mitchell , A. Scedrov, A probabilistic poly-time framework for protocol analysis, Proceedings of the 5th ACM conference on Computer and communications security, p.112-121, November 02-05, 1998, San Francisco, California, United States [doi>10.1145/288090.288117]
• 30: Patrick Lincoln , John C. Mitchell , Mark Mitchell , Andre Scedrov, Probabilistic Polynomial-Time Equivalence and Security Analysis, Proceedings of the Wold Congress on Formal Methods in the Development of Computing Systems-Volume I, p.776-793, September 20-24, 1999
• 31: Gavin Lowe, Casper: A Compiler for the Analysis of Security Protocols, Proceedings of the 10th Computer Security Foundations Workshop (CSFW '97), p.18, June 10-12, 1997
• 32: P. Mateus, J. Mitchell, and A. Scedrov. Composition of cryptographic protocols in a probabilistic polynomial-time process calculus. In 14th International Conference on Concurrency Theory (CONCUR), 2003.
• 33: C. Meadows. Applying formal methods to the analysis of a key management protocol. Journal of Computer Security, 1(1):5-35, 1992.
• 34: C. Meadows. The NRL protocol analyzer: an overview. J. Logic Programming, 26(2):113-131, 1996.
• 35: Catherine Meadows , Paul Syverson , Iliano Cervesato, Formal specification and analysis of the group domain of interpretation protocol using NPATRL and the NRL protocol analyzer, Journal of Computer Security, v.12 n.6, p.893-931, December 2004
• 36: D. Micciancio and B. Warinschi. Completeness theorems for the Abadi-Rogaway language of encrypted expressions. 2003. J. Cryptology, to appear. Preliminary version in Workshop on Issues in the Theory of Security (WITS'02), Portland, Oregon, January 14-15, 2002. See http://www-cse.ucsd.edu/~bogdan/research.html.
• 37: J. Millen. CAPSL: Common authentication protocol specification language. Technical Report MP 97B48, The MITRE Corporation, 1997.
• 38: Jonathan Millen, On the freedom of decryption, Information Processing Letters, v.86 n.6, p.329-333, 30 June 2003 [doi>10.1016/S0020-0190(03)00211-4]
• 39: J. Millen and V. Shmatikov. Symbolic protocol analysis with products and Diffie-Hellman exponentiation. In Proc. IEEE Computer Science Foundation Workshop (CFSW), pages 47-61, 2003.
• 40: J. Mitchell , M. Mitchell , A. Scedrov, A Linguistic Characterization of Bounded Oracle Computation and Probabilistic Polynomial Time, Proceedings of the 39th Annual Symposium on Foundations of Computer Science, p.725, November 08-11, 1998
• 41: J. Mitchell, A. Ramanathan, V. Teague, and A. Scedrov. A probabilistic polynomial-time calculus for the analysis of cryptographic protocols. In 17th Annual Conference on the Mathematical Foundations of Programming Semantics, 2001. Electronic Notes in Theoretical Computer Science, Volume 45.
• 42: B. Pfitzmann, M. Schunter, and M. Waidner. Provably secure certified mail. Research Report RZ 3207, IBM Research, 2000.
• 43: B. Pfitzmann, M. Schunter, and M. Waidner. Secure reactive systems. Research Report RZ 3206, IBM Research, 2000.
• 44: Birgit Pfitzmann , Michael Waidner, Composition and integrity preservation of secure reactive systems, Proceedings of the 7th ACM conference on Computer and communications security, p.245-254, November 01-04, 2000, Athens, Greece [doi>10.1145/352600.352639]
• 45: Birgit Pfitzmann , Michael Waidner, A Model for Asynchronous Reactive Systems and its Application to Secure Message Transmission, Proceedings of the 2001 IEEE Symposium on Security and Privacy, p.184, May 14-16, 2001
• 46: A. W. Roscoe, Modelling and verifying key-exchange protocols using CSP and FDR, Proceedings of the The Eighth IEEE Computer Security Foundations Workshop (CSFW '95), p.98, March 13-15, 1995
• 47: B. Warinschi. A computational analysis of the Needham-Schroeder protocol. In IEEE Computer Security Foundations Workshop (CFSW), pages 248-262, 2003.

INDEX TERMS

Primary Classification:
  C. Computer Systems Organization
  C.2 COMPUTER-COMMUNICATION NETWORKS

Additional Classification:
  C. Computer Systems Organization
  C.2 COMPUTER-COMMUNICATION NETWORKS
      C.2.2 Network Protocols

  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

General Terms:
Security, Theory, Verification

Keywords:
cryptography, formal methods, security protocols