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