From e41142896fdbceae5a23b7d5f5bf8481e41ae390 Mon Sep 17 00:00:00 2001 From: Your Name Date: Wed, 11 Mar 2026 17:11:44 +0100 Subject: [PATCH] Proved basic properties of Blanchet protocol --- InductiveVerification/Blanchet.lean | 226 +++++++++++++++++++++++++++ InductiveVerification/Event.lean | 21 +-- InductiveVerification/Message.lean | 114 ++++++++++---- InductiveVerification/NS_Public.lean | 62 ++++---- InductiveVerification/Public.lean | 189 +++++++++++++++++----- 5 files changed, 490 insertions(+), 122 deletions(-) create mode 100644 InductiveVerification/Blanchet.lean diff --git a/InductiveVerification/Blanchet.lean b/InductiveVerification/Blanchet.lean new file mode 100644 index 0000000..9b53c2b --- /dev/null +++ b/InductiveVerification/Blanchet.lean @@ -0,0 +1,226 @@ +import InductiveVerification.Public + +-- The Blanchet Protocol +namespace Blanchet + +variable [InvKey] +variable [Bad] +variable [AgentKeys] +open Msg +open Event +open Bad +open HasInitState +open InvKey + +-- Define the inductive set `blanchet` +inductive blanchet : List Event → Prop +| Nil : blanchet [] +| Fake : blanchet evsf → + X ∈ synth (analz (spies evsf)) → + blanchet (Says Agent.Spy B X :: evsf) +| B1 : blanchet evs1 → + sk ∈ symKeys → + -- sk is fresh + Key sk ∉ used evs1 ∪ Key '' keysFor (used evs1) → + blanchet (Says A B (Crypt (pubEK B) (Sign (priSK A) ⦃Agent B, Key sk⦄)) :: evs1) +| B2 : blanchet evs2 → + Nonce s ∉ used evs2 → + Says A B (Crypt (pubEK B) (Sign (priSK A) ⦃Agent B, Key k⦄)) ∈ evs2 → + blanchet (Says B A (Crypt k (Nonce s)) :: evs2) + +-- A "possibility property": there are traces that reach the end +theorem possibility_property : + ∃ sk ∈ symKeys, ∃ s, ∃ evs, blanchet evs ∧ Says B A (Crypt sk s) ∈ evs +:= by + obtain ⟨sk, _, _⟩ := symK_supply (evs := []) + exists sk + simp_all + exists Nonce 0 + exists [ + Says B A (Crypt sk (Nonce 0)), + Says A B (Crypt (pubEK B) (Sign (priSK A) ⦃Agent B, Key sk⦄)), + ] + constructor + · apply blanchet.B2 + · apply_rules [ blanchet.B1, blanchet.Nil ]; simp_all + · simp [used] + · tauto + · simp + +-- Spy never sees another agent's private key unless it's bad at the start +@[simp, grind =] +theorem Spy_see_priEK {h : blanchet evs} : + (Key (priEK A) ∈ parts (spies evs)) ↔ A ∈ bad := by + constructor + · induction h with + | Nil => simp [ priEK, initState ] + | Fake _ h => + intro h₁; simp at h₁ + apply Or.imp_left (f := Fake_parts_sing (h := h)) at h₁ + simp_all + | B1 => simp_all; + | B2 => simp_all; + · intro _; apply_rules [ parts_increasing, Spy_spies_bad_privateKey ] + +@[simp] +theorem Spy_analz_priEK {h : blanchet evs} : + Key (priEK A) ∈ analz (spies evs) ↔ A ∈ bad +:= by grind + +@[simp, grind =] +theorem Spy_see_priSK {h : blanchet evs} : + Key (priSK A) ∈ parts (spies evs) ↔ A ∈ bad +:= by + constructor + · induction h with + | Nil => simp [ priSK, initState ] + | Fake _ h => + intro h₁; simp at h₁ + apply Or.imp_left (f := Fake_parts_sing (h := h)) at h₁ + simp_all + | B1 => simp_all; + | B2 => simp_all; + · intro _; apply_rules [ parts_increasing, Spy_spies_bad_privateKey ] + +@[simp] +theorem Spy_analz_priSK {h : blanchet evs} : + Key (priSK A) ∈ analz (spies evs) ↔ A ∈ bad +:= by grind + +-- Unicity for NS1: nonce NA identifies agents A and B +@[grind! .] +theorem unique_B1 { h : blanchet evs } : + (Crypt (pubEK B) (Sign (priSK A) ⦃Agent B, Key sk⦄) ∈ parts (spies evs) → + (Crypt (pubEK B') (Sign (priSK A') ⦃Agent B', Key sk⦄) ∈ parts (spies evs) → + Key sk ∉ analz (spies evs) → + A = A' ∧ B = B')) := by + intro h₁ h₂ h₃ + induction h with + | Nil => simp_all [ initState ] + | Fake _ a a_ih => + apply mt (h₁ := analz_spies_mono) at h₃; + simp [*, priSK] at * + apply Or.imp_left (f := Fake_parts_sing (h := a)) at h₁ + apply Or.imp_left (f := Fake_parts_sing (h := a)) at h₂ + simp_all; + | B1 => + simp [*] at *; expand_parts_element at h₁; expand_parts_element at h₂; grind + | B2 => simp_all; grind + +lemma keysFor_used_knows_Spy_helper : + K ∈ keysFor (analz (spies evs)) → K ∈ keysFor (used evs) +:= by + aapply keysFor_mono; apply analz_knows_Spy_subset_used + +-- Spy does not see the key sent in B1 if A and B are secure +@[grind! .] +theorem Spy_not_see_sk { h : blanchet evs } + { not_bad_A : A ∉ bad } + { not_bad_B : B ∉ bad } : + Says A B (Crypt (pubEK B) (Sign (priSK A) ⦃Agent B, Key sk⦄)) ∈ evs → + Key sk ∉ analz (spies evs) := by + intro h₁ h₂ + induction h with + | Nil => simp_all + | Fake _ a => apply Fake_analz_insert at a; apply a at h₂; simp_all + | B1 _ _ a => + simp_all; obtain ⟨a, b⟩ := a; rcases h₁ with (_ | h) + · simp_all; apply a; aapply analz_knows_Spy_subset_used + · have _ := h; apply Says_imp_used at h; apply used_parts_subset_parts at h; + apply mt (h₁ := keysFor_used_knows_Spy_helper) at b + apply analz_insert_Crypt_subset at h₂; simp at h₂ + apply analz_insert_Crypt_subset at h₂; simp at h₂ + rw [analz_insert_Key] at h₂ + cases h₂; all_goals simp_all[Set.subset_def] + | B2 => apply analz_insert_Crypt_subset at h₂; simp at h₂; grind + +-- Authentication for `A`: if she receives message 2 and has used `sk` to start +-- a run, then `B` has sent message 2. +theorem A_trusts_B2 {h : blanchet evs } + { not_bad_A : A ∉ bad } + { not_bad_B : B ∉ bad } : + Says A B (Crypt (pubEK B) (Sign (priSK A) ⦃Agent B, Key sk⦄)) ∈ evs → + Says B' A (Crypt sk (Number s)) ∈ evs → + Says B A (Crypt sk (Number s)) ∈ evs +:= by + intro h₁ h₂; + apply Says_imp_parts_knows_Spy at h₂ + -- use unique_NA to show that B' = B + induction h with + | Nil => simp_all + | Fake _ a => + have snssk := h₁; apply Spy_not_see_sk at snssk <;> try assumption + apply mt (h₁ := analz_spies_mono) at snssk + simp [*] at * + cases h₁ + · simp_all + · apply Or.imp_left (f := Fake_parts_sing (h := a)) at h₂; simp_all + · aapply blanchet.Fake + | B1 => simp [*] at *; expand_parts_element at h₂; simp_all [keysFor]; grind + | B2 => simp [*] at *; grind + +theorem sk_symmetric_B1 {h :blanchet evs } + { not_bad_A : A ∉ bad } : + Says A B (Crypt (pubEK B) (Sign (priSK A) ⦃Agent B, Key sk⦄)) ∈ evs → + sk ∈ symKeys +:= by + intro h₁; induction h <;> simp_all + · grind + · cases h₁ <;> simp_all + +-- If the encrypted message appears then it originated with Alice in `NS1` +lemma B_trusts_B1 { h : blanchet evs} + { not_bad_A : A ∉ bad } : + Crypt (pubEK B) (Sign (priSK A) ⦃Agent B, Key sk⦄) ∈ parts (spies evs) → + Key sk ∉ analz (spies evs) → + Says A B (Crypt (pubEK B) (Sign (priSK A) ⦃Agent B, Key sk⦄)) ∈ evs +:= by + intro h₁ h₂ + induction h with + | Nil => simp [initState] at h₁ + | Fake _ a => + apply mt (h₁ := analz_spies_mono) at h₂ + simp at h₁; apply Or.imp_left (f := Fake_parts_sing (h := a)) at h₁; simp_all + | B1 => apply mt (h₁ := analz_spies_mono) at h₂; simp_all; grind + | B2 => apply mt (h₁ := analz_spies_mono) at h₂; simp_all; + +-- Authenticity Properties obtained from `NS2` + +-- B only respods to requests from A +theorem B_is_response { h : blanchet evs } + { not_bad_B : B ∉ bad } : + Says B A (Crypt sk (Nonce s)) ∈ evs → + Says A B (Crypt (pubEK B) (Sign (priSK A) ⦃Agent B, Key sk⦄)) ∈ evs +:= by + intro h₁ + induction h <;> simp_all <;> grind + +-- `s` remains secret +theorem Spy_not_see_s { h : blanchet evs } + { not_bad_A : A ∉ bad } + { not_bad_B : B ∉ bad } : + Says B A (Crypt sk (Nonce s)) ∈ evs → + Nonce s ∉ analz (spies evs) +:= by + intro h₁ + induction h with + | Nil => simp_all + | Fake _ a => intro h₂; apply Fake_analz_insert at a; apply a at h₂; simp_all; + | B1 _ _ a => + simp at a; obtain ⟨a, b⟩ := a; + simp [*, analz_insert_Crypt_element] at * + have _ := h₁; apply Says_imp_parts_knows_Spy at h₁ + expand_parts_element at h₁; simp_all; intro h₁ h₂ + rw[analz_insert_Key] at h₂; simp at h₂; grind; + aapply mt (h₁ := keysFor_used_knows_Spy_helper) + | B2 h not_used a a_ih => + simp at h₁; rcases h₁ with (_ | h) <;> simp_all[analz_insert_Crypt_element] + . apply And.intro; + · have b := a; apply Spy_not_see_sk at a; apply sk_symmetric_B1 at b + all_goals simp_all + · grind + · apply Says_imp_used at h + apply used_parts_subset_parts at h; rw[Set.subset_def] at h + intro _ _; simp_all + +end Blanchet diff --git a/InductiveVerification/Event.lean b/InductiveVerification/Event.lean index 23c44c9..6ecf119 100644 --- a/InductiveVerification/Event.lean +++ b/InductiveVerification/Event.lean @@ -15,7 +15,6 @@ class HasInitState (α : Type) where variable [ hasInitStateAgent : HasInitState Agent ] open HasInitState -attribute [simp] initState -- Define the `bad` set abbrev DecidableMem ( A : Set Agent ) := (a : Agent) → Decidable (a ∈ A) @@ -214,18 +213,12 @@ lemma parts_insert_spies [Bad] : by apply parts_insert -lemma analz_spies_mono [InvKey] [Bad] - { h : M ∈ analz (knows Agent.Spy evs) } : - M ∈ analz (knows Agent.Spy (ev :: evs)) +lemma analz_spies_mono [InvKey] [Bad] : + M ∈ analz (knows Agent.Spy evs) → M ∈ analz (knows Agent.Spy (ev :: evs)) := by + intro h aapply analz_mono; exact knows_subset_knows_Cons -lemma analz_spies_mono_neg [InvKey] [Bad] - { h : M ∉ analz (knows Agent.Spy (ev :: evs)) } : - M ∉ analz (knows Agent.Spy evs) -:= by - intro h₁; apply h; aapply analz_spies_mono - -- Knowledge of Agents lemma knows_subset_knows_Says [Bad] : ∀ {A A' B : Agent} {X : Msg} {evs : List Event}, @@ -382,10 +375,6 @@ lemma parts_knows_Spy_subset_used [Bad] : · simp; apply subset_trans; apply ih; simp · apply subset_trans; apply ih; simp -lemma parts_knows_Spy_subset_used_neg [Bad] : - M ∉ used evs → M ∉ parts (knows Agent.Spy evs) := by - intro h₁ h₂; apply h₁; aapply parts_knows_Spy_subset_used - lemma analz_knows_Spy_subset_used [Bad] [InvKey] : analz (knows Agent.Spy evs) ⊆ used evs := by @@ -393,10 +382,6 @@ lemma analz_knows_Spy_subset_used [Bad] [InvKey] : · exact analz_subset_parts · exact parts_knows_Spy_subset_used -lemma analz_knows_Spy_subset_used_neg [Bad] [InvKey] : - M ∉ used evs → M ∉ analz (knows Agent.Spy evs) := by - intro h₁ h₂; apply h₁; aapply analz_knows_Spy_subset_used - -- Parts of what the Spy knows are a subset of what is used lemma usedI [Bad] : X ∈ parts (knows Agent.Spy evs) → X ∈ used evs := by diff --git a/InductiveVerification/Message.lean b/InductiveVerification/Message.lean index 33f9bdc..eddc150 100644 --- a/InductiveVerification/Message.lean +++ b/InductiveVerification/Message.lean @@ -25,6 +25,9 @@ class InvKey where all_symmetric : Bool invKey_spec : ∀ K : Key, invKey (invKey K) = K invKey_symmetric : all_symmetric → invKey = id +-- There are infinitely many keys of each type + symKey_supply : ∀ N : Key, ∃ n > N, invKey n = n + asymKey_supply : (¬all_symmetric) → (∀ N : Key, ∃ n > N, invKey n ≠ n) open InvKey @@ -132,6 +135,16 @@ lemma keysFor_union (H H' : Set Msg) [InvKey] : keysFor (H ∪ H') = keysFor H constructor · intro h; simp_all; grind · intro h; simp_all; grind + +@[simp] +lemma keysFor_iunion [InvKey] {T : Type} {H : T → Set Msg} : + keysFor (⋃ (x : T), H x) = ⋃ x, keysFor (H x) +:= by + ext + simp[keysFor] + constructor + · intro h; obtain ⟨x, ⟨X, i, h⟩, _⟩ := h; exists i; exists x; simp [*]; exists X + · intro h; obtain ⟨i, x, ⟨X, h⟩, _⟩ := h; exists x; simp [*]; exists X; exists i -- Monotonicity lemma keysFor_mono [InvKey] : Monotone keysFor := by @@ -146,31 +159,61 @@ lemma keysFor_insert_Agent (A : Agent) (H : Set Msg) [InvKey] : keysFor (insert (Agent A) H) = keysFor H := by simp[keysFor] +@[simp] +lemma keysFor_singleton_Agent [InvKey] : + keysFor {Agent agt} = ∅ := by + rw[Set.singleton_def, keysFor_insert_Agent, keysFor_empty] + @[simp] lemma keysFor_insert_Nonce (N : Nat) (H : Set Msg) [InvKey] : keysFor (insert (Nonce N) H) = keysFor H := by simp[keysFor] +@[simp] +lemma keysFor_singleton_Nonce [InvKey] : + keysFor {Nonce N} = ∅ := by + rw[Set.singleton_def, keysFor_insert_Nonce, keysFor_empty] + @[simp] lemma keysFor_insert_Number (N : Nat) (H : Set Msg) [InvKey] : - keysFor (insert (Msg.Hash (Nonce N)) H) = keysFor H := by + keysFor (insert (Number N) H) = keysFor H := by simp[keysFor] +@[simp] +lemma keysFor_singleton_Number [InvKey] : + keysFor {Number N} = ∅ := by + rw[Set.singleton_def, keysFor_insert_Number, keysFor_empty] + @[simp] lemma keysFor_insert_Key (K : Key) (H : Set Msg) [InvKey] : keysFor (insert (Key K) H) = keysFor H := by simp[keysFor] +@[simp] +lemma keysFor_singleton_Key [InvKey] : + keysFor {Key K} = ∅ := by + rw[Set.singleton_def, keysFor_insert_Key, keysFor_empty] + @[simp] lemma keysFor_insert_Hash (X : Msg) (H : Set Msg) [InvKey] : keysFor (insert (Hash X) H) = keysFor H := by simp[keysFor] +@[simp] +lemma keysFor_singleton_Hash [InvKey] : + keysFor {Hash H} = ∅ := by + rw[Set.singleton_def, keysFor_insert_Hash, keysFor_empty] + @[simp] lemma keysFor_insert_MPair (X Y : Msg) (H : Set Msg) [InvKey] : keysFor (insert ⦃X, Y⦄ H) = keysFor H := by simp[keysFor] +@[simp] +lemma keysFor_singleton_MPair [InvKey] : + keysFor {⦃X, Y⦄} = ∅ := by + rw[Set.singleton_def, keysFor_insert_MPair, keysFor_empty] + @[simp] lemma keysFor_insert_Crypt (K : Key) (X : Msg) (H : Set Msg) [InvKey] : keysFor (insert (Crypt K X) H) = insert (invKey K) (keysFor H) := by @@ -178,6 +221,11 @@ lemma keysFor_insert_Crypt (K : Key) (X : Msg) (H : Set Msg) [InvKey] : ext grind +@[simp] +lemma keysFor_singleton_Crypt [InvKey] : + keysFor {Crypt K X} = {invKey K} := by + rw[Set.singleton_def, keysFor_insert_Crypt, keysFor_empty, ←Set.singleton_def] + @[simp] lemma keysFor_image_Key (E : Set Key) [InvKey] : keysFor (Key '' E) = ∅ := by simp[keysFor] @@ -585,6 +633,37 @@ by | Crypt K X ih => rcases ih with ⟨N, h⟩; exists N; have ins_crypt := parts_insert_Crypt (H := {}) (K := K) (X := X); simp_all; + +lemma msg_Key_supply [InvKey] {msg : Msg} : ∃ N, ∀ n, N ≤ n → + (Key n ∉ parts {msg} ∧ n ∉ keysFor (parts {msg})):= +by + induction msg with + | Agent a => exists 0; + have ins_agt := parts_insert_Agent (H := {}) (agt := a); + simp_all + | Number a => exists 0; + have ins_number := parts_insert_Number (H := {}) (N := a); + simp_all; + | Nonce n => exists 0; + have ins_nonce := parts_insert_Nonce (H := {}) (N := n); + simp_all; + | Key k => exists k.succ; + intro _ _; + have ins_key := parts_insert_Key (H := {}) (K := k); + simp_all; grind; + | Hash X ih => exists 0; + have ins_hash := parts_insert_Hash (H := {}) (X := X); + simp_all; + | MPair X Y ihX ihY => + rcases ihX with ⟨wX, hH⟩; + cases ihY with + | intro wY hY => exists Nat.max wX wY; intro n h₁; + have ins_mpair := parts_insert_MPair (H := {}) (X := X) (Y := Y); + simp_all; + | Crypt K X ih => rcases ih with ⟨N, h⟩; exists Nat.succ (Nat.max N (invKey K)); + intro _ _; + have ins_crypt := parts_insert_Crypt (H := {}) (K := K) (X := X); + simp_all; grind -- Inductive relation "analz" inductive analz [InvKey] (H : Set Msg) : Set Msg @@ -610,16 +689,6 @@ lemma analz_insert_mono [InvKey] : := by apply_rules [ analz_mono, Set.subset_insert] -lemma analz_mono_neg [InvKey] { h : A ⊆ B } : - X ∉ analz B → X ∉ analz A -:= by - intro h₁ h₂; apply h₁; aapply analz_mono; - -lemma analz_insert_mono_neg [InvKey] : - X ∉ analz (insert Y H) → X ∉ analz H -:= by - apply_rules [ analz_mono_neg, Set.subset_insert ] - -- Making it safe speeds up proofs -- @[simp] lemma MPair_analz {H : Set Msg} {X Y : Msg} {P : Prop} [InvKey] : @@ -783,11 +852,10 @@ lemma analz_insert_Hash {H : Set Msg} {X : Msg} [InvKey] : · apply analz_insert @[simp] -lemma analz_insert_Key {H : Set Msg} {K : Key} [InvKey] : - K ∉ keysFor (analz H) → +lemma analz_insert_Key [InvKey] {H : Set Msg} {K : Key} + { hK : K ∉ keysFor (analz H) } : analz (insert (Key K) H) = insert (Key K) (analz H) := by - intro hK ext x constructor · intro h @@ -1614,24 +1682,12 @@ by cases h; contradiction; assumption · apply analz_mono; apply Set.subset_insert - - -- Fake parts for single messages -lemma Fake_parts_sing [InvKey] {H : Set Msg} {X : Msg} : - X ∈ synth (analz H) → parts {X} ⊆ synth (analz H) ∪ parts H := +lemma Fake_parts_sing [InvKey] {H : Set Msg} {X : Msg} + {h : X ∈ synth (analz H)} : + (Y ∈ parts {X} → Y ∈ synth (analz H) ∪ parts H) := by - intro h rw[Set.singleton_def] apply subset_trans (b := parts (insert X H)) · apply parts_mono; simp · aapply Fake_parts_insert - --- Often the result of Fake_parts_sing needs to be applied to a term in a --- disjunction -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 - diff --git a/InductiveVerification/NS_Public.lean b/InductiveVerification/NS_Public.lean index da3eb7a..e490396 100644 --- a/InductiveVerification/NS_Public.lean +++ b/InductiveVerification/NS_Public.lean @@ -5,6 +5,7 @@ namespace NS_Public variable [InvKey] variable [Bad] +variable [AgentKeys] open Msg open Event open Bad @@ -52,10 +53,10 @@ theorem Spy_see_priEK {h : ns_public evs} : (Key (priEK A) ∈ parts (spies evs)) ↔ A ∈ bad := by constructor · induction h with - | Nil => simp [ priEK ] + | Nil => simp [ priEK, initState ] | Fake _ h => - apply Fake_parts_sing at h - intro h₁; simp at h₁; apply Fake_parts_sing_helper (h := h) at h₁ + intro h₁; simp at h₁ + apply Or.imp_left (f := Fake_parts_sing (h := h)) at h₁ simp_all | NS1 => simp_all | NS2 => simp_all @@ -76,12 +77,11 @@ theorem no_nonce_NS1_NS2 { evs: List Event} { h : ns_public evs } : Nonce NA ∈ analz (spies evs))) := by intro h₁ h₂ induction h with - | Nil => simp at h₂ + | Nil => simp [ initState ] at h₂ | Fake _ h => simp [*] at * - apply Fake_parts_sing at h - apply Fake_parts_sing_helper (h := h) at h₁ - apply Fake_parts_sing_helper (h := h) at h₂ + apply Or.imp_left (f := Fake_parts_sing (h := h)) at h₁ + apply Or.imp_left (f := Fake_parts_sing (h := h)) at h₂ simp_all; grind | NS1 => simp [*] at * @@ -102,13 +102,12 @@ theorem unique_NA { h : ns_public evs } : A = A' ∧ B = B'))) := by intro h₁ h₂ h₃ induction h with - | Nil => simp_all + | Nil => simp_all [ initState ] | Fake _ a a_ih => - apply Fake_parts_sing at a; - apply analz_spies_mono_neg at h₃; + apply mt (h₁ := analz_spies_mono) at h₃; simp [*] at * - apply Fake_parts_sing_helper (h := a) at h₁ - apply Fake_parts_sing_helper (h := a) at h₂ + apply Or.imp_left (f := Fake_parts_sing (h := a)) at h₁ + apply Or.imp_left (f := Fake_parts_sing (h := a)) at h₂ simp_all | NS1 => simp [*] at *; expand_parts_element at h₁; expand_parts_element at h₂; grind @@ -160,13 +159,11 @@ theorem A_trusts_NS2 {h : ns_public evs } | Nil => simp_all | Fake _ a => have snsNA := h₁; apply Spy_not_see_NA at snsNA <;> try assumption - apply analz_spies_mono_neg at snsNA + apply mt (h₁ := analz_spies_mono) at snsNA; simp [*] at * cases h₁ · simp_all - · apply Fake_parts_sing at a; - apply Fake_parts_sing_helper (h := a) at h₂; simp at h₂ - grind + · apply Or.imp_left (f := Fake_parts_sing (h := a)) at h₂; simp at h₂; grind · aapply ns_public.Fake | NS1 => simp [*] at *; expand_parts_element at h₂; grind | NS2 => simp [*] at *; grind @@ -180,14 +177,13 @@ lemma B_trusts_NS1 { h : ns_public evs} : := by intro h₁ h₂ induction h with - | Nil => simp at h₁ + | Nil => simp [ initState ] at h₁ | Fake _ a => - apply analz_spies_mono_neg at h₂ - simp at h₁; apply Fake_parts_sing at a; - apply Fake_parts_sing_helper (h := a) at h₁; simp_all - | NS1 => apply analz_spies_mono_neg at h₂; simp_all; grind - | NS2 => apply analz_spies_mono_neg at h₂; simp_all; - | NS3 => apply analz_spies_mono_neg at h₂; simp_all; + apply mt (h₁ := analz_spies_mono) at h₂ + simp at h₁; apply Or.imp_left (f := Fake_parts_sing (h := a)) at h₁; simp_all + | NS1 => apply mt (h₁ := analz_spies_mono) at h₂; simp_all; grind + | NS2 => apply mt (h₁ := analz_spies_mono) at h₂; simp_all; + | NS3 => apply mt (h₁ := analz_spies_mono) at h₂; simp_all; -- Authenticity Properties obtained from `NS2` @@ -201,14 +197,15 @@ theorem unique_NB { h : ns_public evs } : -- Proof closely follows that of unique_NA intro h₁ h₂ h₃ induction h with - | Nil => aesop (add safe analz_insertI) + | Nil => simp_all [ initState ] | Fake _ a => - apply Fake_parts_sing at a; simp [*] at * - apply Fake_parts_sing_helper (h := a) at h₁; - apply Fake_parts_sing_helper (h := a) at h₂; simp [*] at * - apply analz_insert_mono_neg at h₃ + simp [*] at * + apply Or.imp_left (f := Fake_parts_sing (h := a)) at h₁; + apply Or.imp_left (f := Fake_parts_sing (h := a)) at h₂ + simp [*] at * + apply mt (h₁ := analz_insert_mono) at h₃ grind - | NS1 => apply analz_spies_mono_neg at h₃; simp_all + | NS1 => apply mt (h₁ := analz_spies_mono) at h₃; simp_all | NS2 => simp [*] at *; expand_parts_element at h₁; expand_parts_element at h₂; grind | NS3 => simp_all; grind @@ -255,8 +252,7 @@ theorem B_trusts_NS3 { h : ns_public evs } | Nil => simp_all | Fake _ a => simp [*] at * - apply Fake_parts_sing at a - apply Fake_parts_sing_helper (h := a) at h₂; simp at h₂ + apply Or.imp_left (f := Fake_parts_sing (h := a)) at h₂; simp at h₂ grind | NS1 => simp_all | NS2 => simp [*] at *; expand_parts_element at h₂; grind @@ -277,8 +273,8 @@ theorem B_trusts_protocol { h : ns_public evs } | Nil => simp_all | Fake _ a => simp [*] at * - apply Fake_parts_sing at a - apply Fake_parts_sing_helper (h := a) at h₁; expand_parts_element at h₁ + apply Or.imp_left (f := Fake_parts_sing (h := a)) at h₁ + expand_parts_element at h₁ grind | NS1 => simp_all | NS2 => simp [*] at *; expand_parts_element at h₁; grind diff --git a/InductiveVerification/Public.lean b/InductiveVerification/Public.lean index 26aaf34..6abf863 100644 --- a/InductiveVerification/Public.lean +++ b/InductiveVerification/Public.lean @@ -21,9 +21,30 @@ inductive KeyMode | Signature | Encryption -axiom publicKey : KeyMode → Agent → Key -axiom injective_publicKey : ∀ {b c : KeyMode} {A A' : Agent}, - publicKey b A = publicKey c A' → b = c ∧ A = A' +-- TODO replace axioms with classes +-- Also make sure that there are infinite key supplies +class AgentKeys where + publicKey : KeyMode → Agent → Key + injective_publicKey : ∀ {b c : KeyMode} {A A' : Agent}, + publicKey b A = publicKey c A' → b = c ∧ A = A' + privateKey_neq_publicKey : invKey (publicKey b A) ≠ publicKey c A' + not_surjective_publicKey_asymK : (¬all_symmetric) → + (∀ K : Key, ∃ K' > K, + K' ∉ symKeys ∧ + (∀ b : KeyMode, ∀ A : Agent, + publicKey b A ≠ K' ∧ invKey (publicKey b A) ≠ K')) +-- Symmetric Keys +-- For some protocols, it is convenient to equip agents with symmetric as +-- well as asymmetric keys. The theory ‹Shared› assumes that all keys +-- are symmetric. + shrK : Agent → Key + inj_shrK : Function.Injective shrK + sym_shrK : ∀ {A : Agent}, shrK A ∈ symKeys + not_surjective_shrK_symK : ∀ K : Key, ∃ K' > K, + K' ∈ symKeys ∧ (∀ A : Agent, shrK A ≠ K') + +open AgentKeys +variable [AgentKeys] noncomputable abbrev pubEK (A : Agent) : Key := publicKey KeyMode.Encryption A noncomputable abbrev pubSK (A : Agent) : Key := publicKey KeyMode.Signature A @@ -33,28 +54,27 @@ noncomputable abbrev priSK (A : Agent) : Key := privateKey KeyMode.Signature A noncomputable abbrev pubK (A : Agent) : Key := pubEK A noncomputable abbrev priK (A : Agent) : Key := invKey (pubEK A) +abbrev Sign (K : Key) (M : Msg) := ⦃Msg.Crypt K M, M⦄ + attribute [simp] pubEK attribute [simp] pubSK -- attribute [simp] priEK -- attribute [simp] priSK +attribute [simp] privateKey_neq_publicKey -- Axioms for private and public keys -@[simp] -axiom privateKey_neq_publicKey {b c : KeyMode} {A A' : Agent} : - privateKey b A ≠ publicKey c A' - @[simp] lemma publicKey_neq_privateKey {b c : KeyMode} {A A' : Agent} : publicKey b A ≠ privateKey c A' := by exact privateKey_neq_publicKey.symm -- Basic properties of pubK and priK -omit [InvKey] in @[simp] lemma publicKey_inject {b c : KeyMode} {A A' : Agent} : (publicKey b A = publicKey c A') ↔ (b = c ∧ A = A') := by grind[injective_publicKey] +omit [AgentKeys] in lemma invKey_injective: Function.Injective invKey := by intro _ _ _ simp_all[invKey_eq] @@ -67,23 +87,42 @@ by lemma not_symKeys_priK {b : KeyMode} {A : Agent} : privateKey b A ∉ symKeys := by simp [symKeys, privateKey, invKey_eq, privateKey_neq_publicKey] + +@[simp] +lemma pubK_neq_symK {b : KeyMode} {A : Agent} {h : K ∈ symKeys} : + publicKey b A ≠ K +:= by + intro h₁; have h₂ := not_symKeys_pubK (b := b) (A := A); simp_all -lemma syKey_neq_priEK : - K ∈ symKeys → K ≠ priEK A := by - intro _ _ - have _ := not_symKeys_pubK (b := KeyMode.Encryption) (A := A) - simp_all[symKeys, invKey_eq] +@[simp] +lemma priK_neq_symK {b : KeyMode} {A : Agent} {h : K ∈ symKeys} : + privateKey b A ≠ K +:= by + intro h₁; have h₂ := not_symKeys_priK (b := b) (A := A); simp_all +@[simp] +lemma symK_neq_pubK {b : KeyMode} {A : Agent} {h : K ∈ symKeys} : + K ≠ publicKey b A +:= by intro h₁; aapply pubK_neq_symK; simp_all + +@[simp] +lemma symK_neq_priK {b : KeyMode} {A : Agent} {h : K ∈ symKeys} : + K ≠ privateKey b A +:= by intro h₁; aapply priK_neq_symK; simp_all + +omit [AgentKeys] in lemma symKeys_neq_imp_neq : ((K ∈ symKeys) ≠ (K' ∈ symKeys)) → K ≠ K' := by intro h eq rw[eq] at h contradiction +omit [AgentKeys] in @[simp] lemma symKeys_invKey_iff : (invKey K ∈ symKeys) = (K ∈ symKeys) := by simp [symKeys, invKey_eq] +omit [AgentKeys] in lemma analz_symKeys_Decrypt : Msg.Crypt K X ∈ analz H → K ∈ symKeys → Msg.Key K ∈ analz H → X ∈ analz H := by simp [symKeys] @@ -92,11 +131,11 @@ lemma analz_symKeys_Decrypt : -- "Image" equations that hold for injective functions +omit [AgentKeys] in @[simp] lemma invKey_image_eq : (invKey x ∈ invKey '' A) ↔ (x ∈ A) := by simp [Set.mem_image] -omit [InvKey] in @[simp] lemma publicKey_image_eq : (publicKey b x ∈ publicKey c '' AA) ↔ (b = c ∧ x ∈ AA) := by @@ -117,17 +156,6 @@ lemma publicKey_notin_image_privateKey : publicKey b A ∉ invKey '' ( publicKey c '' AS ) := by simp [privateKey_neq_publicKey] --- Symmetric Keys --- For some protocols, it is convenient to equip agents with symmetric as --- well as asymmetric keys. The theory ‹Shared› assumes that all keys --- are symmetric. -axiom shrK : Agent → Key - -axiom inj_shrK : Function.Injective shrK - --- All shared keys are symmetric -axiom sym_shrK : ∀ {A : Agent}, shrK A ∈ symKeys - -- Injectiveness: Agents' long-term keys are distinct. @[simp] lemma invKey_shrK : @@ -139,8 +167,8 @@ lemma analz_shrK_Decrypt : by intro _ _ aapply analz.decrypt; rw[invKey_shrK]; assumption - - + +omit [AgentKeys] in lemma analz_Decrypt' : Msg.Crypt K X ∈ analz H → K ∈ symKeys → Msg.Key K ∈ analz H → X ∈ analz H := by intro _ _ _ @@ -189,7 +217,6 @@ lemma shrK_notin_image_privateKey : shrK x ∉ (invKey '' ((publicKey b) '' AA )) := by simp -omit [InvKey] in @[simp] lemma shrK_image_eq : (shrK x ∈ shrK '' AA) ↔ (x ∈ AA) := by grind[inj_shrK] @@ -199,7 +226,6 @@ attribute [simp] invKey_K variable [Bad] open Bad -- Fill in definition for Initial States of Agents -@[simp] instance : HasInitState Agent where initState | Agent.Server => @@ -226,7 +252,7 @@ lemma used_parts_subset_parts : simp[used]; intro A h₁ X h₂; simp; exists A cases A all_goals ( - simp_all[-parts_union] + simp_all[-parts_union, initState] apply_rules [parts_trans, h₂, Set.singleton_subset_iff.mpr] ) | cons e evs ih => @@ -260,6 +286,12 @@ lemma keysFor_parts_initState {C : Agent} : keysFor (parts (initState C)) = ∅ := by cases C <;> simp[initState, keysFor] + +@[simp] +lemma keysFor_used_empty : + keysFor (used []) = ∅ +:= by + rw[used, keysFor_iunion]; simp; lemma Crypt_notin_initState {B : Agent} : Msg.Crypt K X ∉ parts ( initState B ) := by @@ -268,7 +300,7 @@ lemma Crypt_notin_initState {B : Agent} : @[simp] lemma Crypt_notin_used_empty : Msg.Crypt K X ∉ used [] := by - simp[used]; intro A; cases A <;> simp + simp[used]; intro A; cases A <;> simp[initState] -- Basic properties of shrK @@ -339,7 +371,7 @@ lemma publicKey_in_initState {b : KeyMode} {A : Agent} {B : Agent} : @[simp] lemma spies_pubK : Msg.Key (publicKey b A) ∈ spies evs := by induction evs with - | nil => simp [spies, knows] + | nil => simp [spies, knows, initState] cases b <;> tauto | cons e evs ih => cases e <;> rw [spies] <;> apply knows_subset_knows_Cons <;> assumption @@ -352,14 +384,14 @@ lemma analz_spies_pubK : Msg.Key (publicKey b A) ∈ analz (spies evs) := by @[grind .] lemma Spy_spies_bad_privateKey { h : A ∈ bad } : Msg.Key (privateKey b A) ∈ spies evs := by induction evs with - | nil => simp_all [spies, knows, pubSK, pubEK]; cases b <;> tauto + | nil => simp_all [spies, knows, initState]; cases b <;> tauto | cons e evs ih => cases e <;> rw[spies] <;> aapply knows_subset_knows_Cons -- Spy sees long-term shared keys of bad agents lemma Spy_spies_bad_shrK {h : A ∈ bad} : Msg.Key (shrK A) ∈ spies evs := by induction evs with - | nil => simp [spies, knows]; exists A + | nil => simp [spies, knows, initState]; exists A | cons e evs ih => cases e <;> rw [spies] <;> aapply knows_subset_knows_Cons @@ -374,6 +406,19 @@ lemma privateKey_into_used : Msg.Key (privateKey b A) ∈ used evs := by aapply initState_into_used apply parts_increasing exact priK_in_initState + +@[simp] +lemma shrK_into_used: Msg.Key (shrK A) ∈ used evs := by + aapply initState_into_used + apply parts_increasing + exact shrK_in_initState + +@[grind .] +lemma analz_priK_Decrypt : + Msg.Crypt (priSK A) X ∈ analz (spies evs) → X ∈ analz (spies evs) := +by + intro h; aapply analz.decrypt + simp[priSK, privateKey, invKey_spec] -- For case analysis on whether or not an agent is compromised lemma Crypt_Spy_analz_bad : @@ -396,6 +441,35 @@ lemma Crypt_synth_analz_pubK : (Msg.Crypt (pubEK A) X ∈ (analz (spies evs)) ∨ ( X ∈ synth (analz (spies evs)))) := by simp[Crypt_synth_EK]; +@[simp] +lemma Crypt_synth_priK : + (Msg.Crypt (priSK A) X ∈ synth (spies evs)) ↔ + (Msg.Crypt (priSK A) X ∈ spies evs ∨ + (Msg.Key (priSK A) ∈ spies evs ∧ X ∈ synth (spies evs))) := +by simp[Crypt_synth_EK] + +@[simp] +lemma Crypt_synth_analz_priK : + (Msg.Crypt (priSK A) X ∈ synth (analz (spies evs))) ↔ + (Msg.Crypt (priSK A) X ∈ analz (spies evs) ∨ + (Msg.Key (priSK A) ∈ analz (spies evs) ∧ X ∈ synth (analz (spies evs)))) := +by simp[Crypt_synth_EK]; + +@[grind .] +lemma Crypt_synth_analz_priK_decrypt : + (Msg.Crypt (priSK A) X ∈ synth (analz (spies evs))) → + (X ∈ analz (spies evs) ∨ + (Msg.Key (priSK A) ∈ analz (spies evs) ∧ X ∈ synth (analz (spies evs)))) := +by simp[Crypt_synth_EK]; grind + +@[simp] +lemma Sign_synth_priK : + (Sign (priSK A) X ∈ synth (analz (spies evs))) ↔ + (Msg.Crypt (priSK A) X ∈ analz (spies evs) ∨ Msg.Key (priSK A) ∈ analz (spies evs)) ∧ + X ∈ synth (analz (spies evs)) +:= by + simp[Sign, Crypt_synth_EK]; grind + @[simp] lemma Nonce_notin_initState {B : Agent} : Msg.Nonce N ∉ parts (initState B) := by cases B <;> @@ -403,7 +477,7 @@ lemma Nonce_notin_initState {B : Agent} : Msg.Nonce N ∉ parts (initState B) := @[simp] lemma Nonce_notin_used_empty : Msg.Nonce N ∉ used [] := by - simp [used]; intro A; cases A <;> simp + simp [used, initState]; intro A; cases A <;> simp -- Supply fresh nonces for possibility theorems lemma Nonce_supply_lemma : ∃ N, ∀ n, N ≤ n → Msg.Nonce n ∉ used evs := by @@ -429,11 +503,42 @@ lemma Nonce_supply_lemma : ∃ N, ∀ n, N ≤ n → Msg.Nonce n ∉ used evs := lemma Nonce_supply1 : ∃ N, Msg.Nonce N ∉ used evs := by obtain ⟨N, h⟩ := Nonce_supply_lemma exact ⟨N, h N (le_refl N)⟩ - --- TODO is this really needed? --- lemma Nonce_supply : Msg.Nonce (Classical.some (Nonce_supply_lemma.some_spec)) ∉ used evs := by --- obtain ⟨N, h⟩ := Nonce_supply_lemma --- exact h (Classical.some (Nonce_supply_lemma.some_spec)) (le_refl _) + +lemma symK_supply_lemma : ∀ K, ∃ K' > K, + K' ∈ symKeys ∧ Msg.Key K' ∉ used evs ∪ Msg.Key '' keysFor (used evs) := +by + induction evs with + | nil => + intro K + have exK := not_surjective_shrK_symK (K := K); + rcases exK with ⟨K' , ⟨_, symK, exK⟩⟩; + exists K'; + apply And.intro + · assumption + · apply And.intro + · assumption + · simp_all[used]; intro A; cases A <;> + simp_all[initState, pubK_neq_symK, priK_neq_symK, symK_neq_priK] + rw[Eq.comm]; apply exK + | cons e evs ih => + intro K + cases e with + | Says _ _ m => + simp[used]; + obtain ⟨K₁, ks⟩ := msg_Key_supply (msg := m); + obtain ⟨K', _, _, _⟩ := ih ( K := Nat.max K₁ K); exists K'; simp_all; grind + | Notes A m => + simp[used]; + obtain ⟨K₁, ks⟩ := msg_Key_supply (msg := m); + obtain ⟨K', _, _, _⟩ := ih ( K := Nat.max K₁ K); exists K'; + apply ks at K'; by_cases h : A ∈ bad <;> simp_all <;> grind + | Gets => exact ih (K := K) + +lemma symK_supply : ∃ K ∈ symKeys, + Msg.Key K ∉ used evs ∪ Msg.Key '' keysFor (used evs) := +by + obtain ⟨K, _, _, _⟩ := symK_supply_lemma (K := 0) (evs := evs) + exists K -- Specialized Rewriting for Theorems About `analz` and Image omit [InvKey] [Bad] in @@ -445,7 +550,7 @@ omit [InvKey] [Bad] in lemma insert_Key_image : insert (Msg.Key K) (Msg.Key '' KK ∪ C) = Msg.Key '' (insert K KK) ∪ C := by rw[insert_Key_singleton, Set.image_insert_eq, Set.insert_eq, Set.union_assoc, Set.image_singleton] -omit [Bad] in +omit [Bad] [AgentKeys] in lemma Crypt_imp_keysFor : Msg.Crypt K X ∈ H → K ∈ symKeys → K ∈ keysFor H := by intro h₁ h₂ @@ -455,7 +560,7 @@ lemma Crypt_imp_keysFor : -- Lemma for the trivial direction of the if-and-only-if of the -- Session Key Compromise Theorem -omit [Bad] in +omit [Bad] [AgentKeys] in @[simp] lemma analz_image_freshK_lemma : ((Msg.Key K ∈ analz (Msg.Key '' nE ∪ H)) →