[STATEMENT]
lemma Inputs_A_Card_form_9: 

     "\<lbrakk> Inputs A (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk,   
                             Cert1, Cert2, Cert3\<rbrace> \<in> set evs; 
         evs \<in> srb \<rbrakk>  
  \<Longrightarrow>    Cert3 = Crypt (crdK (Card A)) (Nonce Na)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Inputs A (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk, Cert1, Cert2, Cert3\<rbrace> \<in> set evs; evs \<in> srb\<rbrakk> \<Longrightarrow> Cert3 = Crypt (crdK (Card A)) (Nonce Na)
[PROOF STEP]
apply (erule rev_mp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evs \<in> srb \<Longrightarrow> Inputs A (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk, Cert1, Cert2, Cert3\<rbrace> \<in> set evs \<longrightarrow> Cert3 = Crypt (crdK (Card A)) (Nonce Na)
[PROOF STEP]
apply (erule srb.induct)
[PROOF STATE]
proof (prove)
goal (20 subgoals):
 1. Inputs A (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk, Cert1, Cert2, Cert3\<rbrace> \<in> set [] \<longrightarrow> Cert3 = Crypt (crdK (Card A)) (Nonce Na)
 2. \<And>evsF X Ba Aa. \<lbrakk>evsF \<in> srb; Inputs A (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk, Cert1, Cert2, Cert3\<rbrace> \<in> set evsF \<longrightarrow> Cert3 = Crypt (crdK (Card A)) (Nonce Na); X \<in> synth (analz (knows Spy evsF)); illegalUse (Card Ba)\<rbrakk> \<Longrightarrow> Inputs A (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk, Cert1, Cert2, Cert3\<rbrace> \<in> set (Says Spy Aa X # Inputs Spy (Card Ba) X # evsF) \<longrightarrow> Cert3 = Crypt (crdK (Card A)) (Nonce Na)
 3. \<And>evsFo Nba Aa Ba. \<lbrakk>evsFo \<in> srb; Inputs A (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk, Cert1, Cert2, Cert3\<rbrace> \<in> set evsFo \<longrightarrow> Cert3 = Crypt (crdK (Card A)) (Nonce Na); Nonce Nba \<in> analz (knows Spy evsFo); Key (pairK (Aa, Ba)) \<in> knows Spy evsFo\<rbrakk> \<Longrightarrow> Inputs A (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk, Cert1, Cert2, Cert3\<rbrace> \<in> set (Notes Spy (Key (sesK (Nba, pairK (Aa, Ba)))) # evsFo) \<longrightarrow> Cert3 = Crypt (crdK (Card A)) (Nonce Na)
 4. \<And>evsrb Aa Ba X. \<lbrakk>evsrb \<in> srb; Inputs A (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk, Cert1, Cert2, Cert3\<rbrace> \<in> set evsrb \<longrightarrow> Cert3 = Crypt (crdK (Card A)) (Nonce Na); Says Aa Ba X \<in> set evsrb\<rbrakk> \<Longrightarrow> Inputs A (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk, Cert1, Cert2, Cert3\<rbrace> \<in> set (Gets Ba X # evsrb) \<longrightarrow> Cert3 = Crypt (crdK (Card A)) (Nonce Na)
 5. \<And>evs1 Aa Ba. \<lbrakk>evs1 \<in> srb; Inputs A (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk, Cert1, Cert2, Cert3\<rbrace> \<in> set evs1 \<longrightarrow> Cert3 = Crypt (crdK (Card A)) (Nonce Na); Aa \<noteq> Server\<rbrakk> \<Longrightarrow> Inputs A (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk, Cert1, Cert2, Cert3\<rbrace> \<in> set (Says Aa Server \<lbrace>Agent Aa, Agent Ba\<rbrace> # evs1) \<longrightarrow> Cert3 = Crypt (crdK (Card A)) (Nonce Na)
 6. \<And>evs2 Aa Ba. \<lbrakk>evs2 \<in> srb; Inputs A (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk, Cert1, Cert2, Cert3\<rbrace> \<in> set evs2 \<longrightarrow> Cert3 = Crypt (crdK (Card A)) (Nonce Na); Gets Server \<lbrace>Agent Aa, Agent Ba\<rbrace> \<in> set evs2\<rbrakk> \<Longrightarrow> Inputs A (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk, Cert1, Cert2, Cert3\<rbrace> \<in> set (Says Server Aa \<lbrace>Nonce (Pairkey (Aa, Ba)), Crypt (shrK Aa) \<lbrace>Nonce (Pairkey (Aa, Ba)), Agent Ba\<rbrace>\<rbrace> # evs2) \<longrightarrow> Cert3 = Crypt (crdK (Card A)) (Nonce Na)
 7. \<And>evs3 Aa Ba Pka Certificate. \<lbrakk>evs3 \<in> srb; Inputs A (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk, Cert1, Cert2, Cert3\<rbrace> \<in> set evs3 \<longrightarrow> Cert3 = Crypt (crdK (Card A)) (Nonce Na); legalUse Card Aa; Says Aa Server \<lbrace>Agent Aa, Agent Ba\<rbrace> \<in> set evs3; Gets Aa \<lbrace>Nonce Pka, Certificate\<rbrace> \<in> set evs3\<rbrakk> \<Longrightarrow> Inputs A (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk, Cert1, Cert2, Cert3\<rbrace> \<in> set (Inputs Aa (Card Aa) (Agent Aa) # evs3) \<longrightarrow> Cert3 = Crypt (crdK (Card A)) (Nonce Na)
 8. \<And>evs4 Naa Aa. \<lbrakk>evs4 \<in> srb; Inputs A (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk, Cert1, Cert2, Cert3\<rbrace> \<in> set evs4 \<longrightarrow> Cert3 = Crypt (crdK (Card A)) (Nonce Na); Nonce Naa \<notin> used evs4; legalUse Card Aa; Aa \<noteq> Server; Inputs Aa (Card Aa) (Agent Aa) \<in> set evs4\<rbrakk> \<Longrightarrow> Inputs A (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk, Cert1, Cert2, Cert3\<rbrace> \<in> set (Outpts (Card Aa) Aa \<lbrace>Nonce Naa, Crypt (crdK (Card Aa)) (Nonce Naa)\<rbrace> # evs4) \<longrightarrow> Cert3 = Crypt (crdK (Card A)) (Nonce Na)
 9. \<And>evs4F Naa Aa. \<lbrakk>evs4F \<in> srb; Inputs A (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk, Cert1, Cert2, Cert3\<rbrace> \<in> set evs4F \<longrightarrow> Cert3 = Crypt (crdK (Card A)) (Nonce Na); Nonce Naa \<notin> used evs4F; illegalUse (Card Aa); Inputs Spy (Card Aa) (Agent Aa) \<in> set evs4F\<rbrakk> \<Longrightarrow> Inputs A (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk, Cert1, Cert2, Cert3\<rbrace> \<in> set (Outpts (Card Aa) Spy \<lbrace>Nonce Naa, Crypt (crdK (Card Aa)) (Nonce Naa)\<rbrace> # evs4F) \<longrightarrow> Cert3 = Crypt (crdK (Card A)) (Nonce Na)
 10. \<And>evs5 Aa Naa Certificate Ba. \<lbrakk>evs5 \<in> srb; Inputs A (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk, Cert1, Cert2, Cert3\<rbrace> \<in> set evs5 \<longrightarrow> Cert3 = Crypt (crdK (Card A)) (Nonce Na); Outpts (Card Aa) Aa \<lbrace>Nonce Naa, Certificate\<rbrace> \<in> set evs5; \<forall>p q. Certificate \<noteq> \<lbrace>p, q\<rbrace>\<rbrakk> \<Longrightarrow> Inputs A (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk, Cert1, Cert2, Cert3\<rbrace> \<in> set (Says Aa Ba \<lbrace>Agent Aa, Nonce Naa\<rbrace> # evs5) \<longrightarrow> Cert3 = Crypt (crdK (Card A)) (Nonce Na)
A total of 20 subgoals...
[PROOF STEP]
apply (simp_all (no_asm_simp))
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>evsF X Ba. \<lbrakk>evsF \<in> srb; Inputs A (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk, Cert1, Cert2, Cert3\<rbrace> \<in> set evsF \<longrightarrow> Cert3 = Crypt (crdK (Card A)) (Nonce Na); X \<in> synth (analz (knows Spy evsF)); illegalUse (Card Ba)\<rbrakk> \<Longrightarrow> A = Spy \<and> A = Ba \<and> \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk, Cert1, Cert2, Cert3\<rbrace> = X \<longrightarrow> Cert3 = Crypt (crdK (Card Spy)) (Nonce Na)
 2. \<And>evs9 Aa Pka Cert1a Naa Cert2a Nba Cert3a Ba. \<lbrakk>evs9 \<in> srb; Inputs A (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk, Cert1, Cert2, Cert3\<rbrace> \<in> set evs9 \<longrightarrow> Cert3 = Crypt (crdK (Card A)) (Nonce Na); legalUse Card Aa; Gets Aa \<lbrace>Nonce Pka, Cert1a\<rbrace> \<in> set evs9; Outpts (Card Aa) Aa \<lbrace>Nonce Naa, Cert2a\<rbrace> \<in> set evs9; Gets Aa \<lbrace>Nonce Nba, Cert3a\<rbrace> \<in> set evs9; \<forall>p q. Cert2a \<noteq> \<lbrace>p, q\<rbrace>\<rbrakk> \<Longrightarrow> A = Aa \<and> B = Ba \<and> Na = Naa \<and> Nb = Nba \<and> Pk = Pka \<and> Cert1 = Cert1a \<and> Cert2 = Cert3a \<and> Cert3 = Cert2a \<longrightarrow> Cert2a = Crypt (crdK (Card Aa)) (Nonce Naa)
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>evs9 Aa Pka Cert1a Naa Cert2a Nba Cert3a Ba. \<lbrakk>evs9 \<in> srb; Inputs A (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk, Cert1, Cert2, Cert3\<rbrace> \<in> set evs9 \<longrightarrow> Cert3 = Crypt (crdK (Card A)) (Nonce Na); legalUse Card Aa; Gets Aa \<lbrace>Nonce Pka, Cert1a\<rbrace> \<in> set evs9; Outpts (Card Aa) Aa \<lbrace>Nonce Naa, Cert2a\<rbrace> \<in> set evs9; Gets Aa \<lbrace>Nonce Nba, Cert3a\<rbrace> \<in> set evs9; \<forall>p q. Cert2a \<noteq> \<lbrace>p, q\<rbrace>\<rbrakk> \<Longrightarrow> A = Aa \<and> B = Ba \<and> Na = Naa \<and> Nb = Nba \<and> Pk = Pka \<and> Cert1 = Cert1a \<and> Cert2 = Cert3a \<and> Cert3 = Cert2a \<longrightarrow> Cert2a = Crypt (crdK (Card Aa)) (Nonce Naa)
[PROOF STEP]
apply (blast dest!: Outpts_A_Card_form_4)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done