Semantics and logic for security protocols
Bart Jacobs, Ichiro Hasuo · Journal of Computer Security · 2009
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 pa rticipants). 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.