Automating ban logic

BAN Logic is a well-known formalism for the analysis of protocols used for authentication in distributed systems. This formalism deals with the evolution of beliefs of trustworthy principals executing an authentication protocol. The evolution of beliefs as a consequence of communication between the principals is modeled by the inference rules of the logic. The logic has been successful in formally discovering flaws and redundancies in a number of widely used protocols. A probabilistic extension of the logic allows calculation of a measure of trust in the goal of a protocol. This thesis proposes a Prolog program to automate BAN logic analysis of authentication protocols. The program provides a protocol-independent inference engine, which takes as input the specification of a protocol, and generates all the logical statements describing the state of the principals executing the protocol. A proof explanation faciUty in the program provides a stepwise description of all minimal proofs of the logical statements attained during a protocol run. The program enables automatic identification of redundant assumptions and also facilitates probabilistic analysis of protocols. It has been used to perform machine-aided BAN logic analysis of several well-known protocols.