author  paulson 
Tue, 01 Jul 1997 10:39:28 +0200  
changeset 3472  fb3c38c88c08 
parent 3414  804c8a178a7f 
child 3512  9dcb4daa15e8 
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 
3472
fb3c38c88c08
Deleted the obsolete operators newK, newN and nPair
paulson
parents:
3414
diff
changeset

17 
isSym_keys "isSymKey K" (*All keys are symmetric*) 
fb3c38c88c08
Deleted the obsolete operators newK, newN and nPair
paulson
parents:
3414
diff
changeset

18 
inj_shrK "inj shrK" (*No two agents have the same longterm key*) 
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 

1934  64 
end 