import InductiveVerification.Public
set_option diagnostics true

-- The Needham-Schroeder Public-Key Protocol
namespace NS_Public

variable [InvKey]
variable [Bad]
open Msg
open Event
open Bad
open HasInitState
open InvKey

-- Define the inductive set `ns_public`
inductive ns_public : List Event → Prop
| Nil : ns_public []
| Fake : ns_public evsf →
    X ∈ synth (analz (spies evsf)) →
    ns_public (Says Agent.Spy B X :: evsf)
| NS1 : ns_public evs1 →
    Nonce NA ∉ used evs1 →
    ns_public (Says A B (Crypt (pubEK B) ⦃Nonce NA, Agent A⦄) :: evs1)
| NS2 : ns_public evs2 →
    Nonce NB ∉ used evs2 →
    Says A' B (Crypt (pubEK B) ⦃Nonce NA, Agent A⦄) ∈ evs2 →
    ns_public (Says B A (Crypt (pubEK A) ⦃Nonce NA, Nonce NB, Agent B⦄) :: evs2)
| NS3 : ns_public evs3 →
    Says A B (Crypt (pubEK B) ⦃Nonce NA, Agent A⦄) ∈ evs3 →
    Says B' A (Crypt (pubEK A) ⦃Nonce NA, Nonce NB, Agent B⦄) ∈ evs3 →
    ns_public (Says A B (Crypt (pubEK B) (Nonce NB)) :: evs3)

-- A "possibility property": there are traces that reach the end
theorem possibility_property :
  ∃ NB, ∃ evs, ns_public evs ∧ Says A B (Crypt (pubEK B) (Nonce NB)) ∈ evs := by
  exists 1
  exists [ Says A B (Crypt (pubEK B) (Nonce 1)),
           Says B A (Crypt (pubEK A) ⦃Nonce 0, Nonce 1, Agent B⦄),
           Says A B (Crypt (pubEK B) ⦃Nonce 0, Agent A⦄),
         ]
  constructor
  · apply ns_public.NS3
    · apply ns_public.NS2
      · apply_rules [ns_public.NS1, ns_public.Nil, Nonce_notin_used_empty]
      · simp
      · left
    all_goals tauto
  · simp

-- Spy never sees another agent's private key unless it's bad at the start
set_option trace.aesop true
@[simp]
theorem Spy_see_priEK {h : ns_public evs} :
  (Key (priEK A) ∈ parts (spies evs)) ↔ A ∈ bad := by
  constructor
  -- · induction h <;> aesop (add norm spies, norm knows, norm initState, norm pubEK, norm priEK, norm pubSK, norm priSK, norm injective_publicKey)
  · induction h with
    | Nil => simp[spies, knows, initState]; intro h; cases h with
             | inl h => cases h with
               | inl => aesop (add norm pubEK, norm pubSK, safe forward injective_publicKey)
               | inr h => simp[pubEK, priEK] at h; cases h with
                | intro _ h => apply publicKey_neq_privateKey at h; contradiction
             | inr h => simp[pubSK, priEK] at h; cases h with
               | intro _ h => apply publicKey_neq_privateKey at h; contradiction
    | Fake _ h ih => apply Fake_parts_sing at h
                     simp[spies, knows]
                     intro h₁; apply ih;
                     cases h₁ with
                      | inl h₁ => apply h at h₁; cases h₁ with 
                        | inl h₁ => cases h₁; aapply analz_subset_parts
                        | inr => assumption
                      | inr => assumption
    | NS1 _ _ ih => aesop (add norm spies, norm knows)
    | NS2 _ _ _ ih => aesop (add norm spies, norm knows)
    | NS3 _ _ _ ih => rw[spies, knows]; simp; intro _; apply ih; grind
  · intro h₁; apply parts_increasing; aapply Spy_spies_bad_privateKey

@[simp]
theorem Spy_analz_priEK {h : ns_public evs} :
  Key (priEK A) ∈ analz (spies evs) ↔ A ∈ bad := by
  constructor
  · intro h₁; apply analz_subset_parts at h₁; aapply Spy_see_priEK.mp
  · intro h₁; apply analz_increasing; aapply Spy_spies_bad_privateKey

