src/HOL/Auth/README.html
author paulson
Fri Jul 04 17:34:55 1997 +0200 (1997-07-04)
changeset 3500 0d8ad2f192d8
parent 3119 bb2ee88aa43f
child 4594 f8d4387b40d9
permissions -rw-r--r--
New constant "certificate"--just an abbreviation
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@3119
     8
HREF="http://www.cl.cam.ac.uk/ftp/papers/reports/TR409-lcp-Proving-Properties-of-Security-Protocols-by-Induction.dvi.gz">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@3119
    15
<LI>the Needham-Schroeder protocol (<A
paulson@3119
    16
HREF="http://www.cl.cam.ac.uk/ftp/papers/reports/TR413-lcp-Mechanized-Proofs-of-Security-Protocols-Needham-Schroeder-with-Public-Keys.dvi.gz">public-key</A>
paulson@3119
    17
and shared-key versions)
paulson@3119
    18
paulson@3119
    19
<LI>two versions of the Yahalom protocol
paulson@3119
    20
paulson@3119
    21
<LI>a novel <A HREF="http://www.cl.cam.ac.uk/ftp/papers/reports/TR418-lcp-recur.ps.gz">recursive</A> authentication protocol 
paulson@3119
    22
</UL>
paulson@3119
    23
paulson@3119
    24
<HR>
paulson@3119
    25
<P>Last modified 7 May 1997
paulson@3119
    26
paulson@3119
    27
<ADDRESS>
paulson@3119
    28
<A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
paulson@3119
    29
</ADDRESS>
paulson@3119
    30
</BODY></HTML>