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