| author | paulson |
| Wed, 21 Aug 2002 15:53:30 +0200 | |
| changeset 13508 | 890d736b93a5 |
| parent 6452 | 6a1b393ccdc0 |
| child 14004 | f7382ee9b574 |
| permissions | -rw-r--r-- |
|
3119
bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset
|
1 |
<!-- $Id$ --> |
|
bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset
|
2 |
<HTML><HEAD><TITLE>HOL/Auth/README</TITLE></HEAD><BODY> |
|
bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset
|
3 |
|
| 13508 | 4 |
<H1>Auth--The Inductive Approach to Verifying Security Protocols</H1> |
|
3119
bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset
|
5 |
|
|
bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset
|
6 |
<P>Cryptographic protocols are of major importance, especially with the |
| 13508 | 7 |
growing use of the Internet. This directory demonstrates a new proof method, |
8 |
which is described in <A |
|
9 |
HREF="http://www.cl.cam.ac.uk/users/lcp/papers/protocols.html">various |
|
10 |
papers</A>. The operational semantics of protocol participants is defined |
|
11 |
inductively. |
|
12 |
||
13 |
<P>This directory contains proofs concerning |
|
|
3119
bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset
|
14 |
|
|
bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset
|
15 |
<UL> |
|
bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset
|
16 |
<LI>three versions of the Otway-Rees protocol |
|
bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset
|
17 |
|
| 4594 | 18 |
<LI>the Needham-Schroeder protocol (public-key and shared-key versions) |
|
3119
bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset
|
19 |
|
| 6452 | 20 |
<LI>two versions of Kerberos: the simplified form published in the BAN paper |
21 |
and also the full protocol (Kerberos IV) |
|
| 6400 | 22 |
|
23 |
<LI>three versions of the Yahalom protocol, including a bad one that |
|
24 |
illustrates the purpose of the Oops rule |
|
|
3119
bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset
|
25 |
|
| 4594 | 26 |
<LI>a novel recursive authentication protocol |
27 |
||
28 |
<LI>the Internet protocol TLS |
|
|
3119
bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset
|
29 |
</UL> |
|
bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset
|
30 |
|
|
bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset
|
31 |
<HR> |
| 13508 | 32 |
<P>Last modified 20 August 2002 |
|
3119
bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset
|
33 |
|
|
bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset
|
34 |
<ADDRESS> |
| 13508 | 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> |
|
|
3119
bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset
|
38 |
</ADDRESS> |
|
bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset
|
39 |
</BODY></HTML> |