|
1 (* Title: HOL/Quotient_Examples/Quotient_Message.thy |
|
2 Author: Christian Urban |
|
3 |
|
4 Message datatype, based on an older version by Larry Paulson. |
|
5 *) |
|
6 theory Quotient_Message |
|
7 imports Main Quotient_Syntax |
|
8 begin |
|
9 |
|
10 subsection{*Defining the Free Algebra*} |
|
11 |
|
12 datatype |
|
13 freemsg = NONCE nat |
|
14 | MPAIR freemsg freemsg |
|
15 | CRYPT nat freemsg |
|
16 | DECRYPT nat freemsg |
|
17 |
|
18 inductive |
|
19 msgrel::"freemsg \<Rightarrow> freemsg \<Rightarrow> bool" (infixl "\<sim>" 50) |
|
20 where |
|
21 CD: "CRYPT K (DECRYPT K X) \<sim> X" |
|
22 | DC: "DECRYPT K (CRYPT K X) \<sim> X" |
|
23 | NONCE: "NONCE N \<sim> NONCE N" |
|
24 | MPAIR: "\<lbrakk>X \<sim> X'; Y \<sim> Y'\<rbrakk> \<Longrightarrow> MPAIR X Y \<sim> MPAIR X' Y'" |
|
25 | CRYPT: "X \<sim> X' \<Longrightarrow> CRYPT K X \<sim> CRYPT K X'" |
|
26 | DECRYPT: "X \<sim> X' \<Longrightarrow> DECRYPT K X \<sim> DECRYPT K X'" |
|
27 | SYM: "X \<sim> Y \<Longrightarrow> Y \<sim> X" |
|
28 | TRANS: "\<lbrakk>X \<sim> Y; Y \<sim> Z\<rbrakk> \<Longrightarrow> X \<sim> Z" |
|
29 |
|
30 lemmas msgrel.intros[intro] |
|
31 |
|
32 text{*Proving that it is an equivalence relation*} |
|
33 |
|
34 lemma msgrel_refl: "X \<sim> X" |
|
35 by (induct X, (blast intro: msgrel.intros)+) |
|
36 |
|
37 theorem equiv_msgrel: "equivp msgrel" |
|
38 proof (rule equivpI) |
|
39 show "reflp msgrel" by (simp add: reflp_def msgrel_refl) |
|
40 show "symp msgrel" by (simp add: symp_def, blast intro: msgrel.SYM) |
|
41 show "transp msgrel" by (simp add: transp_def, blast intro: msgrel.TRANS) |
|
42 qed |
|
43 |
|
44 subsection{*Some Functions on the Free Algebra*} |
|
45 |
|
46 subsubsection{*The Set of Nonces*} |
|
47 |
|
48 fun |
|
49 freenonces :: "freemsg \<Rightarrow> nat set" |
|
50 where |
|
51 "freenonces (NONCE N) = {N}" |
|
52 | "freenonces (MPAIR X Y) = freenonces X \<union> freenonces Y" |
|
53 | "freenonces (CRYPT K X) = freenonces X" |
|
54 | "freenonces (DECRYPT K X) = freenonces X" |
|
55 |
|
56 theorem msgrel_imp_eq_freenonces: |
|
57 assumes a: "U \<sim> V" |
|
58 shows "freenonces U = freenonces V" |
|
59 using a by (induct) (auto) |
|
60 |
|
61 subsubsection{*The Left Projection*} |
|
62 |
|
63 text{*A function to return the left part of the top pair in a message. It will |
|
64 be lifted to the initial algrebra, to serve as an example of that process.*} |
|
65 fun |
|
66 freeleft :: "freemsg \<Rightarrow> freemsg" |
|
67 where |
|
68 "freeleft (NONCE N) = NONCE N" |
|
69 | "freeleft (MPAIR X Y) = X" |
|
70 | "freeleft (CRYPT K X) = freeleft X" |
|
71 | "freeleft (DECRYPT K X) = freeleft X" |
|
72 |
|
73 text{*This theorem lets us prove that the left function respects the |
|
74 equivalence relation. It also helps us prove that MPair |
|
75 (the abstract constructor) is injective*} |
|
76 lemma msgrel_imp_eqv_freeleft_aux: |
|
77 shows "freeleft U \<sim> freeleft U" |
|
78 by (induct rule: freeleft.induct) (auto) |
|
79 |
|
80 theorem msgrel_imp_eqv_freeleft: |
|
81 assumes a: "U \<sim> V" |
|
82 shows "freeleft U \<sim> freeleft V" |
|
83 using a |
|
84 by (induct) (auto intro: msgrel_imp_eqv_freeleft_aux) |
|
85 |
|
86 subsubsection{*The Right Projection*} |
|
87 |
|
88 text{*A function to return the right part of the top pair in a message.*} |
|
89 fun |
|
90 freeright :: "freemsg \<Rightarrow> freemsg" |
|
91 where |
|
92 "freeright (NONCE N) = NONCE N" |
|
93 | "freeright (MPAIR X Y) = Y" |
|
94 | "freeright (CRYPT K X) = freeright X" |
|
95 | "freeright (DECRYPT K X) = freeright X" |
|
96 |
|
97 text{*This theorem lets us prove that the right function respects the |
|
98 equivalence relation. It also helps us prove that MPair |
|
99 (the abstract constructor) is injective*} |
|
100 lemma msgrel_imp_eqv_freeright_aux: |
|
101 shows "freeright U \<sim> freeright U" |
|
102 by (induct rule: freeright.induct) (auto) |
|
103 |
|
104 theorem msgrel_imp_eqv_freeright: |
|
105 assumes a: "U \<sim> V" |
|
106 shows "freeright U \<sim> freeright V" |
|
107 using a |
|
108 by (induct) (auto intro: msgrel_imp_eqv_freeright_aux) |
|
109 |
|
110 subsubsection{*The Discriminator for Constructors*} |
|
111 |
|
112 text{*A function to distinguish nonces, mpairs and encryptions*} |
|
113 fun |
|
114 freediscrim :: "freemsg \<Rightarrow> int" |
|
115 where |
|
116 "freediscrim (NONCE N) = 0" |
|
117 | "freediscrim (MPAIR X Y) = 1" |
|
118 | "freediscrim (CRYPT K X) = freediscrim X + 2" |
|
119 | "freediscrim (DECRYPT K X) = freediscrim X - 2" |
|
120 |
|
121 text{*This theorem helps us prove @{term "Nonce N \<noteq> MPair X Y"}*} |
|
122 theorem msgrel_imp_eq_freediscrim: |
|
123 assumes a: "U \<sim> V" |
|
124 shows "freediscrim U = freediscrim V" |
|
125 using a by (induct) (auto) |
|
126 |
|
127 subsection{*The Initial Algebra: A Quotiented Message Type*} |
|
128 |
|
129 quotient_type msg = freemsg / msgrel |
|
130 by (rule equiv_msgrel) |
|
131 |
|
132 text{*The abstract message constructors*} |
|
133 |
|
134 quotient_definition |
|
135 "Nonce :: nat \<Rightarrow> msg" |
|
136 is |
|
137 "NONCE" |
|
138 |
|
139 quotient_definition |
|
140 "MPair :: msg \<Rightarrow> msg \<Rightarrow> msg" |
|
141 is |
|
142 "MPAIR" |
|
143 |
|
144 quotient_definition |
|
145 "Crypt :: nat \<Rightarrow> msg \<Rightarrow> msg" |
|
146 is |
|
147 "CRYPT" |
|
148 |
|
149 quotient_definition |
|
150 "Decrypt :: nat \<Rightarrow> msg \<Rightarrow> msg" |
|
151 is |
|
152 "DECRYPT" |
|
153 |
|
154 lemma [quot_respect]: |
|
155 shows "(op = ===> op \<sim> ===> op \<sim>) CRYPT CRYPT" |
|
156 by (auto intro: CRYPT) |
|
157 |
|
158 lemma [quot_respect]: |
|
159 shows "(op = ===> op \<sim> ===> op \<sim>) DECRYPT DECRYPT" |
|
160 by (auto intro: DECRYPT) |
|
161 |
|
162 text{*Establishing these two equations is the point of the whole exercise*} |
|
163 theorem CD_eq [simp]: |
|
164 shows "Crypt K (Decrypt K X) = X" |
|
165 by (lifting CD) |
|
166 |
|
167 theorem DC_eq [simp]: |
|
168 shows "Decrypt K (Crypt K X) = X" |
|
169 by (lifting DC) |
|
170 |
|
171 subsection{*The Abstract Function to Return the Set of Nonces*} |
|
172 |
|
173 quotient_definition |
|
174 "nonces:: msg \<Rightarrow> nat set" |
|
175 is |
|
176 "freenonces" |
|
177 |
|
178 text{*Now prove the four equations for @{term nonces}*} |
|
179 |
|
180 lemma [quot_respect]: |
|
181 shows "(op \<sim> ===> op =) freenonces freenonces" |
|
182 by (simp add: msgrel_imp_eq_freenonces) |
|
183 |
|
184 lemma [quot_respect]: |
|
185 shows "(op = ===> op \<sim>) NONCE NONCE" |
|
186 by (simp add: NONCE) |
|
187 |
|
188 lemma nonces_Nonce [simp]: |
|
189 shows "nonces (Nonce N) = {N}" |
|
190 by (lifting freenonces.simps(1)) |
|
191 |
|
192 lemma [quot_respect]: |
|
193 shows " (op \<sim> ===> op \<sim> ===> op \<sim>) MPAIR MPAIR" |
|
194 by (simp add: MPAIR) |
|
195 |
|
196 lemma nonces_MPair [simp]: |
|
197 shows "nonces (MPair X Y) = nonces X \<union> nonces Y" |
|
198 by (lifting freenonces.simps(2)) |
|
199 |
|
200 lemma nonces_Crypt [simp]: |
|
201 shows "nonces (Crypt K X) = nonces X" |
|
202 by (lifting freenonces.simps(3)) |
|
203 |
|
204 lemma nonces_Decrypt [simp]: |
|
205 shows "nonces (Decrypt K X) = nonces X" |
|
206 by (lifting freenonces.simps(4)) |
|
207 |
|
208 subsection{*The Abstract Function to Return the Left Part*} |
|
209 |
|
210 quotient_definition |
|
211 "left:: msg \<Rightarrow> msg" |
|
212 is |
|
213 "freeleft" |
|
214 |
|
215 lemma [quot_respect]: |
|
216 shows "(op \<sim> ===> op \<sim>) freeleft freeleft" |
|
217 by (simp add: msgrel_imp_eqv_freeleft) |
|
218 |
|
219 lemma left_Nonce [simp]: |
|
220 shows "left (Nonce N) = Nonce N" |
|
221 by (lifting freeleft.simps(1)) |
|
222 |
|
223 lemma left_MPair [simp]: |
|
224 shows "left (MPair X Y) = X" |
|
225 by (lifting freeleft.simps(2)) |
|
226 |
|
227 lemma left_Crypt [simp]: |
|
228 shows "left (Crypt K X) = left X" |
|
229 by (lifting freeleft.simps(3)) |
|
230 |
|
231 lemma left_Decrypt [simp]: |
|
232 shows "left (Decrypt K X) = left X" |
|
233 by (lifting freeleft.simps(4)) |
|
234 |
|
235 subsection{*The Abstract Function to Return the Right Part*} |
|
236 |
|
237 quotient_definition |
|
238 "right:: msg \<Rightarrow> msg" |
|
239 is |
|
240 "freeright" |
|
241 |
|
242 text{*Now prove the four equations for @{term right}*} |
|
243 |
|
244 lemma [quot_respect]: |
|
245 shows "(op \<sim> ===> op \<sim>) freeright freeright" |
|
246 by (simp add: msgrel_imp_eqv_freeright) |
|
247 |
|
248 lemma right_Nonce [simp]: |
|
249 shows "right (Nonce N) = Nonce N" |
|
250 by (lifting freeright.simps(1)) |
|
251 |
|
252 lemma right_MPair [simp]: |
|
253 shows "right (MPair X Y) = Y" |
|
254 by (lifting freeright.simps(2)) |
|
255 |
|
256 lemma right_Crypt [simp]: |
|
257 shows "right (Crypt K X) = right X" |
|
258 by (lifting freeright.simps(3)) |
|
259 |
|
260 lemma right_Decrypt [simp]: |
|
261 shows "right (Decrypt K X) = right X" |
|
262 by (lifting freeright.simps(4)) |
|
263 |
|
264 subsection{*Injectivity Properties of Some Constructors*} |
|
265 |
|
266 lemma NONCE_imp_eq: |
|
267 shows "NONCE m \<sim> NONCE n \<Longrightarrow> m = n" |
|
268 by (drule msgrel_imp_eq_freenonces, simp) |
|
269 |
|
270 text{*Can also be proved using the function @{term nonces}*} |
|
271 lemma Nonce_Nonce_eq [iff]: |
|
272 shows "(Nonce m = Nonce n) = (m = n)" |
|
273 proof |
|
274 assume "Nonce m = Nonce n" |
|
275 then show "m = n" by (lifting NONCE_imp_eq) |
|
276 next |
|
277 assume "m = n" |
|
278 then show "Nonce m = Nonce n" by simp |
|
279 qed |
|
280 |
|
281 lemma MPAIR_imp_eqv_left: |
|
282 shows "MPAIR X Y \<sim> MPAIR X' Y' \<Longrightarrow> X \<sim> X'" |
|
283 by (drule msgrel_imp_eqv_freeleft) (simp) |
|
284 |
|
285 lemma MPair_imp_eq_left: |
|
286 assumes eq: "MPair X Y = MPair X' Y'" |
|
287 shows "X = X'" |
|
288 using eq by (lifting MPAIR_imp_eqv_left) |
|
289 |
|
290 lemma MPAIR_imp_eqv_right: |
|
291 shows "MPAIR X Y \<sim> MPAIR X' Y' \<Longrightarrow> Y \<sim> Y'" |
|
292 by (drule msgrel_imp_eqv_freeright) (simp) |
|
293 |
|
294 lemma MPair_imp_eq_right: |
|
295 shows "MPair X Y = MPair X' Y' \<Longrightarrow> Y = Y'" |
|
296 by (lifting MPAIR_imp_eqv_right) |
|
297 |
|
298 theorem MPair_MPair_eq [iff]: |
|
299 shows "(MPair X Y = MPair X' Y') = (X=X' & Y=Y')" |
|
300 by (blast dest: MPair_imp_eq_left MPair_imp_eq_right) |
|
301 |
|
302 lemma NONCE_neqv_MPAIR: |
|
303 shows "\<not>(NONCE m \<sim> MPAIR X Y)" |
|
304 by (auto dest: msgrel_imp_eq_freediscrim) |
|
305 |
|
306 theorem Nonce_neq_MPair [iff]: |
|
307 shows "Nonce N \<noteq> MPair X Y" |
|
308 by (lifting NONCE_neqv_MPAIR) |
|
309 |
|
310 text{*Example suggested by a referee*} |
|
311 |
|
312 lemma CRYPT_NONCE_neq_NONCE: |
|
313 shows "\<not>(CRYPT K (NONCE M) \<sim> NONCE N)" |
|
314 by (auto dest: msgrel_imp_eq_freediscrim) |
|
315 |
|
316 theorem Crypt_Nonce_neq_Nonce: |
|
317 shows "Crypt K (Nonce M) \<noteq> Nonce N" |
|
318 by (lifting CRYPT_NONCE_neq_NONCE) |
|
319 |
|
320 text{*...and many similar results*} |
|
321 lemma CRYPT2_NONCE_neq_NONCE: |
|
322 shows "\<not>(CRYPT K (CRYPT K' (NONCE M)) \<sim> NONCE N)" |
|
323 by (auto dest: msgrel_imp_eq_freediscrim) |
|
324 |
|
325 theorem Crypt2_Nonce_neq_Nonce: |
|
326 shows "Crypt K (Crypt K' (Nonce M)) \<noteq> Nonce N" |
|
327 by (lifting CRYPT2_NONCE_neq_NONCE) |
|
328 |
|
329 theorem Crypt_Crypt_eq [iff]: |
|
330 shows "(Crypt K X = Crypt K X') = (X=X')" |
|
331 proof |
|
332 assume "Crypt K X = Crypt K X'" |
|
333 hence "Decrypt K (Crypt K X) = Decrypt K (Crypt K X')" by simp |
|
334 thus "X = X'" by simp |
|
335 next |
|
336 assume "X = X'" |
|
337 thus "Crypt K X = Crypt K X'" by simp |
|
338 qed |
|
339 |
|
340 theorem Decrypt_Decrypt_eq [iff]: |
|
341 shows "(Decrypt K X = Decrypt K X') = (X=X')" |
|
342 proof |
|
343 assume "Decrypt K X = Decrypt K X'" |
|
344 hence "Crypt K (Decrypt K X) = Crypt K (Decrypt K X')" by simp |
|
345 thus "X = X'" by simp |
|
346 next |
|
347 assume "X = X'" |
|
348 thus "Decrypt K X = Decrypt K X'" by simp |
|
349 qed |
|
350 |
|
351 lemma msg_induct_aux: |
|
352 shows "\<lbrakk>\<And>N. P (Nonce N); |
|
353 \<And>X Y. \<lbrakk>P X; P Y\<rbrakk> \<Longrightarrow> P (MPair X Y); |
|
354 \<And>K X. P X \<Longrightarrow> P (Crypt K X); |
|
355 \<And>K X. P X \<Longrightarrow> P (Decrypt K X)\<rbrakk> \<Longrightarrow> P msg" |
|
356 by (lifting freemsg.induct) |
|
357 |
|
358 lemma msg_induct [case_names Nonce MPair Crypt Decrypt, cases type: msg]: |
|
359 assumes N: "\<And>N. P (Nonce N)" |
|
360 and M: "\<And>X Y. \<lbrakk>P X; P Y\<rbrakk> \<Longrightarrow> P (MPair X Y)" |
|
361 and C: "\<And>K X. P X \<Longrightarrow> P (Crypt K X)" |
|
362 and D: "\<And>K X. P X \<Longrightarrow> P (Decrypt K X)" |
|
363 shows "P msg" |
|
364 using N M C D by (rule msg_induct_aux) |
|
365 |
|
366 subsection{*The Abstract Discriminator*} |
|
367 |
|
368 text{*However, as @{text Crypt_Nonce_neq_Nonce} above illustrates, we don't |
|
369 need this function in order to prove discrimination theorems.*} |
|
370 |
|
371 quotient_definition |
|
372 "discrim:: msg \<Rightarrow> int" |
|
373 is |
|
374 "freediscrim" |
|
375 |
|
376 text{*Now prove the four equations for @{term discrim}*} |
|
377 |
|
378 lemma [quot_respect]: |
|
379 shows "(op \<sim> ===> op =) freediscrim freediscrim" |
|
380 by (auto simp add: msgrel_imp_eq_freediscrim) |
|
381 |
|
382 lemma discrim_Nonce [simp]: |
|
383 shows "discrim (Nonce N) = 0" |
|
384 by (lifting freediscrim.simps(1)) |
|
385 |
|
386 lemma discrim_MPair [simp]: |
|
387 shows "discrim (MPair X Y) = 1" |
|
388 by (lifting freediscrim.simps(2)) |
|
389 |
|
390 lemma discrim_Crypt [simp]: |
|
391 shows "discrim (Crypt K X) = discrim X + 2" |
|
392 by (lifting freediscrim.simps(3)) |
|
393 |
|
394 lemma discrim_Decrypt [simp]: |
|
395 shows "discrim (Decrypt K X) = discrim X - 2" |
|
396 by (lifting freediscrim.simps(4)) |
|
397 |
|
398 end |
|
399 |