# HG changeset patch
# User paulson
# Date 1279016839 -3600
# Node ID 56426b8425a069c2893cb2013b45aaf1a5aacf50
# Parent  868ceaa6b039245bcd73a7ddb7582f45e1925f12# Parent  4c25d41b998204ff6bd167ead74e261b05bd3d9c
merged

diff -r 868ceaa6b039 -r 56426b8425a0 src/HOL/Auth/KerberosIV.thy
--- a/src/HOL/Auth/KerberosIV.thy	Tue Jul 13 11:23:21 2010 +0100
+++ b/src/HOL/Auth/KerberosIV.thy	Tue Jul 13 11:27:19 2010 +0100
@@ -33,20 +33,20 @@
  (* A is the true creator of X if she has sent X and X never appeared on
     the trace before this event. Recall that traces grow from head. *)
   Issues :: "[agent, agent, msg, event list] => bool"
-             ("_ Issues _ with _ on _") where
-   "A Issues B with X on evs =
+             ("_ Issues _ with _ on _" [50, 0, 0, 50] 50) where
+   "(A Issues B with X on evs) =
       (\<exists>Y. Says A B Y \<in> set evs & X \<in> parts {Y} &
         X \<notin> parts (spies (takeWhile (% z. z  \<noteq> Says A B Y) (rev evs))))"
 
 definition
  (* Yields the subtrace of a given trace from its beginning to a given event *)
-  before :: "[event, event list] => event list" ("before _ on _")
-  where "before ev on evs = takeWhile (% z. z ~= ev) (rev evs)"
+  before :: "[event, event list] => event list" ("before _ on _" [0, 50] 50)
+  where "(before ev on evs) = takeWhile (% z. z ~= ev) (rev evs)"
 
 definition
  (* States than an event really appears only once on a trace *)
-  Unique :: "[event, event list] => bool" ("Unique _ on _")
-  where "Unique ev on evs = (ev \<notin> set (tl (dropWhile (% z. z \<noteq> ev) evs)))"
+  Unique :: "[event, event list] => bool" ("Unique _ on _" [0, 50] 50)
+  where "(Unique ev on evs) = (ev \<notin> set (tl (dropWhile (% z. z \<noteq> ev) evs)))"
 
 
 consts
@@ -96,7 +96,7 @@
   "expiredA T evs == authlife + T < CT evs"
 
 abbreviation
-  valid :: "[nat, nat] => bool" ("valid _ wrt _") where
+  valid :: "[nat, nat] => bool" ("valid _ wrt _" [0, 50] 50) where
   "valid T1 wrt T2 == T1 <= replylife + T2"
 
 (*---------------------------------------------------------------------*)
@@ -332,8 +332,7 @@
 lemma K3_msg_in_parts_spies:
      "Says Kas' A (Crypt KeyA \<lbrace>authK, Peer, Ta, authTicket\<rbrace>)
                \<in> set evs \<Longrightarrow> authTicket \<in> parts (spies evs)"
-apply blast
-done
+by blast
 
 lemma Oops_range_spies1:
      "\<lbrakk> Says Kas A (Crypt KeyA \<lbrace>Key authK, Peer, Ta, authTicket\<rbrace>)
@@ -347,8 +346,7 @@
 lemma K5_msg_in_parts_spies:
      "Says Tgs' A (Crypt authK \<lbrace>servK, Agent B, Ts, servTicket\<rbrace>)
                \<in> set evs \<Longrightarrow> servTicket \<in> parts (spies evs)"
-apply blast
-done
+by blast
 
 lemma Oops_range_spies2:
      "\<lbrakk> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Ts, servTicket\<rbrace>)
@@ -361,8 +359,7 @@
 lemma Says_ticket_parts:
      "Says S A (Crypt K \<lbrace>SesKey, B, TimeStamp, Ticket\<rbrace>) \<in> set evs
       \<Longrightarrow> Ticket \<in> parts (spies evs)"
-apply blast
-done
+by blast
 
 (*Spy never sees another agent's shared key! (unless it's lost at start)*)
 lemma Spy_see_shrK [simp]:
@@ -408,21 +405,21 @@
 
 subsection{*Lemmas for reasoning about predicate "before"*}
 
