Verification and modelling of authentication protocols

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 [BAN1] 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 protocol participants as finite state machines. Also, actions of intruders, consequences of such intrusions, and the respective counter-measures can be modelled and simulated.