Your Name
1497 lines
47 KiB
Lean4
1497 lines
47 KiB
Lean4
import Mathlib
|
||
|
||
-- Keys are integers
|
||
abbrev Key := Nat
|
||
|
||
-- Define constants
|
||
def all_symmetric : Bool := true -- true if all keys are symmetric
|
||
|
||
-- Define the inverse of a symmetric key
|
||
def invKey : Key → Key := fun k => k -- Placeholder definition
|
||
|
||
-- Specification for invKey
|
||
axiom invKey_spec : ∀ K : Key, invKey (invKey K) = K
|
||
axiom invKey_symmetric : all_symmetric → invKey = id
|
||
|
||
-- Define the set of symmetric keys
|
||
@[grind]
|
||
def symKeys : Set Key := { K | invKey K = K }
|
||
|
||
-- Define the datatype for agents
|
||
@[grind]
|
||
inductive Agent
|
||
| Server : Agent
|
||
| Friend : Nat → Agent
|
||
| Spy : Agent
|
||
|
||
@[grind]
|
||
inductive Msg
|
||
| Agent : Agent → Msg -- Agent names
|
||
| Number : Nat → Msg -- Ordinary integers, timestamps, ...
|
||
| Nonce : Nat → Msg -- Unguessable nonces
|
||
| Key : Key → Msg -- Crypto keys
|
||
| Hash : Msg → Msg -- Hashing
|
||
| MPair : Msg → Msg → Msg -- Compound messages
|
||
| Crypt : Key → Msg → Msg -- Encryption, public- or shared-key
|
||
|
||
namespace Msg
|
||
-- Define concrete syntax for message tuples
|
||
notation "⦃" x ", " y "⦄" => MPair x y
|
||
notation "⦃" x ", " y ", " z "⦄" => MPair x (MPair y z)
|
||
end Msg
|
||
|
||
open Msg
|
||
open Agent
|
||
-- Define HPair
|
||
def HPair (X Y : Msg) : Msg :=
|
||
⦃Hash ⦃X, Y⦄, Y⦄
|
||
|
||
notation "⦃" x ", " y "⦄ₕ" => HPair x y
|
||
|
||
-- Define keysFor
|
||
@[simp]
|
||
def keysFor (H : Set Msg) : Set Key :=
|
||
invKey '' { K | ∃ X, Crypt K X ∈ H }
|
||
|
||
-- Define the inductive set `parts`
|
||
@[grind]
|
||
inductive parts (H : Set Msg) : Set Msg
|
||
| inj {X : Msg} : X ∈ H → parts H X
|
||
| fst {X Y : Msg} : ⦃X, Y⦄ ∈ parts H → parts H X
|
||
| snd {X Y : Msg} : ⦃X, Y⦄ ∈ parts H → parts H Y
|
||
| body {K : Key} {X : Msg} : Crypt K X ∈ parts H → parts H X
|
||
|
||
-- Monotonicity lemmas
|
||
|
||
/--
|
||
An `apply` tactic that also calls the assumptions
|
||
-/
|
||
syntax "aapply" term : tactic
|
||
macro_rules
|
||
|`(tactic| aapply $l:term) => `(tactic| apply $l <;> try assumption)
|
||
|
||
@[simp]
|
||
lemma parts_mono: Monotone parts := by
|
||
intro _ _ h _ a
|
||
induction a
|
||
· apply parts.inj; aapply h
|
||
· aapply parts.fst
|
||
· aapply parts.snd
|
||
· aapply parts.body
|
||
|
||
-- Equations for injective constructors
|
||
@[simp]
|
||
lemma Friend_image_eq {A : Set Nat} {x : Nat} :
|
||
((Friend x) ∈ Friend '' A) = (x ∈ A) := by
|
||
simp
|
||
|
||
@[simp]
|
||
lemma Key_image_eq {A : Set Key} {x : Key} :
|
||
(Key x ∈ Key '' A) = (x ∈ A) := by
|
||
simp
|
||
|
||
@[simp]
|
||
lemma Nonce_Key_image_eq {A : Set Key} {x : Nat} :
|
||
(Nonce x ∉ Key '' A) := by
|
||
simp
|
||
|
||
-- Lemma: Inverse of keys
|
||
@[simp]
|
||
lemma invKey_eq (K K' : Key) : (invKey K = invKey K') ↔ (K = K') := by
|
||
apply Iff.intro
|
||
case mp =>
|
||
intro h
|
||
rw [←invKey_spec K, ←invKey_spec K', h]
|
||
case mpr =>
|
||
intro h
|
||
rw [h]
|
||
|
||
-- Lemmas for the `keysFor` operator
|
||
@[simp]
|
||
lemma keysFor_empty : keysFor ∅ = ∅ := by
|
||
simp
|
||
|
||
@[simp]
|
||
lemma keysFor_union (H H' : Set Msg) : keysFor (H ∪ H') = keysFor H ∪ keysFor H' := by
|
||
simp
|
||
ext
|
||
constructor
|
||
· intro h; simp_all; grind
|
||
· intro h; simp_all; grind
|
||
|
||
-- Monotonicity
|
||
@[simp]
|
||
lemma keysFor_mono {G H : Set Msg} (h : G ⊆ H) : keysFor G ⊆ keysFor H := by
|
||
simp
|
||
grind
|
||
|
||
-- Lemmas for `keysFor` with specific message types
|
||
@[simp]
|
||
lemma keysFor_insert_Agent (A : Agent) (H : Set Msg) :
|
||
keysFor (insert (Agent A) H) = keysFor H := by
|
||
simp
|
||
|
||
@[simp]
|
||
lemma keysFor_insert_Nonce (N : Nat) (H : Set Msg) :
|
||
keysFor (insert (Nonce N) H) = keysFor H := by
|
||
simp
|
||
|
||
@[simp]
|
||
lemma keysFor_insert_Number (N : Nat) (H : Set Msg) :
|
||
keysFor (insert (Msg.Hash (Nonce N)) H) = keysFor H := by
|
||
simp
|
||
|
||
@[simp]
|
||
lemma keysFor_insert_Key (K : Key) (H : Set Msg) :
|
||
keysFor (insert (Key K) H) = keysFor H := by
|
||
simp
|
||
|
||
@[simp]
|
||
lemma keysFor_insert_Hash (X : Msg) (H : Set Msg) :
|
||
keysFor (insert (Hash X) H) = keysFor H := by
|
||
simp
|
||
|
||
@[simp]
|
||
lemma keysFor_insert_MPair (X Y : Msg) (H : Set Msg) :
|
||
keysFor (insert ⦃X, Y⦄ H) = keysFor H := by
|
||
simp
|
||
|
||
@[simp]
|
||
lemma keysFor_insert_Crypt (K : Key) (X : Msg) (H : Set Msg) :
|
||
keysFor (insert (Crypt K X) H) = insert (invKey K) (keysFor H) := by
|
||
simp[insert,Set.insert,invKey]
|
||
ext
|
||
grind
|
||
|
||
@[simp]
|
||
lemma keysFor_image_Key (E : Set Key) : keysFor (Key '' E) = ∅ := by
|
||
simp
|
||
|
||
@[simp]
|
||
lemma Crypt_imp_invKey_keysFor (K : Key) (X : Msg) (H : Set Msg) :
|
||
Crypt K X ∈ H → invKey K ∈ keysFor H := by
|
||
intro h
|
||
simp
|
||
exact ⟨_, h⟩
|
||
|
||
-- MPair_parts lemma
|
||
@[simp]
|
||
lemma MPair_parts {H : Set Msg} {X Y : Msg} { P : Prop} :
|
||
⦃X, Y⦄ ∈ parts H → (parts H X → parts H Y → P) → P :=
|
||
by
|
||
grind
|
||
|
||
-- parts_increasing lemma
|
||
@[simp]
|
||
lemma parts_increasing {H : Set Msg} : H ⊆ parts H :=
|
||
λ _ hx => parts.inj hx
|
||
|
||
-- parts_empty_aux lemma
|
||
@[simp]
|
||
lemma parts_empty_aux {X : Msg} : parts ∅ X → False :=
|
||
by
|
||
intro h
|
||
induction h <;> assumption
|
||
|
||
-- parts_empty lemma
|
||
@[simp]
|
||
lemma parts_empty : parts ∅ = ∅ :=
|
||
Set.eq_empty_of_forall_notMem @parts_empty_aux
|
||
|
||
-- parts_emptyE lemma
|
||
lemma parts_emptyE {X : Msg} {P: Prop} : X ∈ parts ∅ → P :=
|
||
λ h => False.elim (parts_empty_aux h)
|
||
|
||
-- parts_singleton lemma
|
||
lemma parts_singleton {H : Set Msg} {X : Msg} :
|
||
X ∈ parts H → ∃ Y ∈ H, X ∈ parts {Y} :=
|
||
by
|
||
intro h
|
||
induction h with
|
||
| inj h => exact ⟨_, h, parts.inj (Set.mem_singleton _)⟩
|
||
| fst _ ih => rcases ih with ⟨Z, ⟨l, r⟩⟩; exists Z; and_intros; apply l; apply parts.fst; exact r
|
||
| snd _ ih => rcases ih with ⟨Z, ⟨l, r⟩⟩; exists Z; and_intros; apply l; apply parts.snd; exact r
|
||
| body _ ih => rcases ih with ⟨Z, ⟨l, r⟩⟩; exists Z; and_intros; apply l; apply parts.body; exact r
|
||
|
||
-- parts_union lemma
|
||
@[simp]
|
||
lemma parts_union {G H : Set Msg} : parts (G ∪ H) = parts G ∪ parts H :=
|
||
by
|
||
apply Set.ext
|
||
intro X
|
||
constructor
|
||
· intro h
|
||
induction h with
|
||
| inj h => cases h with
|
||
| inl hG => exact Or.inl (parts.inj hG)
|
||
| inr hH => exact Or.inr (parts.inj hH)
|
||
| fst h ih => cases ih with
|
||
| inl hG => exact Or.inl (parts.fst hG)
|
||
| inr hH => exact Or.inr (parts.fst hH)
|
||
| snd h ih => cases ih with
|
||
| inl hG => exact Or.inl (parts.snd hG)
|
||
| inr hH => exact Or.inr (parts.snd hH)
|
||
| body h ih => cases ih with
|
||
| inl hG => exact Or.inl (parts.body hG)
|
||
| inr hH => exact Or.inr (parts.body hH)
|
||
· intro h
|
||
cases h with
|
||
| inl hG => induction hG with
|
||
| inj hG => exact parts.inj (Or.inl hG)
|
||
| fst h ih => exact parts.fst ih
|
||
| snd h ih => exact parts.snd ih
|
||
| body h ih => exact parts.body ih
|
||
| inr hH => induction hH with
|
||
| inj hH => exact parts.inj (Or.inr hH)
|
||
| fst h ih => exact parts.fst ih
|
||
| snd h ih => exact parts.snd ih
|
||
| body h ih => exact parts.body ih
|
||
|
||
-- parts_insert lemma
|
||
@[simp]
|
||
lemma parts_insert {X : Msg} {H : Set Msg} :
|
||
parts (insert X H) = parts {X} ∪ parts H :=
|
||
by
|
||
rw [Set.insert_eq, parts_union]
|
||
|
||
-- parts_insert2 lemma
|
||
@[simp]
|
||
lemma parts_insert2 {X Y : Msg} {H : Set Msg} :
|
||
parts (insert X (insert Y H)) = parts {X} ∪ parts {Y} ∪ parts H :=
|
||
by
|
||
rw [Set.insert_eq, Set.insert_eq, parts_union, parts_union]
|
||
grind
|
||
|
||
-- parts_image lemma
|
||
@[simp]
|
||
lemma parts_image {f : Msg → Msg} {A : Set Msg} :
|
||
parts (f '' A) = ⋃ x ∈ A, parts {f x} :=
|
||
by
|
||
apply Set.ext
|
||
intro X
|
||
constructor
|
||
· intro h
|
||
induction h with
|
||
| inj h => rcases h with ⟨a, ha, rfl⟩; exact Set.mem_biUnion ha (parts.inj (Set.mem_singleton _))
|
||
| fst _ ih => simp_all; rcases ih with ⟨W, ⟨_, r⟩⟩; apply parts.fst at r; exists W;
|
||
| snd _ ih => simp_all; rcases ih with ⟨W, ⟨_, r⟩⟩; apply parts.snd at r; exists W;
|
||
| body _ ih => simp_all; rcases ih with ⟨K, ⟨_, r⟩⟩; apply parts.body at r; exists K;
|
||
· intro h
|
||
simp_all
|
||
rcases h with ⟨W, ⟨_, r⟩⟩; induction r with
|
||
| inj a => simp_all; apply parts.inj; exists W;
|
||
| fst _ ih => exact parts.fst ih
|
||
| snd _ ih => exact parts.snd ih
|
||
| body _ ih => exact parts.body ih
|
||
|
||
-- parts_insert_subset lemma
|
||
@[simp]
|
||
lemma parts_insert_subset {X : Msg} {H : Set Msg} :
|
||
insert X (parts H) ⊆ parts (insert X H) :=
|
||
by
|
||
intro x hx
|
||
cases hx with
|
||
| inl h => simp_all; left; apply parts.inj; simp;
|
||
| inr h => induction h with
|
||
| inj h => exact parts.inj (Set.mem_insert_of_mem _ h)
|
||
| fst h ih => exact parts.fst ih
|
||
| snd h ih => exact parts.snd ih
|
||
| body h ih => exact parts.body ih
|
||
|
||
|
||
-- Idempotence and transitivity lemmas for `parts`
|
||
@[simp]
|
||
lemma parts_partsD {H : Set Msg} : parts (parts H) ⊆ parts H :=
|
||
by
|
||
intro x h
|
||
induction h
|
||
· assumption
|
||
· aapply parts.fst
|
||
· aapply parts.snd
|
||
· aapply parts.body
|
||
|
||
abbrev partsClosureOperator : ClosureOperator (Set Msg) :=
|
||
ClosureOperator.mk' parts parts_mono @parts_increasing @parts_partsD
|
||
|
||
@[simp]
|
||
lemma parts_idem {H : Set Msg} : parts (parts H) = parts H :=
|
||
by apply partsClosureOperator.idempotent
|
||
|
||
@[simp]
|
||
lemma parts_subset_iff {G H : Set Msg} : (G ⊆ parts H) ↔ (parts G ⊆ parts H) :=
|
||
by apply partsClosureOperator.le_closure_iff
|
||
|
||
@[simp, grind]
|
||
lemma parts_trans {G H : Set Msg} {X : Msg} :
|
||
X ∈ parts G → G ⊆ parts H → X ∈ parts H :=
|
||
by intro a b; apply parts_mono at b; rw[parts_idem] at b; apply b; apply a;
|
||
|
||
-- Cut lemma
|
||
@[simp]
|
||
lemma parts_cut {G H : Set Msg} {X Y : Msg} :
|
||
Y ∈ parts (insert X G) → X ∈ parts H → Y ∈ parts (G ∪ H) :=
|
||
by
|
||
intro a b; rw[parts_union]; rw[parts_insert] at a; cases a <;> grind
|
||
|
||
-- Rewrite rules for pulling out atomic messages
|
||
|
||
@[simp]
|
||
lemma parts_insert_Agent {H : Set Msg} {agt : Agent} :
|
||
parts (insert (Agent agt) H) = insert (Agent agt) (parts H) :=
|
||
by
|
||
ext
|
||
constructor
|
||
· intro h; rw[parts_insert] at h; cases h with
|
||
| inl h => induction h with
|
||
| inj => simp_all
|
||
| fst _ a_ih => cases a_ih; contradiction; right; aapply parts.fst
|
||
| snd _ a_ih => cases a_ih; contradiction; right; aapply parts.snd
|
||
| body _ a_ih => cases a_ih; contradiction; right; aapply parts.body
|
||
| inr h => right; assumption
|
||
· apply parts_insert_subset
|
||
|
||
@[simp]
|
||
lemma parts_insert_Nonce {H : Set Msg} {N : Nat} :
|
||
parts (insert (Nonce N) H) = insert (Nonce N) (parts H) :=
|
||
by
|
||
ext
|
||
constructor
|
||
· intro h; rw[parts_insert] at h; cases h with
|
||
| inl h => induction h with
|
||
| inj => simp_all
|
||
| fst _ a_ih => cases a_ih; contradiction; right; aapply parts.fst
|
||
| snd _ a_ih => cases a_ih; contradiction; right; aapply parts.snd
|
||
| body _ a_ih => cases a_ih; contradiction; right; aapply parts.body
|
||
| inr h => right; assumption
|
||
· apply parts_insert_subset
|
||
|
||
@[simp]
|
||
lemma parts_insert_Number {H : Set Msg} {N : Nat} :
|
||
parts (insert (Number N) H) = insert (Number N) (parts H) :=
|
||
by
|
||
ext
|
||
constructor
|
||
· intro h; rw[parts_insert] at h; cases h with
|
||
| inl h => induction h with
|
||
| inj => simp_all
|
||
| fst _ a_ih => cases a_ih; contradiction; right; aapply parts.fst
|
||
| snd _ a_ih => cases a_ih; contradiction; right; aapply parts.snd
|
||
| body _ a_ih => cases a_ih; contradiction; right; aapply parts.body
|
||
| inr h => right; assumption
|
||
· apply parts_insert_subset
|
||
|
||
@[simp]
|
||
lemma parts_insert_Key {H : Set Msg} {K : Key} :
|
||
parts (insert (Key K) H) = insert (Key K) (parts H) :=
|
||
by
|
||
ext
|
||
constructor
|
||
· intro h; rw[parts_insert] at h; cases h with
|
||
| inl h => induction h with
|
||
| inj => simp_all
|
||
| fst _ a_ih => cases a_ih; contradiction; right; aapply parts.fst
|
||
| snd _ a_ih => cases a_ih; contradiction; right; aapply parts.snd
|
||
| body _ a_ih => cases a_ih; contradiction; right; aapply parts.body
|
||
| inr h => right; assumption
|
||
· apply parts_insert_subset
|
||
|
||
@[simp]
|
||
lemma parts_insert_Hash {H : Set Msg} {X : Msg} :
|
||
parts (insert (Hash X) H) = insert (Hash X) (parts H) :=
|
||
by
|
||
ext
|
||
constructor
|
||
· intro h; rw[parts_insert] at h; cases h with
|
||
| inl h => induction h with
|
||
| inj => simp_all
|
||
| fst _ a_ih => cases a_ih; contradiction; right; aapply parts.fst
|
||
| snd _ a_ih => cases a_ih; contradiction; right; aapply parts.snd
|
||
| body _ a_ih => cases a_ih; contradiction; right; aapply parts.body
|
||
| inr h => right; assumption
|
||
· apply parts_insert_subset
|
||
|
||
@[simp]
|
||
lemma parts_insert_Crypt {H : Set Msg} {K : Key} {X : Msg} :
|
||
parts (insert (Crypt K X) H) = insert (Crypt K X) (parts (insert X H)) :=
|
||
by
|
||
ext x
|
||
constructor
|
||
· intro h; rw[parts_insert] at h; cases h with
|
||
| inl h => induction h with
|
||
| inj => left; assumption;
|
||
| fst _ a_ih => cases a_ih; contradiction; right; aapply parts.fst
|
||
| snd _ a_ih => cases a_ih; contradiction; right; aapply parts.snd
|
||
| body _ a_ih => cases a_ih with
|
||
| inl => simp_all; right; left; apply parts_increasing; trivial;
|
||
| inr h => apply parts.body at h; right; exact h;
|
||
| inr => right; simp; right; assumption;
|
||
· intro h; cases h with
|
||
| inl => apply parts.inj; left; assumption
|
||
| inr h =>
|
||
apply (parts_cut (G := H) (H := {Crypt K X}) (X := X) (Y := x)) at h
|
||
rw[←Set.singleton_union, Set.union_comm]
|
||
apply h
|
||
apply parts.body (K := K) (X := X)
|
||
apply parts.inj
|
||
trivial
|
||
|
||
@[simp]
|
||
lemma parts_insert_MPair {H: Set Msg} {X Y : Msg} :
|
||
parts (insert ⦃X, Y⦄ H) = insert ⦃X, Y⦄ (parts (insert X (insert Y H))) :=
|
||
by
|
||
ext x
|
||
constructor;
|
||
· intro h; rw[parts_insert] at h; cases h with
|
||
| inl h => induction h with
|
||
| inj => simp_all;
|
||
| @fst A B _ a_ih => cases a_ih with
|
||
| inl h => cases h; right; apply parts.inj; left; trivial
|
||
| inr h => right; aapply parts.fst;
|
||
| @snd A B _ a_ih => cases a_ih with
|
||
| inl h => cases h; right; apply parts.inj; right; left; trivial;
|
||
| inr h => right; aapply parts.snd;
|
||
| body _ a_ih => cases a_ih; contradiction; right; aapply parts.body
|
||
| inr h => simp; right; right; right; assumption;
|
||
· intro h; cases h with
|
||
| inl => rw[parts_insert]; left; apply parts.inj; assumption;
|
||
| inr h => simp_all; cases h with
|
||
| inl h =>
|
||
left;
|
||
apply parts_trans ( H := {⦃X, Y⦄}) at h;
|
||
simp at h;
|
||
apply h;
|
||
apply parts.fst;
|
||
apply parts.inj;
|
||
trivial;
|
||
| inr h => cases h with
|
||
| inl h =>
|
||
left;
|
||
apply parts_trans ( H := {⦃X, Y⦄}) at h;
|
||
simp at h;
|
||
apply h;
|
||
apply parts.snd;
|
||
apply parts.inj;
|
||
trivial;
|
||
| inr => right; assumption;
|
||
|
||
@[simp]
|
||
lemma parts_image_Key {N : Set Key} : parts (Key '' N) = Key '' N :=
|
||
by
|
||
ext
|
||
constructor
|
||
· intro a; simp; induction a <;> simp_all;
|
||
· simp; intro y _ _; apply parts.inj; simp; exists y;
|
||
|
||
-- In any message, there is an upper bound N on its greatest nonce.
|
||
lemma msg_Nonce_supply {msg : Msg} : ∃ N, ∀ n, N ≤ n → Nonce n ∉ 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 n.succ;
|
||
intro _ _ _;
|
||
have ins_nonce := parts_insert_Nonce (H := {}) (N := n);
|
||
simp_all;
|
||
| Key k => exists 0;
|
||
have ins_key := parts_insert_Key (H := {}) (K := k);
|
||
simp_all;
|
||
| 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₁ h₂;
|
||
have ins_mpair := parts_insert_MPair (H := {}) (X := X) (Y := Y);
|
||
simp_all;
|
||
| Crypt K X ih => rcases ih with ⟨N, h⟩; exists N;
|
||
have ins_crypt := parts_insert_Crypt (H := {}) (K := K) (X := X);
|
||
simp_all;
|
||
|
||
-- Inductive relation "analz"
|
||
inductive analz (H : Set Msg) : Set Msg
|
||
| inj {X : Msg} : X ∈ H → analz H X
|
||
| fst {X Y : Msg} : ⦃X, Y⦄ ∈ analz H → analz H X
|
||
| snd {X Y : Msg} : ⦃X, Y⦄ ∈ analz H → analz H Y
|
||
| decrypt {K : Key} {X : Msg} :
|
||
Crypt K X ∈ analz H → Key (invKey K) ∈ analz H → analz H X
|
||
|
||
-- Monotonicity
|
||
lemma analz_mono : Monotone analz :=
|
||
by
|
||
intro A B h₁ X h₂
|
||
induction h₂ with
|
||
| inj h => exact analz.inj (h₁ h)
|
||
| fst h ih => exact analz.fst ih
|
||
| snd h ih => exact analz.snd ih
|
||
| decrypt h₁ h₂ ih₁ ih₂ => exact analz.decrypt ih₁ ih₂
|
||
|
||
-- Making it safe speeds up proofs
|
||
@[simp]
|
||
lemma MPair_analz {H : Set Msg} {X Y : Msg} {P : Prop} :
|
||
⦃X, Y⦄ ∈ analz H → (analz H X → analz H Y → P) → P :=
|
||
by
|
||
intro h ih
|
||
apply ih
|
||
· apply analz.fst h
|
||
· apply analz.snd h
|
||
|
||
@[simp]
|
||
lemma analz_increasing {H : Set Msg} : H ⊆ analz H :=
|
||
λ _ hx => analz.inj hx
|
||
|
||
lemma analz_into_parts {H : Set Msg} {X : Msg} : X ∈ analz H → X ∈ parts H :=
|
||
by
|
||
intro h
|
||
induction h with
|
||
| inj h => aapply parts.inj
|
||
| fst _ ih => aapply parts.fst
|
||
| snd _ ih => aapply parts.snd
|
||
| decrypt _ _ ih₁ => aapply parts.body
|
||
|
||
lemma analz_subset_parts {H : Set Msg} : analz H ⊆ parts H :=
|
||
λ _ hx => analz_into_parts hx
|
||
|
||
@[simp]
|
||
lemma analz_parts {H : Set Msg} : analz (parts H) = parts H :=
|
||
by
|
||
ext X; constructor
|
||
· intro h; induction h with
|
||
| inj => assumption;
|
||
| fst => aapply parts.fst;
|
||
| snd => aapply parts.snd;
|
||
| decrypt => aapply parts.body;
|
||
· apply analz_increasing;
|
||
|
||
lemma not_parts_not_analz {H : Set Msg} {X : Msg} :
|
||
X ∉ parts H → X ∉ analz H :=
|
||
λ h₁ h₂ => h₁ (analz_into_parts h₂)
|
||
|
||
@[simp]
|
||
lemma parts_analz {H : Set Msg} : parts (analz H) = parts H :=
|
||
by
|
||
ext; constructor;
|
||
· intro h; induction h with
|
||
| inj => aapply analz_subset_parts
|
||
| fst => aapply parts.fst
|
||
| snd => aapply parts.snd
|
||
| body => aapply parts.body
|
||
· apply parts_mono; apply analz_increasing;
|
||
|
||
@[simp]
|
||
lemma analz_insertI {X : Msg} {H : Set Msg} :
|
||
insert X (analz H) ⊆ analz (insert X H) :=
|
||
by
|
||
intro x hx
|
||
cases hx with
|
||
| inl h => apply analz.inj; left; assumption;
|
||
| inr h => exact analz_mono (Set.subset_insert _ _) h
|
||
|
||
-- General equational properties
|
||
|
||
@[simp]
|
||
lemma analz_empty : analz ∅ = ∅ :=
|
||
by
|
||
ext; constructor;
|
||
· intro h; induction h <;> contradiction;
|
||
· apply analz_increasing
|
||
|
||
|
||
@[simp]
|
||
lemma analz_union {G H : Set Msg} : analz G ∪ analz H ⊆ analz (G ∪ H) :=
|
||
by
|
||
intro x hx
|
||
cases hx with
|
||
| inl hG => exact analz_mono (Set.subset_union_left) hG;
|
||
| inr hH => exact analz_mono (Set.subset_union_right) hH
|
||
|
||
lemma analz_insert {X : Msg} {H : Set Msg} :
|
||
insert X (analz H) ⊆ analz (insert X H) :=
|
||
by
|
||
intro x hx
|
||
cases hx with
|
||
| inl h => apply analz.inj; left; assumption
|
||
| inr h => exact analz_mono (Set.subset_insert _ _) h
|
||
|
||
-- Rewrite rules for pulling out atomic messages
|
||
|
||
@[simp]
|
||
lemma analz_insert_Agent {H : Set Msg} {agt : Agent} :
|
||
analz (insert (Agent agt) H) = insert (Agent agt) (analz H) :=
|
||
by
|
||
ext
|
||
constructor
|
||
· intro h
|
||
induction h with
|
||
| inj h => cases h with
|
||
| inl h => exact Or.inl h
|
||
| inr h => exact Or.inr (analz.inj h)
|
||
| fst _ ih => right; cases ih; contradiction; aapply analz.fst;
|
||
| snd _ ih => right; cases ih; contradiction; aapply analz.snd;
|
||
| decrypt _ _ ih₁ ih₂ => right; cases ih₁; contradiction;
|
||
cases ih₂; contradiction;
|
||
aapply analz.decrypt;
|
||
· apply analz_insert
|
||
|
||
@[simp]
|
||
lemma analz_insert_Nonce {H : Set Msg} {N : Nat} :
|
||
analz (insert (Nonce N) H) = insert (Nonce N) (analz H) :=
|
||
by
|
||
ext
|
||
constructor
|
||
· intro h
|
||
induction h with
|
||
| inj h => cases h with
|
||
| inl h => exact Or.inl h
|
||
| inr h => exact Or.inr (analz.inj h)
|
||
| fst _ ih => right; cases ih; contradiction; aapply analz.fst;
|
||
| snd _ ih => right; cases ih; contradiction; aapply analz.snd;
|
||
| decrypt _ _ ih₁ ih₂ => right; cases ih₁; contradiction;
|
||
cases ih₂; contradiction;
|
||
aapply analz.decrypt;
|
||
· apply analz_insert
|
||
|
||
@[simp]
|
||
lemma analz_insert_Number {H : Set Msg} {N : Nat} :
|
||
analz (insert (Number N) H) = insert (Number N) (analz H) :=
|
||
by
|
||
ext
|
||
constructor
|
||
· intro h
|
||
induction h with
|
||
| inj h => cases h with
|
||
| inl h => exact Or.inl h
|
||
| inr h => exact Or.inr (analz.inj h)
|
||
| fst _ ih => right; cases ih; contradiction; aapply analz.fst;
|
||
| snd _ ih => right; cases ih; contradiction; aapply analz.snd;
|
||
| decrypt _ _ ih₁ ih₂ => right; cases ih₁; contradiction;
|
||
cases ih₂; contradiction;
|
||
aapply analz.decrypt;
|
||
· apply analz_insert
|
||
|
||
@[simp]
|
||
lemma analz_insert_Hash {H : Set Msg} {X : Msg} :
|
||
analz (insert (Hash X) H) = insert (Hash X) (analz H) :=
|
||
by
|
||
ext
|
||
constructor
|
||
· intro h
|
||
induction h with
|
||
| inj h => cases h with
|
||
| inl h => exact Or.inl h
|
||
| inr h => exact Or.inr (analz.inj h)
|
||
| fst _ ih => right; cases ih; contradiction; aapply analz.fst;
|
||
| snd _ ih => right; cases ih; contradiction; aapply analz.snd;
|
||
| decrypt _ _ ih₁ ih₂ => right; cases ih₁; contradiction;
|
||
cases ih₂; contradiction;
|
||
aapply analz.decrypt;
|
||
· apply analz_insert
|
||
|
||
@[simp]
|
||
lemma analz_insert_Key {H : Set Msg} {K : Key} :
|
||
K ∉ keysFor (analz H) →
|
||
analz (insert (Key K) H) = insert (Key K) (analz H) :=
|
||
by
|
||
intro hK
|
||
ext x
|
||
constructor
|
||
· intro h
|
||
induction h with
|
||
| inj h => cases h with
|
||
| inl h => exact Or.inl h
|
||
| inr h => exact Or.inr (analz.inj h)
|
||
| fst _ ih => right; cases ih; contradiction; aapply analz.fst;
|
||
| snd _ ih => right; cases ih; contradiction; aapply analz.snd;
|
||
| @decrypt _ _ _ _ ih₁ ih₂ =>
|
||
right
|
||
cases ih₂ with
|
||
| inl h => simp at h; simp at ih₁; apply Crypt_imp_invKey_keysFor at ih₁
|
||
rw[h] at ih₁; contradiction;
|
||
| inr => cases ih₁; simp_all; aapply analz.decrypt
|
||
· apply analz_insert
|
||
|
||
@[simp]
|
||
lemma analz_insert_MPair {H : Set Msg} {X Y : Msg} :
|
||
analz (insert ⦃X, Y⦄ H) = insert ⦃X, Y⦄ (analz (insert X (insert Y H))) :=
|
||
by
|
||
ext
|
||
constructor
|
||
· intro h
|
||
induction h with
|
||
| inj h => cases h with
|
||
| inl h => exact Or.inl h
|
||
| inr => right; apply analz.inj; right; right; assumption
|
||
| fst _ ih => right; cases ih
|
||
· simp_all; apply analz.inj; left; trivial
|
||
· aapply analz.fst
|
||
| snd _ ih => right; cases ih
|
||
· simp_all; apply analz.inj; right; left; trivial
|
||
· aapply analz.snd
|
||
| decrypt h₁ h₂ ih₁ ih₂ =>
|
||
right
|
||
cases ih₂; contradiction
|
||
cases ih₁; contradiction
|
||
aapply analz.decrypt
|
||
· intro h
|
||
cases h with
|
||
| inl => apply analz.inj; left; trivial
|
||
| inr h => induction h with
|
||
| inj a => cases a with
|
||
| inl h => apply analz.fst; apply analz.inj; left; rw[h]
|
||
| inr h => cases h with
|
||
| inl h => apply analz.snd; apply analz.inj; left; rw[h]
|
||
| inr => apply analz.inj; right; assumption
|
||
| fst => aapply analz.fst
|
||
| snd => aapply analz.snd
|
||
| decrypt => aapply analz.decrypt
|
||
|
||
lemma analz_insert_Decrypt {H : Set Msg} {K : Key} {X : Msg} :
|
||
Key (invKey K) ∈ analz H →
|
||
analz (insert (Crypt K X) H) = insert (Crypt K X) (analz (insert X H)) :=
|
||
by
|
||
intro
|
||
ext
|
||
constructor
|
||
· intro h
|
||
induction h with
|
||
| inj h => cases h with
|
||
| inl => left; assumption;
|
||
| inr => right; apply analz.inj; right; assumption
|
||
| fst _ ih => right; cases ih; contradiction; aapply analz.fst
|
||
| snd _ ih => right; cases ih; contradiction; aapply analz.snd
|
||
| decrypt _ _ ih₁ ih₂ => cases ih₁ with
|
||
| inl h => right; apply analz.inj; left; simp_all
|
||
| inr => right; cases ih₂; contradiction; aapply analz.decrypt
|
||
· intro h
|
||
cases h with
|
||
| inl h => apply analz.inj; left; assumption
|
||
| inr h => induction h with
|
||
| inj a => cases a with
|
||
| inl h => apply analz.decrypt; apply analz.inj; left; rw[h]
|
||
apply analz_mono; apply Set.subset_insert; assumption
|
||
| inr => apply analz.inj; right; assumption
|
||
| fst => aapply analz.fst
|
||
| snd => aapply analz.snd
|
||
| decrypt => aapply analz.decrypt
|
||
|
||
-- TODO split into two lemmata
|
||
@[simp]
|
||
lemma analz_Crypt {H : Set Msg} {K : Key} {X : Msg} :
|
||
(Key (invKey K) ∉ analz H) →
|
||
(analz (insert (Crypt K X) H) = insert (Crypt K X) (analz H)) :=
|
||
by
|
||
intro h
|
||
ext
|
||
constructor
|
||
· intro a; induction a with
|
||
| inj a => cases a; left; assumption; right; aapply analz.inj
|
||
| fst _ a_ih => cases a_ih; contradiction; right; aapply analz.fst
|
||
| snd _ a_ih => cases a_ih; contradiction; right; aapply analz.snd
|
||
| decrypt h₁ h₂ ih₁ ih₂ =>
|
||
cases ih₂; contradiction
|
||
cases ih₁; simp_all; right; aapply analz.decrypt
|
||
· intro a; cases a with
|
||
| inl => apply analz.inj; left; assumption
|
||
| inr => apply analz_mono; apply Set.subset_insert; assumption
|
||
|
||
-- This rule supposes "for the sake of argument" that we have the key.
|
||
lemma analz_insert_Crypt_subset {H : Set Msg} {K : Key} {X : Msg} :
|
||
analz (insert (Crypt K X) H) ⊆ insert (Crypt K X) (analz (insert X H)) :=
|
||
by
|
||
intro Y h
|
||
induction h with
|
||
| inj h => cases h with
|
||
| inl => left; assumption
|
||
| inr => right; apply analz.inj; right; assumption
|
||
| fst _ ih => right; cases ih; contradiction; aapply analz.fst
|
||
| snd _ ih => right; cases ih; contradiction; aapply analz.snd
|
||
| decrypt _ _ ih₁ ih₂ =>
|
||
right
|
||
cases ih₂; contradiction
|
||
cases ih₁ with
|
||
| inl => simp_all; apply analz.inj; left; trivial
|
||
| inr => aapply analz.decrypt
|
||
|
||
@[simp]
|
||
lemma analz_image_Key {N : Set Key} : analz (Key '' N) = Key '' N :=
|
||
by
|
||
apply Set.ext
|
||
intro X
|
||
constructor
|
||
· intro h
|
||
induction h <;> simp_all
|
||
· intro h
|
||
rcases h with ⟨k, hk, rfl⟩
|
||
exact analz.inj ⟨k, hk, rfl⟩
|
||
|
||
-- Idempotence and transitivity
|
||
|
||
@[simp]
|
||
lemma analz_analzD {H : Set Msg} {X : Msg} : X ∈ analz (analz H) → X ∈ analz H :=
|
||
by
|
||
intro h
|
||
induction h with
|
||
| inj h => exact h
|
||
| fst h ih => exact analz.fst ih
|
||
| snd h ih => exact analz.snd ih
|
||
| decrypt h₁ h₂ ih₁ ih₂ => exact analz.decrypt ih₁ ih₂
|
||
|
||
abbrev analzClosureOperator : ClosureOperator (Set Msg) :=
|
||
ClosureOperator.mk' analz analz_mono @analz_increasing @analz_analzD
|
||
|
||
@[simp]
|
||
lemma analz_idem {H : Set Msg} : analz (analz H) = analz H :=
|
||
by apply analzClosureOperator.idempotent
|
||
|
||
@[simp]
|
||
lemma analz_subset_iff {G H : Set Msg} : (G ⊆ analz H) ↔ (analz G ⊆ analz H) :=
|
||
by apply analzClosureOperator.le_closure_iff
|
||
|
||
@[simp]
|
||
lemma analz_trans {G H : Set Msg} {X : Msg} :
|
||
X ∈ analz G → G ⊆ analz H → X ∈ analz H :=
|
||
by
|
||
intro hG hGH
|
||
apply analz_mono at hGH; rw [ analz_idem ] at hGH; apply hGH; assumption;
|
||
|
||
-- Cut; Lemma 2 of Lowe
|
||
@[simp]
|
||
lemma analz_cut {H : Set Msg} {X Y : Msg} :
|
||
Y ∈ analz (insert X H) → X ∈ analz H → Y ∈ analz H :=
|
||
by
|
||
intro hY _
|
||
apply analz_trans; apply hY
|
||
intro a h; cases h; simp_all; aapply analz.inj
|
||
|
||
-- Simplification of messages involving forwarding of unknown components
|
||
@[simp]
|
||
lemma analz_insert_eq {H : Set Msg} {X : Msg} :
|
||
X ∈ analz H → analz (insert X H) = analz H :=
|
||
by
|
||
intro
|
||
ext
|
||
constructor
|
||
· intro; aapply analz_cut
|
||
· apply analz_mono; apply Set.subset_insert
|
||
|
||
-- A congruence rule for "analz"
|
||
@[simp]
|
||
lemma analz_subset_cong {G G' H H' : Set Msg} :
|
||
analz G ⊆ analz G' → analz H ⊆ analz H' → analz (G ∪ H) ⊆ analz (G' ∪ H') :=
|
||
by
|
||
intro hG hH
|
||
have a_sub := analz_subset_iff (G := G ∪ H) (H := G' ∪ H')
|
||
apply a_sub.mp
|
||
apply subset_trans (b := analz G ∪ analz H)
|
||
apply Set.union_subset_union (h₁ := @analz_increasing (H := G)) (h₂ := @analz_increasing (H := H))
|
||
apply subset_trans (b := analz G' ∪ analz H')
|
||
apply Set.union_subset_union (h₁ := hG) (h₂ := hH)
|
||
apply analz_union
|
||
|
||
lemma analz_cong {G G' H H' : Set Msg} :
|
||
analz G = analz G' → analz H = analz H' → analz (G ∪ H) = analz (G' ∪ H') :=
|
||
by
|
||
intro hG hH
|
||
ext
|
||
constructor
|
||
· apply analz_subset_cong; aapply Eq.subset; aapply Eq.subset
|
||
· apply analz_subset_cong; rw[Eq.comm] at hG; aapply Eq.subset; rw[Eq.comm] at hH; aapply Eq.subset
|
||
|
||
|
||
lemma analz_insert_cong {H H' : Set Msg} {X : Msg} :
|
||
analz H = analz H' → analz (insert X H) = analz (insert X H') :=
|
||
by
|
||
intro hH
|
||
rw [Set.insert_eq, Set.insert_eq]
|
||
exact analz_cong rfl hH
|
||
|
||
-- If there are no pairs or encryptions, then analz does nothing
|
||
lemma analz_trivial {H : Set Msg} :
|
||
(∀ X Y, ⦃X, Y⦄ ∉ H) → (∀ X K, Crypt K X ∉ H) → analz H = H :=
|
||
by
|
||
intro hPairs hCrypts
|
||
apply Set.ext
|
||
intro X
|
||
constructor
|
||
· intro h
|
||
induction h with
|
||
| inj h => exact h
|
||
| fst => simp_all
|
||
| snd => simp_all
|
||
| decrypt h₁ _ _ => simp_all
|
||
· exact analz.inj
|
||
|
||
-- Inductive relation "synth"
|
||
|
||
inductive synth (H : Set Msg) : Set Msg
|
||
| inj {X : Msg} : X ∈ H → synth H X
|
||
| agent {agt : Agent} : synth H (Agent agt)
|
||
| number {n : Nat} : synth H (Number n)
|
||
| hash {X : Msg} : synth H X → synth H (Hash X)
|
||
| mpair {X Y : Msg} : synth H X → synth H Y → synth H ⦃X, Y⦄
|
||
| crypt {K : Key} {X : Msg} : synth H X → Key K ∈ H → synth H (Crypt K X)
|
||
|
||
-- Monotonicity
|
||
lemma synth_mono : Monotone synth := by
|
||
intro _ _ h _ hx
|
||
induction hx with
|
||
| inj hG => exact synth.inj (h hG)
|
||
| agent => exact synth.agent
|
||
| number => exact synth.number
|
||
| hash _ ih => exact synth.hash ih
|
||
| mpair _ _ ihX ihY => exact synth.mpair ihX ihY
|
||
| crypt => aapply synth.crypt; aapply h
|
||
|
||
-- Simplification rules for `synth`
|
||
@[simp]
|
||
lemma synth_increasing {H : Set Msg} : H ⊆ synth H :=
|
||
λ _ hx => synth.inj hx
|
||
|
||
-- Unions
|
||
lemma synth_union {G H : Set Msg} : synth G ∪ synth H ⊆ synth (G ∪ H) :=
|
||
by
|
||
intro x hx
|
||
cases hx with
|
||
| inl hG => exact synth_mono (Set.subset_union_left) hG
|
||
| inr hH => exact synth_mono (Set.subset_union_right) hH
|
||
|
||
lemma synth_insert {X : Msg} {H : Set Msg} :
|
||
insert X (synth H) ⊆ synth (insert X H) :=
|
||
by
|
||
intro x hx
|
||
cases hx with
|
||
| inl h => apply synth.inj; left; assumption
|
||
| inr h => exact synth_mono (Set.subset_insert _ _) h
|
||
|
||
-- Idempotence and transitivity
|
||
@[simp]
|
||
lemma synth_synthD {H : Set Msg} {X : Msg} : X ∈ synth (synth H) → X ∈ synth H :=
|
||
by
|
||
intro h
|
||
induction h with
|
||
| inj h => exact h
|
||
| agent => exact synth.agent
|
||
| number => exact synth.number
|
||
| hash _ ih => exact synth.hash ih
|
||
| mpair _ _ ihX ihY => exact synth.mpair ihX ihY
|
||
| crypt _ a => cases a; aapply synth.crypt;
|
||
|
||
abbrev synthClosureOperator : ClosureOperator (Set Msg) :=
|
||
ClosureOperator.mk' synth synth_mono @synth_increasing @synth_synthD
|
||
|
||
@[simp]
|
||
lemma synth_idem {H : Set Msg} : synth (synth H) = synth H :=
|
||
by apply synthClosureOperator.idempotent
|
||
|
||
@[simp]
|
||
lemma synth_subset_iff {G H : Set Msg} : (G ⊆ synth H) ↔ (synth G ⊆ synth H) :=
|
||
by apply synthClosureOperator.le_closure_iff
|
||
|
||
@[simp, grind]
|
||
lemma synth_trans {G H : Set Msg} {X : Msg} :
|
||
X ∈ synth G → G ⊆ synth H → X ∈ synth H :=
|
||
by
|
||
intro hG hGH; apply synth_mono at hGH; rw[synth_idem] at hGH; apply hGH; apply hG
|
||
|
||
-- Cut; Lemma 2 of Lowe
|
||
@[simp]
|
||
lemma synth_cut {H : Set Msg} {X Y : Msg} :
|
||
Y ∈ synth (insert X H) → X ∈ synth H → Y ∈ synth H :=
|
||
by
|
||
intro hY hX; apply synth_trans; apply hY
|
||
intro a h; cases h; simp_all; aapply synth.inj
|
||
|
||
@[simp]
|
||
lemma Crypt_synth_eq {H : Set Msg} {K : Key} {X : Msg} :
|
||
Key K ∉ H → (Crypt K X ∈ synth H ↔ Crypt K X ∈ H) :=
|
||
by
|
||
intro hK
|
||
constructor
|
||
· intro h
|
||
cases h; assumption; contradiction
|
||
· intro h
|
||
exact synth.inj h
|
||
|
||
@[simp]
|
||
lemma keysFor_synth {H : Set Msg} :
|
||
keysFor (synth H) = keysFor H ∪ invKey '' {K | Key K ∈ H} :=
|
||
by
|
||
ext K
|
||
simp
|
||
constructor
|
||
· intro h
|
||
rcases h with ⟨Y, ⟨⟨X, h⟩, _⟩⟩;
|
||
cases h with
|
||
| inj h => left; exists Y; apply And.intro; exists X; assumption
|
||
| crypt _ _ => right; exists Y
|
||
· intro h; cases h with
|
||
| inl h => cases h with
|
||
| intro Y h =>
|
||
exists Y; rcases h with ⟨⟨X, _⟩, _⟩;
|
||
apply And.intro
|
||
· exists X; aapply synth.inj
|
||
· assumption
|
||
| inr h =>
|
||
rcases h with ⟨Y, ⟨_, _⟩⟩;
|
||
exists Y; apply And.intro
|
||
· exists Number 0; aapply synth.crypt; apply synth.number
|
||
· assumption
|
||
|
||
|
||
-- Combinations of parts, analz, and synth
|
||
|
||
@[simp]
|
||
lemma parts_synth {H : Set Msg} : parts (synth H) = parts H ∪ synth H :=
|
||
by
|
||
apply Set.ext
|
||
intro X
|
||
constructor
|
||
· intro h
|
||
induction h with
|
||
| inj => right; assumption
|
||
| fst _ ih => cases ih with
|
||
| inl => left; aapply parts.fst
|
||
| inr h => cases h
|
||
· left; apply parts.fst; aapply parts.inj;
|
||
· right; assumption
|
||
| snd _ ih => cases ih with
|
||
| inl => left; aapply parts.snd
|
||
| inr h => cases h
|
||
· left; apply parts.snd; aapply parts.inj;
|
||
· right; assumption
|
||
| body h ih => cases ih with
|
||
| inl h => left; aapply parts.body
|
||
| inr h => cases h
|
||
· left; aapply parts.body; aapply parts.inj
|
||
· right; assumption
|
||
· intro h
|
||
cases h with
|
||
| inl h =>
|
||
apply parts_mono
|
||
· apply synth_increasing
|
||
· assumption
|
||
| inr h => exact parts.inj h
|
||
|
||
@[simp]
|
||
lemma analz_analz_Un {G H : Set Msg} : analz (analz G ∪ H) = analz (G ∪ H) :=
|
||
by
|
||
apply analz_cong
|
||
· exact analz_idem
|
||
· trivial
|
||
|
||
@[simp]
|
||
lemma analz_synth_Un {G H : Set Msg} : analz (synth G ∪ H) = analz (G ∪ H) ∪ synth G :=
|
||
by
|
||
ext
|
||
constructor
|
||
· intro h; induction h with
|
||
| inj a => cases a
|
||
· right; assumption
|
||
· left; apply analz.inj; right; assumption
|
||
| fst _ ih =>
|
||
cases ih with
|
||
| inl => left; aapply analz.fst
|
||
| inr h =>
|
||
cases h
|
||
· left; apply analz.fst; apply analz.inj; left; assumption
|
||
· right; assumption
|
||
| snd _ ih =>
|
||
cases ih with
|
||
| inl => left; aapply analz.snd
|
||
| inr h =>
|
||
cases h
|
||
· left; apply analz.snd; apply analz.inj; left; assumption
|
||
· right; assumption
|
||
| decrypt _ _ ih₁ ih₂ =>
|
||
cases ih₂ with
|
||
| inl => cases ih₁ with
|
||
| inl => left; aapply analz.decrypt
|
||
| inr h => cases h
|
||
· left; aapply analz.decrypt; apply analz.inj; left; assumption
|
||
· right; assumption
|
||
| inr h => cases h; cases ih₁ with
|
||
| inl => left; aapply analz.decrypt; apply analz.inj; left; assumption
|
||
| inr h => cases h
|
||
· left; aapply analz.decrypt <;> (apply analz.inj; left; assumption)
|
||
· right; assumption
|
||
· apply sup_le (a := analz (G ∪ H)) (b := synth G) (c := analz ( synth G ∪ H ))
|
||
· apply analz_mono; apply Set.union_subset_union; apply synth_increasing; trivial
|
||
· apply analz_subset_iff.mpr; apply analz_mono; exact le_sup_left
|
||
|
||
@[simp]
|
||
lemma analz_synth {H : Set Msg} : analz (synth H) = analz H ∪ synth H :=
|
||
by have asu := analz_synth_Un (G := H) (H := ∅); simp_all
|
||
|
||
-- For reasoning about the Fake rule in traces
|
||
|
||
lemma parts_insert_subset_Un {G H : Set Msg} {X : Msg} :
|
||
X ∈ G → parts (insert X H) ⊆ parts G ∪ parts H :=
|
||
by
|
||
intro hX
|
||
rw [Set.insert_eq, parts_union]
|
||
apply Set.union_subset_union
|
||
· apply parts_mono; simp_all
|
||
· trivial
|
||
|
||
lemma Fake_parts_insert {H : Set Msg} {X : Msg} :
|
||
X ∈ synth (analz H) → parts (insert X H) ⊆ synth (analz H) ∪ parts H :=
|
||
by
|
||
intro hX
|
||
rw [parts_insert]
|
||
apply sup_le
|
||
· apply subset_trans (b := synth (analz H) ∪ parts (analz H))
|
||
· rw [Set.union_comm, ←parts_synth]; apply parts_mono; simp; assumption
|
||
· rw [parts_analz]
|
||
· apply le_sup_of_le_right; trivial
|
||
|
||
lemma Fake_parts_insert_in_Un {H : Set Msg} {X Z : Msg} :
|
||
Z ∈ parts (insert X H) → X ∈ synth (analz H) → Z ∈ synth (analz H) ∪ parts H :=
|
||
by
|
||
intro hZ hX
|
||
exact Set.mem_of_subset_of_mem (Fake_parts_insert hX) hZ
|
||
|
||
lemma Fake_analz_insert {G H : Set Msg} {X : Msg} :
|
||
X ∈ synth (analz G) → analz (insert X H) ⊆ synth (analz G) ∪ analz (G ∪ H) :=
|
||
by
|
||
intro
|
||
apply subset_trans (b := analz (synth (analz G) ∪ H))
|
||
· apply analz_mono; rw[Set.insert_eq]; apply Set.union_subset_union; simp_all; trivial;
|
||
· rw[analz_synth_Un, Set.union_comm, analz_analz_Un]
|
||
|
||
@[simp]
|
||
lemma analz_conj_parts {H : Set Msg} {X : Msg} :
|
||
(X ∈ analz H ∧ X ∈ parts H) ↔ X ∈ analz H :=
|
||
by
|
||
constructor
|
||
· intro h
|
||
exact h.1
|
||
· intro h
|
||
exact ⟨h, analz_subset_parts h⟩
|
||
|
||
@[simp]
|
||
lemma analz_disj_parts {H : Set Msg} {X : Msg} :
|
||
(X ∈ analz H ∨ X ∈ parts H) ↔ X ∈ parts H :=
|
||
by
|
||
constructor
|
||
· intro h
|
||
cases h with
|
||
| inl h => apply analz_conj_parts.mpr at h; cases h; assumption
|
||
| inr h => assumption
|
||
· intro h
|
||
exact Or.inr h
|
||
|
||
@[simp]
|
||
lemma MPair_synth_analz {H : Set Msg} {X Y : Msg} :
|
||
⦃X, Y⦄ ∈ synth (analz H) ↔ X ∈ synth (analz H) ∧ Y ∈ synth (analz H) :=
|
||
by
|
||
constructor
|
||
· intro h; cases h
|
||
· apply And.intro
|
||
· apply synth.inj; aapply analz.fst
|
||
· apply synth.inj; aapply analz.snd
|
||
· apply And.intro <;> assumption
|
||
· intro h; exact synth.mpair h.1 h.2
|
||
|
||
lemma Crypt_synth_analz {H : Set Msg} {K : Key} {X : Msg} :
|
||
Key K ∈ analz H → Key (invKey K) ∈ analz H → ((Crypt K X ∈ synth (analz H)) ↔ X ∈ synth (analz H)) :=
|
||
by
|
||
intro _ _
|
||
constructor
|
||
· intro h; cases h
|
||
· apply synth.inj; aapply analz.decrypt
|
||
· assumption
|
||
· intro _; aapply synth.crypt
|
||
|
||
@[simp]
|
||
lemma Hash_synth_analz {H : Set Msg} {X Y : Msg} :
|
||
X ∉ synth (analz H) → ((Hash ⦃X, Y⦄ ∈ synth (analz H)) ↔ Hash ⦃X, Y⦄ ∈ analz H) :=
|
||
by
|
||
intro _
|
||
constructor
|
||
· intro h; cases h with
|
||
| inj => assumption
|
||
| hash h => cases h with
|
||
| inj a => apply analz.fst at a; apply synth.inj at a; contradiction
|
||
| mpair => contradiction
|
||
· intro h; aapply synth.inj
|
||
|
||
-- HPair: a combination of Hash and MPair
|
||
|
||
-- Freeness
|
||
|
||
@[simp]
|
||
lemma Agent_neq_HPair {A : Agent} {X Y : Msg} : Agent A ≠ ⦃X, Y⦄ₕ :=
|
||
by simp [HPair]
|
||
|
||
@[simp]
|
||
lemma Nonce_neq_HPair {N : Nat} {X Y : Msg} : Nonce N ≠ ⦃X, Y⦄ₕ :=
|
||
by simp [HPair]
|
||
|
||
@[simp]
|
||
lemma Number_neq_HPair {N : Nat} {X Y : Msg} : Number N ≠ ⦃X, Y⦄ₕ :=
|
||
by simp [HPair]
|
||
|
||
@[simp]
|
||
lemma Key_neq_HPair {K : Key} {X Y : Msg} : Key K ≠ ⦃X, Y⦄ₕ :=
|
||
by simp [HPair]
|
||
|
||
@[simp]
|
||
lemma Hash_neq_HPair {Z X Y : Msg} : Hash Z ≠ ⦃X, Y⦄ₕ :=
|
||
by simp [HPair]
|
||
|
||
@[simp]
|
||
lemma Crypt_neq_HPair {K : Key} {X' X Y : Msg} : Crypt K X' ≠ ⦃X, Y⦄ₕ :=
|
||
by simp [HPair]
|
||
|
||
@[simp]
|
||
lemma HPair_eq {X' Y' X Y : Msg} : (⦃X', Y'⦄ₕ = ⦃X, Y⦄ₕ) ↔ (X' = X ∧ Y' = Y) :=
|
||
by simp [HPair]
|
||
|
||
@[simp]
|
||
lemma MPair_eq_HPair {X' Y' X Y : Msg} : (⦃X', Y'⦄ = ⦃X, Y⦄ₕ) ↔ (X' = Hash ⦃X, Y⦄ ∧ Y' = Y) :=
|
||
by simp [HPair]
|
||
|
||
@[simp]
|
||
lemma HPair_eq_MPair {X' Y' X Y : Msg} : (⦃X, Y⦄ₕ = ⦃X', Y'⦄) ↔ (X' = Hash ⦃X, Y⦄ ∧ Y' = Y) :=
|
||
by simp [HPair]; nth_rw 1 [Eq.comm]; nth_rw 2 [Eq.comm]
|
||
|
||
-- Specialized laws, proved in terms of those for Hash and MPair
|
||
|
||
@[simp]
|
||
lemma keysFor_insert_HPair {H : Set Msg} {X Y : Msg} :
|
||
keysFor (insert (⦃X, Y⦄ₕ) H) = keysFor H :=
|
||
by simp [HPair]
|
||
|
||
@[simp]
|
||
lemma parts_insert_HPair {H : Set Msg} {X Y : Msg} :
|
||
parts (insert (⦃X, Y⦄ₕ) H) = insert (⦃X, Y⦄ₕ) (insert (Hash ⦃X, Y⦄) (parts (insert Y H))) :=
|
||
by
|
||
simp [HPair]; rw[←Set.union_empty (a:= {⦃Hash ⦃X, Y⦄, Y⦄}), ←Set.insert_eq, parts_insert_MPair, parts_insert_Hash]
|
||
rw[Set.insert_eq, Set.insert_eq, Set.insert_eq, Set.insert_eq, Set.insert_eq]
|
||
rw[Set.union_empty]; simp only [Set.union_assoc]
|
||
|
||
@[simp]
|
||
lemma analz_insert_HPair {H : Set Msg} {X Y : Msg} :
|
||
analz (insert (⦃X, Y⦄ₕ) H) = insert (⦃X, Y⦄ₕ) (insert (Hash ⦃X, Y⦄) (analz (insert Y H))) :=
|
||
by simp [HPair]
|
||
|
||
@[simp]
|
||
lemma HPair_synth_analz {H : Set Msg} {X Y : Msg} :
|
||
X ∉ synth (analz H) →
|
||
((⦃X, Y⦄ₕ ∈ synth (analz H)) ↔ (Hash ⦃X, Y⦄ ∈ analz H ∧ Y ∈ synth (analz H))) :=
|
||
by
|
||
intro _; simp [HPair]; intro _; constructor
|
||
· intro h; cases h with
|
||
| inj => assumption
|
||
| hash a => cases a with
|
||
| inj a => apply analz.fst at a; apply synth.inj at a; contradiction
|
||
| mpair => contradiction
|
||
· intro _; aapply synth.inj
|
||
|
||
-- We do NOT want Crypt... messages broken up in protocols!!
|
||
-- TODO rewrite this
|
||
attribute [-simp] parts.body
|
||
|
||
-- Rewrites to push in Key and Crypt messages, so that other messages can
|
||
-- be pulled out using the `analz_insert` rules
|
||
|
||
lemma pushKeysAgent {K : Key} {C : Agent} {H : Set Msg}:
|
||
insert (Key K) (insert (Agent C) H) = insert (Agent C) (insert (Key K) H) :=
|
||
by simp [Set.insert_comm]
|
||
|
||
lemma pushKeysNumber {K : Key} {N : Nat} {H : Set Msg}:
|
||
insert (Key K) (insert (Number N) H) = insert (Number N) (insert (Key K) H) :=
|
||
by simp [Set.insert_comm]
|
||
|
||
lemma pushKeysNonce {K : Key} {N : Nat} {H : Set Msg}:
|
||
insert (Key K) (insert (Nonce N) H) = insert (Nonce N) (insert (Key K) H) :=
|
||
by simp [Set.insert_comm]
|
||
|
||
lemma pushKeysHash {K : Key} {X : Msg} {H : Set Msg}:
|
||
insert (Key K) (insert (Hash X) H) = insert (Hash X) (insert (Key K) H) :=
|
||
by simp [Set.insert_comm]
|
||
|
||
lemma pushKeysMPair {K : Key} {X Y : Msg} {H : Set Msg}:
|
||
insert (Key K) (insert ⦃X, Y⦄ H) = insert ⦃X, Y⦄ (insert (Key K) H) :=
|
||
by simp [Set.insert_comm]
|
||
|
||
lemma pushKeysCrypt {K K' : Key} {X : Msg} {H : Set Msg}:
|
||
insert (Key K) (insert (Crypt K' N) H) = insert (Crypt K' N) (insert (Key K) H) :=
|
||
by simp [Set.insert_comm]
|
||
|
||
lemma pushCryptsAgent {X : Msg} {K : Key} {C : Agent} {H : Set Msg} :
|
||
insert (Crypt K X) (insert (Agent C) H) = insert (Agent C) (insert (Crypt K X) H) :=
|
||
by simp [Set.insert_comm]
|
||
|
||
lemma pushCryptsNonce {X : Msg} {K : Key} {N : Nat} {H : Set Msg} :
|
||
insert (Crypt K X) (insert (Nonce N) H) = insert (Nonce N) (insert (Crypt K X) H) :=
|
||
by simp [Set.insert_comm]
|
||
|
||
lemma pushCryptsNumber {X : Msg} {K : Key} {N : Nat} {H : Set Msg} :
|
||
insert (Crypt K X) (insert (Number N) H) = insert (Number N) (insert (Crypt K X) H) :=
|
||
by simp [Set.insert_comm]
|
||
|
||
lemma pushCryptsHash {X X' : Msg} {K : Key} {H : Set Msg} :
|
||
insert (Crypt K X) (insert (Hash X') H) = insert (Hash X') (insert (Crypt K X) H) :=
|
||
by simp [Set.insert_comm]
|
||
|
||
lemma pushCryptsMPair {X X' Y : Msg} {K : Key} {H : Set Msg} :
|
||
insert (Crypt K X) (insert ⦃X', Y⦄ H) = insert ⦃X', Y⦄ (insert (Crypt K X) H) :=
|
||
by simp [Set.insert_comm]
|
||
|
||
-- The set of key-free messages
|
||
|
||
inductive keyfree : Set Msg
|
||
| agent {A : Agent} : keyfree (Agent A)
|
||
| number {N : Nat} : keyfree (Number N)
|
||
| nonce {N : Nat} : keyfree (Nonce N)
|
||
| hash {X : Msg} : keyfree (Hash X)
|
||
| mpair {X Y : Msg} : keyfree X → keyfree Y → keyfree ⦃X, Y⦄
|
||
| crypt {K : Key} {X : Msg} : keyfree X → keyfree (Crypt K X)
|
||
|
||
-- Inductive cases
|
||
lemma keyfree_KeyE {K : Key} : ¬keyfree (Key K) :=
|
||
by intro h; cases h
|
||
|
||
lemma keyfree_MPairEL {X Y : Msg} : keyfree ⦃X, Y⦄ → keyfree X :=
|
||
by intro h; cases h; assumption
|
||
|
||
lemma keyfree_MPairER {X Y : Msg} : keyfree ⦃X, Y⦄ → keyfree Y :=
|
||
by intro h; cases h; assumption
|
||
|
||
lemma keyfree_CryptE {K : Key} {X : Msg} : keyfree (Crypt K X) → keyfree X :=
|
||
by intro h; cases h; assumption
|
||
|
||
-- Parts of key-free messages remain key-free
|
||
lemma parts_keyfree : parts keyfree ⊆ keyfree :=
|
||
by
|
||
intro X h
|
||
induction h with
|
||
| inj => assumption
|
||
| fst => aapply keyfree_MPairEL
|
||
| snd => aapply keyfree_MPairER
|
||
| body => aapply keyfree_CryptE
|
||
|
||
-- The key-free part of a set of messages can be removed from the scope of the `analz` operator
|
||
lemma analz_keyfree_into_Un {G H : Set Msg} {X : Msg} :
|
||
X ∈ analz (G ∪ H) → G ⊆ keyfree → X ∈ parts G ∪ analz H :=
|
||
by
|
||
intro hG hKeyFree
|
||
induction hG with
|
||
| inj h => cases h with
|
||
| inl hG => exact Or.inl (parts.inj hG)
|
||
| inr hH => exact Or.inr (analz.inj hH)
|
||
| fst _ ih =>
|
||
cases ih
|
||
· left; aapply parts.fst
|
||
· right; aapply analz.fst
|
||
| snd _ ih =>
|
||
cases ih
|
||
· left; aapply parts.snd
|
||
· right; aapply analz.snd
|
||
| @decrypt K _ h₁ h₂ ih₁ ih₂ => cases ih₂ with
|
||
| inl h => apply parts_mono at hKeyFree
|
||
apply subset_trans (c := keyfree) at hKeyFree
|
||
have pkf := parts_keyfree
|
||
apply hKeyFree at pkf
|
||
apply pkf at h
|
||
have kf_k := keyfree_KeyE (K := invKey K)
|
||
contradiction
|
||
| inr =>
|
||
cases ih₁
|
||
· left; aapply parts.body
|
||
· right; aapply analz.decrypt
|
||
|
||
-- Crypt and Hash are not in the image of Key
|
||
@[simp]
|
||
lemma Crypt_notin_image_Key {K : Key} {X : Msg} {A : Set Key} : Crypt K X ∉ Key '' A :=
|
||
by simp
|
||
|
||
@[simp]
|
||
lemma Hash_notin_image_Key {X : Msg} {A : Set Key} : Hash X ∉ Key '' A :=
|
||
by simp
|
||
|
||
-- Monotonicity of `synth` over `analz`
|
||
lemma synth_analz_mono {G H : Set Msg} : G ⊆ H → synth (analz G) ⊆ synth (analz H) :=
|
||
λ h => synth_mono (analz_mono h)
|
||
|
||
-- Simplification for Fake cases
|
||
@[simp]
|
||
lemma Fake_analz_eq {H : Set Msg} {X : Msg} :
|
||
X ∈ synth (analz H) → synth (analz (insert X H)) = synth (analz H) :=
|
||
by
|
||
intro hX
|
||
ext
|
||
constructor
|
||
· apply synth_subset_iff.mp
|
||
apply subset_trans (b := synth (analz H) ∪ analz H)
|
||
· apply Fake_analz_insert (G := H) (H := H) (X := X) at hX
|
||
rw[Set.union_self] at hX
|
||
assumption
|
||
· apply sup_le_iff.mpr; apply And.intro
|
||
· trivial
|
||
· exact synth_increasing
|
||
· apply synth_analz_mono; simp
|
||
|
||
-- Generalizations of `analz_insert_eq`
|
||
lemma gen_analz_insert_eq {H G : Set Msg} {X : Msg} :
|
||
X ∈ analz H → H ⊆ G → analz (insert X G) = analz G :=
|
||
by
|
||
intro hX hSubset
|
||
apply Set.ext
|
||
intro Y
|
||
constructor
|
||
· intro h
|
||
induction h with
|
||
| inj h => cases h with
|
||
| inl hX' => apply analz_mono at hSubset; apply hSubset at hX; rw[hX']; assumption
|
||
| inr hG => aapply analz.inj
|
||
| fst h ih => exact analz.fst ih
|
||
| snd h ih => exact analz.snd ih
|
||
| decrypt h₁ h₂ ih₁ ih₂ => exact analz.decrypt ih₁ ih₂
|
||
· intro h
|
||
exact analz_mono (Set.subset_insert _ _) h
|
||
|
||
lemma synth_analz_insert_eq {H G : Set Msg} {X : Msg} {K : Key} :
|
||
X ∈ synth (analz H) → H ⊆ G → ((Key K ∈ analz (insert X G)) ↔ (Key K ∈ analz G)) :=
|
||
by
|
||
intro h₁ h₂
|
||
constructor
|
||
· induction h₁ with
|
||
| inj a => apply gen_analz_insert_eq (G := G) at a; apply a at h₂; simp[h₂]
|
||
| agent => rw [analz_insert_Agent]; intro h; cases h; contradiction; assumption
|
||
| number => rw [analz_insert_Number]; intro h; cases h; contradiction; assumption
|
||
| hash => rw [analz_insert_Hash]; intro h; cases h; contradiction; assumption
|
||
| @mpair _ Y h₁ _ _ ih₂ => rw [analz_insert_MPair]; intro h; cases h with
|
||
| inl => contradiction
|
||
| inr h => apply Fake_analz_insert (H := insert Y G) at h₁; apply h₁ at h;
|
||
cases h with
|
||
| inl h => cases h; aapply analz_mono
|
||
| inr h => apply ih₂; have b := h₂; apply subset_trans (c := insert Y G) at b
|
||
have c := Set.subset_insert (x := Y) (s := G)
|
||
apply b at c
|
||
apply sup_le (a := H) (b := insert Y G) (c := insert Y G) at c
|
||
have e := le_refl (a := insert Y G)
|
||
apply c at e
|
||
apply analz_mono at e
|
||
aapply e
|
||
| crypt b a a_ih => intro h; apply a_ih; apply analz_insert_Crypt_subset at h
|
||
cases h; contradiction; assumption
|
||
· apply analz_mono; apply Set.subset_insert
|
||
|
||
|
||
|
||
-- Fake parts for single messages
|
||
lemma Fake_parts_sing {H : Set Msg} {X : Msg} :
|
||
X ∈ synth (analz H) → parts {X} ⊆ 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
|