-lemma used_Says_rev: "used (evs @ [Says A B X]) = parts {X} \<union> (used evs)";
+lemma used_Says_rev: "used (evs @ [Says A B X]) = parts {X} \<union> (used evs)"
 apply (induct_tac "evs")
 apply simp
 apply (induct_tac "a")
 apply auto
 done
 
-lemma used_Notes_rev: "used (evs @ [Notes A X]) = parts {X} \<union> (used evs)";
+lemma used_Notes_rev: "used (evs @ [Notes A X]) = parts {X} \<union> (used evs)"
 apply (induct_tac "evs")
 apply simp
 apply (induct_tac "a")
 apply auto
 done
 
-lemma used_Gets_rev: "used (evs @ [Gets B X]) = used evs";
+lemma used_Gets_rev: "used (evs @ [Gets B X]) = used evs"
 apply (induct_tac "evs")
 apply simp
 apply (induct_tac "a")
@@ -448,13 +445,11 @@
 done
 
 lemma set_evs_rev: "set evs = set (rev evs)"
-apply auto
-done
+by auto
 
 lemma takeWhile_void [rule_format]:
       "x \<notin> set evs \<longrightarrow> takeWhile (\<lambda>z. z \<noteq> x) evs = evs"
-apply auto
-done
+by auto
 
 
 subsection{*Regularity Lemmas*}
@@ -612,11 +607,7 @@
       (\<exists>A. servTicket =
               Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Ts\<rbrace>)
        | servTicket \<in> analz (spies evs)"
-apply (frule Says_imp_spies [THEN analz.Inj], auto)
- apply (force dest!: servTicket_form)
-apply (frule analz_into_parts)
-apply (frule servTicket_form, auto)
-done
+by (metis Says_imp_analz_Spy Says_imp_parts_knows_Spy analz.Decrypt analz.Snd invKey_K servTicket_form)
 
 
 subsection{*Authenticity theorems: confirm origin of sensitive messages*}
@@ -735,8 +726,7 @@
          (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta,
             Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>\<rbrace>)
         \<in> set evs"
-apply (blast dest!: servTicket_authentic_Tgs K4_imp_K2)
-done
+by (blast dest!: servTicket_authentic_Tgs K4_imp_K2)
 
 lemma u_servTicket_authentic_Kas:
      "\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
@@ -746,8 +736,7 @@
            Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>\<rbrace>)
              \<in> set evs
            & servKlife + Ts <= authKlife + Ta"
-apply (blast dest!: servTicket_authentic_Tgs u_K4_imp_K2)
-done
+by (blast dest!: servTicket_authentic_Tgs u_K4_imp_K2)
 
 lemma servTicket_authentic:
      "\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
@@ -760,8 +749,7 @@
      & Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts,
                    Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>\<rbrace>)
        \<in> set evs"
-apply (blast dest: servTicket_authentic_Tgs K4_imp_K2)
-done
+by (blast dest: servTicket_authentic_Tgs K4_imp_K2)
 
 lemma u_servTicket_authentic:
      "\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
@@ -775,8 +763,7 @@
                    Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>\<rbrace>)
        \<in> set evs
      & servKlife + Ts <= authKlife + Ta)"
-apply (blast dest: servTicket_authentic_Tgs u_K4_imp_K2)
-done
+by (blast dest: servTicket_authentic_Tgs u_K4_imp_K2)
 
 lemma u_NotexpiredSK_NotexpiredAK:
      "\<lbrakk> \<not> expiredSK Ts evs; servKlife + Ts <= authKlife + Ta \<rbrakk>
@@ -924,9 +911,10 @@
 apply (erule kerbIV.induct, analz_mono_contra)
 apply (frule_tac [7] K5_msg_in_parts_spies)
 apply (frule_tac [5] K3_msg_in_parts_spies, simp_all, blast)
-txt{*K2 and K4 remain*}
-prefer 2 apply (blast dest!: unique_CryptKey)
+txt{*K2*}
 apply (blast dest!: servK_authentic Says_Tgs_message_form authKeys_used)
+txt{*K4 remain*}
+apply (blast dest!: unique_CryptKey)
 done
 
 
@@ -1028,10 +1016,8 @@
                 \<lbrace>Key servK, Agent B, Number Ts,
                   Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace> \<rbrace>)
      | AKcryptSK authK servK evs)"
