Abstract
Cryptographic protocols are usually specified in an informal language, with crucial elements of the protocol left implicit. We suggest that this is one reason that such protocols are difficult to analyse, and are subject to subtle and nonintuitive attacks. We present an approach for formalising and analysing cryptographic protocols in the situation calculus, in which all aspects of a protocol must be explicitly specified. We provide a declarative specification of underlying assumptions and capabilities, such that a protocol is translated into a sequence of actions to be executed by the principals, and a successful attack is an executable plan by an intruder that compromises the goal of the protocol. Our prototype verification software takes a protocol specification, translates it into a high-level situation calculus (Golog) program, and outputs any attacks that can be found. We describe the structure and operation of our prototype software, and discuss performance issues.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Aiello, L.C., Massacci, F.: Planning attacks to security protocols: Case studies in logic programming. In: Kakas, A.C., Sadri, F. (eds.) Computat. Logic (Kowalski Festschrift). LNCS (LNAI), vol. 2407, pp. 533–560. Springer, Heidelberg (2002)
Armando, A., Compagna, L., Lierler, Y.: Automatic Compilation of Protocol Insecurity Problems into Logic Programming. In: Proceedings of JELIA, pp. 617–627 (2004)
Brackin, S., Meadows, C., Millen, J.: CAPSL Interface for the NRL Protocol Analyzer. In: Proceedings of ASSET 1999. IEEE Press (1999)
Burrows, M., Abadi, M., Needham, R.: A logic of authentication. ACM Transactions on Computer Systems 8(1), 18–36 (1990)
Dolev, D., Yao, A.C.: On the Security of Public Key Protocols. IEEE Trans. on Inf. Theory 2(29), 198–208 (1983)
Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning about Knowledge. The MIT Press (1995)
Halpern, J.Y., Pucella, R.: On the Relationship between Strand Spaces and Multi-Agent Systems, CoRR, cs.CR/0306107 (2003)
Hernández-Orallo, J., Pinto, J.: Especificación formal de protocolos criptográficos en Cálculo de Situaciones. Novatica 143, 57–63 (2000)
Hunter, A., Delgrande, J.: Belief Change and Cryptographic Protocol Verification. In: Proceedings of AAAI (2007)
Levesque, H.J., Pirri, F., Reiter, R.: Foundations for the Situation Calculus. Linköping Electronic Articles in Computer and Information Science 3(18) (1998)
Levesque, H.J., Raymond, R., Lesperance, Y., Lin, F., Scherl, R.: GOLOG: A Logic Programming Language for Dynamic Domains. Journal of Logic Programming (31), 1–3 (1997)
Lowe, G.: Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, pp. 147–166. Springer, Heidelberg (1996)
Thayer, J., Herzog, J., Guttman, J.: Strand Spaces: Proving Security Protocols Correct. Journal of Computer Security 7(2-3), 191–230 (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hunter, A., Delgrande, J.P., McBride, R. (2013). Protocol Verification in a Theory of Action. In: Zaïane, O.R., Zilles, S. (eds) Advances in Artificial Intelligence. Canadian AI 2013. Lecture Notes in Computer Science(), vol 7884. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-38457-8_5
Download citation
DOI: https://doi.org/10.1007/978-3-642-38457-8_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-38456-1
Online ISBN: 978-3-642-38457-8
eBook Packages: Computer ScienceComputer Science (R0)