Reference from ESORICS proceedings

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)

Proceedings table of contents