An introduction to BAN logic (a logic of authentication)

Speaker: Alexandru Dragomir (University of Bucharest)

Abstract: One of the first and most discussed logical approaches to the problem of verifying security protocols is the one proposed in BAN logic [1]. BAN logic is a many-sorted modal logic used for its intuitive and compelling set of inference rules devised for reasoning about an agent’s beliefs, trust and message exchange. My presentation will focus on (1) presenting the language and inference rules of BAN logic, (2) following the original paper’s analysis of the Otway-Rees protocol, (3) presenting some objections to using BAN, and (4) discussing the problem of offering a semantics of BAN logic.

References:
[1] M. Burrows, M. Abadi, R. Needham, A logic of authentication. Proc. Roy. Soc. London Ser. A 426, no. 1871, 233–271, 1989.