Fourth European Symposium on Research in Computer Security (ESORICS 96)
Formal Semantics for Authentification Logics
Gabriele Wedel, Volker Kessler
Keywords : Formal verification, logic of authentication, cryptographic protocols, key management.
Abstract : We present a new BAN-like logic and a new formal semantics Ior 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-logic, including negation. We replace the critical idealization step by changing the set of premises. The formal semantics enables us to detect Haws in previous logics. We apply the logic to a new authentication protocol designed for UMTS.
(Pages 219-241)