paulson@1934

1 
(* Title: HOL/Auth/Shared

paulson@1934

2 
ID: $Id$

paulson@1934

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory

paulson@1934

4 
Copyright 1996 University of Cambridge

paulson@1934

5 

paulson@1934

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

paulson@1934

7 

paulson@3512

8 
Shared, longterm keys; initial states of agents

paulson@1934

9 
*)

paulson@1934

10 

paulson@3512

11 
Shared = Event + Finite +

paulson@1934

12 

paulson@1934

13 
consts

paulson@1943

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

paulson@1967

15 

paulson@1934

16 
rules

paulson@3472

17 
isSym_keys "isSymKey K" (*All keys are symmetric*)

paulson@3472

18 
inj_shrK "inj shrK" (*No two agents have the same longterm key*)

paulson@1934

19 

paulson@1934

20 
primrec initState agent

paulson@2319

21 
(*Server knows all longterm keys; other agents know only their own*)

paulson@2032

22 
initState_Server "initState lost Server = Key `` range shrK"

paulson@2032

23 
initState_Friend "initState lost (Friend i) = {Key (shrK (Friend i))}"

paulson@2064

24 
initState_Spy "initState lost Spy = Key``shrK``lost"

paulson@2032

25 

paulson@1934

26 

paulson@2516

27 
rules

paulson@2516

28 
(*Unlike the corresponding property of nonces, this cannot be proved.

paulson@2516

29 
We have infinitely many agents and there is nothing to stop their

paulson@2516

30 
longterm keys from exhausting all the natural numbers. The axiom

paulson@2516

31 
assumes that their keys are dispersed so as to leave room for infinitely

paulson@2516

32 
many fresh session keys. We could, alternatively, restrict agents to

paulson@2516

33 
an unspecified finite number.*)

nipkow@3414

34 
Key_supply_ax "finite KK ==> EX K. K ~: KK & Key K ~: used evs"

paulson@2516

35 

paulson@1934

36 
end
