148 ==> B=B' & ofr=ofr' & A=A' & r=r' & L=L' & C=C'" |
148 ==> B=B' & ofr=ofr' & A=A' & r=r' & L=L' & C=C'" |
149 by (auto simp: pro_def dest: prom_inj) |
149 by (auto simp: pro_def dest: prom_inj) |
150 |
150 |
151 subsubsection{*protocol*} |
151 subsubsection{*protocol*} |
152 |
152 |
153 consts p1 :: "event list set" |
153 inductive_set p1 :: "event list set" |
154 |
154 where |
155 inductive p1 |
155 |
156 intros |
156 Nil: "[]:p1" |
157 |
157 |
158 Nil: "[]:p1" |
158 | Fake: "[| evsf:p1; X:synth (analz (spies evsf)) |] ==> Says Spy B X # evsf : p1" |
159 |
159 |
160 Fake: "[| evsf:p1; X:synth (analz (spies evsf)) |] ==> Says Spy B X # evsf : p1" |
160 | Request: "[| evsr:p1; Nonce n ~:used evsr; I:agl |] ==> req A r n I B # evsr : p1" |
161 |
161 |
162 Request: "[| evsr:p1; Nonce n ~:used evsr; I:agl |] ==> req A r n I B # evsr : p1" |
162 | Propose: "[| evsp:p1; Says A' B {|Agent A,Number r,I,cons M L|}:set evsp; |
163 |
163 I:agl; J:agl; isin (Agent C, app (J, del (Agent B, I))); |
164 Propose: "[| evsp:p1; Says A' B {|Agent A,Number r,I,cons M L|}:set evsp; |
164 Nonce ofr ~:used evsp |] ==> pro B ofr A r I (cons M L) J C # evsp : p1" |
165 I:agl; J:agl; isin (Agent C, app (J, del (Agent B, I))); |
|
166 Nonce ofr ~:used evsp |] ==> pro B ofr A r I (cons M L) J C # evsp : p1" |
|
167 |
165 |
168 subsubsection{*Composition of Traces*} |
166 subsubsection{*Composition of Traces*} |
169 |
167 |
170 lemma "evs':p1 ==> |
168 lemma "evs':p1 ==> |
171 evs:p1 & (ALL n. Nonce n:used evs' --> Nonce n ~:used evs) --> |
169 evs:p1 & (ALL n. Nonce n:used evs' --> Nonce n ~:used evs) --> |
179 apply (erule_tac A'=A' in p1.Propose, auto simp: pro_def) |
177 apply (erule_tac A'=A' in p1.Propose, auto simp: pro_def) |
180 done |
178 done |
181 |
179 |
182 subsubsection{*Valid Offer Lists*} |
180 subsubsection{*Valid Offer Lists*} |
183 |
181 |
184 consts valid :: "agent => nat => agent => msg set" |
182 inductive_set |
185 |
183 valid :: "agent => nat => agent => msg set" |
186 inductive "valid A n B" |
184 for A :: agent and n :: nat and B :: agent |
187 intros |
185 where |
188 Request [intro]: "cons (anchor A n B) nil:valid A n B" |
186 Request [intro]: "cons (anchor A n B) nil:valid A n B" |
189 |
187 |
190 Propose [intro]: "L:valid A n B |
188 | Propose [intro]: "L:valid A n B |
191 ==> cons (chain (next_shop (head L)) ofr A L C) L:valid A n B" |
189 ==> cons (chain (next_shop (head L)) ofr A L C) L:valid A n B" |
192 |
190 |
193 subsubsection{*basic properties of valid*} |
191 subsubsection{*basic properties of valid*} |
194 |
192 |
195 lemma valid_not_empty: "L:valid A n B ==> EX M L'. L = cons M L'" |
193 lemma valid_not_empty: "L:valid A n B ==> EX M L'. L = cons M L'" |
282 apply (induct i) |
280 apply (induct i) |
283 (* i = 0 *) |
281 (* i = 0 *) |
284 apply clarify |
282 apply clarify |
285 apply (frule len_not_empty, clarsimp) |
283 apply (frule len_not_empty, clarsimp) |
286 apply (frule len_not_empty, clarsimp) |
284 apply (frule len_not_empty, clarsimp) |
287 apply (ind_cases "{|x,xa,l'a|}:valid A n B") |
285 apply (ind_cases "{|x,xa,l'a|}:valid A n B" for x xa l'a) |
288 apply (ind_cases "{|x,M,l'a|}:valid A n B") |
286 apply (ind_cases "{|x,M,l'a|}:valid A n B" for x l'a) |
289 apply (simp add: chain_def) |
287 apply (simp add: chain_def) |
290 (* i > 0 *) |
288 (* i > 0 *) |
291 apply clarify |
289 apply clarify |
292 apply (frule len_not_empty, clarsimp) |
290 apply (frule len_not_empty, clarsimp) |
293 apply (ind_cases "{|x,repl(l',Suc na,M)|}:valid A n B") |
291 apply (ind_cases "{|x,repl(l',Suc na,M)|}:valid A n B" for x l' na) |
294 apply (frule len_not_empty, clarsimp) |
292 apply (frule len_not_empty, clarsimp) |
295 apply (ind_cases "{|x,l'|}:valid A n B") |
293 apply (ind_cases "{|x,l'|}:valid A n B" for x l') |
296 by (drule_tac x=l' in spec, simp, blast) |
294 by (drule_tac x=l' in spec, simp, blast) |
297 |
295 |
298 subsubsection{*insertion resilience: |
296 subsubsection{*insertion resilience: |
299 except at the beginning, no offer can be inserted*} |
297 except at the beginning, no offer can be inserted*} |
300 |
298 |
306 --> ins (L,Suc i,M) ~:valid A n B" |
304 --> ins (L,Suc i,M) ~:valid A n B" |
307 apply (induct i) |
305 apply (induct i) |
308 (* i = 0 *) |
306 (* i = 0 *) |
309 apply clarify |
307 apply clarify |
310 apply (frule len_not_empty, clarsimp) |
308 apply (frule len_not_empty, clarsimp) |
311 apply (ind_cases "{|x,l'|}:valid A n B", simp) |
309 apply (ind_cases "{|x,l'|}:valid A n B" for x l', simp) |
312 apply (ind_cases "{|x,M,l'|}:valid A n B", clarsimp) |
310 apply (ind_cases "{|x,M,l'|}:valid A n B" for x l', clarsimp) |
313 apply (ind_cases "{|head l',l'|}:valid A n B", simp, simp) |
311 apply (ind_cases "{|head l',l'|}:valid A n B" for l', simp, simp) |
314 (* i > 0 *) |
312 (* i > 0 *) |
315 apply clarify |
313 apply clarify |
316 apply (frule len_not_empty, clarsimp) |
314 apply (frule len_not_empty, clarsimp) |
317 apply (ind_cases "{|x,l'|}:valid A n B") |
315 apply (ind_cases "{|x,l'|}:valid A n B" for x l') |
318 apply (frule len_not_empty, clarsimp) |
316 apply (frule len_not_empty, clarsimp) |
319 apply (ind_cases "{|x,ins(l',Suc na,M)|}:valid A n B") |
317 apply (ind_cases "{|x,ins(l',Suc na,M)|}:valid A n B" for x l' na) |
320 apply (frule len_not_empty, clarsimp) |
318 apply (frule len_not_empty, clarsimp) |
321 by (drule_tac x=l' in spec, clarsimp) |
319 by (drule_tac x=l' in spec, clarsimp) |
322 |
320 |
323 subsubsection{*truncation resilience: |
321 subsubsection{*truncation resilience: |
324 only shop i can truncate at offer i*} |
322 only shop i can truncate at offer i*} |
327 --> cons M (trunc (L,Suc i)):valid A n B --> shop M = shop (ith (L,i))" |
325 --> cons M (trunc (L,Suc i)):valid A n B --> shop M = shop (ith (L,i))" |
328 apply (induct i) |
326 apply (induct i) |
329 (* i = 0 *) |
327 (* i = 0 *) |
330 apply clarify |
328 apply clarify |
331 apply (frule len_not_empty, clarsimp) |
329 apply (frule len_not_empty, clarsimp) |
332 apply (ind_cases "{|x,l'|}:valid A n B") |
330 apply (ind_cases "{|x,l'|}:valid A n B" for x l') |
333 apply (frule len_not_empty, clarsimp) |
331 apply (frule len_not_empty, clarsimp) |
334 apply (ind_cases "{|M,l'|}:valid A n B") |
332 apply (ind_cases "{|M,l'|}:valid A n B" for l') |
335 apply (frule len_not_empty, clarsimp, simp) |
333 apply (frule len_not_empty, clarsimp, simp) |
336 (* i > 0 *) |
334 (* i > 0 *) |
337 apply clarify |
335 apply clarify |
338 apply (frule len_not_empty, clarsimp) |
336 apply (frule len_not_empty, clarsimp) |
339 apply (ind_cases "{|x,l'|}:valid A n B") |
337 apply (ind_cases "{|x,l'|}:valid A n B" for x l') |
340 apply (frule len_not_empty, clarsimp) |
338 apply (frule len_not_empty, clarsimp) |
341 by (drule_tac x=l' in spec, clarsimp) |
339 by (drule_tac x=l' in spec, clarsimp) |
342 |
340 |
343 subsubsection{*declarations for tactics*} |
341 subsubsection{*declarations for tactics*} |
344 |
342 |
373 |
371 |
374 lemma p1_is_Gets_correct [iff]: "Gets_correct p1" |
372 lemma p1_is_Gets_correct [iff]: "Gets_correct p1" |
375 by (auto simp: Gets_correct_def dest: p1_has_no_Gets) |
373 by (auto simp: Gets_correct_def dest: p1_has_no_Gets) |
376 |
374 |
377 lemma p1_is_one_step [iff]: "one_step p1" |
375 lemma p1_is_one_step [iff]: "one_step p1" |
378 by (unfold one_step_def, clarify, ind_cases "ev#evs:p1", auto) |
376 by (unfold one_step_def, clarify, ind_cases "ev#evs:p1" for ev evs, auto) |
379 |
377 |
380 lemma p1_has_only_Says' [rule_format]: "evs:p1 ==> |
378 lemma p1_has_only_Says' [rule_format]: "evs:p1 ==> |
381 ev:set evs --> (EX A B X. ev=Says A B X)" |
379 ev:set evs --> (EX A B X. ev=Says A B X)" |
382 by (erule p1.induct, auto simp: req_def pro_def) |
380 by (erule p1.induct, auto simp: req_def pro_def) |
383 |
381 |