Verifying security protocols using BAN logic

Speaker: Alexandru Dragomir (University of Bucharest)

Abstract: Epistemic logics – logics aimed at reasoning about knowledge and belief – are widely considered to be suitable for modelling, analyzing and predicting vulnerabilities of security protocols. One of the first and most discussed logical approaches to the problem of verifying security protocols is the one proposed in BAN logic (Burrows, Abadi & Needham 1989), a many-sorted epistemic 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) briefly presenting the language and inference rules of BAN logic, (2) offering a presentation of the Otway-Rees, Needham-Schroeder and Kerberos protocols, and (3) analysing the aforementioned protocols using BAN logic.