-- Lammata for some very specific recurring cases in the following proof
lemma no_nonce_NS1_NS2_helper1
{h : synth (analz (spies evsf)) ⦃Nonce NA, Msg.Agent A⦄}
: Nonce NA ∈ analz (knows Agent.Spy evsf) := by
  cases h with
  | inj => aapply analz.fst
  | mpair n => cases n; assumption

lemma no_nonce_NS1_NS2_helper2
{ih : Crypt (pubEK C) ⦃NA', ⦃Nonce NA, Msg.Agent D⦄⦄ ∈ parts (spies evsf)
  → Crypt (pubEK B) ⦃Nonce NA, Msg.Agent A⦄ ∈ parts (spies evsf)
  → Nonce NA ∈ analz (spies evsf)}
{h : parts {X} ⊆ synth (analz (spies evsf)) ∪ parts (spies evsf)}
{h₁ : Crypt (pubEK C) ⦃NA', ⦃Nonce NA, Msg.Agent D⦄⦄ ∈ parts (knows Agent.Spy evsf)}
{h₂ : Crypt (pubEK B) ⦃Nonce NA, Msg.Agent A⦄ ∈ parts {X} ∨
      Crypt (pubEK B) ⦃Nonce NA, Msg.Agent A⦄ ∈ parts (knows Agent.Spy evsf)}
: Nonce NA ∈ analz (knows Agent.Spy evsf) := by
  apply ih at h₁; cases h₂ with
  | inl h₂ => apply h at h₂; cases h₂ with
    | inl h₂ => cases h₂ with
      | inj => apply h₁; aapply analz_subset_parts
      | crypt h₂ => aapply no_nonce_NS1_NS2_helper1
    | inr => aapply h₁
  | inr => aapply h₁

-- It is impossible to re-use a nonce in both NS1 and NS2, provided the nonce is secret
theorem no_nonce_NS1_NS2 { evs: List Event} { h : ns_public evs  } {A B C D : Agent} :
  (Crypt (pubEK C) ⦃NA', Nonce NA, Agent D⦄ ∈ parts (spies evs) →
  (Crypt (pubEK B) ⦃Nonce NA, Agent A⦄ ∈ parts (spies evs) →
  Nonce NA ∈ analz (spies evs))) := by
  intro h₁ h₂
  induction h with
  | Nil => rw[spies, knows] at h₂; simp[initState] at h₂
  | Fake _ h ih => 
      apply Fake_parts_sing at h
      simp[spies, knows] at h₁
      apply analz_insert; right;
      cases h₁ with 
      | inl h₁ => simp_all; apply h at h₁; cases h₁ with
        | inl h₁ => cases h₁ with
          | inj h₁ => apply analz_subset_parts at h₁
                      aapply no_nonce_NS1_NS2_helper2
          | crypt h₁ => cases h₁ with
            | inj => apply analz.fst; aapply analz.snd
            | mpair _ h₁ => aapply no_nonce_NS1_NS2_helper1
        | inr h₁ => aapply no_nonce_NS1_NS2_helper2
      | inr h₁ => simp[spies, knows] at h₂; aapply no_nonce_NS1_NS2_helper2
  | NS1 =>
    simp[spies] at h₁; simp[spies] at h₂; cases h₂ with
    | inl h => rcases h with ⟨_ , ⟨n , _⟩⟩;
               apply parts.body at h₁; apply parts.snd at h₁; apply parts.fst at h₁
               apply parts_knows_Spy_subset_used at h₁; rw[n] at h₁; contradiction
    | inr => rw[spies, knows]; apply analz_mono; apply Set.subset_insert; simp_all
  | NS2 =>
    simp[spies] at h₁; simp[spies] at h₂; cases h₁ with
    | inl h => rcases h with ⟨_, ⟨_, ⟨n, _⟩⟩⟩
               apply parts.body at h₂; apply parts.fst at h₂
               apply parts_knows_Spy_subset_used at h₂; rw[n] at h₂; contradiction
    | inr => rw[spies, knows]; apply analz_mono; apply Set.subset_insert; simp_all
  | NS3 => rw[spies, knows]; apply analz_mono; apply Set.subset_insert; simp_all

lemma unique_Nonce_apply_ih {P : Prop}
{h₃ : Nonce NA ∉ analz (spies (Says Agent.Spy C X :: evsf))}
{h₁ : M₁ ∈ parts (spies evsf)}
{h₂ : M₂ ∈ parts (spies evsf)}
{a_ih : M₁ ∈ parts (spies evsf)
  → M₂ ∈ parts (spies evsf)
  → Nonce NA ∉ analz (spies evsf) → P}
: P := by
  simp[spies, knows] at h₃; apply Set.notMem_subset at h₃
  · aapply a_ih;
  · apply analz_mono; apply Set.subset_insert    

lemma unique_NA_apply_ih {P : Prop}
{a_ih : Crypt (pubEK B) ⦃Nonce NA, Msg.Agent A⦄ ∈ parts (spies evsf)
  → Crypt (pubEK B') ⦃Nonce NA, Msg.Agent A'⦄ ∈ parts (spies evsf)
  → Nonce NA ∉ analz (spies evsf) → P}
{h₃ : Nonce NA ∉ analz (spies (Says Agent.Spy C X :: evsf))}
{h₁ : Crypt (pubEK B) ⦃Nonce NA, Msg.Agent A⦄ ∈ parts (spies evsf)}
{h₂ : Crypt (pubEK B') ⦃Nonce NA, Msg.Agent A'⦄ ∈ parts (spies evsf)}
: P := by
  aapply unique_Nonce_apply_ih (h₁ := h₁) (h₂ := h₂)

lemma unique_NA_contradict
{h₃ : Nonce NA ∉ analz (spies (Says Agent.Spy B X :: evsf))}
{h₂ : synth (analz (spies evsf)) ⦃Nonce NA, Msg.Agent A'⦄}
{P : Prop}
: P := by
  apply MPair_synth_analz.mp at h₂; rcases h₂ with ⟨⟨n⟩, m⟩;
  simp[spies, knows] at h₃; apply Set.notMem_subset at h₃
  · contradiction;
  · apply analz_mono; apply Set.subset_insert 

-- Unicity for NS1: nonce NA identifies agents A and B
theorem unique_NA { h : ns_public evs } :
  (Crypt (pubEK B) ⦃Nonce NA, Agent A⦄ ∈ parts (spies evs) →
  (Crypt (pubEK B') ⦃Nonce NA, Agent A'⦄ ∈ parts (spies evs) →
  (Nonce NA ∉ analz (spies evs) →
  A = A' ∧ B = B'))) := by
  induction h with
  | Nil => aesop (add norm spies, norm knows, safe analz_insertI)
  | Fake _ a a_ih =>
    apply Fake_parts_sing at a; intro h₁ h₂ h₃;
    simp[spies, knows] at h₁; cases h₁ with
    | inl h₁ => apply a at h₁; cases h₁ with
      | inl h₁ => cases h₁ with
        | inj h₁ => simp[spies, knows] at h₂; cases h₂ with
          | inl h₂ => apply a at h₂; cases h₂ with
            | inl h₂ => cases h₂ with
              | inj h₂ => apply analz_subset_parts at h₁
                          apply analz_subset_parts at h₂
                          aapply unique_NA_apply_ih   
              | crypt h₂ => aapply unique_NA_contradict
            | inr h₂ => apply analz_subset_parts at h₁
                        aapply unique_NA_apply_ih
          | inr h₂ => apply analz_subset_parts at h₁
                      aapply unique_NA_apply_ih
        | crypt h₁ => aapply unique_NA_contradict
      | inr h₁ => simp[spies] at h₁; simp[spies, knows] at h₂; cases h₂ with
        | inl h₂ => apply a at h₂; cases h₂ with
          | inl h₂ => cases h₂ with
            | inj h₂ => apply analz_subset_parts at h₂
                        aapply unique_NA_apply_ih
            | crypt => aapply unique_NA_contradict
          | inr => aapply unique_NA_apply_ih
        | inr => aapply unique_NA_apply_ih
    | inr => simp[spies, knows] at h₂; cases h₂ with
      | inl h₂ => apply a at h₂; cases h₂ with
        | inl h₂ => cases h₂ with
          | inj h₂ => apply analz_subset_parts at h₂
                      aapply unique_NA_apply_ih
          | crypt => aapply unique_NA_contradict
        | inr => aapply unique_NA_apply_ih
      | inr => aapply unique_NA_apply_ih
  | NS1 _ _ a_ih => intro h₁ h₂ h₃; simp at h₁; cases h₁ with
    | inl h₁ => simp at h₂; cases h₂ with
      | inl h₂ => rcases h₁ with ⟨h₁, _⟩; rcases h₂ with ⟨h₂, _⟩;
                  apply injective_publicKey at h₁;
                  apply injective_publicKey at h₂;
                  simp_all;
      | inr h₂ => apply parts.body at h₂; apply parts.fst at h₂; 
                  apply parts_knows_Spy_subset_used at h₂; simp_all;
    | inr h₁ => simp at h₂; cases h₂ with
      | inl h₂ => apply parts.body at h₁; apply parts.fst at h₁;
                  apply parts_knows_Spy_subset_used at h₁; simp_all;
      | inr => aapply unique_NA_apply_ih;
  | NS2 _ _ _ a_ih => intro h₁ h₂ h₃; simp_all; apply a_ih
                      apply Set.notMem_subset at h₃
                      · apply h₃;
                      · apply_rules [analz_mono, Set.subset_insert]
  | NS3 _ _ _ a_ih => intro h₁ h₂ h₃; simp_all; apply a_ih; 
                      apply Set.notMem_subset at h₃
                      · apply h₃;
                      · apply_rules [analz_mono, Set.subset_insert]

-- Spy does not see the nonce sent in NS1 if A and B are secure
theorem Spy_not_see_NA { h : ns_public evs  }
  { not_bad_A : A ∉ bad }
  { not_bad_B : B ∉ bad } :
  Says A B (Crypt (pubEK B) ⦃Nonce NA, Agent A⦄) ∈ evs →
  Nonce NA ∉ analz (spies evs) := by
  intro h₁ h₄
  induction h with
  | Nil => simp_all
  | Fake _ a a_ih => 
    apply Fake_analz_insert at a; apply a at h₄; simp_all; cases h₁ with
    | inl h => rcases h with ⟨l, _⟩; simp_all [Spy_in_bad];
    | inr h => cases h₄ with
      | inl h₄ => cases h₄; apply a_ih at h; contradiction;
      | inr => apply a_ih at h; contradiction;
  | NS1 _ a a_ih => simp_all; cases h₁ with
    | inl h => rcases h with ⟨_, ⟨_, ⟨_, ⟨h, _⟩⟩⟩⟩; simp_all; apply a
               apply parts_knows_Spy_subset_used
               aapply analz_subset_parts
    | inr h => apply analz_insert_Crypt_subset at h₄; cases h₄ with
      | inl h₄ => contradiction; 
      | inr h₄ => simp at h₄; cases h₄
                  · simp_all; apply a; apply Says_imp_used at h;
                    apply used_parts_subset_parts at h; simp at h; apply h;
                    tauto;
                  · simp_all;
  | NS2 _ not_used_NB a a_ih =>
    cases h₁ with | tail _ b =>
      have _ := h₄
      simp at h₄; apply analz_insert_Crypt_subset at h₄
      simp at h₄; rcases h₄ with ( h | ( h | h ))
      · simp at a_ih; have c := b; apply a_ih at c; rw[h] at b;
        have _ := c; rw[h] at c;
        apply Says_imp_parts_knows_Spy at b
        apply Says_imp_parts_knows_Spy at a
        apply unique_NA at b; apply b at a; apply a at c; simp_all
        assumption
      · rw [h] at b
        apply not_used_NB; apply parts_knows_Spy_subset_used; apply parts.fst;
        apply parts.body; apply Says_imp_parts_knows_Spy; assumption
      · aapply a_ih
  | NS3 _ a₁ a₂ a_ih => 
    cases h₁ with | tail _ b =>
      have _ := h₄
      simp at h₄; apply analz_insert_Crypt_subset at h₄
      simp at h₄; rcases h₄ with ( h | ( h | h ))
      · have c := b; have d := a₁; have e := a₂
        rw[h] at b; apply Says_imp_parts_knows_Spy at b
        apply Says_imp_parts_knows_Spy at a₂
        aapply a_ih; apply no_nonce_NS1_NS2
        · assumption
        · rw[h]; exact a₂
        · rw[h]; exact b
      · aapply a_ih; aapply analz.inj
      · aapply a_ih; aapply analz.fst
      · aapply a_ih; aapply analz.snd
      · aapply a_ih; aapply analz.decrypt
      
-- Authentication for `A`: if she receives message 2 and has used `NA` to start a run, then `B` has sent message 2.
theorem A_trusts_NS2 {h : ns_public evs }
  { not_bad_A : A ∉ bad }
  { not_bad_B : B ∉ bad } :
  Says A B (Crypt (pubEK B) ⦃Nonce NA, Agent A⦄) ∈ evs →
  Says B' A (Crypt (pubEK B) ⦃Nonce NA, Nonce NB, Agent B⦄) ∈ evs →
  Says B A (Crypt (pubEK B) ⦃Nonce NA, Nonce NB, Agent B⦄) ∈ evs
:= by
   intro h₁ h₂;
   -- have snsNA := h₁; apply Spy_not_see_NA at snsNA <;> try assumption
   apply Says_imp_parts_knows_Spy at h₂
   -- use unique_NA to show that B' = B
   induction h with
  | Nil => simp_all
  | Fake _ a a_ih => 
    have snsNA := h₁; apply Spy_not_see_NA at snsNA <;> try assumption
    cases h₁
    · have _ := Spy_in_bad; contradiction
    · right; simp at h₂; cases h₂ with
    | inl h₂ => apply Fake_parts_sing at a; apply a at h₂; cases h₂ with
      | inl h₂ => aapply a_ih; cases h₂ with
        | inj => aapply analz_subset_parts
        | crypt h => apply False.elim; apply snsNA
                     apply MPair_synth_analz.mp at h; rcases h with ⟨⟨l⟩ , _⟩; 
                     aapply analz_spies_mono
      | inr h₂ => aapply a_ih;
    | inr => aapply a_ih;
    · aapply ns_public.Fake
  | NS1 _ a a_ih => right; simp at h₂; cases h₁
                    · apply False.elim; apply a
                      apply parts_knows_Spy_subset_used; apply parts.fst
                      aapply parts.body
                    · aapply a_ih; 
  | NS2 _ _ a a_ih => simp at h₁; have b := h₁; have snsNA := h₁
                      apply Spy_not_see_NA at snsNA <;> try assumption
                      simp at h₂; cases h₂ with
      | inl h => apply Says_imp_parts_knows_Spy at a
                 apply Says_imp_parts_knows_Spy at b
                 rcases h with ⟨e₁ , ⟨e₂ , ⟨e₃, e₄⟩⟩⟩
                 apply unique_NA at a
                 rw[e₂] at b; rw[e₂] at snsNA
                 apply a at b
                 apply b at snsNA
                 simp_all[-e₄]; assumption
      | inr => right; aapply a_ih
  | NS3 _ _ a a_ih => simp at h₁; simp at h₂; right; aapply a_ih
  
-- If the encrypted message appears then it originated with Alice in `NS1`
lemma B_trusts_NS1 { h : ns_public evs} :
  Crypt (pubEK B) ⦃Nonce NA, Agent A⦄ ∈ parts (spies evs) →
  Nonce NA ∉ analz (spies evs) →
  Says A B (Crypt (pubEK B) ⦃Nonce NA, Agent A⦄) ∈ evs
:= by
  intro h₁ h₂
  induction h with
  | Nil => simp[spies] at h₁; rw[knows] at h₁; simp[initState] at h₁
  | Fake _ a a_ih => simp at h₁; cases h₁ with
    | inl h₁ => apply Fake_parts_sing at a; apply a at h₁; cases h₁ with
      | inl h₁ => cases h₁ with
        | inj h₁ => right; apply analz_subset_parts at h₁; aapply a_ih
                    aapply analz_spies_mono_neg
        | crypt h₁ => apply False.elim;
                      apply MPair_synth_analz.mp at h₁
                      rcases h₁ with ⟨⟨h₁⟩, _⟩; aapply analz_spies_mono_neg
      | inr => right; aapply a_ih; aapply analz_spies_mono_neg
    | inr h₁ => right; aapply a_ih; aapply analz_spies_mono_neg
  | NS1 _ _ a_ih => simp at h₁; cases h₁ with
    | inl h₁ => rcases h₁ with ⟨e₁, ⟨e₂, e₃⟩⟩; apply injective_publicKey at e₁
                simp_all
    | inr => right; aapply a_ih; aapply analz_spies_mono_neg
  | NS2 _ _ _ a_ih => simp at h₁; right; aapply a_ih; aapply analz_spies_mono_neg
  | NS3 _ _ _ a_ih => simp at h₁; right; aapply a_ih; aapply analz_spies_mono_neg
  
-- Authenticity Properties obtained from `NS2`

-- Helper lemmas for unique_NB
lemma unique_NB_apply_ih {P : Prop}
{ a_ih :
  Crypt (pubEK A) ⦃Nonce NA, ⦃Nonce NB, Msg.Agent B⦄⦄ ∈ parts (spies evsf) →
    Crypt (pubEK A') ⦃Nonce NA', ⦃Nonce NB, Msg.Agent B'⦄⦄ ∈ parts (spies evsf) →
      Nonce NB ∉ analz (spies evsf) → P }
{ h₁ : Crypt (pubEK A) ⦃Nonce NA, ⦃Nonce NB, Msg.Agent B⦄⦄ ∈ parts (spies evsf) }
{ h₂ : Crypt (pubEK A') ⦃Nonce NA', ⦃Nonce NB, Msg.Agent B'⦄⦄ ∈ parts (spies evsf) }
{ h₃ : Nonce NB ∉ analz (spies (Says Agent.Spy B X :: evsf)) }
: P := by
  aapply unique_Nonce_apply_ih (h₁ := h₁) (h₂ := h₂) (h₃ := h₃)

lemma unique_NB_contradict
{ h₃ : Nonce NB ∉ analz (spies (Says Agent.Spy B X :: evsf)) }
{ h₂ : synth (analz (spies evsf)) ⦃Nonce NA', ⦃Nonce NB, Msg.Agent B'⦄⦄ }
{P : Prop}
: P := by
  apply MPair_synth_analz.mp at h₂; apply False.elim
  rcases h₂ with ⟨_, r⟩; cases r with
    | inj r => aapply analz_spies_mono_neg; aapply analz.fst
    | mpair r₁ _ => cases r₁; aapply analz_spies_mono_neg

-- Unicity for `NS2`: nonce `NB` identifies nonce `NA` and agent `A`
theorem unique_NB { h : ns_public evs } :
  (Crypt (pubEK A) ⦃Nonce NA, Nonce NB, Agent B⦄ ∈ parts (spies evs) →
  (Crypt (pubEK A') ⦃Nonce NA', Nonce NB, Agent B'⦄ ∈ parts (spies evs) →
  (Nonce NB ∉ analz (spies evs) →
  A = A' ∧ NA = NA' ∧ B = B'))) := by
  -- Proof closely follows that of unique_NA
  induction h with
  | Nil => aesop (add norm spies, norm knows, safe analz_insertI)
  | Fake _ a a_ih =>
    apply Fake_parts_sing at a; intro h₁ h₂ h₃;
    simp[spies, knows] at h₁; cases h₁ with
    | inl h₁ => apply a at h₁; cases h₁ with
      | inl h₁ => cases h₁ with
        | inj h₁ => simp[spies, knows] at h₂; cases h₂ with
          | inl h₂ => apply a at h₂; cases h₂ with
            | inl h₂ => cases h₂ with
              | inj h₂ => apply analz_subset_parts at h₁
                          apply analz_subset_parts at h₂
                          aapply unique_NB_apply_ih
              | crypt h₂ => aapply unique_NB_contradict
            | inr h₂ => apply analz_subset_parts at h₁
                        aapply unique_NB_apply_ih
          | inr h₂ => apply analz_subset_parts at h₁
                      aapply unique_NB_apply_ih
        | crypt h₁ => aapply unique_NB_contradict
      | inr h₁ => simp[spies] at h₁; simp[spies, knows] at h₂; cases h₂ with
        | inl h₂ => apply a at h₂; cases h₂ with
          | inl h₂ => cases h₂ with
            | inj h₂ => apply analz_subset_parts at h₂
                        aapply unique_NB_apply_ih
            | crypt => aapply unique_NB_contradict
          | inr => aapply unique_NB_apply_ih
        | inr => aapply unique_NB_apply_ih
    | inr => simp[spies, knows] at h₂; cases h₂ with
      | inl h₂ => apply a at h₂; cases h₂ with
        | inl h₂ => cases h₂ with
          | inj h₂ => apply analz_subset_parts at h₂
                      aapply unique_NB_apply_ih
          | crypt => aapply unique_NB_contradict
        | inr => aapply unique_NB_apply_ih
      | inr => aapply unique_NB_apply_ih
  | NS1 _ _ a_ih => intro h₁ h₂ h₃; simp at h₁; simp at h₂; aapply a_ih
                    aapply analz_spies_mono_neg
  | NS2 _ _ _ a_ih => intro h₁ h₂ h₃; simp at h₁; simp at h₂; cases h₁ with
    | inl h₁ => rcases h₁ with ⟨e₁, _⟩; apply injective_publicKey at e₁
                cases h₂ with
      | inl h₂ => rcases h₂ with ⟨e₂, _⟩; apply injective_publicKey at e₂
                  simp_all
      | inr h₂ => apply parts.body at h₂; apply parts.snd at h₂
                  apply parts.fst at h₂; apply parts_knows_Spy_subset_used at h₂;
                  simp_all;
    | inr h₁ => cases h₂ with
      | inl h₂ => apply parts.body at h₁; apply parts.snd at h₁
                  apply parts.fst at h₁; apply parts_knows_Spy_subset_used at h₁;
                  simp_all
      | inr => aapply a_ih; aapply analz_spies_mono_neg
  | NS3 _ _ _ a_ih => intro h₁ h₂ h₃; simp_all; apply a_ih; 
                      apply Set.notMem_subset at h₃
                      · apply h₃;
                      · apply_rules [analz_mono, Set.subset_insert]

-- `NB` remains secret 
theorem Spy_not_see_NB { h : ns_public evs }
  { not_bad_A : A ∉ bad }
  { not_bad_B : B ∉ bad } :
  Says B A (Crypt (pubEK A) ⦃Nonce NA, Nonce NB, Agent B⦄) ∈ evs →
  Nonce NB ∉ analz (spies evs)
:= by
  intro h₁ h₄
  induction h with
  | Nil => simp_all
  | Fake _ a a_ih => 
    apply Fake_analz_insert at a; apply a at h₄; simp_all; cases h₁ with
    | inl h => rcases h with ⟨l, _⟩; simp_all [Spy_in_bad];
    | inr h => cases h₄ with
      | inl h₄ => cases h₄; apply a_ih at h; contradiction;
      | inr => apply a_ih at h; contradiction;
  | NS1 _ a a_ih => simp at h₁; simp[spies, knows] at h₄
                    apply analz_insert_Crypt_subset at h₄; simp at h₄
                    cases h₄ with
    | inl e => rw[e] at h₁; apply a; apply parts_knows_Spy_subset_used
               apply parts.fst; apply parts.snd; apply parts.body
               aapply Says_imp_parts_knows_Spy
    | inr => aapply a_ih
  | NS2 _ not_used_NB a a_ih => simp at h₁; simp[spies, knows] at h₄; 
                                cases h₁ with
    | inl h => rcases h with ⟨_, ⟨_, ⟨e₃, _⟩⟩⟩; apply injective_publicKey at e₃;
               simp_all; apply not_used_NB; apply parts_knows_Spy_subset_used;
               aapply analz_subset_parts
    | inr h => apply analz_insert_Crypt_subset at h₄; simp at h₄; cases h₄ with
      | inl e => aapply a_ih; rw[e]; apply Says_imp_parts_knows_Spy at a
                 apply Says_imp_parts_knows_Spy at h; rw[e] at h
                 aapply no_nonce_NS1_NS2
      | inr h => cases h
                 · simp_all; apply not_used_NB; apply parts_knows_Spy_subset_used
                   apply parts.fst; apply parts.snd; apply parts.body
                   aapply Says_imp_parts_knows_Spy
                 · aapply a_ih
  | @NS3 evs3 _ B' _ _ _ _ a₁ a₂ a_ih => 
    cases h₁ with | tail _ b =>
      simp at h₄; by_cases bad_B' : Key (invKey (pubEK B')) ∈ analz (spies evs3)
      · have aC := bad_B'; apply analz_subset_parts at bad_B'
        apply Spy_see_priEK.mp at bad_B'; have c := b; apply a_ih at c; 
        apply analz_insert_Decrypt at aC; rw[aC] at h₄; simp at h₄; cases h₄ with
    | inl h₄ =>
        apply Says_imp_parts_knows_Spy at a₂
        apply Says_imp_parts_knows_Spy at b; rw[h₄] at b
        apply unique_NB at a₂; apply a₂ at b;
        rw[h₄] at c; simp_all; assumption
    | inr h₄ => aapply a_ih
      · apply analz_Crypt at aC; rw[aC] at h₄; simp at h₄; aapply a_ih;

-- Authentication for `B`: if he receives message 3 and has used `NB` in message 2, then `A` has sent message 3.
theorem B_trusts_NS3 { h : ns_public evs } 
  { not_bad_A : A ∉ bad }
  { not_bad_B : B ∉ bad } :
  Says B A (Crypt (pubEK A) ⦃Nonce NA, Nonce NB, Agent B⦄) ∈ evs →
  Says A' B (Crypt (pubEK B) (Nonce NB)) ∈ evs →
  Says A B (Crypt (pubEK B) (Nonce NB)) ∈ evs
:= by 
  intro h₁ h₂
  apply Says_imp_parts_knows_Spy at h₂
  induction h with
  | Nil => simp_all
  | Fake _ a a_ih => right; simp at h₁; simp at h₂; cases h₁ with
    | inl => simp_all[Spy_in_bad]
    | inr h₁ => cases h₂ with
      | inl h₂ => apply Fake_parts_sing at a; apply a at h₂; cases h₂ with
        | inl h₂ => simp at h₂; cases h₂ with
          | inj => aapply a_ih; aapply analz_subset_parts;
          | crypt h₂ => cases h₂; apply Spy_not_see_NB at h₁ <;> simp_all
        | inr => aapply a_ih
      | inr => aapply a_ih
  | NS1 _ a a_ih => right; simp at h₂; simp at h₁; aapply a_ih;
  | NS2 _ _ a a_ih => right; simp at h₁; simp at h₂; cases h₁ with
    | inl => apply parts.body at h₂; apply parts_knows_Spy_subset_used at h₂
             simp_all
    | inr => aapply a_ih
  | NS3 _ a₁ a₂ a_ih => simp at h₁; simp at h₂; cases h₂ with
    | inl h₂ => simp_all; left; rcases h₂ with ⟨e₁, _⟩
                apply injective_publicKey at e₁; simp_all
                have h₁c := h₁
                apply Says_imp_parts_knows_Spy at h₁
                apply Says_imp_parts_knows_Spy at a₂
                apply unique_NB at h₁; apply h₁ at a₂
                apply Spy_not_see_NB at h₁c
                apply a₂ at h₁c
                all_goals simp_all
    | inr => right; aapply a_ih

-- Overall guarantee for `B`
  
-- If NS3 has been sent and the nonce NB agrees with the nonce B joined with NA, then A initiated the run using NA
theorem B_trusts_protocol { h : ns_public evs  }
  { not_bad_A : A ∉ bad }
  { not_bad_B : B ∉ bad } :
  Crypt (pubEK B) (Nonce NB) ∈ parts (spies evs) →
  Says B A (Crypt (pubEK A) ⦃Nonce NA, Nonce NB, Agent B⦄) ∈ evs →
  Says A B (Crypt (pubEK B) ⦃Nonce NA, Agent A⦄) ∈ evs := by
  intro h₁ h₂
  induction h with
  | Nil => simp_all
  | Fake _ a a_ih => right; simp at h₁; simp at h₂; cases h₂ with
    | inl => simp_all[Spy_in_bad]
    | inr h₂ => cases h₁ with
      | inl h₁ => apply Fake_parts_sing at a; apply a at h₁; cases h₁ with
        | inl h₁ => simp at h₁; cases h₁ with
          | inj => aapply a_ih; aapply analz_subset_parts
          | crypt h₁ => cases h₁; apply Spy_not_see_NB at h₂ <;> simp_all
        | inr => aapply a_ih
      | inr => aapply a_ih
  | NS1 _ a a_ih => right; simp at h₂; simp at h₁; aapply a_ih;
  | NS2 _ _ a a_ih => right; simp at h₁; simp at h₂; cases h₂ with
    | inl => apply parts.body at h₁; apply parts_knows_Spy_subset_used at h₁
             simp_all
    | inr => aapply a_ih
  | NS3 _ a₁ a₂ a_ih => simp at h₁; simp at h₂; cases h₁ with
    | inl h₁ => simp_all; rcases h₁ with ⟨e₁, _⟩
                apply injective_publicKey at e₁; simp_all
                have h₂c := h₂
                apply Says_imp_parts_knows_Spy at h₂
                apply Says_imp_parts_knows_Spy at a₂
                apply unique_NB at h₂; apply h₂ at a₂
                apply Spy_not_see_NB at h₂c
                apply a₂ at h₂c
                all_goals simp_all
    | inr => right; aapply a_ih

end NS_Public