author  paulson 
Thu, 19 Dec 1996 11:58:39 +0100  
changeset 2451  ce85a2aafc7a 
parent 2318  6d3f7c7f70b0 
child 2497  47de509bdd55 
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 

6 
Theory of Public Keys (common to all symmetrickey protocols) 

7 

8 
Server keys; initial states of agents; new nonces and keys; function "sees" 

9 
*) 

10 

11 
Public = Message + List + 

12 

13 
consts 

14 
pubK :: agent => key 

15 

16 
syntax 

17 
priK :: agent => key 

18 

19 
translations 

20 
"priK x" == "invKey(pubK x)" 

21 

22 
consts (*Initial states of agents  parameter of the construction*) 

23 
initState :: [agent set, agent] => msg set 

24 

25 
primrec initState agent 

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

27 
initState_Server "initState lost Server = 

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

29 
initState_Friend "initState lost (Friend i) = 

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

31 
initState_Spy "initState lost Spy = 

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

33 

34 

35 
datatype (*Messages, and components of agent stores*) 

36 
event = Says agent agent msg 

37 

38 
consts 

39 
sees1 :: [agent, event] => msg set 

40 

41 
primrec sees1 event 

42 
(*Spy reads all traffic whether addressed to him or not*) 

43 
sees1_Says "sees1 A (Says A' B X) = (if A:{B,Spy} then {X} else {})" 

44 

45 
consts 

46 
sees :: [agent set, agent, event list] => msg set 

47 

48 
primrec sees list 

49 
sees_Nil "sees lost A [] = initState lost A" 

50 
sees_Cons "sees lost A (ev#evs) = sees1 A ev Un sees lost A evs" 

51 

52 

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

53 
(*Agents generate "random" nonces, uniquely determined by their argument.*) 
2318  54 
consts 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2318
diff
changeset

55 
newN :: nat => nat 
2318  56 

57 
rules 

58 

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

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

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

61 
priK_neq_pubK "priK A ~= pubK B" 
2318  62 

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

63 
inj_newN "inj newN" 
2318  64 

65 
end 