Título: An epistemic analysis of authentication
Autores: Frydrychowicz, Maja
Fecha: 2011
Publicador: McGill University - MCGILL
Fuente:
Tipo: Electronic Thesis or Dissertation
Tema: Applied Sciences - Computer Science
Descripción: 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. In response, we use epistemic modal logic 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, as well as its predecessor, the Needham-Schroeder Public-Key Protocol, which is vulnerable to an impersonation attack. 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 by highlighting the role of agent knowledge.
Les protocoles d'authentification ont pour but d'empêcher l'usurpation d'identité: A est authentifié à B si B connaît l'identité de A. Il existe plusieurs approches formelles pour vérifier l'authentification dans les systèmes informatiques distribués. Cependent, bien que l'authentification soit directement liée à la connaissance des agents, elle a seulement été définie de façon formelle avec des algèbres de processus, le plus souvent en termes de contraintes sur l'ordre des évènements d'un protocole. Afin de combler cette lacune, nous utilisons la logique modale épistémique afin de définir l'authentification en termes de connaissances communes et donc comme un exemple d'actions coordonnées. Nous appliquons notre définition à la vérification formelle du protocole Needham-Schroeder-Lowe, ainsi qu'à son ancêtre, le protocole Needham-Schroeder, qui est vulnérable à une attaque d'usurpation d'identité. Ce faisant, nous raisonnons sur l'évolution de la connaissance avec une relation de conséquence épistémique définie en lien à des séquences état-action. Les résultats de notre vérification ajoutent aux autres analyses par algèbres de processus de ces deux protocoles en mettant de l'avant le rôle de la connaissance des agents.
Idioma: en