Semantics and logic for security protocols

B.P.F. Jacobs, I. Hasuo

Research output: Contribution to journalArticleAcademicpeer-review

6 Citations (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.
Original languageEnglish
Pages (from-to)909-944
JournalJournal of Computer Security
Issue number6
Publication statusPublished - 2009


Dive into the research topics of 'Semantics and logic for security protocols'. Together they form a unique fingerprint.

Cite this