The Modelling and Analysis of Security Protocols: the CSP Approach

9.3. BAN logic and derivatives

The BAN logic of authentication due to Burrows, Abadi and Needham [20] was one of the first attempts to make the reasoning about the properties of security protocols more systematic. The basic idea is to reason about the states of belief of the (legitimate) agents involved. This involves understanding how such beliefs evolve as new information is received. To this end, initial knowledge, assumptions and the steps of the protocol are mapped into formulae in the logic in a process known as idealization. It must be stressed that the BAN logic really is about authentication. This seems obvious, given that the authors clearly describe it as such, but it is a fact that often seemed to have been overlooked. Many researchers ...