author  paulson 
Fri, 29 Nov 1996 18:03:21 +0100  
changeset 2284  80ebd1a213fd 
parent 2121  7e118eb32bdc 
child 2373  490ffa16952e 
permissions  rwrr 
1839  1 
(* Title: HOL/Auth/Message 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1996 University of Cambridge 

5 

6 
Datatypes of agents and messages; 

1913  7 
Inductive relations "parts", "analz" and "synth" 
1839  8 
*) 
9 

10 
Message = Arith + 

11 

12 
(*Is there a difference between a nonce and arbitrary numerical data? 

13 
Do we need a type of nonces?*) 

14 

15 
types 

16 
key = nat 

17 

18 
consts 

19 
invKey :: key=>key 

20 

21 
rules 

22 
invKey "invKey (invKey K) = K" 

23 

24 
(*The inverse of a symmetric key is itself; 

25 
that of a public key is the private key and vice versa*) 

26 

27 
constdefs 

28 
isSymKey :: key=>bool 

29 
"isSymKey K == (invKey K = K)" 

30 

2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2121
diff
changeset

31 
(*We do not assume Crypt (invKey K) (Crypt K X) = X 
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2121
diff
changeset

32 
because Crypt a is constructor! We assume that encryption is injective, 
1839  33 
which is not true in the real world. The alternative is to take 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2121
diff
changeset

34 
Crypt an as uninterpreted function symbol satisfying the equation 
1839  35 
above. This seems to require moving to ZF and regarding msg as an 
36 
inductive definition instead of a datatype.*) 

37 

38 
datatype (*We allow any number of friendly agents*) 

2032  39 
agent = Server  Friend nat  Spy 
1839  40 

41 
datatype (*Messages are agent names, nonces, keys, pairs and encryptions*) 

42 
msg = Agent agent 

43 
 Nonce nat 

44 
 Key key 

45 
 MPair msg msg 

2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2121
diff
changeset

46 
 Crypt key msg 
1839  47 

48 
(*Allows messages of the form {A,B,NA}, etc...*) 

49 
syntax 

1947  50 
"@MTuple" :: "['a, args] => 'a * 'b" ("(2{_,/ _})") 
1839  51 

52 
translations 

53 
"{x, y, z}" == "{x, {y, z}}" 

54 
"{x, y}" == "MPair x y" 

55 

56 

57 
constdefs (*Keys useful to decrypt elements of a message set*) 

58 
keysFor :: msg set => key set 

2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2121
diff
changeset

59 
"keysFor H == invKey `` {K. EX X. Crypt K X : H}" 
1839  60 

61 
(** Inductive definition of all "parts" of a message. **) 

62 

63 
consts parts :: msg set => msg set 

64 
inductive "parts H" 

65 
intrs 

66 
Inj "X: H ==> X: parts H" 

67 
Fst "{X,Y} : parts H ==> X : parts H" 

68 
Snd "{X,Y} : parts H ==> Y : parts H" 

2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2121
diff
changeset

69 
Body "Crypt K X : parts H ==> X : parts H" 
1839  70 

71 

1913  72 
(** Inductive definition of "analz"  what can be broken down from a set of 
1839  73 
messages, including keys. A form of downward closure. Pairs can 
74 
be taken apart; messages decrypted with known keys. **) 

75 

1913  76 
consts analz :: msg set => msg set 
77 
inductive "analz H" 

1839  78 
intrs 
1913  79 
Inj "X: H ==> X: analz H" 
80 
Fst "{X,Y} : analz H ==> X : analz H" 

81 
Snd "{X,Y} : analz H ==> Y : analz H" 

2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2121
diff
changeset

82 
Decrypt "[ Crypt K X : analz H; Key(invKey K): analz H ] ==> X : analz H" 
1839  83 

84 

1913  85 
(** Inductive definition of "synth"  what can be built up from a set of 
1839  86 
messages. A form of upward closure. Pairs can be built, messages 
87 
encrypted with known keys. Agent names may be quoted. **) 

88 

1913  89 
consts synth :: msg set => msg set 
90 
inductive "synth H" 

1839  91 
intrs 
1913  92 
Inj "X: H ==> X: synth H" 
93 
Agent "Agent agt : synth H" 

94 
MPair "[ X: synth H; Y: synth H ] ==> {X,Y} : synth H" 

2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2121
diff
changeset

95 
Crypt "[ X: synth H; Key(K): H ] ==> Crypt K X : synth H" 
1839  96 

97 
end 