[STATEMENT]
lemma NC2_not_NonceCCA:
     "[|Hash \<lbrace>Agent C', Nonce N', Agent C, Nonce N\<rbrace>
          \<in> parts (knows Spy evs);
        Nonce N \<notin> analz (knows Spy evs);
       evs \<in> set_cr|]
      ==> Crypt KC1 \<lbrace>\<lbrace>Agent B, Nonce N\<rbrace>, Hash p\<rbrace> \<notin> parts (knows Spy evs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Hash \<lbrace>Agent C', Nonce N', Agent C, Nonce N\<rbrace> \<in> parts (knows Spy evs); Nonce N \<notin> analz (knows Spy evs); evs \<in> set_cr\<rbrakk> \<Longrightarrow> Crypt KC1 \<lbrace>\<lbrace>Agent B, Nonce N\<rbrace>, Hash p\<rbrace> \<notin> parts (knows Spy evs)
[PROOF STEP]
apply (erule rev_mp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Nonce N \<notin> analz (knows Spy evs); evs \<in> set_cr\<rbrakk> \<Longrightarrow> Hash \<lbrace>Agent C', Nonce N', Agent C, Nonce N\<rbrace> \<in> parts (knows Spy evs) \<longrightarrow> Crypt KC1 \<lbrace>\<lbrace>Agent B, Nonce N\<rbrace>, Hash p\<rbrace> \<notin> parts (knows Spy evs)
[PROOF STEP]
apply (erule rev_mp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evs \<in> set_cr \<Longrightarrow> Nonce N \<notin> analz (knows Spy evs) \<longrightarrow> Hash \<lbrace>Agent C', Nonce N', Agent C, Nonce N\<rbrace> \<in> parts (knows Spy evs) \<longrightarrow> Crypt KC1 \<lbrace>\<lbrace>Agent B, Nonce N\<rbrace>, Hash p\<rbrace> \<notin> parts (knows Spy evs)
[PROOF STEP]
apply (erule set_cr.induct, analz_mono_contra, simp_all)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>evsf X. \<lbrakk>evsf \<in> set_cr; X \<in> synth (analz (knows Spy evsf)); Nonce N \<notin> analz (knows Spy evsf); Hash \<lbrace>Agent C', Nonce N', Agent C, Nonce N\<rbrace> \<in> parts (knows Spy evsf) \<longrightarrow> Crypt KC1 \<lbrace>\<lbrace>Agent B, Nonce N\<rbrace>, Hash p\<rbrace> \<notin> parts (knows Spy evsf)\<rbrakk> \<Longrightarrow> Hash \<lbrace>Agent C', Nonce N', Agent C, Nonce N\<rbrace> \<in> parts (insert X (knows Spy evsf)) \<longrightarrow> Crypt KC1 \<lbrace>\<lbrace>Agent B, Nonce N\<rbrace>, Hash p\<rbrace> \<notin> parts (insert X (knows Spy evsf))
 2. \<And>evs3 Ca k NC2 KC1a SKi X NC1 i EKi. \<lbrakk>evs3 \<in> set_cr; Ca = Cardholder k; Nonce NC2 \<notin> used evs3; Key KC1a \<notin> used evs3; KC1a \<in> symKeys; Gets (Cardholder k) \<lbrace>sign (invKey SKi) \<lbrace>Agent X, Nonce NC1\<rbrace>, cert (CA i) EKi onlyEnc (priSK RCA), cert (CA i) SKi onlySig (priSK RCA)\<rbrace> \<in> set evs3; Says (Cardholder k) (CA i) \<lbrace>Agent (Cardholder k), Nonce NC1\<rbrace> \<in> set evs3; Nonce N \<notin> analz (knows Spy evs3); Hash \<lbrace>Agent C', Nonce N', Agent C, Nonce N\<rbrace> \<in> parts (knows Spy evs3) \<longrightarrow> Crypt KC1 \<lbrace>\<lbrace>Agent B, Nonce N\<rbrace>, Hash p\<rbrace> \<notin> parts (knows Spy evs3)\<rbrakk> \<Longrightarrow> Hash \<lbrace>Agent C', Nonce N', Agent C, Nonce N\<rbrace> \<in> parts (knows Spy evs3) \<longrightarrow> N = NC2 \<longrightarrow> B = Cardholder k \<longrightarrow> KC1 = KC1a \<longrightarrow> p \<noteq> Pan (pan (Cardholder k))
 3. \<And>evs6 NonceCCA KC2 KC3 cardSK i Ca NC3 CardSecret. \<lbrakk>evs6 \<in> set_cr; Nonce NonceCCA \<notin> used evs6; KC2 \<in> symKeys; KC3 \<in> symKeys; cardSK \<notin> symKeys; Notes (CA i) (Key cardSK) \<notin> set evs6; Gets (CA i) \<lbrace>Crypt KC3 \<lbrace>Agent Ca, Nonce NC3, Key KC2, Key cardSK, Crypt (invKey cardSK) (Hash \<lbrace>Agent Ca, Nonce NC3, Key KC2, Key cardSK, Pan (pan Ca), Nonce CardSecret\<rbrace>)\<rbrace>, Crypt (pubEK (CA i)) \<lbrace>Key KC3, Pan (pan Ca), Nonce CardSecret\<rbrace>\<rbrace> \<in> set evs6; Nonce N \<notin> analz (knows Spy evs6); Hash \<lbrace>Agent C', Nonce N', Agent C, Nonce N\<rbrace> \<in> parts (knows Spy evs6) \<longrightarrow> Crypt KC1 \<lbrace>\<lbrace>Agent B, Nonce N\<rbrace>, Hash p\<rbrace> \<notin> parts (knows Spy evs6)\<rbrakk> \<Longrightarrow> C' = Ca \<and> N' = NC3 \<and> C = CA i \<and> N = NonceCCA \<longrightarrow> Crypt KC1 \<lbrace>\<lbrace>Agent B, Nonce NonceCCA\<rbrace>, Hash p\<rbrace> \<notin> parts (knows Spy evs6)
[PROOF STEP]
apply (blast dest: Hash_imp_parts2)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done