author  paulson 
Thu, 29 Mar 2001 10:44:37 +0200  
changeset 11230  756c5034f08b 
parent 11192  5fd02b905a9a 
child 11245  3d9d25a3375b 
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 

11189  10 
theory Message = Main 
11 
files ("Message_lemmas.ML"): 

12 

13 
(*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*) 

14 
lemma [simp] : "A Un (B Un A) = B Un A" 

15 
by blast 

1839  16 

17 
types 

18 
key = nat 

19 

20 
consts 

11189  21 
invKey :: "key=>key" 
1839  22 

11189  23 
axioms 
24 
invKey [simp] : "invKey (invKey K) = K" 

1839  25 

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

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

28 

29 
constdefs 

11230
756c5034f08b
misc tidying; changing the predicate isSymKey to the set symKeys
paulson
parents:
11192
diff
changeset

30 
symKeys :: "key set" 
756c5034f08b
misc tidying; changing the predicate isSymKey to the set symKeys
paulson
parents:
11192
diff
changeset

31 
"symKeys == {K. invKey K = K}" 
1839  32 

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

2032  34 
agent = Server  Friend nat  Spy 
1839  35 

3668  36 
datatype 
7057
b9ddbb925939
tweaked proofs to handle new freeness reasoning for data c onstructors
paulson
parents:
6807
diff
changeset

37 
msg = Agent agent (*Agent names*) 
b9ddbb925939
tweaked proofs to handle new freeness reasoning for data c onstructors
paulson
parents:
6807
diff
changeset

38 
 Number nat (*Ordinary integers, timestamps, ...*) 
b9ddbb925939
tweaked proofs to handle new freeness reasoning for data c onstructors
paulson
parents:
6807
diff
changeset

39 
 Nonce nat (*Unguessable nonces*) 
b9ddbb925939
tweaked proofs to handle new freeness reasoning for data c onstructors
paulson
parents:
6807
diff
changeset

40 
 Key key (*Crypto keys*) 
5234  41 
 Hash msg (*Hashing*) 
42 
 MPair msg msg (*Compound messages*) 

43 
 Crypt key msg (*Encryption, public or sharedkey*) 

1839  44 

5234  45 

46 
(*Concrete syntax: messages appear as {A,B,NA}, etc...*) 

47 
syntax 

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

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

9686  50 
syntax (xsymbols) 
11189  51 
"@MTuple" :: "['a, args] => 'a * 'b" ("(2\<lbrace>_,/ _\<rbrace>)") 
9686  52 

1839  53 
translations 
54 
"{x, y, z}" == "{x, {y, z}}" 

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

56 

57 

2484  58 
constdefs 
59 
(*Message Y, paired with a MAC computed with the help of X*) 

11189  60 
HPair :: "[msg,msg] => msg" ("(4Hash[_] /_)" [0, 1000]) 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2484
diff
changeset

61 
"Hash[X] Y == { Hash{X,Y}, Y}" 
2484  62 

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

11189  64 
keysFor :: "msg set => key set" 
11192  65 
"keysFor H == invKey ` {K. \<exists>X. Crypt K X \<in> H}" 
1839  66 

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

68 

11189  69 
consts parts :: "msg set => msg set" 
1839  70 
inductive "parts H" 
11189  71 
intros 
11192  72 
Inj [intro]: "X \<in> H ==> X \<in> parts H" 
73 
Fst: "{X,Y} \<in> parts H ==> X \<in> parts H" 

74 
Snd: "{X,Y} \<in> parts H ==> Y \<in> parts H" 

75 
Body: "Crypt K X \<in> parts H ==> X \<in> parts H" 

11189  76 

77 

78 
(*Monotonicity*) 

79 
lemma parts_mono: "G<=H ==> parts(G) <= parts(H)" 

80 
apply auto 

81 
apply (erule parts.induct) 

82 
apply (auto dest: Fst Snd Body) 

83 
done 

1839  84 

85 

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

89 

11189  90 
consts analz :: "msg set => msg set" 
1913  91 
inductive "analz H" 
11189  92 
intros 
11192  93 
Inj [intro,simp] : "X \<in> H ==> X \<in> analz H" 
94 
Fst: "{X,Y} \<in> analz H ==> X \<in> analz H" 

95 
Snd: "{X,Y} \<in> analz H ==> Y \<in> analz H" 

11189  96 
Decrypt [dest]: 
11192  97 
"[Crypt K X \<in> analz H; Key(invKey K): analz H] ==> X \<in> analz H" 
1839  98 

99 

11189  100 
(*Monotonicity; Lemma 1 of Lowe's paper*) 
101 
lemma analz_mono: "G<=H ==> analz(G) <= analz(H)" 

102 
apply auto 

103 
apply (erule analz.induct) 

104 
apply (auto dest: Fst Snd) 

105 
done 

106 

1913  107 
(** Inductive definition of "synth"  what can be built up from a set of 
1839  108 
messages. A form of upward closure. Pairs can be built, messages 
3668  109 
encrypted with known keys. Agent names are public domain. 
110 
Numbers can be guessed, but Nonces cannot be. **) 

1839  111 

11189  112 
consts synth :: "msg set => msg set" 
1913  113 
inductive "synth H" 
11189  114 
intros 
11192  115 
Inj [intro]: "X \<in> H ==> X \<in> synth H" 
116 
Agent [intro]: "Agent agt \<in> synth H" 

117 
Number [intro]: "Number n \<in> synth H" 

118 
Hash [intro]: "X \<in> synth H ==> Hash X \<in> synth H" 

119 
MPair [intro]: "[X \<in> synth H; Y \<in> synth H] ==> {X,Y} \<in> synth H" 

120 
Crypt [intro]: "[X \<in> synth H; Key(K) \<in> H] ==> Crypt K X \<in> synth H" 

11189  121 

122 
(*Monotonicity*) 

123 
lemma synth_mono: "G<=H ==> synth(G) <= synth(H)" 

124 
apply auto 

125 
apply (erule synth.induct) 

126 
apply (auto dest: Fst Snd Body) 

127 
done 

128 

129 
(*NO Agent_synth, as any Agent name can be synthesized. Ditto for Number*) 

11192  130 
inductive_cases Nonce_synth [elim!]: "Nonce n \<in> synth H" 
131 
inductive_cases Key_synth [elim!]: "Key K \<in> synth H" 

132 
inductive_cases Hash_synth [elim!]: "Hash X \<in> synth H" 

133 
inductive_cases MPair_synth [elim!]: "{X,Y} \<in> synth H" 

134 
inductive_cases Crypt_synth [elim!]: "Crypt K X \<in> synth H" 

11189  135 

136 
use "Message_lemmas.ML" 

137 

138 
method_setup spy_analz = {* 

139 
Method.no_args (Method.METHOD (fn facts => spy_analz_tac 1)) *} 

140 
"for proving the Fake case when analz is involved" 

1839  141 

142 
end 