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