loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
10th Computer Security Foundations Workshop (CSFW '97)
Mechanized proofs for a recursive authentication protocol
Rockport, Massachusetts
June 10-June 12
ISBN: 0-8186-7990-5
ASCII Text
x 
 
L.C. Paulson, "Mechanized proofs for a recursive authentication protocol," Computer Security Foundations Workshop, IEEE, pp. 84, 10th Computer Security Foundations Workshop (CSFW '97), 1997.
 
 
BibTex
x
 
@article{ 10.1109/CSFW.1997.596790,
author = {L.C. Paulson},
title = {Mechanized proofs for a recursive authentication protocol},
journal ={Computer Security Foundations Workshop, IEEE},
volume = {0},
year = {1997},
issn = {1063-6900},
pages = {84},
doi = {http://doi.ieeecomputersociety.org/10.1109/CSFW.1997.596790},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - Computer Security Foundations Workshop, IEEE
TI - Mechanized proofs for a recursive authentication protocol
SN - 1063-6900
SP
EP
A1 - L.C. Paulson,
PY - 1997
KW - protocols; mechanized proofs; recursive authentication protocol; Isabelle/HOL; inductive approach; message nesting; session keys; agents; mutual authentication; basic security theorem; adjacent pairs; honest agents; protocol complexity; specification; symmetry
VL - 0
JA - Computer Security Foundations Workshop, IEEE
ER -
 
L.C. Paulson, Comput. Lab., Cambridge Univ., UK
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.
Index Terms:
protocols; mechanized proofs; recursive authentication protocol; Isabelle/HOL; inductive approach; message nesting; session keys; agents; mutual authentication; basic security theorem; adjacent pairs; honest agents; protocol complexity; specification; symmetry
Citation:
L.C. Paulson, "Mechanized proofs for a recursive authentication protocol," csfw, pp.84, 10th Computer Security Foundations Workshop (CSFW '97), 1997
Usage of this product signifies your acceptance of the Terms of Use.