src/HOL/Auth/README.html
author paulson
Fri, 11 Jul 1997 13:26:15 +0200
changeset 3512 9dcb4daa15e8
parent 3119 bb2ee88aa43f
child 4594 f8d4387b40d9
permissions -rw-r--r--
Moving common declarations and proofs from theories "Shared" and "Public" to "Event". NB the original "Event" theory was later renamed "Shared". Addition of the Notes constructor to datatype "event".

<!-- $Id$ -->
<HTML><HEAD><TITLE>HOL/Auth/README</TITLE></HEAD><BODY>

<H2>Auth--The Inductive Approach to Verifying Security Protocols</H2>

<P>Cryptographic protocols are of major importance, especially with the
growing use of the Internet.  This directory demonstrates a <A
HREF="http://www.cl.cam.ac.uk/ftp/papers/reports/TR409-lcp-Proving-Properties-of-Security-Protocols-by-Induction.dvi.gz">new
proof method</A>.  The operational semantics of protocol participants is
defined inductively.  The directory contains proofs concerning

<UL>
<LI>three versions of the Otway-Rees protocol

<LI>the Needham-Schroeder protocol (<A
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>
and shared-key versions)

<LI>two versions of the Yahalom protocol

<LI>a novel <A HREF="http://www.cl.cam.ac.uk/ftp/papers/reports/TR418-lcp-recur.ps.gz">recursive</A> authentication protocol 
</UL>

<HR>
<P>Last modified 7 May 1997

<ADDRESS>
<A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
</ADDRESS>
</BODY></HTML>