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