A calculus of challenges and responses

ABSTRACT

This paper presents a novel approach for concisely abstracting authentication protocols and for subsequently analyzing those abstractions in a sound manner, i.e., deriving authentication guarantees for protocol abstractions suffices for proving these guarantees for the actual protocols. The abstractions are formalized in a process calculus which constitutes a higher-level abstraction of the ρspi calculus and is specifically tailored towards reasoning about challenge-response mechanisms within authentication protocols. Furthermore, it allows for expressing protocols without having to include details on the specific structure of exchanged messages. This in particular entails that many authentication protocols share a common abstraction so that a single validation of this abstraction already gives rise to security guarantees for all these protocols. Such an abstract validation can be automatically performed using static analysis techniques based on an effect system proposed in this paper. Finally, extensions to additional protocol classes enjoy a soundness theorem provided that these extensions satisfy certain explicit, easily checkable conditions.

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: 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
• 3: Martín Abadi , Bruno Blanchet, Analyzing security protocols with secrecy types and logic programs, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.33-44, January 16-18, 2002, Portland, Oregon
• 4: Martín Abadi , Andrew D. Gordon, A calculus for cryptographic protocols: the spi calculus, Proceedings of the 4th ACM conference on Computer and communications security, p.36-47, April 01-04, 1997, Zurich, Switzerland [doi>10.1145/266420.266432]
• 5: Roberto M. Amadio , Denis Lugiez , Vincent Vanackère, On the symbolic reduction of processes with cryptographic functions, Theoretical Computer Science, v.290 n.1, p.695-740, 1 January 2003 [doi>10.1016/S0304-3975(02)00090-7]
• 6: Michael Backes , Agostino Cortesi , Matteo Maffei, Causality-based Abstraction of Multiplicity in Security Protocols, Proceedings of the 20th IEEE Computer Security Foundations Symposium, p.355-369, July 06-08, 2007 [doi>10.1109/CSF.2007.11]
• 7: 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
• 8: Bruno Blanchet, From Secrecy to Authenticity in Security Protocols, Proceedings of the 9th International Symposium on Static Analysis, p.342-359, September 17-20, 2002
• 9: B. Blanchet and A. Podelski. Verification of cryptographic protocols: Tagging enforces termination. In Proc. 6th International Conference on Foundations of Software Science and Computation Structures (FOSSACS), pages 136--152, 2003.
• 10: Chiara Bodei , Mikael Buchholtz , Pierpaolo Degano , Flemming Nielson , Hanne Riis Nielson, Static validation of security protocols, Journal of Computer Security, v.13 n.3, p.347-390, May 2005
• 11: 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
• 12: M. Bugliesi, R. Focardi, and M. Maffei. Compositional analysis of authentication protocols. In Proc. 13th European Symposium on Programming (ESOP), volume 2986 of Lecture Notes in Computer Science, pages 140--154. Springer-Verlag, 2004.
• 13: Michele Bugliesi , Riccardo Focardi , Matteo Maffei, Analysis of Typed Analyses of Authentication Protocols, Proceedings of the 18th IEEE workshop on Computer Security Foundations, p.112-125, June 20-22, 2005 [doi>10.1109/CSFW.2005.8]
• 14: M. Bugliesi, R. Focardi, and M. Maffei. Dynamic types for authentication, 2007. To appear in Journal of Computer Security.
• 15: Anupam Datta , Ante Derek , John C. Mitchell , Arnab Roy, Protocol Composition Logic (PCL), Electronic Notes in Theoretical Computer Science (ENTCS), 172, p.311-358, April, 2007 [doi>10.1016/j.entcs.2007.02.012]
• 16: Anupam Datta , Ante Derek , John C. Mitchell , Dusko Pavlovic, A derivation system and compositional logic for security protocols, Journal of Computer Security, v.13 n.3, p.423-482, May 2005
• 17: S. F. Doghmi, J. D. Guttman, and F. J. Thayer. Searching for shapes in cryptographic protocols. In Proc. 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Lecture Notes in Computer Science, pages 523--538. Springer-Verlag, 2007.
• 18: D. Dolev and A. C. Yao. On the security of public key protocols. IEEE Transactions on Information Theory, 29(2):198--208, 1983.
• 19: Nancy Durgin , John Mitchell , Dusko Pavlovic, A compositional logic for proving security properties of protocols, Journal of Computer Security, v.11 n.4, p.677-721, July 2003
• 20: H. Gao, P. Degano, C. Bodei, and H. R. Nielson. Detecting replay attacks by freshness annotations. In WITS '07: Proceedings of the 7th Workshop on Issues in the theory of security, pages 85--100, 2007.
• 21: Andrew D. Gordon , Alan Jeffrey, Types and effects for asymmetric cryptographic protocols, Journal of Computer Security, v.12 n.3,4, p.435-483, May 2004
• 22: Joshua D. Guttman , F. Javier Thayer, Protocol Independence through Disjoint Encryption, Proceedings of the 13th IEEE workshop on Computer Security Foundations, p.24, July 03-05, 2000
• 23: 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]
• 24: Christian Haack , Alan Jeffrey, Pattern-matching spi-calculus, Information and Computation, v.204 n.8, p.1195-1263, August 2006 [doi>10.1016/j.ic.2006.04.004]
• 25: Gavin Lowe, A Hierarchy of Authentication Specifications, Proceedings of the 10th IEEE workshop on Computer Security Foundations, p.31, June 10-12, 1997
• 26: M. Maffei. Dynamic Typing for Security Protocols. PhD thesis, Università Ca'Foscari di Venezia, Dipartimento di Informatica, 2006.
• 27: C. Meadows. Open issues in formal methods for cryptographic protocol analysis. In Proc. 2000 DARPA Information Survivability Conference and Exposition (DISCEX), pages 237--250, 2000.
• 28: Jonathan Millen , Vitaly Shmatikov, Constraint solving for bounded-process cryptographic protocol analysis, Proceedings of the 8th ACM conference on Computer and Communications Security, November 05-08, 2001, Philadelphia, PA, USA [doi>10.1145/501983.502007]
• 29: Christoffer Rosenkilde Nielsen , Flemming Nielson , Hanne Riis Nielson, Cryptographic Pattern Matching, Electronic Notes in Theoretical Computer Science (ENTCS), 168, p.91-107, February, 2007 [doi>10.1016/j.entcs.2006.08.024]
• 30: 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]

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

General Terms:
Security, Verification

Keywords:
authentication protocols, process calculi, static analysis