Analyzing security protocols with secrecy types and logic programs

ABSTRACT

We study and further develop two language-based techniques for analyzing security protocols. One is based on a typed process calculus; the other, on untyped logic programs. Both focus on secrecy properties. We contribute to these two techniques, in particular by extending the former with a flexible, generic treatment of many cryptographic operations. We also establish an equivalence between the two techniques.

REFERENCES

• 1: Martín Abadi, Secrecy by typing in security protocols, Journal of the ACM (JACM), v.46 n.5, p.749-786, Sept. 1999 [doi>10.1145/324133.324266]
• 2: M.Abadi.Security protocols and their properties.In F.Bauer and R.Steinbrueggen,editors,Foundations of Secure Computation ,NATO Science Series,pages 39-60.IOS Press,2000.Volume for the 20th International Summer School on Foundations of Secure Computation,held in Marktoberdorf,Germany (1999).
• 3: Martín Abadi , Anindya Banerjee , Nevin Heintze , Jon G. Riecke, A core calculus of dependency, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.147-160, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292555]
• 4: Martín Abadi , Bruno Blanchet, Secrecy Types for Asymmetric Communication, Proceedings of the 4th International Conference on Foundations of Software Science and Computation Structures, p.25-41, April 02-06, 2001
• 5: Martín Abadi , Cédric Fournet, Mobile values, new names, and secure communication, Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.104-115, January 2001, London, United Kingdom
• 6: 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]
• 7: Roberto M. Amadio , Denis Lugiez, On the Reachability Problem in Cryptographic Protocols, Proceedings of the 11th International Conference on Concurrency Theory, p.380-394, August 22-25, 2000
• 8: Bruno Blanchet, An Efficient Cryptographic Protocol Verifier Based on Prolog Rules, Proceedings of the 14th IEEE Workshop on Computer Security Foundations, p.82, June 11-13, 2001
• 9: C.Bodei.Security Issues in Process Calculi .PhD thesis,Universit`a di Pisa,Jan.2000.
• 10: Chiara Bodei , Pierpaolo Degano , Flemming Nielson , Hanne Riis Nielson, Control Flow Analysis for the pi-calculus, Proceedings of the 9th International Conference on Concurrency Theory, p.84-98, September 08-11, 1998
• 11: Luca Cardelli , Giorgio Ghelli , Andrew D. Gordon, Secrecy and Group Creation, Proceedings of the 11th International Conference on Concurrency Theory, p.365-379, August 22-25, 2000
• 12: 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
• 13: Mads Dam, Proving Trust in Systems of 2nd-Order Processes: Preliminary Results, Proceedings of the Thirty-First Annual Hawaii International Conference on System Sciences-Volume 7, p.255, January 06-09, 1998 [doi>10.1109/HICSS.1998.649220]
• 14: M.Debbabi,M.Mejri,N.Tawbi,and I.Yahmadi.A new algorithm for the automatic eri .cation of authentication protocols:From speci .cations to .aws and attack scenarios.In Proceedings of the DIMACS Workshop on Design and Formal Veri .cation of Security Protocols ,Rutgers University,New Jersey, Sept.1997.
• 15: G.Denker,J.Meseguer,and C.Talcott.Protocol speci .cation and analysis in Maude.In N.Heintze and J.Wing,editors,Proc.of Workshop on Formal Methods and Security Protocols ,Indianapolis,Indiana, 25 June 1998.
• 16: Antonio Durante , Riccardo Focardi , Roberto Gorrieri, CVS: A Compiler for the Analysis of Cryptographic Protocols, Proceedings of the 1999 IEEE Computer Security Foundations Workshop, p.203, June 28-30, 1999
• 17: Nancy Durgin , John Mitchell , Dusko Pavlovic, A Compositional Logic for Protocol Correctness, Proceedings of the 14th IEEE Workshop on Computer Security Foundations, p.241, June 11-13, 2001
• 18: N.A.Durgin and J.C.Mitchell.Analysis of security protocols.In M.Broy and R.Steinbruggen,editors, Calculational System Design,pages 369 -395.IOS Press,1999.
• 19: Riccardo Focardi , Roberto Gorrieri, The Compositional Security Checker: A Tool for the Verification of Information Flow Security Properties, IEEE Transactions on Software Engineering, v.23 n.9, p.550-571, September 1997 [doi>10.1109/32.629493]
• 20: Andrew D. Gordon , Alan Jeffrey, Authenticity by Typing for Security Protocols, Proceedings of the 14th IEEE Workshop on Computer Security Foundations, p.145, June 11-13, 2001
• 21: Nevin Heintze , Jon G. Riecke, The SLam calculus: programming with secrecy and integrity, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.365-377, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268976]
• 22: Matthew Hennessy , James Riely, Information Flow vs. Resource Access in the Asynchronous Pi-Calculus, Proceedings of the 27th International Colloquium on Automata, Languages and Programming, p.415-427, July 09-15, 2000
• 23: Kohei Honda , Vasco Thudichum Vasconcelos , Nobuko Yoshida, Secure Information Flow as Typed Process Behaviour, Proceedings of the 9th European Symposium on Programming Languages and Systems, p.180-199, April 02, 2000
• 24: R.Kemmerer,C.Meadows,and J.Millen.Three systems for cryptographic protocol analysis.Journal of Cryptology ,7(2):79 -130,Spring 1994.
• 25: H. Krawczyk, SKEME: a versatile secure key exchange mechanism for Internet, Proceedings of the 1996 Symposium on Network and Distributed System Security (SNDSS '96), p.114, February 22-23, 1996
• 26: 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]
• 27: Gavin Lowe, Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR, Proceedings of the Second International Workshop on Tools and Algorithms for Construction and Analysis of Systems, p.147-166, March 27-29, 1996
• 28: C. Meadows, Languages for Formal Specification of Security Protocols, Proceedings of the 10th Computer Security Foundations Workshop (CSFW '97), p.96, June 10-12, 1997
• 29: Robin Milner, Communicating and mobile systems: the &pgr;-calculus, Cambridge University Press, New York, NY, 1999
• 30: James H. Morris, Jr., Protection in programming languages, Communications of the ACM, v.16 n.1, p.15-21, Jan. 1973 [doi>10.1145/361932.361937]
• 31: Andrew C. Myers, JFlow: practical mostly-static information flow control, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.228-241, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292561]
• 32: Roger M. Needham , Michael D. Schroeder, Using encryption for authentication in large networks of computers, Communications of the ACM, v.21 n.12, p.993-999, Dec. 1978 [doi>10.1145/359657.359659]
• 33: Lawrence C. Paulson, The inductive approach to verifying cryptographic protocols, Journal of Computer Security, v.6 n.1-2, p.85-128, Sept. 1998
• 34: E.Sumii and B.C.Pierce.Logical relations and encryption (Extended abstract).In 14th IEEE Computer Security Foundations Workshop (CSFW-14),pages 256-269,June 2001.
• 35: Dennis Volpano , Cynthia Irvine , Geoffrey Smith, A sound type system for secure flow analysis, Journal of Computer Security, v.4 n.2-3, p.167-187, Jan. 1996
• 36: Christoph Weidenbach, Towards an Automatic Analysis of Security Protocols in First-Order Logic, Proceedings of the 16th International Conference on Automated Deduction: Automated Deduction, p.314-328, July 07-10, 1999