[STATEMENT]
lemma servK_authentic:
     "\<lbrakk> Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>
           \<in> parts (spies evs);
         Key authK \<notin> analz (spies evs);
         authK \<notin> range shrK;
         evs \<in> kerbV \<rbrakk>
 \<Longrightarrow> \<exists>A ST. Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace>
       \<in> set evs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy evs); Key authK \<notin> analz (knows Spy evs); authK \<notin> range shrK; evs \<in> kerbV\<rbrakk> \<Longrightarrow> \<exists>A ST. Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set evs
[PROOF STEP]
apply (erule rev_mp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Key authK \<notin> analz (knows Spy evs); authK \<notin> range shrK; evs \<in> kerbV\<rbrakk> \<Longrightarrow> Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy evs) \<longrightarrow> (\<exists>A ST. Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set evs)
[PROOF STEP]
apply (erule rev_mp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>authK \<notin> range shrK; evs \<in> kerbV\<rbrakk> \<Longrightarrow> Key authK \<notin> analz (knows Spy evs) \<longrightarrow> Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy evs) \<longrightarrow> (\<exists>A ST. Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set evs)
[PROOF STEP]
apply (erule kerbV.induct, analz_mono_contra)
[PROOF STATE]
proof (prove)
goal (10 subgoals):
 1. authK \<notin> range shrK \<Longrightarrow> Key authK \<notin> analz (knows Spy []) \<longrightarrow> Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy []) \<longrightarrow> (\<exists>A ST. Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set [])
 2. \<And>evsf X Ba. \<lbrakk>authK \<notin> range shrK; evsf \<in> kerbV; X \<in> synth (analz (knows Spy evsf)); Key authK \<notin> analz (knows Spy evsf); Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy evsf) \<longrightarrow> (\<exists>A ST. Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set evsf)\<rbrakk> \<Longrightarrow> Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy (Says Spy Ba X # evsf)) \<longrightarrow> (\<exists>A ST. Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set (Says Spy Ba X # evsf))
 3. \<And>evs1 A. \<lbrakk>authK \<notin> range shrK; evs1 \<in> kerbV; Key authK \<notin> analz (knows Spy evs1); Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy evs1) \<longrightarrow> (\<exists>A ST. Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set evs1)\<rbrakk> \<Longrightarrow> Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy (Says A Kas \<lbrace>Agent A, Agent Tgs, Number (CT evs1)\<rbrace> # evs1)) \<longrightarrow> (\<exists>Aa ST. Says Tgs Aa \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set (Says A Kas \<lbrace>Agent A, Agent Tgs, Number (CT evs1)\<rbrace> # evs1))
 4. \<And>evs2 authKa A' A T1. \<lbrakk>authK \<notin> range shrK; evs2 \<in> kerbV; Key authKa \<notin> used evs2; authKa \<in> symKeys; Says A' Kas \<lbrace>Agent A, Agent Tgs, Number T1\<rbrace> \<in> set evs2; Key authK \<notin> analz (knows Spy evs2); Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy evs2) \<longrightarrow> (\<exists>A ST. Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set evs2)\<rbrakk> \<Longrightarrow> Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy (Says Kas A \<lbrace>Crypt (shrK A) \<lbrace>Key authKa, Agent Tgs, Number (CT evs2)\<rbrace>, Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authKa, Number (CT evs2)\<rbrace>\<rbrace> # evs2)) \<longrightarrow> (\<exists>Aa ST. Says Tgs Aa \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set (Says Kas A \<lbrace>Crypt (shrK A) \<lbrace>Key authKa, Agent Tgs, Number (CT evs2)\<rbrace>, Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authKa, Number (CT evs2)\<rbrace>\<rbrace> # evs2))
 5. \<And>evs3 A T1 Kas' authKa Ta authTicket Ba. \<lbrakk>authK \<notin> range shrK; evs3 \<in> kerbV; A \<noteq> Kas; A \<noteq> Tgs; Says A Kas \<lbrace>Agent A, Agent Tgs, Number T1\<rbrace> \<in> set evs3; Says Kas' A \<lbrace>Crypt (shrK A) \<lbrace>Key authKa, Agent Tgs, Number Ta\<rbrace>, authTicket\<rbrace> \<in> set evs3; valid Ta wrt T1; Key authK \<notin> analz (knows Spy evs3); Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy evs3) \<longrightarrow> (\<exists>A ST. Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set evs3)\<rbrakk> \<Longrightarrow> Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy (Says A Tgs \<lbrace>authTicket, Crypt authKa \<lbrace>Agent A, Number (CT evs3)\<rbrace>, Agent Ba\<rbrace> # evs3)) \<longrightarrow> (\<exists>Aa ST. Says Tgs Aa \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set (Says A Tgs \<lbrace>authTicket, Crypt authKa \<lbrace>Agent A, Number (CT evs3)\<rbrace>, Agent Ba\<rbrace> # evs3))
 6. \<And>evs4 servKa Ba authKa A' A Ta T2. \<lbrakk>authK \<notin> range shrK; evs4 \<in> kerbV; Key servKa \<notin> used evs4; servKa \<in> symKeys; Ba \<noteq> Tgs; authKa \<in> symKeys; Says A' Tgs \<lbrace>Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authKa, Number Ta\<rbrace>, Crypt authKa \<lbrace>Agent A, Number T2\<rbrace>, Agent Ba\<rbrace> \<in> set evs4; \<not> expiredAK Ta evs4; \<not> expiredA T2 evs4; servKlife + CT evs4 \<le> authKlife + Ta; Key authK \<notin> analz (knows Spy evs4); Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy evs4) \<longrightarrow> (\<exists>A ST. Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set evs4)\<rbrakk> \<Longrightarrow> Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy (Says Tgs A \<lbrace>Crypt authKa \<lbrace>Key servKa, Agent Ba, Number (CT evs4)\<rbrace>, Crypt (shrK Ba) \<lbrace>Agent A, Agent Ba, Key servKa, Number (CT evs4)\<rbrace>\<rbrace> # evs4)) \<longrightarrow> (\<exists>Aa ST. Says Tgs Aa \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set (Says Tgs A \<lbrace>Crypt authKa \<lbrace>Key servKa, Agent Ba, Number (CT evs4)\<rbrace>, Crypt (shrK Ba) \<lbrace>Agent A, Agent Ba, Key servKa, Number (CT evs4)\<rbrace>\<rbrace> # evs4))
 7. \<And>evs5 authKa servKa A authTicket T2 Ba Tgs' Tsa servTicket. \<lbrakk>authK \<notin> range shrK; evs5 \<in> kerbV; authKa \<in> symKeys; servKa \<in> symKeys; A \<noteq> Kas; A \<noteq> Tgs; Says A Tgs \<lbrace>authTicket, Crypt authKa \<lbrace>Agent A, Number T2\<rbrace>, Agent Ba\<rbrace> \<in> set evs5; Says Tgs' A \<lbrace>Crypt authKa \<lbrace>Key servKa, Agent Ba, Number Tsa\<rbrace>, servTicket\<rbrace> \<in> set evs5; valid Tsa wrt T2; Key authK \<notin> analz (knows Spy evs5); Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy evs5) \<longrightarrow> (\<exists>A ST. Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set evs5)\<rbrakk> \<Longrightarrow> Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy (Says A Ba \<lbrace>servTicket, Crypt servKa \<lbrace>Agent A, Number (CT evs5)\<rbrace>\<rbrace> # evs5)) \<longrightarrow> (\<exists>Aa ST. Says Tgs Aa \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set (Says A Ba \<lbrace>servTicket, Crypt servKa \<lbrace>Agent A, Number (CT evs5)\<rbrace>\<rbrace> # evs5))
 8. \<And>evs6 Ba A' A servKa Tsa T3 Ta2. \<lbrakk>authK \<notin> range shrK; evs6 \<in> kerbV; Ba \<noteq> Kas; Ba \<noteq> Tgs; Says A' Ba \<lbrace>Crypt (shrK Ba) \<lbrace>Agent A, Agent Ba, Key servKa, Number Tsa\<rbrace>, Crypt servKa \<lbrace>Agent A, Number T3\<rbrace>\<rbrace> \<in> set evs6; \<not> expiredSK Tsa evs6; \<not> expiredA T3 evs6; Key authK \<notin> analz (knows Spy evs6); Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy evs6) \<longrightarrow> (\<exists>A ST. Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set evs6)\<rbrakk> \<Longrightarrow> Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy (Says Ba A (Crypt servKa (Number Ta2)) # evs6)) \<longrightarrow> (\<exists>Aa ST. Says Tgs Aa \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set (Says Ba A (Crypt servKa (Number Ta2)) # evs6))
 9. \<And>evsO1 A authKa Ta authTicket. \<lbrakk>authK \<notin> range shrK; evsO1 \<in> kerbV; A \<noteq> Spy; Says Kas A \<lbrace>Crypt (shrK A) \<lbrace>Key authKa, Agent Tgs, Number Ta\<rbrace>, authTicket\<rbrace> \<in> set evsO1; expiredAK Ta evsO1; Key authK \<notin> analz (knows Spy evsO1); Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy evsO1) \<longrightarrow> (\<exists>A ST. Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set evsO1)\<rbrakk> \<Longrightarrow> Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy (Notes Spy \<lbrace>Agent A, Agent Tgs, Number Ta, Key authKa\<rbrace> # evsO1)) \<longrightarrow> (\<exists>Aa ST. Says Tgs Aa \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set (Notes Spy \<lbrace>Agent A, Agent Tgs, Number Ta, Key authKa\<rbrace> # evsO1))
 10. \<And>evsO2 A authKa servKa Ba Tsa servTicket. \<lbrakk>authK \<notin> range shrK; evsO2 \<in> kerbV; A \<noteq> Spy; Says Tgs A \<lbrace>Crypt authKa \<lbrace>Key servKa, Agent Ba, Number Tsa\<rbrace>, servTicket\<rbrace> \<in> set evsO2; expiredSK Tsa evsO2; Key authK \<notin> analz (knows Spy evsO2); Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy evsO2) \<longrightarrow> (\<exists>A ST. Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set evsO2)\<rbrakk> \<Longrightarrow> Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy (Notes Spy \<lbrace>Agent A, Agent Ba, Number Tsa, Key servKa\<rbrace> # evsO2)) \<longrightarrow> (\<exists>Aa ST. Says Tgs Aa \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set (Notes Spy \<lbrace>Agent A, Agent Ba, Number Tsa, Key servKa\<rbrace> # evsO2))
[PROOF STEP]
apply (frule_tac [7] Says_ticket_parts)
[PROOF STATE]
proof (prove)
goal (10 subgoals):
 1. authK \<notin> range shrK \<Longrightarrow> Key authK \<notin> analz (knows Spy []) \<longrightarrow> Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy []) \<longrightarrow> (\<exists>A ST. Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set [])
 2. \<And>evsf X Ba. \<lbrakk>authK \<notin> range shrK; evsf \<in> kerbV; X \<in> synth (analz (knows Spy evsf)); Key authK \<notin> analz (knows Spy evsf); Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy evsf) \<longrightarrow> (\<exists>A ST. Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set evsf)\<rbrakk> \<Longrightarrow> Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy (Says Spy Ba X # evsf)) \<longrightarrow> (\<exists>A ST. Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set (Says Spy Ba X # evsf))
 3. \<And>evs1 A. \<lbrakk>authK \<notin> range shrK; evs1 \<in> kerbV; Key authK \<notin> analz (knows Spy evs1); Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy evs1) \<longrightarrow> (\<exists>A ST. Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set evs1)\<rbrakk> \<Longrightarrow> Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy (Says A Kas \<lbrace>Agent A, Agent Tgs, Number (CT evs1)\<rbrace> # evs1)) \<longrightarrow> (\<exists>Aa ST. Says Tgs Aa \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set (Says A Kas \<lbrace>Agent A, Agent Tgs, Number (CT evs1)\<rbrace> # evs1))
 4. \<And>evs2 authKa A' A T1. \<lbrakk>authK \<notin> range shrK; evs2 \<in> kerbV; Key authKa \<notin> used evs2; authKa \<in> symKeys; Says A' Kas \<lbrace>Agent A, Agent Tgs, Number T1\<rbrace> \<in> set evs2; Key authK \<notin> analz (knows Spy evs2); Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy evs2) \<longrightarrow> (\<exists>A ST. Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set evs2)\<rbrakk> \<Longrightarrow> Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy (Says Kas A \<lbrace>Crypt (shrK A) \<lbrace>Key authKa, Agent Tgs, Number (CT evs2)\<rbrace>, Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authKa, Number (CT evs2)\<rbrace>\<rbrace> # evs2)) \<longrightarrow> (\<exists>Aa ST. Says Tgs Aa \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set (Says Kas A \<lbrace>Crypt (shrK A) \<lbrace>Key authKa, Agent Tgs, Number (CT evs2)\<rbrace>, Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authKa, Number (CT evs2)\<rbrace>\<rbrace> # evs2))
 5. \<And>evs3 A T1 Kas' authKa Ta authTicket Ba. \<lbrakk>authK \<notin> range shrK; evs3 \<in> kerbV; A \<noteq> Kas; A \<noteq> Tgs; Says A Kas \<lbrace>Agent A, Agent Tgs, Number T1\<rbrace> \<in> set evs3; Says Kas' A \<lbrace>Crypt (shrK A) \<lbrace>Key authKa, Agent Tgs, Number Ta\<rbrace>, authTicket\<rbrace> \<in> set evs3; valid Ta wrt T1; Key authK \<notin> analz (knows Spy evs3); Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy evs3) \<longrightarrow> (\<exists>A ST. Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set evs3)\<rbrakk> \<Longrightarrow> Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy (Says A Tgs \<lbrace>authTicket, Crypt authKa \<lbrace>Agent A, Number (CT evs3)\<rbrace>, Agent Ba\<rbrace> # evs3)) \<longrightarrow> (\<exists>Aa ST. Says Tgs Aa \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set (Says A Tgs \<lbrace>authTicket, Crypt authKa \<lbrace>Agent A, Number (CT evs3)\<rbrace>, Agent Ba\<rbrace> # evs3))
 6. \<And>evs4 servKa Ba authKa A' A Ta T2. \<lbrakk>authK \<notin> range shrK; evs4 \<in> kerbV; Key servKa \<notin> used evs4; servKa \<in> symKeys; Ba \<noteq> Tgs; authKa \<in> symKeys; Says A' Tgs \<lbrace>Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authKa, Number Ta\<rbrace>, Crypt authKa \<lbrace>Agent A, Number T2\<rbrace>, Agent Ba\<rbrace> \<in> set evs4; \<not> expiredAK Ta evs4; \<not> expiredA T2 evs4; servKlife + CT evs4 \<le> authKlife + Ta; Key authK \<notin> analz (knows Spy evs4); Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy evs4) \<longrightarrow> (\<exists>A ST. Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set evs4)\<rbrakk> \<Longrightarrow> Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy (Says Tgs A \<lbrace>Crypt authKa \<lbrace>Key servKa, Agent Ba, Number (CT evs4)\<rbrace>, Crypt (shrK Ba) \<lbrace>Agent A, Agent Ba, Key servKa, Number (CT evs4)\<rbrace>\<rbrace> # evs4)) \<longrightarrow> (\<exists>Aa ST. Says Tgs Aa \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set (Says Tgs A \<lbrace>Crypt authKa \<lbrace>Key servKa, Agent Ba, Number (CT evs4)\<rbrace>, Crypt (shrK Ba) \<lbrace>Agent A, Agent Ba, Key servKa, Number (CT evs4)\<rbrace>\<rbrace> # evs4))
 7. \<And>evs5 authKa servKa A authTicket T2 Ba Tgs' Tsa servTicket. \<lbrakk>authK \<notin> range shrK; evs5 \<in> kerbV; authKa \<in> symKeys; servKa \<in> symKeys; A \<noteq> Kas; A \<noteq> Tgs; Says A Tgs \<lbrace>authTicket, Crypt authKa \<lbrace>Agent A, Number T2\<rbrace>, Agent Ba\<rbrace> \<in> set evs5; Says Tgs' A \<lbrace>Crypt authKa \<lbrace>Key servKa, Agent Ba, Number Tsa\<rbrace>, servTicket\<rbrace> \<in> set evs5; valid Tsa wrt T2; Key authK \<notin> analz (knows Spy evs5); Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy evs5) \<longrightarrow> (\<exists>A ST. Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set evs5); servTicket \<in> parts (knows Spy evs5)\<rbrakk> \<Longrightarrow> Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy (Says A Ba \<lbrace>servTicket, Crypt servKa \<lbrace>Agent A, Number (CT evs5)\<rbrace>\<rbrace> # evs5)) \<longrightarrow> (\<exists>Aa ST. Says Tgs Aa \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set (Says A Ba \<lbrace>servTicket, Crypt servKa \<lbrace>Agent A, Number (CT evs5)\<rbrace>\<rbrace> # evs5))
 8. \<And>evs6 Ba A' A servKa Tsa T3 Ta2. \<lbrakk>authK \<notin> range shrK; evs6 \<in> kerbV; Ba \<noteq> Kas; Ba \<noteq> Tgs; Says A' Ba \<lbrace>Crypt (shrK Ba) \<lbrace>Agent A, Agent Ba, Key servKa, Number Tsa\<rbrace>, Crypt servKa \<lbrace>Agent A, Number T3\<rbrace>\<rbrace> \<in> set evs6; \<not> expiredSK Tsa evs6; \<not> expiredA T3 evs6; Key authK \<notin> analz (knows Spy evs6); Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy evs6) \<longrightarrow> (\<exists>A ST. Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set evs6)\<rbrakk> \<Longrightarrow> Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy (Says Ba A (Crypt servKa (Number Ta2)) # evs6)) \<longrightarrow> (\<exists>Aa ST. Says Tgs Aa \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set (Says Ba A (Crypt servKa (Number Ta2)) # evs6))
 9. \<And>evsO1 A authKa Ta authTicket. \<lbrakk>authK \<notin> range shrK; evsO1 \<in> kerbV; A \<noteq> Spy; Says Kas A \<lbrace>Crypt (shrK A) \<lbrace>Key authKa, Agent Tgs, Number Ta\<rbrace>, authTicket\<rbrace> \<in> set evsO1; expiredAK Ta evsO1; Key authK \<notin> analz (knows Spy evsO1); Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy evsO1) \<longrightarrow> (\<exists>A ST. Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set evsO1)\<rbrakk> \<Longrightarrow> Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy (Notes Spy \<lbrace>Agent A, Agent Tgs, Number Ta, Key authKa\<rbrace> # evsO1)) \<longrightarrow> (\<exists>Aa ST. Says Tgs Aa \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set (Notes Spy \<lbrace>Agent A, Agent Tgs, Number Ta, Key authKa\<rbrace> # evsO1))
 10. \<And>evsO2 A authKa servKa Ba Tsa servTicket. \<lbrakk>authK \<notin> range shrK; evsO2 \<in> kerbV; A \<noteq> Spy; Says Tgs A \<lbrace>Crypt authKa \<lbrace>Key servKa, Agent Ba, Number Tsa\<rbrace>, servTicket\<rbrace> \<in> set evsO2; expiredSK Tsa evsO2; Key authK \<notin> analz (knows Spy evsO2); Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy evsO2) \<longrightarrow> (\<exists>A ST. Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set evsO2)\<rbrakk> \<Longrightarrow> Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy (Notes Spy \<lbrace>Agent A, Agent Ba, Number Tsa, Key servKa\<rbrace> # evsO2)) \<longrightarrow> (\<exists>Aa ST. Says Tgs Aa \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set (Notes Spy \<lbrace>Agent A, Agent Ba, Number Tsa, Key servKa\<rbrace> # evsO2))
[PROOF STEP]
apply (frule_tac [5] Says_ticket_parts, simp_all)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>evsf X. \<lbrakk>authK \<notin> range shrK; evsf \<in> kerbV; X \<in> synth (analz (knows Spy evsf)); Key authK \<notin> analz (knows Spy evsf); Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy evsf) \<longrightarrow> (\<exists>A ST. Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set evsf)\<rbrakk> \<Longrightarrow> Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (insert X (knows Spy evsf)) \<longrightarrow> (\<exists>A ST. Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set evsf)
 2. \<And>evs2 authKa A' A T1. \<lbrakk>authK \<notin> range shrK; evs2 \<in> kerbV; Key authKa \<notin> used evs2; authKa \<in> symKeys; Says A' Kas \<lbrace>Agent A, Agent Tgs, Number T1\<rbrace> \<in> set evs2; Key authK \<notin> analz (knows Spy evs2); Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy evs2) \<longrightarrow> (\<exists>A ST. Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set evs2)\<rbrakk> \<Longrightarrow> authK = shrK A \<and> servK = authKa \<and> B = Tgs \<and> Ts = Number (CT evs2) \<longrightarrow> (\<exists>Aa ST. Says Tgs Aa \<lbrace>Crypt (shrK A) \<lbrace>Key authKa, Agent Tgs, Number (CT evs2)\<rbrace>, ST\<rbrace> \<in> set evs2)
 3. \<And>evs4 servKa Ba authKa A' A Ta T2. \<lbrakk>authK \<notin> range shrK; evs4 \<in> kerbV; Key servKa \<notin> used evs4; servKa \<in> symKeys; Ba \<noteq> Tgs; authKa \<in> symKeys; Says A' Tgs \<lbrace>Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authKa, Number Ta\<rbrace>, Crypt authKa \<lbrace>Agent A, Number T2\<rbrace>, Agent Ba\<rbrace> \<in> set evs4; \<not> expiredA T2 evs4; servKlife + CT evs4 \<le> authKlife + Ta; Key authK \<notin> analz (knows Spy evs4); Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy evs4) \<longrightarrow> (\<exists>A ST. Says Tgs A \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set evs4)\<rbrakk> \<Longrightarrow> (authK = authKa \<and> servK = servKa \<and> B = Ba \<and> Ts = Number (CT evs4) \<longrightarrow> (\<exists>Aa ST. Aa = A \<and> ST = Crypt (shrK Ba) \<lbrace>Agent A, Agent Ba, Key servKa, Number (CT evs4)\<rbrace> \<or> Says Tgs Aa \<lbrace>Crypt authKa \<lbrace>Key servKa, Agent Ba, Number (CT evs4)\<rbrace>, ST\<rbrace> \<in> set evs4)) \<and> (Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace> \<in> parts (knows Spy evs4) \<longrightarrow> (\<exists>Aa ST. Aa = A \<and> authK = authKa \<and> servK = servKa \<and> B = Ba \<and> Ts = Number (CT evs4) \<and> ST = Crypt (shrK Ba) \<lbrace>Agent A, Agent Ba, Key servKa, Number (CT evs4)\<rbrace> \<or> Says Tgs Aa \<lbrace>Crypt authK \<lbrace>Key servK, Agent B, Ts\<rbrace>, ST\<rbrace> \<in> set evs4))
[PROOF STEP]
apply blast+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done