| Authentication protocols aim to prevent agent impersonation: A is authenticated to B if B knows who A is. Many formal approaches have been used to verify authentication in distributed systems; however, although authentication is directly related to agent knowledge, it has only been formally defined using process algebra, usually in terms of constraints on the order of protocol events [1, 9, 20, 24]. In response, we use epistemic modal logic [14] to define authentication in terms of common knowledge as a form of coordinated action. We apply our definition to verify the Needham-Schroeder-Lowe Public-Key Protocol [20], as well as its predecessor, the Needham-Schroeder Public-Key Protocol [21], which is vulnerable to an impersonation attack [19]. In doing so, we reason about knowledge evolution with an epistemic satisfaction relation on state-action histories. The results of our verification extend previous process-algebraic analyses of the two protocols [20, 24] by highlighting the role of agent knowledge. |
