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

3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3472
diff
changeset

8 
Shared, longterm keys; initial states of agents 
1934  9 
*) 
10 

3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3472
diff
changeset

11 
Shared = Event + 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 
primrec initState agent 

2319  21 
(*Server knows all longterm keys; other agents know only their own*) 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3512
diff
changeset

22 
initState_Server "initState Server = Key `` range shrK" 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3512
diff
changeset

23 
initState_Friend "initState (Friend i) = {Key (shrK (Friend i))}" 
3683  24 
initState_Spy "initState Spy = Key``shrK``bad" 
2032  25 

1934  26 

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

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

28 
(*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

29 
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

30 
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

31 
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

32 
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

33 
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

34 
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

35 

1934  36 
end 