Formal semantics for authentication logics

Abstract

We present a new BAN-like logic and a new formal semantics for logics of authentication. The main focus of this paper is on the foundation of this logic by a possible-worlds semantics. The logic was designed for implementation in the tool AUTLOG and is able to handle most kinds of protocols used in practice. The underlying logic is a K45-1ogic, including negation. We replace the critical idealization step by changing the set of premises. The formal semantics enables us to detect flaws in previous logics. We apply the logic to a new authentication protocol designed for UMTS.