Second European Symposium on Research in Computer Security (ESORICS 92)
Verification and Modelling of Authentication Protocols
Ralf C. Hauser
Keywords :
Abstract : With the emergence of numerous distributed services, the importance of electronic authentication in networks is rapidly increasing. Many authentication protocols have been proposed and discussed. Burrows, Abadi and Needham created a logic of authentication to formally analyze authentication protocols. This BAN-logic has been subject to critique and several extensions have been suggested. Nonetheless, due to its straightforward design and its ease-of-use, it attracts the attention of current research. In this paper, an authentication logic is proposed which is built closely after the BAN-logic. It addresses answers to important criticisms of BAN like the non-disclosure problem, and avoids some newly discovered weaknesses of BAN, e.g. with respect to freshness. It also does not require any idealization which is a major hurdle to the correct usage of BAN. This extended BAN-logic is instrumented as a verification tool which also allows for modelling the different protocols participants as finite state machines. Also, actions of intruders, consequences of such intrusions, and the respective counter-measures can be modelled and simulated.
(Pages 141-154)