src/HOL/Auth/README.html
author paulson
Wed Aug 21 15:53:30 2002 +0200 (2002-08-21)
changeset 13508 890d736b93a5
parent 6452 6a1b393ccdc0
child 14004 f7382ee9b574
permissions -rw-r--r--
Frederic Blanqui's new "guard" examples
     1 <!-- $Id$ -->
     2 <HTML><HEAD><TITLE>HOL/Auth/README</TITLE></HEAD><BODY>
     3 
     4 <H1>Auth--The Inductive Approach to Verifying Security Protocols</H1>
     5 
     6 <P>Cryptographic protocols are of major importance, especially with the
     7 growing use of the Internet.  This directory demonstrates a new proof method,
     8 which is described in <A
     9 HREF="http://www.cl.cam.ac.uk/users/lcp/papers/protocols.html">various
    10 papers</A>.  The operational semantics of protocol participants is defined
    11 inductively.  
    12 
    13 <P>This directory contains proofs concerning
    14 
    15 <UL>
    16 <LI>three versions of the Otway-Rees protocol
    17 
    18 <LI>the Needham-Schroeder protocol (public-key and shared-key versions)
    19 
    20 <LI>two versions of Kerberos: the simplified form published in the BAN paper
    21 	and also the full protocol (Kerberos IV)
    22 
    23 <LI>three versions of the Yahalom protocol, including a bad one that 
    24 	illustrates the purpose of the Oops rule
    25 
    26 <LI>a novel recursive authentication protocol 
    27 
    28 <LI>the Internet protocol TLS
    29 </UL>
    30 
    31 <HR>
    32 <P>Last modified 20 August 2002
    33 
    34 <ADDRESS>
    35 <A
    36 HREF="http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</A>,
    37 <A HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
    38 </ADDRESS>
    39 </BODY></HTML>