equal
deleted
inserted
replaced
126 |
126 |
127 text{*The abstract message constructors*} |
127 text{*The abstract message constructors*} |
128 |
128 |
129 quotient_definition |
129 quotient_definition |
130 "Nonce :: nat \<Rightarrow> msg" |
130 "Nonce :: nat \<Rightarrow> msg" |
131 as |
131 is |
132 "NONCE" |
132 "NONCE" |
133 |
133 |
134 quotient_definition |
134 quotient_definition |
135 "MPair :: msg \<Rightarrow> msg \<Rightarrow> msg" |
135 "MPair :: msg \<Rightarrow> msg \<Rightarrow> msg" |
136 as |
136 is |
137 "MPAIR" |
137 "MPAIR" |
138 |
138 |
139 quotient_definition |
139 quotient_definition |
140 "Crypt :: nat \<Rightarrow> msg \<Rightarrow> msg" |
140 "Crypt :: nat \<Rightarrow> msg \<Rightarrow> msg" |
141 as |
141 is |
142 "CRYPT" |
142 "CRYPT" |
143 |
143 |
144 quotient_definition |
144 quotient_definition |
145 "Decrypt :: nat \<Rightarrow> msg \<Rightarrow> msg" |
145 "Decrypt :: nat \<Rightarrow> msg \<Rightarrow> msg" |
146 as |
146 is |
147 "DECRYPT" |
147 "DECRYPT" |
148 |
148 |
149 lemma [quot_respect]: |
149 lemma [quot_respect]: |
150 shows "(op = ===> op \<sim> ===> op \<sim>) CRYPT CRYPT" |
150 shows "(op = ===> op \<sim> ===> op \<sim>) CRYPT CRYPT" |
151 by (auto intro: CRYPT) |
151 by (auto intro: CRYPT) |
165 |
165 |
166 subsection{*The Abstract Function to Return the Set of Nonces*} |
166 subsection{*The Abstract Function to Return the Set of Nonces*} |
167 |
167 |
168 quotient_definition |
168 quotient_definition |
169 "nonces:: msg \<Rightarrow> nat set" |
169 "nonces:: msg \<Rightarrow> nat set" |
170 as |
170 is |
171 "freenonces" |
171 "freenonces" |
172 |
172 |
173 text{*Now prove the four equations for @{term nonces}*} |
173 text{*Now prove the four equations for @{term nonces}*} |
174 |
174 |
175 lemma [quot_respect]: |
175 lemma [quot_respect]: |
202 |
202 |
203 subsection{*The Abstract Function to Return the Left Part*} |
203 subsection{*The Abstract Function to Return the Left Part*} |
204 |
204 |
205 quotient_definition |
205 quotient_definition |
206 "left:: msg \<Rightarrow> msg" |
206 "left:: msg \<Rightarrow> msg" |
207 as |
207 is |
208 "freeleft" |
208 "freeleft" |
209 |
209 |
210 lemma [quot_respect]: |
210 lemma [quot_respect]: |
211 shows "(op \<sim> ===> op \<sim>) freeleft freeleft" |
211 shows "(op \<sim> ===> op \<sim>) freeleft freeleft" |
212 by (simp add: msgrel_imp_eqv_freeleft) |
212 by (simp add: msgrel_imp_eqv_freeleft) |
229 |
229 |
230 subsection{*The Abstract Function to Return the Right Part*} |
230 subsection{*The Abstract Function to Return the Right Part*} |
231 |
231 |
232 quotient_definition |
232 quotient_definition |
233 "right:: msg \<Rightarrow> msg" |
233 "right:: msg \<Rightarrow> msg" |
234 as |
234 is |
235 "freeright" |
235 "freeright" |
236 |
236 |
237 text{*Now prove the four equations for @{term right}*} |
237 text{*Now prove the four equations for @{term right}*} |
238 |
238 |
239 lemma [quot_respect]: |
239 lemma [quot_respect]: |
363 text{*However, as @{text Crypt_Nonce_neq_Nonce} above illustrates, we don't |
363 text{*However, as @{text Crypt_Nonce_neq_Nonce} above illustrates, we don't |
364 need this function in order to prove discrimination theorems.*} |
364 need this function in order to prove discrimination theorems.*} |
365 |
365 |
366 quotient_definition |
366 quotient_definition |
367 "discrim:: msg \<Rightarrow> int" |
367 "discrim:: msg \<Rightarrow> int" |
368 as |
368 is |
369 "freediscrim" |
369 "freediscrim" |
370 |
370 |
371 text{*Now prove the four equations for @{term discrim}*} |
371 text{*Now prove the four equations for @{term discrim}*} |
372 |
372 |
373 lemma [quot_respect]: |
373 lemma [quot_respect]: |