-apply (unfold AKcryptSK_def)
-apply (simp (no_asm))
-apply blast
-done
+by (auto simp add: AKcryptSK_def)
+
 
 (*A fresh authK cannot be associated with any other
   (with respect to a given trace). *)
@@ -1049,8 +1035,7 @@
   (with respect to a given trace). *)
 lemma Serv_fresh_not_AKcryptSK:
  "Key servK \<notin> used evs \<Longrightarrow> \<not> AKcryptSK authK servK evs"
-apply (unfold AKcryptSK_def, blast)
-done
+by (unfold AKcryptSK_def, blast)
 
 lemma authK_not_AKcryptSK:
      "\<lbrakk> Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, tk\<rbrace>
@@ -1167,8 +1152,7 @@
                      \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
            \<in> set evs \<rbrakk>
       \<Longrightarrow> \<not> AKcryptSK servK SK evs"
-apply (blast dest: AKcryptSKI AKcryptSK_not_AKcryptSK)
-done
+by (blast dest: AKcryptSKI AKcryptSK_not_AKcryptSK)
    
 text{* Big simplification law for keys SK that are not crypted by keys in KK
  It helps prove three, otherwise hard, facts about keys. These facts are
@@ -1349,7 +1333,7 @@
 apply (erule rev_mp)
 apply (erule rev_mp)
 apply (erule kerbIV.induct)
-apply (rule_tac [9] impI)+;
+apply (rule_tac [9] impI)+
   --{*The Oops1 case is unusual: must simplify
     @{term "Authkey \<notin> analz (spies (ev#evs))"}, not letting
    @{text analz_mono_contra} weaken it to
@@ -1387,8 +1371,7 @@
          \<not> expiredSK Ts evs;
          A \<notin> bad;  B \<notin> bad; evs \<in> kerbIV \<rbrakk>
       \<Longrightarrow> Key servK \<notin> analz (spies evs)"
-apply (blast dest: Says_Tgs_message_form Confidentiality_lemma)
-done
+by (blast dest: Says_Tgs_message_form Confidentiality_lemma)
 
 text{* In the real world Tgs CAN check what Kas sends! *}
 lemma Confidentiality_Tgs_bis:
@@ -1401,8 +1384,7 @@
          \<not> expiredAK Ta evs; \<not> expiredSK Ts evs;
          A \<notin> bad;  B \<notin> bad; evs \<in> kerbIV \<rbrakk>
       \<Longrightarrow> Key servK \<notin> analz (spies evs)"
-apply (blast dest!: Confidentiality_Kas Confidentiality_Tgs)
-done
+by (blast dest!: Confidentiality_Kas Confidentiality_Tgs)
 
 text{*Most general form*}
 lemmas Confidentiality_Tgs_ter = authTicket_authentic [THEN Confidentiality_Tgs_bis]
@@ -1419,8 +1401,7 @@
          \<not> expiredAK Ta evs; A \<notin> bad; evs \<in> kerbIV \<rbrakk>
  \<Longrightarrow>Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
        \<in> set evs"
-apply (blast dest: authK_authentic Confidentiality_Auth_A servK_authentic_ter)
-done
+by (blast dest: authK_authentic Confidentiality_Auth_A servK_authentic_ter)
 
 lemma Confidentiality_Serv_A:
      "\<lbrakk> Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>
@@ -1466,8 +1447,7 @@
          \<not> expiredSK Ts evs;
          A \<notin> bad;  B \<notin> bad;  B \<noteq> Tgs; evs \<in> kerbIV \<rbrakk>
       \<Longrightarrow> Key servK \<notin> analz (spies evs)"
-apply (blast dest: u_servTicket_authentic u_NotexpiredSK_NotexpiredAK Confidentiality_Tgs_bis)
-done
+by (blast dest: u_servTicket_authentic u_NotexpiredSK_NotexpiredAK Confidentiality_Tgs_bis)
 
 
 
@@ -1497,9 +1477,10 @@
 apply (erule kerbIV.induct, analz_mono_contra)
 apply (frule_tac [7] K5_msg_in_parts_spies)
 apply (frule_tac [5] K3_msg_in_parts_spies, simp_all, blast)
-txt{*K2 and K4 remain*}
-prefer 2 apply (blast dest!: unique_CryptKey)
+txt{*K2*}
 apply (blast dest!: servK_authentic Says_Tgs_message_form authKeys_used)
+txt{*K4*}
+apply (blast dest!: unique_CryptKey)
 done
 
 
@@ -1511,8 +1492,7 @@
         A \<notin> bad; B \<notin> bad; B \<noteq> Tgs; evs \<in> kerbIV \<rbrakk>
  \<Longrightarrow> Says A B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>,
                Crypt servK \<lbrace>Agent A, Number T3\<rbrace>\<rbrace> \<in> set evs"
-apply (blast dest: servTicket_authentic_Tgs intro: Says_K5)
-done
+by (blast dest: servTicket_authentic_Tgs intro: Says_K5)
 
 text{*The second assumption tells B what kind of key servK is.*}
 lemma B_authenticates_A_r:
@@ -1527,8 +1507,7 @@
          B \<noteq> Tgs; A \<notin> bad;  B \<notin> bad;  evs \<in> kerbIV \<rbrakk>
    \<Longrightarrow> Says A B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>,
                   Crypt servK \<lbrace>Agent A, Number T3\<rbrace> \<rbrace> \<in> set evs"
-apply (blast intro: Says_K5 dest: Confidentiality_B servTicket_authentic_Tgs)
-done
+by (blast intro: Says_K5 dest: Confidentiality_B servTicket_authentic_Tgs)
 
 text{* @{text u_B_authenticates_A} would be the same as @{text B_authenticates_A} because the servK confidentiality assumption is yet unrelaxed*}
 
@@ -1540,8 +1519,7 @@
          B \<noteq> Tgs; A \<notin> bad;  B \<notin> bad;  evs \<in> kerbIV \<rbrakk>
    \<Longrightarrow> Says A B \<lbrace>Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>,
                   Crypt servK \<lbrace>Agent A, Number T3\<rbrace> \<rbrace> \<in> set evs"
-apply (blast intro: Says_K5 dest: u_Confidentiality_B servTicket_authentic_Tgs)
-done
+by (blast intro: Says_K5 dest: u_Confidentiality_B servTicket_authentic_Tgs)
 
 lemma A_authenticates_B:
      "\<lbrakk> Crypt servK (Number T3) \<in> parts (spies evs);
@@ -1552,16 +1530,7 @@
          Key authK \<notin> analz (spies evs); Key servK \<notin> analz (spies evs);
          A \<notin> bad;  B \<notin> bad; evs \<in> kerbIV \<rbrakk>
       \<Longrightarrow> Says B A (Crypt servK (Number T3)) \<in> set evs"
-apply (frule authK_authentic)
-apply assumption+
-apply (frule servK_authentic)
-prefer 2 apply (blast dest: authK_authentic Says_Kas_message_form)
-apply assumption+
-apply (blast dest: K4_imp_K2 Key_unique_SesKey intro!: Says_K6)
-(*Single command proof: slower!
-apply (blast dest: authK_authentic servK_authentic Says_Kas_message_form Key_unique_SesKey K4_imp_K2 intro!: Says_K6)
-*)
-done
+by (blast dest: authK_authentic servK_authentic Says_Kas_message_form Key_unique_SesKey K4_imp_K2 intro: Says_K6)
 
 lemma A_authenticates_B_r:
      "\<lbrakk> Crypt servK (Number T3) \<in> parts (spies evs);
@@ -1615,15 +1584,13 @@
      A \<notin> bad; evs \<in> kerbIV \<rbrakk>
  \<Longrightarrow> Kas Issues A with (Crypt (shrK A) \<lbrace>Key authK, Peer, Ta, authTicket\<rbrace>) 
           on evs"
-apply (blast dest: authK_authentic Kas_Issues_A)
-done
+by (blast dest: authK_authentic Kas_Issues_A)
 
 lemma honest_never_says_newer_timestamp_in_auth:
      "\<lbrakk> (CT evs) \<le> T; A \<notin> bad; Number T \<in> parts {X}; evs \<in> kerbIV \<rbrakk> 
      \<Longrightarrow> \<forall> B Y.  Says A B \<lbrace>Y, X\<rbrace> \<notin> set evs"
 apply (erule rev_mp)
 apply (erule kerbIV.induct)
-apply (simp_all)
 apply force+
 done
 
@@ -1636,7 +1603,7 @@
     "\<lbrakk> Crypt K \<lbrace>Agent A, Number T\<rbrace> \<in> parts (spies evs);
        Key K \<notin> analz (spies evs); evs \<in> kerbIV \<rbrakk>
 \<Longrightarrow> \<exists> B X. Says A Tgs \<lbrace>X, Crypt K \<lbrace>Agent A, Number T\<rbrace>, Agent B\<rbrace> \<in> set evs \<or> 
-           Says A B \<lbrace>X, Crypt K \<lbrace>Agent A, Number T\<rbrace>\<rbrace> \<in> set evs";
+           Says A B \<lbrace>X, Crypt K \<lbrace>Agent A, Number T\<rbrace>\<rbrace> \<in> set evs"
 apply (erule rev_mp)
 apply (erule rev_mp)
 apply (erule kerbIV.induct, analz_mono_contra)
@@ -1684,8 +1651,7 @@
      Key authK \<notin> analz (spies evs);  
      A \<notin> bad; evs \<in> kerbIV \<rbrakk>
  \<Longrightarrow> A Issues Tgs with (Crypt authK \<lbrace>Agent A, Number T2\<rbrace>) on evs"
-apply (blast dest: A_Issues_Tgs Tgs_authenticates_A)
-done
+by (blast dest: A_Issues_Tgs Tgs_authenticates_A)
 
 lemma Tgs_Issues_A:
     "\<lbrakk> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket \<rbrace>)
@@ -1706,7 +1672,7 @@
 txt{*K4*}
 apply (simp add: takeWhile_tail)
 (*Last two thms installed only to derive authK \<notin> range shrK*)
-apply (blast dest: servK_authentic parts_spies_takeWhile_mono [THEN subsetD] parts_spies_evs_revD2 [THEN subsetD] authTicket_authentic Says_Kas_message_form)
+apply (metis knows_Spy_partsEs(2) parts.Fst usedI used_evs_rev used_takeWhile_used)
 done
 
 lemma A_authenticates_and_keydist_to_Tgs:
@@ -1714,8 +1680,7 @@
   Key authK \<notin> analz (spies evs); B \<noteq> Tgs; evs \<in> kerbIV \<rbrakk>
  \<Longrightarrow> \<exists>A. Tgs Issues A with 
           (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket \<rbrace>) on evs"
-apply (blast dest: Tgs_Issues_A servK_authentic_bis)
-done
+by (blast dest: Tgs_Issues_A servK_authentic_bis)
 
 
 
@@ -1751,8 +1716,7 @@
          \<not> expiredSK Ts evs; \<not> expiredAK Ta evs;
          A \<notin> bad;  B \<notin> bad; B \<noteq> Tgs; evs \<in> kerbIV \<rbrakk>
       \<Longrightarrow> B Issues A with (Crypt servK (Number T3)) on evs"
-apply (blast dest!: Confidentiality_B B_Issues_A)
-done
+by (blast dest!: Confidentiality_B B_Issues_A)
 
 lemma u_B_Issues_A_r:
      "\<lbrakk> Says B A (Crypt servK (Number T3)) \<in> set evs;
@@ -1761,8 +1725,7 @@
          \<not> expiredSK Ts evs;
          A \<notin> bad;  B \<notin> bad; B \<noteq> Tgs; evs \<in> kerbIV \<rbrakk>
       \<Longrightarrow> B Issues A with (Crypt servK (Number T3)) on evs"
-apply (blast dest!: u_Confidentiality_B B_Issues_A)
-done
+by (blast dest!: u_Confidentiality_B B_Issues_A)
 
 lemma A_authenticates_and_keydist_to_B:
      "\<lbrakk> Crypt servK (Number T3) \<in> parts (spies evs);
@@ -1773,8 +1736,7 @@
          Key authK \<notin> analz (spies evs); Key servK \<notin> analz (spies evs);
          A \<notin> bad;  B \<notin> bad; B \<noteq> Tgs; evs \<in> kerbIV \<rbrakk>
       \<Longrightarrow> B Issues A with (Crypt servK (Number T3)) on evs"
-apply (blast dest!: A_authenticates_B B_Issues_A)
-done
+by (blast dest!: A_authenticates_B B_Issues_A)
 
 lemma A_authenticates_and_keydist_to_B_r:
      "\<lbrakk> Crypt servK (Number T3) \<in> parts (spies evs);
@@ -1785,8 +1747,7 @@
          \<not> expiredAK Ta evs; \<not> expiredSK Ts evs;
          A \<notin> bad;  B \<notin> bad; B \<noteq> Tgs; evs \<in> kerbIV \<rbrakk>
       \<Longrightarrow> B Issues A with (Crypt servK (Number T3)) on evs"
-apply (blast dest!: A_authenticates_B_r Confidentiality_Serv_A B_Issues_A)
-done
+by (blast dest!: A_authenticates_B_r Confidentiality_Serv_A B_Issues_A)
 
 
 lemma A_Issues_B:
@@ -1809,7 +1770,7 @@
 txt{*K5*}
 apply auto
 apply (simp add: takeWhile_tail)
-txt{*Level 15: case study necessary because the assumption doesn't state
+txt{*Level 15: case analysis necessary because the assumption doesn't state
   the form of servTicket. The guarantee becomes stronger.*}
 apply (blast dest: Says_imp_spies [THEN analz.Inj, THEN analz_Decrypt']
                    K3_imp_K2 servK_authentic_ter
@@ -1829,8 +1790,7 @@
          \<not> expiredAK Ta evs; \<not> expiredSK Ts evs;
          B \<noteq> Tgs; A \<notin> bad;  B \<notin> bad;  evs \<in> kerbIV \<rbrakk>
    \<Longrightarrow> A Issues B with (Crypt servK \<lbrace>Agent A, Number T3\<rbrace>) on evs"
-apply (blast dest!: Confidentiality_Serv_A A_Issues_B)
-done
+by (blast dest!: Confidentiality_Serv_A A_Issues_B)
 
 lemma B_authenticates_and_keydist_to_A:
      "\<lbrakk> Crypt servK \<lbrace>Agent A, Number T3\<rbrace> \<in> parts (spies evs);
@@ -1839,8 +1799,7 @@
          Key servK \<notin> analz (spies evs);
          B \<noteq> Tgs; A \<notin> bad;  B \<notin> bad;  evs \<in> kerbIV \<rbrakk>
    \<Longrightarrow> A Issues B with (Crypt servK \<lbrace>Agent A, Number T3\<rbrace>) on evs"
-apply (blast dest: B_authenticates_A A_Issues_B)
-done
+by (blast dest: B_authenticates_A A_Issues_B)
 
 lemma B_authenticates_and_keydist_to_A_r:
      "\<lbrakk> Crypt servK \<lbrace>Agent A, Number T3\<rbrace> \<in> parts (spies evs);
@@ -1853,8 +1812,7 @@
          \<not> expiredSK Ts evs; \<not> expiredAK Ta evs;
          B \<noteq> Tgs; A \<notin> bad;  B \<notin> bad;  evs \<in> kerbIV \<rbrakk>
    \<Longrightarrow> A Issues B with (Crypt servK \<lbrace>Agent A, Number T3\<rbrace>) on evs"
-apply (blast dest: B_authenticates_A Confidentiality_B A_Issues_B)
-done
+by (blast dest: B_authenticates_A Confidentiality_B A_Issues_B)
 
 text{* @{text u_B_authenticates_and_keydist_to_A} would be the same as @{text B_authenticates_and_keydist_to_A} because the
  servK confidentiality assumption is yet unrelaxed*}
@@ -1866,10 +1824,6 @@
          \<not> expiredSK Ts evs;
          B \<noteq> Tgs; A \<notin> bad;  B \<notin> bad;  evs \<in> kerbIV \<rbrakk>
    \<Longrightarrow> A Issues B with (Crypt servK \<lbrace>Agent A, Number T3\<rbrace>) on evs"
-apply (blast dest: u_B_authenticates_A_r u_Confidentiality_B A_Issues_B)
-done
-
-
-
+by (blast dest: u_B_authenticates_A_r u_Confidentiality_B A_Issues_B)
 
 end