1 <!-- $Id$ --> |
|
2 <HTML><HEAD><TITLE>HOL/Auth/README</TITLE></HEAD><BODY> |
1 <HTML><HEAD><TITLE>HOL/Auth/README</TITLE></HEAD><BODY> |
3 |
2 |
4 <H1>Auth--The Inductive Approach to Verifying Security Protocols</H1> |
3 <H1>Auth--The Inductive Approach to Verifying Security Protocols</H1> |
5 |
4 |
6 <P>Cryptographic protocols are of major importance, especially with the |
5 <P>Cryptographic protocols are of major importance, especially with the |
7 growing use of the Internet. This directory demonstrates a new proof method, |
6 growing use of the Internet. This directory demonstrates the ``inductive |
8 which is described in <A |
7 method'' of protocol verification, which is described in <A |
9 HREF="http://www.cl.cam.ac.uk/users/lcp/papers/protocols.html">various |
8 HREF="http://www.cl.cam.ac.uk/users/lcp/papers/protocols.html">various |
10 papers</A>. The operational semantics of protocol participants is defined |
9 papers</A>. The operational semantics of protocol participants is defined |
11 inductively. |
10 inductively. |
12 |
11 |
13 <P>This directory contains proofs concerning |
12 <P>This directory contains proofs concerning |
14 |
13 |
15 <UL> |
14 <UL> |
16 <LI>three versions of the Otway-Rees protocol |
15 <LI>three versions of the Otway-Rees protocol |
17 |
16 |
18 <LI>the Needham-Schroeder protocol (public-key and shared-key versions) |
17 <LI>the Needham-Schroeder shared-key protocol |
|
18 |
|
19 <LI>the Needham-Schroeder public-key protocol (original and with Lowe's |
|
20 modification) |
19 |
21 |
20 <LI>two versions of Kerberos: the simplified form published in the BAN paper |
22 <LI>two versions of Kerberos: the simplified form published in the BAN paper |
21 and also the full protocol (Kerberos IV) |
23 and also the full protocol (Kerberos IV) |
22 |
24 |
23 <LI>three versions of the Yahalom protocol, including a bad one that |
25 <LI>three versions of the Yahalom protocol, including a bad one that |
24 illustrates the purpose of the Oops rule |
26 illustrates the purpose of the Oops rule |
25 |
27 |
26 <LI>a novel recursive authentication protocol |
28 <LI>a novel recursive authentication protocol |
27 |
29 |
28 <LI>the Internet protocol TLS |
30 <LI>the Internet protocol TLS |
|
31 |
|
32 <LI>The certified e-mail protocol of Abadi et al. |
29 </UL> |
33 </UL> |
30 |
34 |
|
35 <P>Subdirectory <A HREF="Guard/">Guard</A> develops a theory of guardedness, by |
|
36 Frederic Blanqui, and includes proofs of some roving agent protocols. |
|
37 |
31 <HR> |
38 <HR> |
32 <P>Last modified 20 August 2002 |
39 <P>Last modified $Date$ |
33 |
40 |
34 <ADDRESS> |
41 <ADDRESS> |
35 <A |
42 <A |
36 HREF="http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</A>, |
43 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> |
44 <A HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A> |