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>