| author | paulson |
| Tue, 23 Dec 1997 11:56:09 +0100 | |
| changeset 4476 | fbdc87f8ac7e |
| parent 3119 | bb2ee88aa43f |
| child 4594 | f8d4387b40d9 |
| 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 |
|
|
bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset
|
4 |
<H2>Auth--The Inductive Approach to Verifying Security Protocols</H2> |
|
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 |
|
bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset
|
7 |
growing use of the Internet. This directory demonstrates a <A |
|
bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset
|
8 |
HREF="http://www.cl.cam.ac.uk/ftp/papers/reports/TR409-lcp-Proving-Properties-of-Security-Protocols-by-Induction.dvi.gz">new |
|
bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset
|
9 |
proof method</A>. The operational semantics of protocol participants is |
|
bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset
|
10 |
defined inductively. The directory contains proofs concerning |
|
bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset
|
11 |
|
|
bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset
|
12 |
<UL> |
|
bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset
|
13 |
<LI>three versions of the Otway-Rees protocol |
|
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 |
<LI>the Needham-Schroeder protocol (<A |
|
bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset
|
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> |
|
bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset
|
17 |
and shared-key versions) |
|
bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset
|
18 |
|
|
bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset
|
19 |
<LI>two versions of the Yahalom protocol |
|
bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset
|
20 |
|
|
bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset
|
21 |
<LI>a novel <A HREF="http://www.cl.cam.ac.uk/ftp/papers/reports/TR418-lcp-recur.ps.gz">recursive</A> authentication protocol |
|
bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset
|
22 |
</UL> |
|
bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset
|
23 |
|
|
bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset
|
24 |
<HR> |
|
bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset
|
25 |
<P>Last modified 7 May 1997 |
|
bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset
|
26 |
|
|
bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset
|
27 |
<ADDRESS> |
|
bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset
|
28 |
<A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A> |
|
bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset
|
29 |
</ADDRESS> |
|
bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset
|
30 |
</BODY></HTML> |