leopold/inductive-verification-lean
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Simplified proofs in NS_Public
Lean Action CI / build (push) Has been cancelled
Details

Browse Source
This commit is contained in:
Your Name
2026-03-04 00:56:37 +01:00
parent 96e5d59603
commit 7367681bc6
4 changed files with 313 additions and 391 deletions
Download Patch File Download Diff File Expand all files Collapse all files
InductiveVerification/NS_Public.lean
+216 -365
View File
@@ -1,5 +1,4 @@
import InductiveVerification.Public
set_option diagnostics true
-- The Needham-Schroeder Public-Key Protocol
namespace NS_Public
@@ -47,32 +46,33 @@ theorem possibility_property :
all_goals tauto
· simp
-- Lemmata for some very specific recurring cases in the following proof
omit [InvKey] [Bad] in
lemma Fake_parts_sing_helper {A B : Set Msg}
{ h : A ⊆ B } :
X ∈ A ∨ h₁ → X ∈ B ∨ h₁
:= by
intro h; cases h <;> try simp_all
left; aapply h
-- 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
| Nil =>
simp[spies, knows, initState, pubEK, priEK, pubSK]; intro h
rcases h with (((⟨B, bad, h⟩ | ⟨B, bad, h⟩) | ⟨B, h⟩) | ⟨B, h⟩) <;>
try (apply injective_publicKey at h; simp_all)
all_goals (apply publicKey_neq_privateKey at h; contradiction)
| Fake _ h ih =>
apply Fake_parts_sing at h
intro h₁; simp at h₁; apply Fake_parts_sing_helper (h := h) at h₁
simp at h₁; aapply ih;
| NS1 _ _ ih => simp; assumption
| NS2 _ _ _ ih => simp; assumption
| NS3 _ _ _ ih => simp; assumption
· intro h₁; apply parts_increasing; aapply Spy_spies_bad_privateKey
@[simp]
@@ -82,33 +82,8 @@ theorem Spy_analz_priEK {h : ns_public evs} :
· 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} :
theorem no_nonce_NS1_NS2 { evs: List Event} { h : ns_public evs } :
(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
@@ -116,65 +91,40 @@ theorem no_nonce_NS1_NS2 { evs: List Event} { h : ns_public evs } {A B C D : Ag
induction h with
| Nil => rw[spies, knows] at h₂; simp[initState] at h₂
| Fake _ h ih =>
simp; apply analz_insert; right
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
simp at h₁; apply Fake_parts_sing_helper (h := h) at h₁; simp at h₁
simp at h₂; apply Fake_parts_sing_helper (h := h) at h₂; simp at h₂
rcases h₁ with ((_ | _) | _) <;>
rcases h₂ with ((_ | _) | _) <;>
try simp_all
all_goals (aapply ih <;> aapply analz_subset_parts)
| NS1 _ nonce_not_used =>
apply parts_knows_Spy_subset_used_neg at nonce_not_used;
simp[spies] at h₁; rw[parts_element, Set.subset_def] at h₁; simp at h₁;
simp[spies] at h₂; rw[parts_element, Set.subset_def] at h₂; simp at h₂;
apply analz_mono; apply Set.subset_insert
cases h₂ <;> simp_all
| NS2 _ nonce_not_used =>
apply parts_knows_Spy_subset_used_neg at nonce_not_used;
simp[spies] at h₁; rw[parts_element, Set.subset_def] at h₁; simp at h₁;
simp[spies] at h₂; rw[parts_element, Set.subset_def] at h₂; simp at h₂;
apply analz_mono; apply Set.subset_insert
cases h₁ <;> simp_all
| NS3 _ _ _ a_ih => simp at h₁; simp at h₂; apply analz_mono
apply Set.subset_insert; aapply a_ih
@[simp]
lemma injective_pubEK_helper:
( pubEK A = pubEK B ∧ h) ↔ ( A = B ∧ h )
:= by
constructor
· intro h₁
rcases h₁ with ⟨e, _⟩
apply injective_publicKey at e
aapply And.intro; simp_all
· intro h₁; simp_all
-- 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) →
@@ -185,57 +135,33 @@ theorem unique_NA { h : ns_public evs } :
| 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]
simp[spies, knows] at h₁; apply Fake_parts_sing_helper (h := a) at h₁
simp at h₁
simp[spies, knows] at h₂; apply Fake_parts_sing_helper (h := a) at h₂
simp at h₂
simp[spies, knows] at h₃;
rcases h₁ with ((_ | _) | _) <;>
rcases h₂ with ((_ | _) | _) <;>
try (
apply False.elim; apply h₃; apply analz_mono; aapply Set.subset_insert
tauto
)
all_goals (aapply a_ih <;> try aapply analz_subset_parts
all_goals (
intro _; apply h₃; aapply analz_mono; aapply Set.subset_insert
))
| NS1 _ nonce_not_used a_ih =>
intro h₁ h₂ h₃
simp at h₁; rw[parts_element, Set.subset_def] at h₁; simp at h₁
simp at h₂; rw[parts_element, Set.subset_def] at h₂; simp at h₂
apply parts_knows_Spy_subset_used_neg at nonce_not_used
cases h₁ <;> cases h₂ <;> simp_all
aapply a_ih; intro h; apply h₃; apply_rules[analz_mono, Set.subset_insert]
| NS2 _ _ _ a_ih => intro h₁ h₂ h₃; simp_all; apply a_ih; intro h; apply h₃
apply_rules [analz_mono, Set.subset_insert]
| NS3 _ _ _ a_ih => intro h₁ h₂ h₃; simp at h₁; simp at h₂; aapply a_ih
intro 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 }
@@ -247,27 +173,18 @@ theorem Spy_not_see_NA { h : ns_public evs }
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;
have _ := Spy_in_bad; apply Fake_analz_insert at a; apply a at h₄; simp_all
| 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 =>
| inl => simp_all; apply a; aapply analz_knows_Spy_subset_used
| inr h => apply analz_insert_Crypt_subset at h₄; simp at h₄; cases h₄
· simp_all; apply Says_imp_used at h
apply used_parts_subset_parts at h; apply a; apply h; simp
· aapply a_ih
| 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 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
@@ -282,8 +199,8 @@ theorem Spy_not_see_NA { h : ns_public evs }
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₂
simp at h₄; rcases h₄ with ( h | h | h)
· have _ := b; have _ := a₁; have _ := 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
@@ -304,42 +221,38 @@ theorem A_trusts_NS2 {h : ns_public 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
simp at h₁; simp at h₂;
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;
· have _ := Spy_in_bad; simp_all
· right; apply Fake_parts_sing at a;
apply Fake_parts_sing_helper (h := a) at h₂; simp at h₂
rcases h₂ with ((_ | _) | _) <;> aapply a_ih
· aapply analz_subset_parts
· apply False.elim; apply snsNA; apply analz_spies_mono; tauto;
· 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
| 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₂; rcases h₂ with (⟨_ , e₂ , _, e₄⟩ | _)
· apply Says_imp_parts_knows_Spy at a
apply Says_imp_parts_knows_Spy at b
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
· 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`
@@ -351,47 +264,21 @@ lemma B_trusts_NS1 { h : ns_public evs} :
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
| Fake _ a a_ih =>
simp at h₁; apply Fake_parts_sing at a;
apply Fake_parts_sing_helper (h := a) at h₁; simp at h₁
rcases h₁ with ((h₁ | h₁ )| h₁);
· right; aapply a_ih; aapply analz_subset_parts; aapply analz_spies_mono_neg
· apply False.elim; apply h₂; apply analz_spies_mono; simp_all
· right; aapply a_ih; aapply analz_spies_mono_neg
| NS1 _ _ a_ih => simp at h₁; cases h₁
· simp_all
· 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) →
@@ -402,57 +289,31 @@ theorem unique_NB { h : ns_public evs } :
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
intro h₁ h₂ h₃;
apply Fake_parts_sing at a
simp[spies, knows] at h₁; apply Fake_parts_sing_helper (h := a) at h₁
simp at h₁;
simp at h₂; apply Fake_parts_sing_helper (h := a) at h₂; simp at h₂;
apply analz_spies_mono_neg at h₃
rcases h₁ with ((h₁ | h₁) | h₁) <;>
rcases h₂ with ((h₂ | h₂) | h₂) <;>
simp_all
all_goals (aapply a_ih; repeat aapply analz_subset_parts)
| 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]
| NS2 _ nonce_not_used _ a_ih =>
intro h₁ h₂ h₃;
-- This is how to rewrite `M ∈ parts` terms into something useful
-- TODO create a macro for this
-- TODO this should work with analz as well
simp at h₁; rw[parts_element, Set.subset_def] at h₁; simp at h₁
simp at h₂; rw[parts_element, Set.subset_def] at h₂; simp at h₂
apply analz_spies_mono_neg at h₃;
apply parts_knows_Spy_subset_used_neg at nonce_not_used
rcases h₁ with (_ | h₁) <;>
rcases h₂ with (_ | h₂) <;> simp_all
| NS3 _ _ _ a_ih =>
intro h₁ h₂ h₃; apply analz_spies_mono_neg at h₃; simp_all;
-- `NB` remains secret
theorem Spy_not_see_NB { h : ns_public evs }
@@ -464,46 +325,34 @@ theorem Spy_not_see_NB { h : ns_public evs }
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
| Fake _ a a_ih =>
have _ := Spy_in_bad; apply Fake_analz_insert at a; apply a at h₄; simp_all;
| NS1 _ nonce_not_used a_ih =>
simp at h₁
simp[spies, knows] at h₄; apply analz_insert_Crypt_subset at h₄; simp at h₄
apply parts_knows_Spy_subset_used_neg at nonce_not_used
cases h₄ with
| inl e => apply Says_imp_parts_knows_Spy at h₁;
rw[parts_element, Set.subset_def] at h₁; simp_all
| 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;
| NS2 _ not_used_NB a a_ih =>
simp at h₁;
simp[spies, knows] at h₄;
apply parts_knows_Spy_subset_used_neg at not_used_NB
rcases h₁ with (_ | h₁)
· simp_all; apply not_used_NB; aapply analz_subset_parts
· apply analz_insert_Crypt_subset at h₄; simp at h₄; rcases h₄ with (_ |_ |_ )
· aapply a_ih; apply Says_imp_parts_knows_Spy at a;
apply Says_imp_parts_knows_Spy at h₁; simp_all; aapply no_nonce_NS1_NS2
· apply Says_imp_parts_knows_Spy at h₁;
rw[parts_element, Set.subset_def] at h₁; simp_all
· aapply a_ih
| NS3 _ _ a a_ih =>
simp at h₁; simp[analz_insert_Crypt_element] at h₄;
rcases h₄ with (⟨_, _⟩ | ⟨_, _⟩) <;> simp_all
apply Says_imp_parts_knows_Spy at a
apply Says_imp_parts_knows_Spy at h₁; apply unique_NB at a
apply a at h₁; apply h₁ at a_ih; simp_all; assumption
-- 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 }
@@ -517,31 +366,32 @@ theorem B_trusts_NS3 { h : ns_public evs }
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
| Fake _ a a_ih =>
right; simp at h₁
apply Fake_parts_sing at a
simp at h₂; apply Fake_parts_sing_helper (h := a) at h₂; simp at h₂
rw[parts_element, Set.subset_def] at h₂; simp at h₂
have _ := Spy_in_bad
rcases h₁ with (h₁ | h₁) <;> rcases h₂ with ((h₂ | h₂) | h₂) <;> simp_all
· aapply a_ih; aapply analz_subset_parts
· apply Spy_not_see_NB at h₁ <;> simp_all
· 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
| NS2 _ nonce_not_used a a_ih =>
right
apply parts_knows_Spy_subset_used_neg at nonce_not_used;
simp at h₂; rw[parts_element, Set.subset_def] at h₂; simp at h₂
simp at h₁; cases h₁ <;> simp_all; aapply a_ih
| NS3 _ _ a₂ a_ih =>
simp at h₁
simp at h₂; rw[parts_element, Set.subset_def] at h₂; simp at h₂
cases h₂ <;> simp_all
have h₁c := h₁
apply Spy_not_see_NB at h₁c
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 a₂ at h₁c; all_goals simp_all
-- Overall guarantee for `B`
@@ -555,30 +405,31 @@ theorem B_trusts_protocol { h : ns_public evs }
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
| Fake _ a a_ih =>
right
apply Fake_parts_sing at a
simp at h₁; apply Fake_parts_sing_helper (h := a) at h₁;
rw[parts_element, Set.subset_def] at h₁; simp at h₁
have _ := Spy_in_bad
simp at h₂; rcases h₂ with (_ | h₂) <;> simp_all
rcases h₁ with (((_ |_ ) | _) | _) <;> try (aapply a_ih)
· aapply analz_subset_parts
· apply Spy_not_see_NB at h₂ <;> simp_all
· simp_all
| 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
| NS3 _ _ a₂ a_ih =>
simp at h₂
simp at h₁; rw[parts_element, Set.subset_def] at h₁; simp at h₁
cases h₁ <;> simp_all
have h₂c := h₂
apply Spy_not_see_NB at h₂c
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 a₂ at h₂c; all_goals simp_all
end NS_Public