updated text
authorpaulson
Mon May 12 12:26:50 2003 +0200 (2003-05-12)
changeset 14004f7382ee9b574
parent 14003 740788f3f6b7
child 14005 5ba84fdb680b
updated text
src/HOL/Auth/README.html
     1.1 --- a/src/HOL/Auth/README.html	Mon May 12 12:12:19 2003 +0200
     1.2 +++ b/src/HOL/Auth/README.html	Mon May 12 12:26:50 2003 +0200
     1.3 @@ -1,21 +1,23 @@
     1.4 -<!-- $Id$ -->
     1.5  <HTML><HEAD><TITLE>HOL/Auth/README</TITLE></HEAD><BODY>
     1.6  
     1.7  <H1>Auth--The Inductive Approach to Verifying Security Protocols</H1>
     1.8  
     1.9  <P>Cryptographic protocols are of major importance, especially with the
    1.10 -growing use of the Internet.  This directory demonstrates a new proof method,
    1.11 -which is described in <A
    1.12 +growing use of the Internet.  This directory demonstrates the ``inductive
    1.13 +method'' of protocol verification, which is described in <A
    1.14  HREF="http://www.cl.cam.ac.uk/users/lcp/papers/protocols.html">various
    1.15  papers</A>.  The operational semantics of protocol participants is defined
    1.16 -inductively.  
    1.17 +inductively.
    1.18  
    1.19  <P>This directory contains proofs concerning
    1.20  
    1.21  <UL>
    1.22  <LI>three versions of the Otway-Rees protocol
    1.23  
    1.24 -<LI>the Needham-Schroeder protocol (public-key and shared-key versions)
    1.25 +<LI>the Needham-Schroeder shared-key protocol
    1.26 +
    1.27 +<LI>the Needham-Schroeder public-key protocol (original and with Lowe's
    1.28 +modification)
    1.29  
    1.30  <LI>two versions of Kerberos: the simplified form published in the BAN paper
    1.31  	and also the full protocol (Kerberos IV)
    1.32 @@ -26,10 +28,15 @@
    1.33  <LI>a novel recursive authentication protocol 
    1.34  
    1.35  <LI>the Internet protocol TLS
    1.36 +
    1.37 +<LI>The certified e-mail protocol of Abadi et al.
    1.38  </UL>
    1.39  
    1.40 +<P>Subdirectory <A HREF="Guard/">Guard</A> develops a theory of guardedness, by
    1.41 +Frederic Blanqui, and includes proofs of some roving agent protocols.
    1.42 +
    1.43  <HR>
    1.44 -<P>Last modified 20 August 2002
    1.45 +<P>Last modified $Date$
    1.46  
    1.47  <ADDRESS>
    1.48  <A