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