20 | CRYPT: "X \<sim> X' \<Longrightarrow> CRYPT K X \<sim> CRYPT K X'" |
20 | CRYPT: "X \<sim> X' \<Longrightarrow> CRYPT K X \<sim> CRYPT K X'" |
21 | DECRYPT: "X \<sim> X' \<Longrightarrow> DECRYPT K X \<sim> DECRYPT K X'" |
21 | DECRYPT: "X \<sim> X' \<Longrightarrow> DECRYPT K X \<sim> DECRYPT K X'" |
22 | SYM: "X \<sim> Y \<Longrightarrow> Y \<sim> X" |
22 | SYM: "X \<sim> Y \<Longrightarrow> Y \<sim> X" |
23 | TRANS: "\<lbrakk>X \<sim> Y; Y \<sim> Z\<rbrakk> \<Longrightarrow> X \<sim> Z" |
23 | TRANS: "\<lbrakk>X \<sim> Y; Y \<sim> Z\<rbrakk> \<Longrightarrow> X \<sim> Z" |
24 |
24 |
|
25 lemmas msgrel.intros[intro] |
|
26 |
25 text{*Proving that it is an equivalence relation*} |
27 text{*Proving that it is an equivalence relation*} |
26 |
28 |
27 lemma msgrel_refl: "X \<sim> X" |
29 lemma msgrel_refl: "X \<sim> X" |
28 by (induct X, (blast intro: msgrel.intros)+) |
30 by (induct X, (blast intro: msgrel.intros)+) |
29 |
31 |
36 |
38 |
37 subsection{*Some Functions on the Free Algebra*} |
39 subsection{*Some Functions on the Free Algebra*} |
38 |
40 |
39 subsubsection{*The Set of Nonces*} |
41 subsubsection{*The Set of Nonces*} |
40 |
42 |
41 primrec |
43 fun |
42 freenonces :: "freemsg \<Rightarrow> nat set" |
44 freenonces :: "freemsg \<Rightarrow> nat set" |
43 where |
45 where |
44 "freenonces (NONCE N) = {N}" |
46 "freenonces (NONCE N) = {N}" |
45 | "freenonces (MPAIR X Y) = freenonces X \<union> freenonces Y" |
47 | "freenonces (MPAIR X Y) = freenonces X \<union> freenonces Y" |
46 | "freenonces (CRYPT K X) = freenonces X" |
48 | "freenonces (CRYPT K X) = freenonces X" |
47 | "freenonces (DECRYPT K X) = freenonces X" |
49 | "freenonces (DECRYPT K X) = freenonces X" |
48 |
50 |
49 theorem msgrel_imp_eq_freenonces: |
51 theorem msgrel_imp_eq_freenonces: |
50 "U \<sim> V \<Longrightarrow> freenonces U = freenonces V" |
52 assumes a: "U \<sim> V" |
51 by (erule msgrel.induct, auto) |
53 shows "freenonces U = freenonces V" |
|
54 using a by (induct) (auto) |
52 |
55 |
53 subsubsection{*The Left Projection*} |
56 subsubsection{*The Left Projection*} |
54 |
57 |
55 text{*A function to return the left part of the top pair in a message. It will |
58 text{*A function to return the left part of the top pair in a message. It will |
56 be lifted to the initial algrebra, to serve as an example of that process.*} |
59 be lifted to the initial algrebra, to serve as an example of that process.*} |
65 text{*This theorem lets us prove that the left function respects the |
68 text{*This theorem lets us prove that the left function respects the |
66 equivalence relation. It also helps us prove that MPair |
69 equivalence relation. It also helps us prove that MPair |
67 (the abstract constructor) is injective*} |
70 (the abstract constructor) is injective*} |
68 lemma msgrel_imp_eqv_freeleft_aux: |
71 lemma msgrel_imp_eqv_freeleft_aux: |
69 shows "freeleft U \<sim> freeleft U" |
72 shows "freeleft U \<sim> freeleft U" |
70 apply(induct rule: freeleft.induct) |
73 by (induct rule: freeleft.induct) (auto) |
71 apply(auto intro: msgrel.intros) |
|
72 done |
|
73 |
74 |
74 theorem msgrel_imp_eqv_freeleft: |
75 theorem msgrel_imp_eqv_freeleft: |
75 "U \<sim> V \<Longrightarrow> freeleft U \<sim> freeleft V" |
76 assumes a: "U \<sim> V" |
76 apply(erule msgrel.induct) |
77 shows "freeleft U \<sim> freeleft V" |
77 apply(auto intro: msgrel.intros msgrel_imp_eqv_freeleft_aux) |
78 using a |
78 done |
79 by (induct)(auto intro: msgrel_imp_eqv_freeleft_aux) |
79 |
80 |
80 subsubsection{*The Right Projection*} |
81 subsubsection{*The Right Projection*} |
81 |
82 |
82 text{*A function to return the right part of the top pair in a message.*} |
83 text{*A function to return the right part of the top pair in a message.*} |
83 fun |
84 fun |
91 text{*This theorem lets us prove that the right function respects the |
92 text{*This theorem lets us prove that the right function respects the |
92 equivalence relation. It also helps us prove that MPair |
93 equivalence relation. It also helps us prove that MPair |
93 (the abstract constructor) is injective*} |
94 (the abstract constructor) is injective*} |
94 lemma msgrel_imp_eqv_freeright_aux: |
95 lemma msgrel_imp_eqv_freeright_aux: |
95 shows "freeright U \<sim> freeright U" |
96 shows "freeright U \<sim> freeright U" |
96 apply(induct rule: freeright.induct) |
97 by (induct rule: freeright.induct) (auto) |
97 apply(auto intro: msgrel.intros) |
|
98 done |
|
99 |
98 |
100 theorem msgrel_imp_eqv_freeright: |
99 theorem msgrel_imp_eqv_freeright: |
101 "U \<sim> V \<Longrightarrow> freeright U \<sim> freeright V" |
100 assumes a: "U \<sim> V" |
102 by (erule msgrel.induct, auto intro: msgrel.intros msgrel_imp_eqv_freeright_aux) |
101 shows "freeright U \<sim> freeright V" |
|
102 using a |
|
103 by (induct) (auto intro: msgrel_imp_eqv_freeright_aux) |
103 |
104 |
104 subsubsection{*The Discriminator for Constructors*} |
105 subsubsection{*The Discriminator for Constructors*} |
105 |
106 |
106 text{*A function to distinguish nonces, mpairs and encryptions*} |
107 text{*A function to distinguish nonces, mpairs and encryptions*} |
107 fun |
108 fun |
112 | "freediscrim (CRYPT K X) = freediscrim X + 2" |
113 | "freediscrim (CRYPT K X) = freediscrim X + 2" |
113 | "freediscrim (DECRYPT K X) = freediscrim X - 2" |
114 | "freediscrim (DECRYPT K X) = freediscrim X - 2" |
114 |
115 |
115 text{*This theorem helps us prove @{term "Nonce N \<noteq> MPair X Y"}*} |
116 text{*This theorem helps us prove @{term "Nonce N \<noteq> MPair X Y"}*} |
116 theorem msgrel_imp_eq_freediscrim: |
117 theorem msgrel_imp_eq_freediscrim: |
117 "U \<sim> V \<Longrightarrow> freediscrim U = freediscrim V" |
118 assumes a: "U \<sim> V" |
118 by (erule msgrel.induct, auto) |
119 shows "freediscrim U = freediscrim V" |
|
120 using a by (induct, auto) |
119 |
121 |
120 |
122 |
121 subsection{*The Initial Algebra: A Quotiented Message Type*} |
123 subsection{*The Initial Algebra: A Quotiented Message Type*} |
122 |
124 |
123 quotient msg = freemsg / msgrel |
125 quotient msg = freemsg / msgrel |
259 by (drule msgrel_imp_eq_freenonces, simp) |
261 by (drule msgrel_imp_eq_freenonces, simp) |
260 |
262 |
261 text{*Can also be proved using the function @{term nonces}*} |
263 text{*Can also be proved using the function @{term nonces}*} |
262 lemma Nonce_Nonce_eq [iff]: |
264 lemma Nonce_Nonce_eq [iff]: |
263 shows "(Nonce m = Nonce n) = (m = n)" |
265 shows "(Nonce m = Nonce n) = (m = n)" |
264 apply(rule iffI) |
266 proof |
265 apply(lifting NONCE_imp_eq) |
267 assume "Nonce m = Nonce n" |
266 apply(simp) |
268 then show "m = n" by (lifting NONCE_imp_eq) |
267 done |
269 next |
|
270 assume "m = n" |
|
271 then show "Nonce m = Nonce n" by simp |
|
272 qed |
268 |
273 |
269 lemma MPAIR_imp_eqv_left: |
274 lemma MPAIR_imp_eqv_left: |
270 shows "MPAIR X Y \<sim> MPAIR X' Y' \<Longrightarrow> X \<sim> X'" |
275 shows "MPAIR X Y \<sim> MPAIR X' Y' \<Longrightarrow> X \<sim> X'" |
271 by (drule msgrel_imp_eqv_freeleft, simp) |
276 by (drule msgrel_imp_eqv_freeleft) (simp) |
272 |
277 |
273 lemma MPair_imp_eq_left: |
278 lemma MPair_imp_eq_left: |
274 assumes eq: "MPair X Y = MPair X' Y'" |
279 assumes eq: "MPair X Y = MPair X' Y'" |
275 shows "X = X'" |
280 shows "X = X'" |
276 using eq by (lifting MPAIR_imp_eqv_left) |
281 using eq by (lifting MPAIR_imp_eqv_left) |
277 |
282 |
278 lemma MPAIR_imp_eqv_right: |
283 lemma MPAIR_imp_eqv_right: |
279 shows "MPAIR X Y \<sim> MPAIR X' Y' \<Longrightarrow> Y \<sim> Y'" |
284 shows "MPAIR X Y \<sim> MPAIR X' Y' \<Longrightarrow> Y \<sim> Y'" |
280 by (drule msgrel_imp_eqv_freeright, simp) |
285 by (drule msgrel_imp_eqv_freeright) (simp) |
281 |
286 |
282 lemma MPair_imp_eq_right: |
287 lemma MPair_imp_eq_right: |
283 shows "MPair X Y = MPair X' Y' \<Longrightarrow> Y = Y'" |
288 shows "MPair X Y = MPair X' Y' \<Longrightarrow> Y = Y'" |
284 by (lifting MPAIR_imp_eqv_right) |
289 by (lifting MPAIR_imp_eqv_right) |
285 |
290 |