422 |
422 |
423 end |
423 end |
424 *} |
424 *} |
425 |
425 |
426 method_setup analz_freshK = {* |
426 method_setup analz_freshK = {* |
427 Method.ctxt_args (fn ctxt => |
427 Scan.succeed (fn ctxt => |
428 (SIMPLE_METHOD |
428 (SIMPLE_METHOD |
429 (EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]), |
429 (EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]), |
430 REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}), |
430 REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}), |
431 ALLGOALS (asm_simp_tac (Simplifier.context ctxt Public.analz_image_freshK_ss))]))) *} |
431 ALLGOALS (asm_simp_tac (Simplifier.context ctxt Public.analz_image_freshK_ss))]))) *} |
432 "for proving the Session Key Compromise theorem" |
432 "for proving the Session Key Compromise theorem" |
433 |
433 |
434 |
434 |
435 subsection{*Specialized Methods for Possibility Theorems*} |
435 subsection{*Specialized Methods for Possibility Theorems*} |
436 |
436 |
437 method_setup possibility = {* |
437 method_setup possibility = {* |
438 Method.ctxt_args (SIMPLE_METHOD o Public.possibility_tac) *} |
438 Scan.succeed (SIMPLE_METHOD o Public.possibility_tac) *} |
439 "for proving possibility theorems" |
439 "for proving possibility theorems" |
440 |
440 |
441 method_setup basic_possibility = {* |
441 method_setup basic_possibility = {* |
442 Method.ctxt_args (SIMPLE_METHOD o Public.basic_possibility_tac) *} |
442 Scan.succeed (SIMPLE_METHOD o Public.basic_possibility_tac) *} |
443 "for proving possibility theorems" |
443 "for proving possibility theorems" |
444 |
444 |
445 end |
445 end |