833 val shouprubin_assumes_securemeans = thm "shouprubin_assumes_securemeans" |
833 val shouprubin_assumes_securemeans = thm "shouprubin_assumes_securemeans" |
834 val analz_image_Key_Un_Nonce= thm "analz_image_Key_Un_Nonce" |
834 val analz_image_Key_Un_Nonce= thm "analz_image_Key_Un_Nonce" |
835 *} |
835 *} |
836 |
836 |
837 method_setup sc_analz_freshK = {* |
837 method_setup sc_analz_freshK = {* |
838 Method.no_args |
838 Method.ctxt_args (fn ctxt => |
839 (Method.METHOD |
839 (Method.METHOD |
840 (fn facts => EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]), |
840 (fn facts => EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]), |
841 REPEAT_FIRST (rtac analz_image_freshK_lemma), |
841 REPEAT_FIRST (rtac analz_image_freshK_lemma), |
842 ALLGOALS (asm_simp_tac (analz_image_freshK_ss |
842 ALLGOALS (asm_simp_tac (Simplifier.context ctxt analz_image_freshK_ss |
843 addsimps [knows_Spy_Inputs_secureM_sr_Spy, |
843 addsimps [knows_Spy_Inputs_secureM_sr_Spy, |
844 knows_Spy_Outpts_secureM_sr_Spy, |
844 knows_Spy_Outpts_secureM_sr_Spy, |
845 shouprubin_assumes_securemeans, |
845 shouprubin_assumes_securemeans, |
846 analz_image_Key_Un_Nonce]))])) *} |
846 analz_image_Key_Un_Nonce]))]))) *} |
847 "for proving the Session Key Compromise theorem for smartcard protocols" |
847 "for proving the Session Key Compromise theorem for smartcard protocols" |
848 |
848 |
849 |
849 |
850 lemma analz_image_freshK [rule_format]: |
850 lemma analz_image_freshK [rule_format]: |
851 "evs \<in> sr \<Longrightarrow> \<forall> K KK. |
851 "evs \<in> sr \<Longrightarrow> \<forall> K KK. |