Title :
Mechanized proofs for a recursive authentication protocol
Author :
Paulson, Lawrence C.
Author_Institution :
Comput. Lab., Cambridge Univ., UK
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;
Conference_Titel :
Computer Security Foundations Workshop, 1997. Proceedings., 10th
Conference_Location :
Rockport, MA
Print_ISBN :
0-8186-7990-5
DOI :
10.1109/CSFW.1997.596790
