Verifying security protocols using BAN logic – Part 2

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. I will assume knowledge of the basics of BAN logic and focus on presenting and analyzing the Needham-Schroeder and Kerberos protocols using this particular logical framework. Consequently, I will highlight some of the pros and cons of using BAN logic in verifying security protocols.