372 (ALLGOALS (simp_tac (ctxt |
372 (ALLGOALS (simp_tac (ctxt |
373 delsimps @{thms used_Cons_simps} |
373 delsimps @{thms used_Cons_simps} |
374 setSolver safe_solver)) |
374 setSolver safe_solver)) |
375 THEN |
375 THEN |
376 REPEAT_FIRST (eq_assume_tac ORELSE' |
376 REPEAT_FIRST (eq_assume_tac ORELSE' |
377 resolve_tac [refl, conjI, @{thm Nonce_supply}]))) |
377 resolve_tac ctxt [refl, conjI, @{thm Nonce_supply}]))) |
378 |
378 |
379 (*For harder protocols (such as Recur) where we have to set up some |
379 (*For harder protocols (such as Recur) where we have to set up some |
380 nonces and keys initially*) |
380 nonces and keys initially*) |
381 fun basic_possibility_tac ctxt = |
381 fun basic_possibility_tac ctxt = |
382 REPEAT |
382 REPEAT |
383 (ALLGOALS (asm_simp_tac (ctxt setSolver safe_solver)) |
383 (ALLGOALS (asm_simp_tac (ctxt setSolver safe_solver)) |
384 THEN |
384 THEN |
385 REPEAT_FIRST (resolve_tac [refl, conjI])) |
385 REPEAT_FIRST (resolve_tac ctxt [refl, conjI])) |
386 |
386 |
387 val analz_image_freshK_ss = |
387 val analz_image_freshK_ss = |
388 simpset_of |
388 simpset_of |
389 (@{context} delsimps [image_insert, image_Un] |
389 (@{context} delsimps [image_insert, image_Un] |
390 delsimps [@{thm imp_disjL}] (*reduces blow-up*) |
390 delsimps [@{thm imp_disjL}] (*reduces blow-up*) |
401 (*Specialized methods*) |
401 (*Specialized methods*) |
402 |
402 |
403 method_setup analz_freshK = {* |
403 method_setup analz_freshK = {* |
404 Scan.succeed (fn ctxt => |
404 Scan.succeed (fn ctxt => |
405 (SIMPLE_METHOD |
405 (SIMPLE_METHOD |
406 (EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]), |
406 (EVERY [REPEAT_FIRST (resolve_tac ctxt [allI, ballI, impI]), |
407 REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}), |
407 REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}), |
408 ALLGOALS (asm_simp_tac (put_simpset Smartcard.analz_image_freshK_ss ctxt))]))) *} |
408 ALLGOALS (asm_simp_tac (put_simpset Smartcard.analz_image_freshK_ss ctxt))]))) *} |
409 "for proving the Session Key Compromise theorem" |
409 "for proving the Session Key Compromise theorem" |
410 |
410 |
411 method_setup possibility = {* |
411 method_setup possibility = {* |