Authenticity by tagging and typing

ABSTRACT

We propose a type and effect system for <i>authentication</i> protocols built upon a tagging scheme that formalizes the intended semantics of ciphertexts. The main result is that the validation of each component in isolation is provably sound and <i>fully compositional</i>: if all the protocol participants are independently validated, then the protocol as a whole guarantees authentication in the presence of Dolev-Yao intruders. The highly compositional nature of the analysis makes it suitable for multi-protocol systems, where different protocols might be executed concurrently.

REFERENCES

• 1: M. Abadi and C.Fournet. Private authentication. In Proceedings of the 2002 Workshop on Privacy Enhancing Technologies, Lecture Notes in Computer Science, pages 27--40. Springer-Verlag, 2003.
• 2: 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]
• 3: 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]
• 4: B. Blanchet and A. Podelski. Verification of cryptographic protocols: Tagging enforces termination. Proceedings of Foundations of Software Science and Computation Structures, pages 136--152, 2003.
• 5: C. Bodei, M. Buchholtz, P. Degano, F. Nielson, and H. Riis Nielson. Automatic validation of protocol narration. In Proceedings of the 16th IEEE Computer Security Foundations Workshop(CSFW'03), pages 126--140. IEEE Computer Society Press, June 2003.
• 6: C. Bodei, M. Buchholtz, P. Degano, F. Nielson, and H. Riis Nielson. Control flow analysis can find new flaws too. In Proceedings of the Workshop on Issues on the Theory of Security (WITS'04), ENTCS. Elsevier, 2004.
• 7: Michele Boreale, Symbolic Trace Analysis of Cryptographic Protocols, Proceedings of the 28th International Colloquium on Automata, Languages and Programming,, p.667-681, July 08-12, 2001
• 8: Michele Boreale , Rocco de Nicola , Rosario Pugliese, Proof Techniques for Cryptographic Processes, Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, p.157, July 02-05, 1999
• 9: M. Bugliesi, R. Focardi, and M. Maffei. Principles for entity authentication. In Proceedings of 5th International Conference Perspectives of System Informatics (PSI 2003), volume 2890 of Lecture Notes in Computer Science, pages 294--307. Springer-Verlag, July 2003.
• 10: M. Bugliesi, R. Focardi, and M. Maffei. Compositional analysis of authentication protocols. In Proceedings of European Symposium on Programming (ESOP 2004), volume 2986 of Lecture Notes in Computer Science, pages 140--154. Springer-Verlag, 2004.
• 11: 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
• 12: Andrew D. Gordon , Alan Jeffrey, Types and Effects for Asymmetric Cryptographic Protocols, Proceedings of the 15th IEEE Computer Security Foundations Workshop (CSFW'02), p.77, June 24-26, 2002
• 13: J.D. Guttman, F.J. Thayer, J.A. Carlson, J.C.Herzog, J.D. Ramsdell, and B.T. Sniffen. Trust management in strand spaces: a rely-guarantee method. In Proceedings of European Symposium on Programming (ESOP 2004), volume 2986 of Lecture Notes in Computer Science, pages 325--339. Springer-Verlag, 2004.
• 14: Joshua D. Guttman , F. Javier Thayer, Protocol Independence through Disjoint Encryption, Proceedings of the 13th IEEE Computer Security Foundations Workshop (CSFW'00), p.24, July 03-05, 2000
• 15: Joshua D. Guttman , F. Javier Thayer, Authentication tests and the structure of bundles, Theoretical Computer Science, v.283 n.2, p.333-380, June 14, 2002 [doi>10.1016/S0304-3975(01)00139-6]
• 16: 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
• 17: 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
• 18: Gavin Lowe, A Hierarchy of Authentication Specifications, Proceedings of the 10th Computer Security Foundations Workshop (CSFW '97), p.31, June 10-12, 1997
• 19: G. Lowe, Towards a Completeness Result for Model Checking of Security Protocols, Proceedings of the 11th IEEE Computer Security Foundations Workshop, p.96, June 09-11, 1998
• 20: M.Maffei. Tags for multi-protocol authentication. In Proceedings of the 2nd International Workshop on Security Issues in Coordination Models, Languages, and Systems (SECCO '04). To appear. ENTCS, August 2004.
• 21: R.Focardi and M.Maffei. ρ-spi calculus at work: Authentication case studies. In Proceedings of Mefisto Project. To appear. ENTCS, March 2004.
• 22: F. Javier Thayer Fábrega, Strand spaces: proving security protocols correct, Journal of Computer Security, v.7 n.2-3, p.191-230, Jan. 1999
• 23: Thomas Y. C. Woo , Simon S. Lam, A lesson on authentication protocol design, ACM SIGOPS Operating Systems Review, v.28 n.3, p.24-37, July 1994 [doi>10.1145/182110.182113]
• 24: Thomas Y. C. Woo , Simon S. Lam, A Semantic Model for Authentication Protocols, Proceedings of the 1993 IEEE Symposium on Security and Privacy, p.178, May 24-26, 1993

INDEX TERMS

Primary Classification:
  C. Computer Systems Organization
  C.2 COMPUTER-COMMUNICATION NETWORKS
      C.2.2 Network Protocols
          Subjects: Protocol verification

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Program analysis

  K. Computing Milieux
  K.6 MANAGEMENT OF COMPUTING AND INFORMATION SYSTEMS
      K.6.5 Security and Protection (D.4.6, K.4.2)
          Subjects: Authentication

General Terms:
Security, Verification

Keywords:
authentication, process calculi, static analysis