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
     1 <!-- $Id$ -->
     2 <HTML><HEAD><TITLE>HOL/Auth/README</TITLE></HEAD><BODY>
     3 
     4 <H2>Auth--The Inductive Approach to Verifying Security Protocols</H2>
     5 
     6 <P>Cryptographic protocols are of major importance, especially with the
     7 growing use of the Internet.  This directory demonstrates a <A
     8 HREF="http://www.cl.cam.ac.uk/ftp/papers/reports/TR409-lcp-Proving-Properties-of-Security-Protocols-by-Induction.dvi.gz">new
     9 proof method</A>.  The operational semantics of protocol participants is
    10 defined inductively.  The directory contains proofs concerning
    11 
    12 <UL>
    13 <LI>three versions of the Otway-Rees protocol
    14 
    15 <LI>the Needham-Schroeder protocol (<A
    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>
    17 and shared-key versions)
    18 
    19 <LI>two versions of the Yahalom protocol
    20 
    21 <LI>a novel <A HREF="http://www.cl.cam.ac.uk/ftp/papers/reports/TR418-lcp-recur.ps.gz">recursive</A> authentication protocol 
    22 </UL>
    23 
    24 <HR>
    25 <P>Last modified 7 May 1997
    26 
    27 <ADDRESS>
    28 <A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
    29 </ADDRESS>
    30 </BODY></HTML>