|
1 (* Title: HOL/Induct/QuoDataType |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 2004 University of Cambridge |
|
5 |
|
6 *) |
|
7 |
|
8 header{*Defining an Initial Algebra by Quotienting a Free Algebra*} |
|
9 |
|
10 theory QuoDataType = Main: |
|
11 |
|
12 subsection{*Defining the Free Algebra*} |
|
13 |
|
14 text{*Messages with encryption and decryption as free constructors.*} |
|
15 datatype |
|
16 freemsg = NONCE nat |
|
17 | MPAIR freemsg freemsg |
|
18 | CRYPT nat freemsg |
|
19 | DECRYPT nat freemsg |
|
20 |
|
21 text{*The equivalence relation, which makes encryption and decryption inverses |
|
22 provided the keys are the same.*} |
|
23 consts msgrel :: "(freemsg * freemsg) set" |
|
24 |
|
25 syntax |
|
26 "_msgrel" :: "[freemsg, freemsg] => bool" (infixl "~~" 50) |
|
27 syntax (xsymbols) |
|
28 "_msgrel" :: "[freemsg, freemsg] => bool" (infixl "\<sim>" 50) |
|
29 translations |
|
30 "X \<sim> Y" == "(X,Y) \<in> msgrel" |
|
31 |
|
32 text{*The first two rules are the desired equations. The next four rules |
|
33 make the equations applicable to subterms. The last two rules are symmetry |
|
34 and transitivity.*} |
|
35 inductive "msgrel" |
|
36 intros |
|
37 CD: "CRYPT K (DECRYPT K X) \<sim> X" |
|
38 DC: "DECRYPT K (CRYPT K X) \<sim> X" |
|
39 NONCE: "NONCE N \<sim> NONCE N" |
|
40 MPAIR: "\<lbrakk>X \<sim> X'; Y \<sim> Y'\<rbrakk> \<Longrightarrow> MPAIR X Y \<sim> MPAIR X' Y'" |
|
41 CRYPT: "X \<sim> X' \<Longrightarrow> CRYPT K X \<sim> CRYPT K X'" |
|
42 DECRYPT: "X \<sim> X' \<Longrightarrow> DECRYPT K X \<sim> DECRYPT K X'" |
|
43 SYM: "X \<sim> Y \<Longrightarrow> Y \<sim> X" |
|
44 TRANS: "\<lbrakk>X \<sim> Y; Y \<sim> Z\<rbrakk> \<Longrightarrow> X \<sim> Z" |
|
45 |
|
46 |
|
47 text{*Proving that it is an equivalence relation*} |
|
48 |
|
49 lemma msgrel_refl: "X \<sim> X" |
|
50 by (induct X, (blast intro: msgrel.intros)+) |
|
51 |
|
52 theorem equiv_msgrel: "equiv UNIV msgrel" |
|
53 proof (simp add: equiv_def, intro conjI) |
|
54 show "reflexive msgrel" by (simp add: refl_def msgrel_refl) |
|
55 show "sym msgrel" by (simp add: sym_def, blast intro: msgrel.SYM) |
|
56 show "trans msgrel" by (simp add: trans_def, blast intro: msgrel.TRANS) |
|
57 qed |
|
58 |
|
59 |
|
60 subsection{*Some Functions on the Free Algebra*} |
|
61 |
|
62 subsubsection{*The Set of Nonces*} |
|
63 |
|
64 text{*A function to return the set of nonces present in a message. It will |
|
65 be lifted to the initial algrebra, to serve as an example of that process.*} |
|
66 consts |
|
67 freenonces :: "freemsg \<Rightarrow> nat set" |
|
68 |
|
69 primrec |
|
70 "freenonces (NONCE N) = {N}" |
|
71 "freenonces (MPAIR X Y) = freenonces X \<union> freenonces Y" |
|
72 "freenonces (CRYPT K X) = freenonces X" |
|
73 "freenonces (DECRYPT K X) = freenonces X" |
|
74 |
|
75 text{*This theorem lets us prove that the nonces function respects the |
|
76 equivalence relation. It also helps us prove that Nonce |
|
77 (the abstract constructor) is injective*} |
|
78 theorem msgrel_imp_eq_freenonces: "U \<sim> V \<Longrightarrow> freenonces U = freenonces V" |
|
79 by (erule msgrel.induct, auto) |
|
80 |
|
81 |
|
82 subsubsection{*The Left Projection*} |
|
83 |
|
84 text{*A function to return the left part of the top pair in a message. It will |
|
85 be lifted to the initial algrebra, to serve as an example of that process.*} |
|
86 consts free_left :: "freemsg \<Rightarrow> freemsg" |
|
87 primrec |
|
88 "free_left (NONCE N) = NONCE N" |
|
89 "free_left (MPAIR X Y) = X" |
|
90 "free_left (CRYPT K X) = free_left X" |
|
91 "free_left (DECRYPT K X) = free_left X" |
|
92 |
|
93 text{*This theorem lets us prove that the left function respects the |
|
94 equivalence relation. It also helps us prove that MPair |
|
95 (the abstract constructor) is injective*} |
|
96 theorem msgrel_imp_eqv_free_left: |
|
97 "U \<sim> V \<Longrightarrow> free_left U \<sim> free_left V" |
|
98 by (erule msgrel.induct, auto intro: msgrel.intros) |
|
99 |
|
100 |
|
101 subsubsection{*The Right Projection*} |
|
102 |
|
103 text{*A function to return the right part of the top pair in a message.*} |
|
104 consts free_right :: "freemsg \<Rightarrow> freemsg" |
|
105 primrec |
|
106 "free_right (NONCE N) = NONCE N" |
|
107 "free_right (MPAIR X Y) = Y" |
|
108 "free_right (CRYPT K X) = free_right X" |
|
109 "free_right (DECRYPT K X) = free_right X" |
|
110 |
|
111 text{*This theorem lets us prove that the right function respects the |
|
112 equivalence relation. It also helps us prove that MPair |
|
113 (the abstract constructor) is injective*} |
|
114 theorem msgrel_imp_eqv_free_right: |
|
115 "U \<sim> V \<Longrightarrow> free_right U \<sim> free_right V" |
|
116 by (erule msgrel.induct, auto intro: msgrel.intros) |
|
117 |
|
118 |
|
119 subsubsection{*The Discriminator for Nonces*} |
|
120 |
|
121 text{*A function to identify nonces*} |
|
122 consts isNONCE :: "freemsg \<Rightarrow> bool" |
|
123 primrec |
|
124 "isNONCE (NONCE N) = True" |
|
125 "isNONCE (MPAIR X Y) = False" |
|
126 "isNONCE (CRYPT K X) = isNONCE X" |
|
127 "isNONCE (DECRYPT K X) = isNONCE X" |
|
128 |
|
129 text{*This theorem helps us prove @{term "Nonce N \<noteq> MPair X Y"}*} |
|
130 theorem msgrel_imp_eq_isNONCE: |
|
131 "U \<sim> V \<Longrightarrow> isNONCE U = isNONCE V" |
|
132 by (erule msgrel.induct, auto) |
|
133 |
|
134 |
|
135 subsection{*The Initial Algebra: A Quotiented Message Type*} |
|
136 |
|
137 typedef (Msg) msg = "UNIV//msgrel" |
|
138 by (auto simp add: quotient_def) |
|
139 |
|
140 |
|
141 text{*The abstract message constructors*} |
|
142 constdefs |
|
143 Nonce :: "nat \<Rightarrow> msg" |
|
144 "Nonce N == Abs_Msg(msgrel``{NONCE N})" |
|
145 |
|
146 MPair :: "[msg,msg] \<Rightarrow> msg" |
|
147 "MPair X Y == |
|
148 Abs_Msg (\<Union>U \<in> Rep_Msg(X). \<Union>V \<in> Rep_Msg(Y). msgrel``{MPAIR U V})" |
|
149 |
|
150 Crypt :: "[nat,msg] \<Rightarrow> msg" |
|
151 "Crypt K X == |
|
152 Abs_Msg (\<Union>U \<in> Rep_Msg(X). msgrel``{CRYPT K U})" |
|
153 |
|
154 Decrypt :: "[nat,msg] \<Rightarrow> msg" |
|
155 "Decrypt K X == |
|
156 Abs_Msg (\<Union>U \<in> Rep_Msg(X). msgrel``{DECRYPT K U})" |
|
157 |
|
158 |
|
159 text{*Reduces equality of equivalence classes to the @{term msgrel} relation: |
|
160 @{term "(msgrel `` {x} = msgrel `` {y}) = ((x,y) \<in> msgrel)"} *} |
|
161 lemmas equiv_msgrel_iff = eq_equiv_class_iff [OF equiv_msgrel UNIV_I UNIV_I] |
|
162 |
|
163 declare equiv_msgrel_iff [simp] |
|
164 |
|
165 |
|
166 text{*All equivalence classes belong to set of representatives*} |
|
167 lemma msgrel_in_integ [simp]: "msgrel``{U} \<in> Msg" |
|
168 by (auto simp add: Msg_def quotient_def intro: msgrel_refl) |
|
169 |
|
170 lemma inj_on_Abs_Msg: "inj_on Abs_Msg Msg" |
|
171 apply (rule inj_on_inverseI) |
|
172 apply (erule Abs_Msg_inverse) |
|
173 done |
|
174 |
|
175 text{*Reduces equality on abstractions to equality on representatives*} |
|
176 declare inj_on_Abs_Msg [THEN inj_on_iff, simp] |
|
177 |
|
178 declare Abs_Msg_inverse [simp] |
|
179 |
|
180 |
|
181 subsubsection{*Characteristic Equations for the Abstract Constructors*} |
|
182 |
|
183 lemma MPair: "MPair (Abs_Msg(msgrel``{U})) (Abs_Msg(msgrel``{V})) = |
|
184 Abs_Msg (msgrel``{MPAIR U V})" |
|
185 proof - |
|
186 have "congruent2 msgrel (\<lambda>U V. msgrel `` {MPAIR U V})" |
|
187 by (simp add: congruent2_def msgrel.MPAIR) |
|
188 thus ?thesis |
|
189 by (simp add: MPair_def UN_equiv_class2 [OF equiv_msgrel]) |
|
190 qed |
|
191 |
|
192 lemma Crypt: "Crypt K (Abs_Msg(msgrel``{U})) = Abs_Msg (msgrel``{CRYPT K U})" |
|
193 proof - |
|
194 have "congruent msgrel (\<lambda>U. msgrel `` {CRYPT K U})" |
|
195 by (simp add: congruent_def msgrel.CRYPT) |
|
196 thus ?thesis |
|
197 by (simp add: Crypt_def UN_equiv_class [OF equiv_msgrel]) |
|
198 qed |
|
199 |
|
200 lemma Decrypt: |
|
201 "Decrypt K (Abs_Msg(msgrel``{U})) = Abs_Msg (msgrel``{DECRYPT K U})" |
|
202 proof - |
|
203 have "congruent msgrel (\<lambda>U. msgrel `` {DECRYPT K U})" |
|
204 by (simp add: congruent_def msgrel.DECRYPT) |
|
205 thus ?thesis |
|
206 by (simp add: Decrypt_def UN_equiv_class [OF equiv_msgrel]) |
|
207 qed |
|
208 |
|
209 text{*Case analysis on the representation of a msg as an equivalence class.*} |
|
210 lemma eq_Abs_Msg [case_names Abs_Msg, cases type: msg]: |
|
211 "(!!U. z = Abs_Msg(msgrel``{U}) ==> P) ==> P" |
|
212 apply (rule Rep_Msg [of z, unfolded Msg_def, THEN quotientE]) |
|
213 apply (drule arg_cong [where f=Abs_Msg]) |
|
214 apply (auto simp add: Rep_Msg_inverse intro: msgrel_refl) |
|
215 done |
|
216 |
|
217 text{*Establishing these two equations is the point of the whole exercise*} |
|
218 theorem CD_eq: "Crypt K (Decrypt K X) = X" |
|
219 by (cases X, simp add: Crypt Decrypt CD) |
|
220 |
|
221 theorem DC_eq: "Decrypt K (Crypt K X) = X" |
|
222 by (cases X, simp add: Crypt Decrypt DC) |
|
223 |
|
224 |
|
225 subsection{*The Abstract Function to Return the Set of Nonces*} |
|
226 |
|
227 constdefs |
|
228 nonces :: "msg \<Rightarrow> nat set" |
|
229 "nonces X == \<Union>U \<in> Rep_Msg(X). freenonces U" |
|
230 |
|
231 lemma nonces_congruent: "congruent msgrel (\<lambda>x. freenonces x)" |
|
232 by (simp add: congruent_def msgrel_imp_eq_freenonces) |
|
233 |
|
234 |
|
235 text{*Now prove the four equations for @{term nonces}*} |
|
236 |
|
237 lemma nonces_Nonce [simp]: "nonces (Nonce N) = {N}" |
|
238 by (simp add: nonces_def Nonce_def |
|
239 UN_equiv_class [OF equiv_msgrel nonces_congruent]) |
|
240 |
|
241 lemma nonces_MPair [simp]: "nonces (MPair X Y) = nonces X \<union> nonces Y" |
|
242 apply (cases X, cases Y) |
|
243 apply (simp add: nonces_def MPair |
|
244 UN_equiv_class [OF equiv_msgrel nonces_congruent]) |
|
245 done |
|
246 |
|
247 lemma nonces_Crypt [simp]: "nonces (Crypt K X) = nonces X" |
|
248 apply (cases X) |
|
249 apply (simp add: nonces_def Crypt |
|
250 UN_equiv_class [OF equiv_msgrel nonces_congruent]) |
|
251 done |
|
252 |
|
253 lemma nonces_Decrypt [simp]: "nonces (Decrypt K X) = nonces X" |
|
254 apply (cases X) |
|
255 apply (simp add: nonces_def Decrypt |
|
256 UN_equiv_class [OF equiv_msgrel nonces_congruent]) |
|
257 done |
|
258 |
|
259 |
|
260 subsection{*The Abstract Function to Return the Left Part*} |
|
261 |
|
262 constdefs |
|
263 left :: "msg \<Rightarrow> msg" |
|
264 "left X == Abs_Msg (\<Union>U \<in> Rep_Msg(X). msgrel``{free_left U})" |
|
265 |
|
266 lemma left_congruent: "congruent msgrel (\<lambda>U. msgrel `` {free_left U})" |
|
267 by (simp add: congruent_def msgrel_imp_eqv_free_left) |
|
268 |
|
269 text{*Now prove the four equations for @{term left}*} |
|
270 |
|
271 lemma left_Nonce [simp]: "left (Nonce N) = Nonce N" |
|
272 by (simp add: left_def Nonce_def |
|
273 UN_equiv_class [OF equiv_msgrel left_congruent]) |
|
274 |
|
275 lemma left_MPair [simp]: "left (MPair X Y) = X" |
|
276 apply (cases X, cases Y) |
|
277 apply (simp add: left_def MPair |
|
278 UN_equiv_class [OF equiv_msgrel left_congruent]) |
|
279 done |
|
280 |
|
281 lemma left_Crypt [simp]: "left (Crypt K X) = left X" |
|
282 apply (cases X) |
|
283 apply (simp add: left_def Crypt |
|
284 UN_equiv_class [OF equiv_msgrel left_congruent]) |
|
285 done |
|
286 |
|
287 lemma left_Decrypt [simp]: "left (Decrypt K X) = left X" |
|
288 apply (cases X) |
|
289 apply (simp add: left_def Decrypt |
|
290 UN_equiv_class [OF equiv_msgrel left_congruent]) |
|
291 done |
|
292 |
|
293 |
|
294 subsection{*The Abstract Function to Return the Right Part*} |
|
295 |
|
296 constdefs |
|
297 right :: "msg \<Rightarrow> msg" |
|
298 "right X == Abs_Msg (\<Union>U \<in> Rep_Msg(X). msgrel``{free_right U})" |
|
299 |
|
300 lemma right_congruent: "congruent msgrel (\<lambda>U. msgrel `` {free_right U})" |
|
301 by (simp add: congruent_def msgrel_imp_eqv_free_right) |
|
302 |
|
303 text{*Now prove the four equations for @{term right}*} |
|
304 |
|
305 lemma right_Nonce [simp]: "right (Nonce N) = Nonce N" |
|
306 by (simp add: right_def Nonce_def |
|
307 UN_equiv_class [OF equiv_msgrel right_congruent]) |
|
308 |
|
309 lemma right_MPair [simp]: "right (MPair X Y) = Y" |
|
310 apply (cases X, cases Y) |
|
311 apply (simp add: right_def MPair |
|
312 UN_equiv_class [OF equiv_msgrel right_congruent]) |
|
313 done |
|
314 |
|
315 lemma right_Crypt [simp]: "right (Crypt K X) = right X" |
|
316 apply (cases X) |
|
317 apply (simp add: right_def Crypt |
|
318 UN_equiv_class [OF equiv_msgrel right_congruent]) |
|
319 done |
|
320 |
|
321 lemma right_Decrypt [simp]: "right (Decrypt K X) = right X" |
|
322 apply (cases X) |
|
323 apply (simp add: right_def Decrypt |
|
324 UN_equiv_class [OF equiv_msgrel right_congruent]) |
|
325 done |
|
326 |
|
327 |
|
328 subsection{*Injectivity Properties of Some Constructors*} |
|
329 |
|
330 lemma NONCE_imp_eq: "NONCE m \<sim> NONCE n \<Longrightarrow> m = n" |
|
331 by (drule msgrel_imp_eq_freenonces, simp) |
|
332 |
|
333 text{*Can also be proved using the function @{term nonces}*} |
|
334 lemma Nonce_Nonce_eq [iff]: "(Nonce m = Nonce n) = (m = n)" |
|
335 by (auto simp add: Nonce_def msgrel_refl dest: NONCE_imp_eq) |
|
336 |
|
337 lemma MPAIR_imp_eqv_left: "MPAIR X Y \<sim> MPAIR X' Y' \<Longrightarrow> X \<sim> X'" |
|
338 apply (drule msgrel_imp_eqv_free_left) |
|
339 apply (simp add: ); |
|
340 done |
|
341 |
|
342 lemma MPair_imp_eq_left: |
|
343 assumes eq: "MPair X Y = MPair X' Y'" shows "X = X'" |
|
344 proof - |
|
345 from eq |
|
346 have "left (MPair X Y) = left (MPair X' Y')" by simp |
|
347 thus ?thesis by simp |
|
348 qed |
|
349 |
|
350 lemma MPAIR_imp_eqv_right: "MPAIR X Y \<sim> MPAIR X' Y' \<Longrightarrow> Y \<sim> Y'" |
|
351 apply (drule msgrel_imp_eqv_free_right) |
|
352 apply (simp add: ); |
|
353 done |
|
354 |
|
355 lemma MPair_imp_eq_right: "MPair X Y = MPair X' Y' \<Longrightarrow> Y = Y'" |
|
356 apply (cases X, cases X', cases Y, cases Y') |
|
357 apply (simp add: MPair) |
|
358 apply (erule MPAIR_imp_eqv_right) |
|
359 done |
|
360 |
|
361 theorem MPair_MPair_eq [iff]: "(MPair X Y = MPair X' Y') = (X=X' & Y=Y')" |
|
362 apply (blast dest: MPair_imp_eq_left MPair_imp_eq_right) |
|
363 done |
|
364 |
|
365 lemma NONCE_neqv_MPAIR: "NONCE m \<sim> MPAIR X Y \<Longrightarrow> False" |
|
366 by (drule msgrel_imp_eq_isNONCE, simp) |
|
367 |
|
368 theorem Nonce_neq_MPair [iff]: "Nonce N \<noteq> MPair X Y" |
|
369 apply (cases X, cases Y) |
|
370 apply (simp add: Nonce_def MPair) |
|
371 apply (blast dest: NONCE_neqv_MPAIR) |
|
372 done |
|
373 |
|
374 end |
|
375 |