author  nipkow 
Thu, 05 Jun 1997 14:40:35 +0200  
changeset 3414  804c8a178a7f 
parent 2516  4d68fbe6378b 
child 3472  fb3c38c88c08 
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 

2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

11 
Shared = Message + List + Finite + 
1934  12 

13 
consts 

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

1934  16 
rules 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

17 
(*ALL keys are symmetric*) 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

18 
isSym_keys "isSymKey K" 
1934  19 

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

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

23 
primrec initState agent 

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

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

1934  29 

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

31 
event = Says agent agent msg 

32 

33 
consts 

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

35 

36 
primrec sees1 event 

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

1934  39 

40 
consts 

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

43 
primrec sees list 

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

1934  46 

47 

2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

48 
constdefs 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

49 
(*Set of items that might be visible to somebody: complement of the set 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

50 
of fresh items*) 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

51 
used :: event list => msg set 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

52 
"used evs == parts (UN lost B. sees lost B evs)" 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

53 

4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

54 

4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

55 
rules 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

56 
(*Unlike the corresponding property of nonces, this cannot be proved. 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

57 
We have infinitely many agents and there is nothing to stop their 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

58 
longterm keys from exhausting all the natural numbers. The axiom 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

59 
assumes that their keys are dispersed so as to leave room for infinitely 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

60 
many fresh session keys. We could, alternatively, restrict agents to 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

61 
an unspecified finite number.*) 
3414
804c8a178a7f
Modified a few defs and proofs because of the changes to theory Finite.thy.
nipkow
parents:
2516
diff
changeset

62 
Key_supply_ax "finite KK ==> EX K. K ~: KK & Key K ~: used evs" 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

63 

4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

64 

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

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

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

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

68 
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

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

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

71 

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

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

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

75 
newK :: "nat => key" 
1934  76 

77 
rules 

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

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

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

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

81 
inj_newK "inj newK" 
2032  82 

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

83 
newK_neq_shrK "newK i ~= shrK A" 
1934  84 

85 
end 