Reference from ESORICS proceedings

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)

Proceedings table of contents