author  paulson 
Wed, 07 May 1997 12:49:02 +0200  
changeset 3119  bb2ee88aa43f 
child 4594  f8d4387b40d9 
permissions  rwrr 
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>AuthThe 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/TR409lcpProvingPropertiesofSecurityProtocolsbyInduction.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 OtwayRees 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 NeedhamSchroeder 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/TR413lcpMechanizedProofsofSecurityProtocolsNeedhamSchroederwithPublicKeys.dvi.gz">publickey</A> 
bb2ee88aa43f
Description of the Auth directory: security protocols proofs
paulson
parents:
diff
changeset

17 
and sharedkey 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/TR418lcprecur.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> 