Authentication primitives and their compilation

ABSTRACT

Adopting a programming-language perspective, we study the problem of implementing authentication in a distributed system. We define a process calculus with constructs for authentication and show how this calculus can be translated to a lower-level language using marshaling, multiplexing, and cryptographic protocols. Authentication serves for identity-based security in the source language and enables simplifications in the translation. We reason about correctness relying on the concepts of observational equivalence and full abstraction.

REFERENCES

• 1: Martín Abadi, Protection in Programming-Language Translations, Proceedings of the 25th International Colloquium on Automata, Languages and Programming, p.868-883, July 13-17, 1998
• 2: M. Abadi , C. Fournet , G. Gonthier, Secure Implementation of Channel Abstractions, Proceedings of the 13th Annual IEEE Symposium on Logic in Computer Science, p.105, June 21-24, 1998
• 3: Martin Abadi, C~dric Fournet, and Georges Gonthier. Secure communications processing for distributed languages. In Proceedings of the 1999 IEEE Symposium on Security and Privacy, pages 74-88, May 1999.
• 4: 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]
• 5: Martín Abadi , Roger Needham, Prudent Engineering Practice for Cryptographic Protocols, IEEE Transactions on Software Engineering, v.22 n.1, p.6-15, January 1996 [doi>10.1109/32.481513]
• 6: Roberto M. Amadio, On modelling mobility, Theoretical Computer Science, v.240 n.1, p.147-176, June 6 2000 [doi>10.1016/S0304-3975(99)00230-3]
• 7: Ross J. Anderson , Roger M. Needham, Robustness Principles for Public Key Protocols, Proceedings of the 15th Annual International Cryptology Conference on Advances in Cryptology, p.236-247, August 27-31, 1995
• 8: Mihir Bellare , Ran Canetti , Hugo Krawczyk, A modular approach to the design and analysis of authentication and key exchange protocols (extended abstract), Proceedings of the thirtieth annual ACM symposium on Theory of computing, p.419-428, May 24-26, 1998, Dallas, Texas, United States [doi>10.1145/276698.276854]
• 9: Mihir Bellare , Phillip Rogaway, Entity authentication and key distribution, Proceedings of the 13th annual international cryptology conference on Advances in cryptology, p.232-249, January 1994, Santa Barbara, California, United States
• 10: Andrew D. Birrell, Secure communication using remote procedure calls, ACM Transactions on Computer Systems (TOCS), v.3 n.1, p.1-14, Feb. 1985 [doi>10.1145/214451.214452]
• 11: M. Moreale , Cédric Fournet , Cosimo Laneve, Bisimulations in the join-calculus, Proceedings of the IFIP TC2/WG2.2,2.3 International Conference on Programming Concepts and Methods, p.68-86, June 08-12, 1998
• 12: G6rard Boudol, Ilaria Castellani, Matthew Hennessy, and Astrid Kiehn. A theory of processes with localities. Formal Aspects of Computing, 6:165-200, 1994.
• 13: M. Burrows , M. Abadi , R. Needham, A logic of authentication, ACM SIGOPS Operating Systems Review, v.23 n.5, p.1-13, Dec. 3–6, 1989
• 14: C6dric Fournet. The Join-Calculus: a Calculus for Distributed Mobile Programming. PhD thesis, Ecole Polytechnique, Palaiseau, November 1998.
• 15: Cédric Fournet , Georges Gonthier, The reflexive CHAM and the join-calculus, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.372-385, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237805]
• 16: Cédric Fournet , Cosimo Laneve , Luc Maranget , Didier Rémy, Implicit Typing à la ML for the Join-Calculus, Proceedings of the 8th International Conference on Concurrency Theory, p.196-212, July 01-04, 1997
• 17: C~dric Fournet and Luc Maranget. The join-calculus language (version 1.03). Source distribution and documentation available from http://join.inria, fr/, June 1997.
• 18: Richard A. Kemmerer. Analyzing encryption protocols using formal verification techniques. IEEE Journal on Selected Areas in Communications, 7(4):448-457, May 1989.
• 19: Butler Lampson , Martín Abadi , Michael Burrows , Edward Wobber, Authentication in distributed systems: theory and practice, ACM Transactions on Computer Systems (TOCS), v.10 n.4, p.265-310, Nov. 1992 [doi>10.1145/138873.138874]
• 20: 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]
• 21: 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
• 22: Gavin Lowe, A Hierarchy of Authentication Specifications, Proceedings of the 10th Computer Security Foundations Workshop (CSFW '97), p.31, June 10-12, 1997
• 23: Catherine Meadows. A system for the specification and analysis of key management protocols. In Proceedings of the 1991 IEEE Symposium on Research in Security and Privacy, pages 182-195, 1991.
• 24: 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
• 25: Alfred J. Menezes , Scott A. Vanstone , Paul C. Van Oorschot, Handbook of Applied Cryptography, CRC Press, Inc., Boca Raton, FL, 1996
• 26: Jonathan K. Millen , Sidney C. Clark , Sheryl B. Freeman, The interrogator: protocol security analysis, IEEE Transactions on Software Engineering, v.13 n.2, p.274-288, Feb. 1987 [doi>10.1109/TSE.1987.233151]
• 27: Robin Milner , Joachim Parrow , David Walker, A calculus of mobile processes, II, Information and Computation, v.100 n.1, p.41-77, Sept. 1992 [doi>10.1016/0890-5401(92)90009-5]
• 28: 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]
• 29: 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]
• 30: Steve Schneider, Verifying Authentication Protocols in CSP, IEEE Transactions on Software Engineering, v.24 n.9, p.741-758, September 1998 [doi>10.1109/32.713329]
• 31: Peter Sewell , Jan Vitek, Secure Composition of Insecure Components, Proceedings of the 1999 IEEE Computer Security Foundations Workshop, p.136, June 28-30, 1999
• 32: Sun Microsystems, Inc. RMI enhancements. Web pages at http://java.sun, com/products/jdk/1.2/ docs/guide/rmi/, 1997.
• 33: Martin Abadi, Secure Network Objects, Proceedings of the 1996 IEEE Symposium on Security and Privacy, p.211, May 06-08, 1996

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES

  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES

General Terms:
Design, Languages