Typing secure implementation of authentication protocols in environments with compromised principals

摘要

Analyzing the executable code, instead of the high-level model, of security protocols has received attention in recent years. To this end, a number of security type systems have already been proposed. These type systems are sound but incomplete. That is, a well-typed protocol is certainly secure, whereas no judgment can be made about the protocol whose type-annotated code is ill typed. In fact, the type-based analysis of a protocol would have no result unless we are able to find a well-typed code that represents both the protocol and the attacker's capabilities. As there is a very large space of possible type annotations and adversary models, this requires a profound knowledge of the rationale behind the underlying type system as well as the components of the protocol being analyzed. The problem is aggravated when the protocol runs in environments containing compromised principals. These issues have rendered the use of such type systems somewhat impractical. This paper is an attempt to resolve the problem for authentication protocols in environments containing Dolev-Yao attackers. We concretize our ideas in F5, a security type checker, and suggest effective type annotations and so-called attacker interfaces representing the capabilities of a general adversary. Copyright (c) 2013 John Wiley & Sons, Ltd.