Events in security protocols

ABSTRACT

The events of a security protocol and their causal dependency can play an important role in the analysis of security properties. This insight underlies both strand spaces and the inductive method. But neither of these approaches builds up the events of a protocol in a compositional way, so that there is an informal spring from the protocol to its model. By broadening the models to certain kinds of Petri nets, a restricted form of contextual nets, a compositional event-based semantics is given to an economical, but expressive, language for describing security protocols; so the events and dependency of a wide range of protocols are determined once and for all. The net semantics is formally related to a transition semantics, strand spaces and inductive rules, as well as trace languages and event structures, so unifying a range of approaches, as well as providing conditions under which particular, more limited, models are adequate for the analysis of protocols. The net semantics allows the derivation of general properties and proof principles which are demonstrated in establishing an authentication property, following a diagrammatic style of proof.

REFERENCES

• 1: 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]
• 2: I.Cervesato,N.A.Durgin,M.Kanovich,and A.Scedrov.Interpreting strands in linear logic.In FMCS '00 ,2000.
• 3: Nancy Durgin , Patrick Lincoln , John Mitchell , Andre Scedrov , Iliano Cervesato, Relating Strands and Multiset Rewriting for Security Protocol Analysis, Proceedings of the 13th IEEE Computer Security Foundations Workshop (CSFW'00), p.35, July 03-05, 2000
• 4: D.Dolev and A.C.Yao.On the security of public key protocols.IEEE Trans.on Inf.Theory ,2(29),1983.
• 5: Uffe Engberg , Glynn Winskel, Linear Logic on Petri Nets, A Decade of Concurrency, Reflections and Perspectives, REX School/Symposium, p.176-229, June 01-04, 1993
• 6: 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
• 7: Robin Milner, Communicating and mobile systems: the &pgr;-calculus, Cambridge University Press, New York, NY, 1999
• 8: U.Montanari and F.Rossi.Contextual nets.Acta Informatica ,(32),1995.
• 9: Lawrence C. Paulson, Proving Security Protocols Correct, Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, p.370, July 02-05, 1999
• 10: Andrew M. Pitts , Ian D. B. Stark, Observable Properties of Higher Order Functions that Dynamically Create Local Names, or What's new?, Proceedings of the 18th International Symposium on Mathematical Foundations of Computer Science, p.122-141, August 30-September 03, 1993
• 11: R. L. Rivest , A. Shamir , L. Adleman, A method for obtaining digital signatures and public-key cryptosystems, Communications of the ACM, v.21 n.2, p.120-126, Feb. 1978 [doi>10.1145/359340.359342]
• 12: J.Thayer,J.Herzog,and J.Guttman.Strand spaces: Why is a security protocol correct?In 1998 IEEE Symposium on Security and Privacy .
• 13: Glynn Winskel, Event Structures, Proceedings of an Advanced Course on Petri Nets: Central Models and Their Properties, Advances in Petri Nets 1986-Part II, p.325-392, September 08-19, 1986
• 14: Glynn Winskel, Petr nets, algebras, morphisms, and compositionality, Information and Computation, v.72 n.3, p.197-238, March 1987 [doi>10.1016/0890-5401(87)90032-0]
• 15: Glynn Winskel , Mogens Nielsen, Models for concurrency, Handbook of logic in computer science (vol. 4): semantic modelling, Oxford University Press, Oxford, 1995

INDEX TERMS

Primary Classification:
  I. Computing Methodologies
  I.6 SIMULATION AND MODELING
      I.6.5 Model Development
          Subjects: Modeling methodologies

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.2 Design Tools and Techniques
          Subjects: Petri nets
  D.4 OPERATING SYSTEMS
      D.4.6 Security and Protection
          Subjects: Authentication

General Terms:
Algorithms, Security, Theory