Semantics and logic for security protocols

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.