src/HOL/Auth/README.html
author paulson
Thu Mar 18 10:41:33 1999 +0100 (1999-03-18)
changeset 6400 1f495d4d922b
parent 4594 f8d4387b40d9
child 6452 6a1b393ccdc0
permissions -rw-r--r--
added new theory Yahalom_Bad
paulson@3119
     1
<!-- $Id$ -->
paulson@3119
     2
<HTML><HEAD><TITLE>HOL/Auth/README</TITLE></HEAD><BODY>
paulson@3119
     3
paulson@3119
     4
<H2>Auth--The Inductive Approach to Verifying Security Protocols</H2>
paulson@3119
     5
paulson@3119
     6
<P>Cryptographic protocols are of major importance, especially with the
paulson@3119
     7
growing use of the Internet.  This directory demonstrates a <A
paulson@4594
     8
HREF="http://www.cl.cam.ac.uk/users/lcp/papers/protocols.html">new
paulson@3119
     9
proof method</A>.  The operational semantics of protocol participants is
paulson@3119
    10
defined inductively.  The directory contains proofs concerning
paulson@3119
    11
paulson@3119
    12
<UL>
paulson@3119
    13
<LI>three versions of the Otway-Rees protocol
paulson@3119
    14
paulson@4594
    15
<LI>the Needham-Schroeder protocol (public-key and shared-key versions)
paulson@3119
    16
paulson@6400
    17
<LI>the Kerberos protocol (the simplified form published in the BAN paper)
paulson@6400
    18
paulson@6400
    19
<LI>three versions of the Yahalom protocol, including a bad one that 
paulson@6400
    20
	illustrates the purpose of the Oops rule
paulson@3119
    21
paulson@4594
    22
<LI>a novel recursive authentication protocol 
paulson@4594
    23
paulson@4594
    24
<LI>the Internet protocol TLS
paulson@3119
    25
</UL>
paulson@3119
    26
paulson@3119
    27
<HR>
paulson@4594
    28
<P>Last modified 30 Jan 1998
paulson@3119
    29
paulson@3119
    30
<ADDRESS>
paulson@3119
    31
<A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
paulson@3119
    32
</ADDRESS>
paulson@3119
    33
</BODY></HTML>