Semantics and logic for security protocols

Article type: Research Article

Authors: Jacobs, Bart^{a; *; **} | Hasuo, Ichiro^{a; b}

Affiliations: [a] Institute for Computing and Information Sciences, Radboud University Nijmegen, Nijmegen, The Netherlands | [b] Research Institute for Mathematical Sciences, Kyoto University, Kyoto, Japan

Correspondence: [*] Corresponding author: Bart Jacobs, Institute for Computing and Information Sciences, Radboud University Nijmegen, P.O. Box 9010, 6500 GL, Nijmegen, The Netherlands. Tel.: +31 24 3652236; Fax: +31 24 3652298; E-mail: [email protected]; URL: http://www.cs.ru.nl/B.Jacobs.

Note: [**] Also part-time at Technical University Eindhoven, The Netherlands.

Abstract: This paper presents a sound BAN-like logic for reasoning about security protocols with theorem prover support. The logic has formulas for sending and receiving messages (with nonces, public and private encryptions, etc.), and has both temporal and epistemic operators (describing the knowledge of participants). The logic's semantics is based on strand spaces. Several (secrecy or authentication) formulas are proven in general and are applied to the Needham–Schroeder(–Lowe), bilateral key exchange and the Otway–Rees protocols, as illustrations.

Keywords: Security protocols, logic, theorem proving, secrecy, authentication

DOI: 10.3233/JCS-2009-0348

Journal: Journal of Computer Security, vol. 17, no. 6, pp. 909-944, 2009