src/HOL/Auth/README.html
author paulson
Tue Jun 15 10:47:08 2004 +0200 (2004-06-15)
changeset 14946 8aea9f96847f
parent 14004 f7382ee9b574
child 15283 f21466450330
permissions -rw-r--r--
fixed bad link
     1 <HTML><HEAD><TITLE>HOL/Auth/README</TITLE></HEAD><BODY>
     2 
     3 <H1>Auth--The Inductive Approach to Verifying Security Protocols</H1>
     4 
     5 <P>Cryptographic protocols are of major importance, especially with the
     6 growing use of the Internet.  This directory demonstrates the ``inductive
     7 method'' of protocol verification, which is described in <A
     8 HREF="http://www.cl.cam.ac.uk/users/lcp/papers/protocols.html">various
     9 papers</A>.  The operational semantics of protocol participants is defined
    10 inductively.
    11 
    12 <P>This directory contains proofs concerning
    13 
    14 <UL>
    15 <LI>three versions of the Otway-Rees protocol
    16 
    17 <LI>the Needham-Schroeder shared-key protocol
    18 
    19 <LI>the Needham-Schroeder public-key protocol (original and with Lowe's
    20 modification)
    21 
    22 <LI>two versions of Kerberos: the simplified form published in the BAN paper
    23 	and also the full protocol (Kerberos IV)
    24 
    25 <LI>three versions of the Yahalom protocol, including a bad one that 
    26 	illustrates the purpose of the Oops rule
    27 
    28 <LI>a novel recursive authentication protocol 
    29 
    30 <LI>the Internet protocol TLS
    31 
    32 <LI>The certified e-mail protocol of Abadi et al.
    33 </UL>
    34 
    35 <P>Frederic Blanqui has contributed a theory of guardedness, which is
    36 demonstrated by proofs of some roving agent protocols.
    37 
    38 <HR>
    39 <P>Last modified $Date$
    40 
    41 <ADDRESS>
    42 <A
    43 HREF="http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</A>,
    44 <A HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
    45 </ADDRESS>
    46 </BODY></HTML>