author  paulson 
Thu, 18 Sep 1997 13:24:04 +0200  
changeset 3683  aafe719dff14 
parent 3519  ab0a9fbed4c0 
child 5183  89f162de39cf 
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*) 

3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3512
diff
changeset

24 
initState_Server "initState Server = 
2318  25 
insert (Key (priK Server)) (Key `` range pubK)" 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3512
diff
changeset

26 
initState_Friend "initState (Friend i) = 
2318  27 
insert (Key (priK (Friend i))) (Key `` range pubK)" 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3512
diff
changeset

28 
initState_Spy "initState Spy = 
3683  29 
(Key``invKey``pubK``bad) Un (Key `` range pubK)" 
2318  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 