equal
deleted
inserted
replaced
1 <!-- $Id$ --> |
1 <!-- $Id$ --> |
2 <HTML><HEAD><TITLE>HOL/Auth/README</TITLE></HEAD><BODY> |
2 <HTML><HEAD><TITLE>HOL/Auth/README</TITLE></HEAD><BODY> |
3 |
3 |
4 <H2>Auth--The Inductive Approach to Verifying Security Protocols</H2> |
4 <H1>Auth--The Inductive Approach to Verifying Security Protocols</H1> |
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 new proof method, |
8 HREF="http://www.cl.cam.ac.uk/users/lcp/papers/protocols.html">new |
8 which is described in <A |
9 proof method</A>. The operational semantics of protocol participants is |
9 HREF="http://www.cl.cam.ac.uk/users/lcp/papers/protocols.html">various |
10 defined inductively. The directory contains proofs concerning |
10 papers</A>. The operational semantics of protocol participants is defined |
|
11 inductively. |
|
12 |
|
13 <P>This directory contains proofs concerning |
11 |
14 |
12 <UL> |
15 <UL> |
13 <LI>three versions of the Otway-Rees protocol |
16 <LI>three versions of the Otway-Rees protocol |
14 |
17 |
15 <LI>the Needham-Schroeder protocol (public-key and shared-key versions) |
18 <LI>the Needham-Schroeder protocol (public-key and shared-key versions) |
24 |
27 |
25 <LI>the Internet protocol TLS |
28 <LI>the Internet protocol TLS |
26 </UL> |
29 </UL> |
27 |
30 |
28 <HR> |
31 <HR> |
29 <P>Last modified 30 Jan 1998 |
32 <P>Last modified 20 August 2002 |
30 |
33 |
31 <ADDRESS> |
34 <ADDRESS> |
32 <A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A> |
35 <A |
|
36 HREF="http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</A>, |
|
37 <A HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A> |
33 </ADDRESS> |
38 </ADDRESS> |
34 </BODY></HTML> |
39 </BODY></HTML> |