author  paulson 
Thu, 19 Dec 1996 11:58:39 +0100  
changeset 2451  ce85a2aafc7a 
parent 2376  f5c61fd9b9b6 
child 2516  4d68fbe6378b 
permissions  rwrr 
1934  1 
(* Title: HOL/Auth/Shared 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1996 University of Cambridge 

5 

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

7 

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

9 
*) 

10 

11 
Shared = Message + List + 

12 

13 
consts 

1943  14 
shrK :: agent => key (*symmetric keys*) 
1967  15 

1934  16 
rules 
1943  17 
isSym_shrK "isSymKey (shrK A)" 
1934  18 

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

2032  20 
initState :: [agent set, agent] => msg set 
1934  21 

22 
primrec initState agent 

2319  23 
(*Server knows all longterm keys; other agents know only their own*) 
2032  24 
initState_Server "initState lost Server = Key `` range shrK" 
25 
initState_Friend "initState lost (Friend i) = {Key (shrK (Friend i))}" 

2064  26 
initState_Spy "initState lost Spy = Key``shrK``lost" 
2032  27 

1934  28 

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

30 
event = Says agent agent msg 

31 

32 
consts 

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

34 

35 
primrec sees1 event 

2078  36 
(*Spy reads all traffic whether addressed to him or not*) 
37 
sees1_Says "sees1 A (Says A' B X) = (if A:{B,Spy} then {X} else {})" 

1934  38 

39 
consts 

2032  40 
sees :: [agent set, agent, event list] => msg set 
1934  41 

42 
primrec sees list 

2032  43 
sees_Nil "sees lost A [] = initState lost A" 
44 
sees_Cons "sees lost A (ev#evs) = sees1 A ev Un sees lost A evs" 

1934  45 

46 

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

47 
(*Agents generate random (symmetric) keys and nonces. 
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2376
diff
changeset

48 
The numeric argument is typically the length of the current trace. 
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2376
diff
changeset

49 
An injective pairing function allows multiple keys/nonces to be generated 
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2376
diff
changeset

50 
in one protocol round. A typical candidate for npair(i,j) is 
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2376
diff
changeset

51 
2^j(2i+1) 
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2376
diff
changeset

52 
*) 
2376
f5c61fd9b9b6
Temporary additions (random) for the nested OtwayRees protocol
paulson
parents:
2319
diff
changeset

53 

1934  54 
consts 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2376
diff
changeset

55 
nPair :: "nat*nat => nat" 
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2376
diff
changeset

56 
newN :: "nat => nat" 
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2376
diff
changeset

57 
newK :: "nat => key" 
1934  58 

59 
rules 

2376
f5c61fd9b9b6
Temporary additions (random) for the nested OtwayRees protocol
paulson
parents:
2319
diff
changeset

60 
inj_shrK "inj shrK" 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2376
diff
changeset

61 
inj_nPair "inj nPair" 
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2376
diff
changeset

62 
inj_newN "inj newN" 
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2376
diff
changeset

63 
inj_newK "inj newK" 
2032  64 

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

65 
newK_neq_shrK "newK i ~= shrK A" 
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2376
diff
changeset

66 
isSym_newK "isSymKey (newK i)" 
1934  67 

68 
end 