author  paulson 
Fri, 11 Jul 1997 13:26:15 +0200  
changeset 3512  9dcb4daa15e8 
parent 3478  770939fecbb3 
child 3519  ab0a9fbed4c0 
permissions  rwrr 
2318  1 
(* Title: HOL/Auth/Public 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1996 University of Cambridge 

5 

3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3478
diff
changeset

6 
Theory of Public Keys (common to all publickey protocols) 
2318  7 

3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3478
diff
changeset

8 
Private and public keys; initial states of agents 
2318  9 
*) 
10 

3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3478
diff
changeset

11 
Public = Event + 
2318  12 

13 
consts 

14 
pubK :: agent => key 

15 

16 
syntax 

17 
priK :: agent => key 

18 

3478  19 
translations (*BEWARE! expressions like (inj priK) will NOT work!*) 
2318  20 
"priK x" == "invKey(pubK x)" 
21 

22 
primrec initState agent 

23 
(*Agents know their private key and all public keys*) 

24 
initState_Server "initState lost Server = 

25 
insert (Key (priK Server)) (Key `` range pubK)" 

26 
initState_Friend "initState lost (Friend i) = 

27 
insert (Key (priK (Friend i))) (Key `` range pubK)" 

28 
initState_Spy "initState lost Spy = 

29 
(Key``invKey``pubK``lost) Un (Key `` range pubK)" 

30 

31 

32 
rules 

33 
(*Public keys are disjoint, and never clash with private keys*) 

2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2318
diff
changeset

34 
inj_pubK "inj pubK" 
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2318
diff
changeset

35 
priK_neq_pubK "priK A ~= pubK B" 
2318  36 

37 
end 