Mechanized proofs for a recursive authentication protocol

Author

Paulson, Lawrence C.

Author_Institution

Comput. Lab., Cambridge Univ., UK

fYear

1997

fDate

10-12 Jun 1997

Firstpage

84

Lastpage

94

Abstract

A novel protocol has been formally analyzed using the prover Isabelle/HOL, following the inductive approach described in earlier work (L.C. Paulson, 1997). There is no limit on the length of a run, the nesting of messages or the number of agents involved. A single run of the protocol delivers session keys for all the agents, allowing neighbours to perform mutual authentication. The basic security theorem states that session keys are correctly delivered to adjacent pairs of honest agents, regardless of whether other agents in the chain are compromised. The protocol´s complexity caused some difficulties in the specification and proofs, but its symmetry reduced the number of theorems to prove

Keywords

formal specification; formal verification; message authentication; protocols; theorem proving; Isabelle/HOL; adjacent pairs; agents; basic security theorem; honest agents; inductive approach; mechanized proofs; message nesting; mutual authentication; protocol complexity; recursive authentication protocol; session keys; specification; symmetry; Authentication; Laboratories; Protocols; Security;

fLanguage

English

Publisher

ieee

Conference_Titel

Computer Security Foundations Workshop, 1997. Proceedings., 10th

Conference_Location

Rockport, MA

ISSN

1063-6900

Print_ISBN

0-8186-7990-5

Type

conf

DOI

10.1109/CSFW.1997.596790

Filename

596790