src/HOL/Auth/README.html
changeset 4594 f8d4387b40d9
parent 3119 bb2ee88aa43f
child 6400 1f495d4d922b
equal deleted inserted replaced
4593:6fc8f224655f 4594:f8d4387b40d9
     3 
     3 
     4 <H2>Auth--The Inductive Approach to Verifying Security Protocols</H2>
     4 <H2>Auth--The Inductive Approach to Verifying Security Protocols</H2>
     5 
     5 
     6 <P>Cryptographic protocols are of major importance, especially with the
     6 <P>Cryptographic protocols are of major importance, especially with the
     7 growing use of the Internet.  This directory demonstrates a <A
     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
     8 HREF="http://www.cl.cam.ac.uk/users/lcp/papers/protocols.html">new
     9 proof method</A>.  The operational semantics of protocol participants is
     9 proof method</A>.  The operational semantics of protocol participants is
    10 defined inductively.  The directory contains proofs concerning
    10 defined inductively.  The directory contains proofs concerning
    11 
    11 
    12 <UL>
    12 <UL>
    13 <LI>three versions of the Otway-Rees protocol
    13 <LI>three versions of the Otway-Rees protocol
    14 
    14 
    15 <LI>the Needham-Schroeder protocol (<A
    15 <LI>the Needham-Schroeder protocol (public-key and shared-key versions)
    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 
    16 
    19 <LI>two versions of the Yahalom protocol
    17 <LI>two versions of the Yahalom protocol
    20 
    18 
    21 <LI>a novel <A HREF="http://www.cl.cam.ac.uk/ftp/papers/reports/TR418-lcp-recur.ps.gz">recursive</A> authentication protocol 
    19 <LI>a novel recursive authentication protocol 
       
    20 
       
    21 <LI>the Internet protocol TLS
    22 </UL>
    22 </UL>
    23 
    23 
    24 <HR>
    24 <HR>
    25 <P>Last modified 7 May 1997
    25 <P>Last modified 30 Jan 1998
    26 
    26 
    27 <ADDRESS>
    27 <ADDRESS>
    28 <A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
    28 <A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
    29 </ADDRESS>
    29 </ADDRESS>
    30 </BODY></HTML>
    30 </BODY></HTML>