Semantics and logic for security protocols

B.P.F. Jacobs, I. Hasuo

Onderzoeksoutput: Bijdrage aan tijdschriftTijdschriftartikelAcademicpeer review

5 Citaten (Scopus)


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.
Originele taal-2Engels
Pagina's (van-tot)909-944
TijdschriftJournal of Computer Security
Nummer van het tijdschrift6
StatusGepubliceerd - 2009


Duik in de onderzoeksthema's van 'Semantics and logic for security protocols'. Samen vormen ze een unieke vingerafdruk.

Citeer dit