A complete and decidable security-specialised logic and its application to the TESLA protocol

ABSTRACT

We examine a logic to reason about security protocols by means of temporal and epistemic concepts. We report results on completeness and decidability of the formalism as well as its expressiveness. As a case study we apply the formalism in the analysis of TESLA, a secure stream multi-cast protocol.

REFERENCES

• 1: Martín Abadi , Mark R. Tuttle, A semantics for a logic of authentication (extended abstract), Proceedings of the tenth annual ACM symposium on Principles of distributed computing, p.201-216, August 19-21, 1991, Montreal, Quebec, Canada [doi>10.1145/112600.112618]
• 2: R. Accorsi, D. Basin, and L. Viganò. Towards an awareness-based semantics for security protocol analysis. In Post Proc. of LACPV'01, volume 55(1) of ENTCS, pp 5--24. Elsevier, 2003.
• 3: M. Archer. Proving correctness of the basic TESLA multicast stream authentication protocol with TAME. In Proc. of WITS'02, 2002.
• 4: Colin Boyd , Wenbo Mao, On a limitation of BAN logic, Workshop on the theory and application of cryptographic techniques on Advances in cryptology, p.240-247, January 1994, Lofthus, Norway
• 5: Philippa J. Broadfoot , Gavin Lowe, Analysing a Stream Authentication Protocol Using Model Checking, Proceedings of the 7th European Symposium on Research in Computer Security, p.146-161, October 14-16, 2002
• 6: M. Burrows, M. Abadi, and R. Needham. A logic of authentication. In Proc. of the Royal Society of London A, volume 426, pp. 233--271, 1989.
• 7: Edmund M. Clarke , E. Allen Emerson, Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic, Logic of Programs, Workshop, p.52-71, May 01, 1981
• 8: Clare Dixon , Mari-Carmen Fernandez Gago , Michael Fisher , Wiebe van der Hoek, Using Temporal Logics of Knowledge in the Formal Verification of Security Protocols, Proceedings of the 11th International Symposium on Temporal Representation and Reasoning (TIME'04), p.148-151, July 01-03, 2004
• 9: D. Dolev and A. Yao. On the security of public key protocols. IEEE Trans. Inf. Theory, 29(2):198--208, 1983.
• 10: R. Fagin , J. Y. Halpern, Belief, awareness, and limited reasoning, Artificial Intelligence, v.34 n.1, p.39-76, Dec. 1987 [doi>10.1016/0004-3702(87)90003-8]
• 11: Ronald Fagin , Joseph Y. Halpern , Moshe Y. Vardi , Yoram Moses, Reasoning about knowledge, MIT Press, Cambridge, MA, 1995
• 12: Li Gong, R. Needham, and R. Yahalom. Reasoning About Belief in Cryptographic Protocols. In Proceedings of IEEE Symposium on Research in Security and Privacy, pp. 234--248. IEEE Press, 1990.
• 13: Joseph Y. Halpern , Yoram Moses , Moshe Y. Vardi, Algorithmic knowledge, Proceedings of the 5th conference on Theoretical aspects of reasoning about knowledge, p.255-266, March 13-16, 1994, Pacific Grove, California
• 14: J. Y. Halpern and R. Pucella. Modeling Adversaries in a Logic for Security Protocol Analysis. In Proc. of FASec'02, volume 2629 of LNCS, pp. 115--132. Springer-Verlag, 2002.
• 15: R. Kailar and V. D. Gligor. On belief evolution in authentication protocols. In Proc. of Computer Security Foundations Workshop IV, pp. 103--116. IEEE Press, 1991.
• 16: A. Lomuscio and B. Woźna. A combination of explicit and deductive knowledge with branching time: completeness and decidability results. In Post-proc. of DALT'05, volume 3904 of LNAI. 2006. To appear.
• 17: A. Lomuscio and F. Raimondi. MCMAS: A model checker for multi-agent systems. In Proc. of TACAS'06. Springer Verlag, March, 2006. To appear.
• 18: Dan M. Nessett, A critique of the Burrows, Abadi and Needham logic, ACM SIGOPS Operating Systems Review, v.24 n.2, p.35-38, April 1990 [doi>10.1145/382258.382789]
• 19: Adrian Perrig , J. D. Tygar , Dawn Song , Ran Canetti, Efficient Authentication and Signing of Multicast Streams over Lossy Channels, Proceedings of the 2000 IEEE Symposium on Security and Privacy, p.56, May 14-17, 2000
• 20: R. Pucella. Deductive Algorithmic Knowledge. In Proc. of SAIM'04, AI&M 22--2004, 2004.
• 21: R. Ramanujam , S. P. Suresh, Deciding knowledge properties of security protocols, Proceedings of the 10th conference on Theoretical aspects of rationality and knowledge, June 10-12, 2005, Singapore
• 22: M. Wooldridge. Reasoning about Rational Agents. MIT Press, 2000.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
        I.2.11 Distributed Artificial Intelligence
      I.2.4 Knowledge Representation Formalisms and Methods

General Terms:
Security, Theory, Verification

Keywords:
TESLA, epistemic logic, security protocols