src/HOL/Auth/README.html
changeset 3119 bb2ee88aa43f
child 4594 f8d4387b40d9
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Auth/README.html	Wed May 07 12:49:02 1997 +0200
     1.3 @@ -0,0 +1,30 @@
     1.4 +<!-- $Id$ -->
     1.5 +<HTML><HEAD><TITLE>HOL/Auth/README</TITLE></HEAD><BODY>
     1.6 +
     1.7 +<H2>Auth--The Inductive Approach to Verifying Security Protocols</H2>
     1.8 +
     1.9 +<P>Cryptographic protocols are of major importance, especially with the
    1.10 +growing use of the Internet.  This directory demonstrates a <A
    1.11 +HREF="http://www.cl.cam.ac.uk/ftp/papers/reports/TR409-lcp-Proving-Properties-of-Security-Protocols-by-Induction.dvi.gz">new
    1.12 +proof method</A>.  The operational semantics of protocol participants is
    1.13 +defined inductively.  The directory contains proofs concerning
    1.14 +
    1.15 +<UL>
    1.16 +<LI>three versions of the Otway-Rees protocol
    1.17 +
    1.18 +<LI>the Needham-Schroeder protocol (<A
    1.19 +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>
    1.20 +and shared-key versions)
    1.21 +
    1.22 +<LI>two versions of the Yahalom protocol
    1.23 +
    1.24 +<LI>a novel <A HREF="http://www.cl.cam.ac.uk/ftp/papers/reports/TR418-lcp-recur.ps.gz">recursive</A> authentication protocol 
    1.25 +</UL>
    1.26 +
    1.27 +<HR>
    1.28 +<P>Last modified 7 May 1997
    1.29 +
    1.30 +<ADDRESS>
    1.31 +<A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
    1.32 +</ADDRESS>
    1.33 +</BODY></HTML>