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