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