Extending BAN Logic for Reasoning With Modern PKI-Based Protocols

BAN Logic is a well-known authentication logic which, despite other more recent logics and formal methods, remains popular with many protocol designers. BAN Logic however does not properly deal with the issues of certificates and the use of Public Key Infrastructure (PKI). This paper proposes an extension to BAN Logic which focuses on certificate processing within the PKI setting. The extension is along the lines of the work by Gaarder and Snekkenes but better captures current aspects of PKI. In particular, the extension redresses the reasoning on the goodness of private keys, and considers certificate revocation. Common pitfalls in public-key based protocol design are due to insufficient attention placed on the "Intended recipient" as well as the "Stated sender" of a message.