src/HOL/Auth/README.html
author haftmann
Fri Apr 20 11:21:42 2007 +0200 (2007-04-20)
changeset 22744 5cbe966d67a2
parent 15582 7219facb3fd0
child 51404 90a598019aeb
permissions -rw-r--r--
Isar definitions are now added explicitly to code theorem table
webertj@15283
     1
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
webertj@15283
     2
webertj@15582
     3
<!-- $Id$ -->
webertj@15582
     4
webertj@15582
     5
<HTML>
webertj@15582
     6
webertj@15582
     7
<HEAD>
webertj@15582
     8
  <meta http-equiv="content-type" content="text/html;charset=iso-8859-1">
webertj@15582
     9
  <TITLE>HOL/Auth/README</TITLE>
webertj@15582
    10
</HEAD>
webertj@15582
    11
webertj@15582
    12
<BODY>
paulson@3119
    13
paulson@13508
    14
<H1>Auth--The Inductive Approach to Verifying Security Protocols</H1>
paulson@3119
    15
paulson@3119
    16
<P>Cryptographic protocols are of major importance, especially with the
paulson@14004
    17
growing use of the Internet.  This directory demonstrates the ``inductive
paulson@14004
    18
method'' of protocol verification, which is described in <A
paulson@13508
    19
HREF="http://www.cl.cam.ac.uk/users/lcp/papers/protocols.html">various
paulson@13508
    20
papers</A>.  The operational semantics of protocol participants is defined
paulson@14004
    21
inductively.
paulson@13508
    22
paulson@13508
    23
<P>This directory contains proofs concerning
paulson@3119
    24
paulson@3119
    25
<UL>
paulson@3119
    26
<LI>three versions of the Otway-Rees protocol
paulson@3119
    27
paulson@14004
    28
<LI>the Needham-Schroeder shared-key protocol
paulson@14004
    29
paulson@14004
    30
<LI>the Needham-Schroeder public-key protocol (original and with Lowe's
paulson@14004
    31
modification)
paulson@3119
    32
paulson@6452
    33
<LI>two versions of Kerberos: the simplified form published in the BAN paper
paulson@6452
    34
	and also the full protocol (Kerberos IV)
paulson@6400
    35
paulson@6400
    36
<LI>three versions of the Yahalom protocol, including a bad one that 
paulson@6400
    37
	illustrates the purpose of the Oops rule
paulson@3119
    38
paulson@4594
    39
<LI>a novel recursive authentication protocol 
paulson@4594
    40
paulson@4594
    41
<LI>the Internet protocol TLS
paulson@14004
    42
paulson@14004
    43
<LI>The certified e-mail protocol of Abadi et al.
paulson@3119
    44
</UL>
paulson@3119
    45
paulson@14946
    46
<P>Frederic Blanqui has contributed a theory of guardedness, which is
paulson@14946
    47
demonstrated by proofs of some roving agent protocols.
paulson@14004
    48
paulson@3119
    49
<HR>
paulson@14004
    50
<P>Last modified $Date$
paulson@3119
    51
paulson@3119
    52
<ADDRESS>
paulson@13508
    53
<A
paulson@13508
    54
HREF="http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</A>,
paulson@13508
    55
<A HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
paulson@3119
    56
</ADDRESS>
webertj@15582
    57
</BODY>
webertj@15582
    58
</HTML>