class DY.DiffieHellman'.CanDH (Bytes : Type u) : Type u

• dhPk (sk : Bytes) : Bytes
• dh (pk sk : Bytes) : Bytes

structure DY.DiffieHellman'.DhPk.SubF (Bytes : Type) : Type

• sk : Bytes

@[instance_reducible]

instance DY.DiffieHellman'.DhPk.instFunctorSizeOfSubF : ALaCarte.FunctorSizeOf SubF

Equations

• DY.DiffieHellman'.DhPk.instFunctorSizeOfSubF = { sizeOf := fun {t : Type} [SizeOf t] (x : DY.DiffieHellman'.DhPk.SubF t) => match x with | { sk := sk } => sizeOf sk }

@[instance_reducible]

instance DY.DiffieHellman'.DhPk.instRepresentableSubF : ALaCarte.Representable SubF

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance DY.DiffieHellman'.DhPk.instRepresentableDecidableEqSubF : ALaCarte.RepresentableDecidableEq SubF

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance DY.DiffieHellman'.DhPk.instRepresentableOrdSubF : ALaCarte.RepresentableOrd SubF

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance DY.DiffieHellman'.DhPk.instSubBytesFunctorSubF : SubBytesFunctor SubF

Equations

• One or more equations did not get rendered due to their size.

def DY.DiffieHellman'.DhPk.SubF.length [BytesFunctor] : Bytes.PartialLength SubF

Equations

• x✝¹.length x✝ = 32

structure DY.DiffieHellman'.Dh.SubF (Bytes : Type) : Type

• pk : Bytes
• sk : Bytes

@[instance_reducible]

instance DY.DiffieHellman'.Dh.instFunctorSizeOfSubF : ALaCarte.FunctorSizeOf SubF

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance DY.DiffieHellman'.Dh.instRepresentableSubF : ALaCarte.Representable SubF

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance DY.DiffieHellman'.Dh.instRepresentableDecidableEqSubF : ALaCarte.RepresentableDecidableEq SubF

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance DY.DiffieHellman'.Dh.instRepresentableOrdSubF : ALaCarte.RepresentableOrd SubF

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance DY.DiffieHellman'.Dh.instSubBytesFunctorSubF : SubBytesFunctor SubF

Equations

• One or more equations did not get rendered due to their size.

def DY.DiffieHellman'.Dh.SubF.length [BytesFunctor] : Bytes.PartialLength SubF

Equations

• x✝¹.length x✝ = 32

def DY.DiffieHellman'.SubF.length.internal [BytesFunctor] (id✝ : Fin 2) : Bytes.PartialLength (SubF.internal id✝)

Equations

• DY.DiffieHellman'.SubF.length.internal 0 = DY.DiffieHellman'.DhPk.SubF.length
• DY.DiffieHellman'.SubF.length.internal 1 = DY.DiffieHellman'.Dh.SubF.length
• DY.DiffieHellman'.SubF.length.internal ⟨n.succ.succ, isLt⟩ = ⋯.elim

def DY.DiffieHellman'.SubF.internal : Fin 2 → Type → Type

Equations

• DY.DiffieHellman'.SubF.internal 0 = DY.DiffieHellman'.DhPk.SubF
• DY.DiffieHellman'.SubF.internal 1 = DY.DiffieHellman'.Dh.SubF
• DY.DiffieHellman'.SubF.internal ⟨n.succ.succ, isLt⟩ = ⋯.elim

@[instance_reducible]

def DY.DiffieHellman'.SubF : Type → Type

Equations

• DY.DiffieHellman'.SubF = DY.BytesFunctor.combine DY.DiffieHellman'.SubF.internal

@[instance_reducible]

def DY.DiffieHellman'.SubF.length [BytesFunctor] : Bytes.PartialLength SubF

Equations

• DY.DiffieHellman'.SubF.length = DY.Bytes.PartialLength.combine DY.DiffieHellman'.SubF.length.internal

@[reducible, inline]

abbrev DY.DiffieHellman'.DhPk.SubF.pack [BytesFunctor] [BytesFunctor.Has SubF] (x : SubF Bytes) : Bytes

Equations

• x.pack = DY.BytesView.pack x

@[reducible, inline]

abbrev DY.DiffieHellman'.Dh.SubF.pack [BytesFunctor] [BytesFunctor.Has SubF] (x : SubF Bytes) : Bytes

Equations

• x.pack = DY.BytesView.pack x

@[instance_reducible]

instance DY.DiffieHellman'.instCanDHBytes [BytesFunctor] [BytesFunctor.Has SubF] : CanDH Bytes

Equations

• One or more equations did not get rendered due to their size.

theorem DY.DiffieHellman'.dh_commutes [BytesFunctor] [BytesFunctor.Has SubF] (sk1 sk2 : Bytes) : dh (dhPk sk1) sk2 = dh (dhPk sk2) sk1

def DY.DiffieHellman'.dhPk.attackerKnowledge [BytesFunctor] [BytesFunctor.Has SubF] : SubAttackerKnowledge SubF

Equations

• DY.DiffieHellman'.dhPk.attackerKnowledge = { pred := fun (p : DY.Bytes → Prop) (out : DY.Bytes) => ∃ (sk : DY.Bytes), out = DY.DiffieHellman'.dhPk sk ∧ p sk, pred_isMonotonic := ⋯ }

def DY.DiffieHellman'.dh.attackerKnowledge [BytesFunctor] [BytesFunctor.Has SubF] : SubAttackerKnowledge SubF

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

def DY.DiffieHellman'.attackerKnowledge [BytesFunctor] [BytesFunctor.Has SubF] : SubAttackerKnowledge SubF

Equations

• DY.DiffieHellman'.attackerKnowledge = DY.SubAttackerKnowledge.combine' DY.DiffieHellman'.attackerKnowledge.internal

def DY.DiffieHellman'.attackerKnowledge.internal [BytesFunctor] [BytesFunctor.Has SubF] : Fin 2 → SubAttackerKnowledge SubF

Equations

• DY.DiffieHellman'.attackerKnowledge.internal 0 = DY.DiffieHellman'.dhPk.attackerKnowledge
• DY.DiffieHellman'.attackerKnowledge.internal 1 = DY.DiffieHellman'.dh.attackerKnowledge
• DY.DiffieHellman'.attackerKnowledge.internal ⟨n.succ.succ, isLt⟩ = ⋯.elim

theorem DY.DiffieHellman'.attacker_knows_dhPk [BytesFunctor] [BytesFunctor.Has SubF] [ExecTraceTypes] [BaseAttackerKnowledge] [AttackerKnowledge] [AttackerKnowledge.Has attackerKnowledge] (sk : Bytes) (tr : ExecTrace) : sk.AttackerKnows tr → (dhPk sk).AttackerKnows tr

theorem DY.DiffieHellman'.attacker_knows_dh [BytesFunctor] [BytesFunctor.Has SubF] [ExecTraceTypes] [BaseAttackerKnowledge] [AttackerKnowledge] [AttackerKnowledge.Has attackerKnowledge] (pk sk : Bytes) (tr : ExecTrace) : pk.AttackerKnows tr → sk.AttackerKnows tr → (dh pk sk).AttackerKnows tr

def DY.DiffieHellman'.Broken.dhPkInvert [BytesFunctor] [BytesFunctor.Has SubF] (pk : Bytes) : Err Bytes

Equations

• DY.DiffieHellman'.Broken.dhPkInvert pk = match pk.view? DY.DiffieHellman'.DhPk.SubF with | some { sk := sk } => some sk | none => none

theorem DY.DiffieHellman'.Broken.dhPkInvert_dhPk [BytesFunctor] [BytesFunctor.Has SubF] (sk : Bytes) : dhPkInvert (dhPk sk) = some sk

theorem DY.DiffieHellman'.Broken.dhPk_dhPkInvert [BytesFunctor] [BytesFunctor.Has SubF] (pk : Bytes) : match dhPkInvert pk with | none => True | some sk => dhPk sk = pk

structure DY.DiffieHellman'.Broken.BrokenDhEvent [BytesFunctor] : Type

• brokenPk : Bytes

@[instance_reducible]

def DY.DiffieHellman'.Broken.baseAttackerKnowledge [BytesFunctor] [ExecTraceTypes] : SubBaseAttackerKnowledge ExecEntryT

Equations

• DY.DiffieHellman'.Broken.baseAttackerKnowledge = DY.SubBaseAttackerKnowledge.combine DY.DiffieHellman'.Broken.baseAttackerKnowledge.internal

def DY.DiffieHellman'.Broken.ExecEntryT.internal [BytesFunctor] : Fin 1 → Type

Equations

• DY.DiffieHellman'.Broken.ExecEntryT.internal 0 = DY.ProtocolEvent.ExecEntryT DY.DiffieHellman'.Broken.BrokenDhEvent
• DY.DiffieHellman'.Broken.ExecEntryT.internal ⟨n.succ, isLt⟩ = ⋯.elim

def DY.DiffieHellman'.Broken.baseAttackerKnowledge.internal [BytesFunctor] [ExecTraceTypes] (id✝ : Fin 1) : SubBaseAttackerKnowledge (ExecEntryT.internal id✝)

Equations

• DY.DiffieHellman'.Broken.baseAttackerKnowledge.internal 0 = DY.ProtocolEvent.baseAttackerKnowledge DY.DiffieHellman'.Broken.BrokenDhEvent
• DY.DiffieHellman'.Broken.baseAttackerKnowledge.internal ⟨n.succ, isLt⟩ = ⋯.elim

@[instance_reducible]

def DY.DiffieHellman'.Broken.ExecEntryT [BytesFunctor] : Type

Equations

• DY.DiffieHellman'.Broken.ExecEntryT = DY.ExecTraceTypes.combine DY.DiffieHellman'.Broken.ExecEntryT.internal

def DY.DiffieHellman'.Broken.ThisDhPkHasBeenBroken [BytesFunctor] [ExecTraceTypes] [ExecTraceTypes.Has ExecEntryT] (brokenPk : Bytes) (tr : ExecTrace) : Prop

Equations

• DY.DiffieHellman'.Broken.ThisDhPkHasBeenBroken brokenPk tr = DY.Trace.EventLogged { brokenPk := brokenPk } tr

def DY.DiffieHellman'.Broken.OneDhPkHasBeenBroken [BytesFunctor] [ExecTraceTypes] [ExecTraceTypes.Has ExecEntryT] (tr : ExecTrace) : Prop

Equations

• DY.DiffieHellman'.Broken.OneDhPkHasBeenBroken tr = ∃ (brokenPk : DY.Bytes), DY.DiffieHellman'.Broken.ThisDhPkHasBeenBroken brokenPk tr

def DY.DiffieHellman'.Broken.label [BytesFunctor] [ExecTraceTypes] [ExecTraceTypes.Has ExecEntryT] (brokenPk : Bytes) : Label

Equations

• DY.DiffieHellman'.Broken.label brokenPk = { isCorrupt := fun (tr : DY.ExecTrace) => DY.DiffieHellman'.Broken.ThisDhPkHasBeenBroken brokenPk tr, isCorruptLater := ⋯ }

def DY.DiffieHellman'.Broken.breakDhPk [BytesFunctor] [ExecTraceTypes] [ExecTraceTypes.Has ExecEntryT] [BytesFunctor.Has SubF] [ExecTraceTypes.Has Network.ExecEntryT] (msgHandle : Nat) : Traceful Nat

Equations

• One or more equations did not get rendered due to their size.

def DY.DiffieHellman'.Broken.breakDhPk.reachability [BytesFunctor] [ExecTraceTypes] [ExecTraceTypes.Has ExecEntryT] [BytesFunctor.Has SubF] [ExecTraceTypes.Has Network.ExecEntryT] : ReachabilityConfig

Equations

• DY.DiffieHellman'.Broken.breakDhPk.reachability = DY.ReachabilityConfig.make fun (handle : Nat) => DY.DiffieHellman'.Broken.breakDhPk handle

def DY.DiffieHellman'.DhPk.invariants [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesFunctor.Has DiffieHellman'.SubF] [ExecTraceTypes.Has Broken.ExecEntryT] : Bytes.PartialInvariants SubF

Equations

• One or more equations did not get rendered due to their size.

theorem DY.DiffieHellman'.DhPk.invariantsProofs [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesFunctor.Has DiffieHellman'.SubF] [ExecTraceTypes.Has Broken.ExecEntryT] [BytesInvariants] : Bytes.PartialInvariantsProofs invariants

@[simp]

theorem DY.DiffieHellman'.dhPk.WellFormed [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesFunctor.Has SubF] [ExecTraceTypes.Has Broken.ExecEntryT] [BytesInvariants] [BytesInvariants.Has DhPk.invariants] (sk : Bytes) (tr : ProofTrace) : (dhPk sk).WellFormed tr = sk.WellFormed tr

@[simp]

theorem DY.DiffieHellman'.dhPk.label [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesFunctor.Has SubF] [ExecTraceTypes.Has Broken.ExecEntryT] [BytesInvariants] [BytesInvariants.Has DhPk.invariants] (sk : Bytes) (tr : ProofTrace) : (dhPk sk).label tr = Label.pub

@[simp]

theorem DY.DiffieHellman'.dhPk.Invariant [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesFunctor.Has SubF] [ExecTraceTypes.Has Broken.ExecEntryT] [BytesInvariants] [BytesInvariants.Has DhPk.invariants] (sk : Bytes) (tr : ProofTrace) : sk.Invariant tr → (sk.label tr).canFlow (Broken.label (dhPk sk)) (Trace.erase tr) → (dhPk sk).Invariant tr

def DY.DiffieHellman'.Dh.invariants [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesFunctor.Has DiffieHellman'.SubF] : Bytes.PartialInvariants SubF

Equations

• One or more equations did not get rendered due to their size.

theorem DY.DiffieHellman'.Dh.invariantsProofs [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesFunctor.Has DiffieHellman'.SubF] [ExecTraceTypes.Has Broken.ExecEntryT] [BytesInvariants] [BytesInvariants.Has DhPk.invariants] : Bytes.PartialInvariantsProofs invariants

@[instance_reducible]

def DY.DiffieHellman'.invariants [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor.Has SubF] [ExecTraceTypes.Has Broken.ExecEntryT] : Bytes.PartialInvariants SubF

Equations

• DY.DiffieHellman'.invariants = DY.Bytes.PartialInvariants.combine DY.DiffieHellman'.invariants.internal

theorem DY.DiffieHellman'.invariantsProofs [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] [BytesFunctor.Has SubF] [ExecTraceTypes.Has Broken.ExecEntryT] [BytesInvariants.Has DhPk.invariants] : Bytes.PartialInvariantsProofs invariants

theorem DY.DiffieHellman'.invariantsProofs.internal [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] [BytesFunctor.Has SubF] [ExecTraceTypes.Has Broken.ExecEntryT] [BytesInvariants.Has DhPk.invariants] (id✝ : Fin 2) : Bytes.PartialInvariantsProofs (invariants.internal id✝)

def DY.DiffieHellman'.invariants.internal [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor.Has SubF] [ExecTraceTypes.Has Broken.ExecEntryT] (id✝ : Fin 2) : Bytes.PartialInvariants (SubF.internal id✝)

Equations

• DY.DiffieHellman'.invariants.internal 0 = DY.DiffieHellman'.DhPk.invariants
• DY.DiffieHellman'.invariants.internal 1 = DY.DiffieHellman'.Dh.invariants
• DY.DiffieHellman'.invariants.internal ⟨n.succ.succ, isLt⟩ = ⋯.elim

noncomputable def DY.Bytes.dhSkLabel' [BytesFunctor] [BytesFunctor.Has DiffieHellman'.SubF] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] (pk : Bytes) (tr : ProofTrace) : Label

Equations

• pk.dhSkLabel' tr = DY.Bytes.xxxLabel DY.DiffieHellman'.extractDhSk✝ pk tr

theorem DY.Bytes.dhSkLabel'_dhPk [BytesFunctor] [BytesFunctor.Has DiffieHellman'.SubF] [ExecTraceTypes] [ProofTraceTypes] [ExecTraceTypes.Has DiffieHellman'.Broken.ExecEntryT] [BytesInvariants] [BytesInvariants.Has DiffieHellman'.invariants] (sk : Bytes) (tr : ProofTrace) : (DiffieHellman'.dhPk sk).dhSkLabel' tr = sk.label tr

theorem DY.Bytes.dhSkLabel'_later [BytesFunctor] [BytesFunctor.Has DiffieHellman'.SubF] [ExecTraceTypes] [ProofTraceTypes] [ExecTraceTypes.Has DiffieHellman'.Broken.ExecEntryT] [BytesInvariants] [BytesInvariants.Has DiffieHellman'.invariants] [GetLabelLater] (b : Bytes) (tr1 tr2 : ProofTrace) : b.WellFormed tr1 → tr1 ≤ tr2 → b.dhSkLabel' tr1 = b.dhSkLabel' tr2

theorem DY.Bytes.dhSkLabel'_later_fast [BytesFunctor] [BytesFunctor.Has DiffieHellman'.SubF] [ExecTraceTypes] [ProofTraceTypes] [ExecTraceTypes.Has DiffieHellman'.Broken.ExecEntryT] [BytesInvariants] [BytesInvariantsProofs] [BytesInvariants.Has DiffieHellman'.invariants] (b : Bytes) (tr1 tr2 : ProofTrace) : b.Invariant tr1 → tr1 ≤ tr2 → b.dhSkLabel' tr1 = b.dhSkLabel' tr2

@[simp]

theorem DY.DiffieHellman'.dh.WellFormed [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesFunctor.Has SubF] [ExecTraceTypes.Has Broken.ExecEntryT] [BytesInvariants] [BytesInvariants.Has invariants] (pk sk : Bytes) (tr : ProofTrace) : (dh pk sk).WellFormed tr = (pk.WellFormed tr ∧ sk.WellFormed tr)

@[simp]

theorem DY.DiffieHellman'.dh.label [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesFunctor.Has SubF] [ExecTraceTypes.Has Broken.ExecEntryT] [BytesInvariants] [BytesInvariants.Has invariants] (pk sk : Bytes) (tr : ProofTrace) : (dh pk sk).label tr = (pk.dhSkLabel' tr).join (sk.label tr)

@[simp]

theorem DY.DiffieHellman'.dh.Invariant [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesFunctor.Has SubF] [ExecTraceTypes.Has Broken.ExecEntryT] [BytesInvariants] [BytesInvariants.Has invariants] (pk sk : Bytes) (tr : ProofTrace) : pk.Invariant tr ∧ sk.Invariant tr ∧ (sk.label tr).canFlow (Broken.label (dhPk sk)) (Trace.erase tr) → (dh pk sk).Invariant tr

instance DY.DiffieHellman'.instHoareTriplePureBytesDhPkAndInvariantCanFlowLabelLabelEraseEqLabelPub [BytesFunctor] [BytesFunctor.Has SubF] [ExecTraceTypes] [ProofTraceTypes] [ExecTraceTypes.Has Broken.ExecEntryT] [BytesInvariants] [BytesInvariants.Has invariants] (sk : Bytes) : HoareTriplePure (dhPk sk) (fun (tr : ProofTrace) => sk.Invariant tr ∧ (sk.label tr).canFlow (Broken.label (dhPk sk)) (Trace.erase tr)) fun (res : Bytes) (tr : ProofTrace) => res.Invariant tr ∧ res.label tr = Label.pub

instance DY.DiffieHellman'.instHoareTriplePureBytesDhAndInvariantCanFlowLabelLabelDhPkErasePublishableEqLabelJoinDhSkLabel' [BytesFunctor] [BytesFunctor.Has SubF] [ExecTraceTypes] [ProofTraceTypes] [ExecTraceTypes.Has Broken.ExecEntryT] [BytesInvariants] [BytesInvariants.Has invariants] (pk sk : Bytes) : HoareTriplePure (dh pk sk) (fun (tr : ProofTrace) => sk.Invariant tr ∧ (sk.label tr).canFlow (Broken.label (dhPk sk)) (Trace.erase tr) ∧ pk.Publishable tr) fun (res : Bytes) (tr : ProofTrace) => res.Invariant tr ∧ res.label tr = (sk.label tr).join (pk.dhSkLabel' tr)

instance DY.DiffieHellman'.instSubAttackerKnowledgeTheoremSubFAttackerKnowledge [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] [BytesFunctor] [BytesInvariants] [BytesFunctor.Has SubF] [ExecTraceTypes.Has Broken.ExecEntryT] [BytesInvariants.Has invariants] : SubAttackerKnowledgeTheorem dhPk.attackerKnowledge

instance DY.DiffieHellman'.instSubAttackerKnowledgeTheoremSubFAttackerKnowledge_1 [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] [BytesFunctor] [BytesInvariants] [BytesFunctor.Has SubF] [ExecTraceTypes.Has Broken.ExecEntryT] [BytesInvariants.Has invariants] : SubAttackerKnowledgeTheorem dh.attackerKnowledge

@[instance_reducible]

instance DY.DiffieHellman'.Broken.instEventInvBrokenDhEvent [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] : ProtocolEvent.EventInv BrokenDhEvent

Equations

• DY.DiffieHellman'.Broken.instEventInvBrokenDhEvent = { invariant := fun (x : DY.ProofTrace) (x_1 : DY.DiffieHellman'.Broken.BrokenDhEvent) => True }

def DY.DiffieHellman'.Broken.ProofEntryT.internal [BytesFunctor] : Fin 1 → Type

Equations

• DY.DiffieHellman'.Broken.ProofEntryT.internal 0 = DY.ProtocolEvent.ProofEntryT DY.DiffieHellman'.Broken.BrokenDhEvent
• DY.DiffieHellman'.Broken.ProofEntryT.internal ⟨n.succ, isLt⟩ = ⋯.elim

@[instance_reducible]

def DY.DiffieHellman'.Broken.ProofEntryT [BytesFunctor] : Type

Equations

• DY.DiffieHellman'.Broken.ProofEntryT = DY.ProofTraceTypes.combine DY.DiffieHellman'.Broken.ProofEntryT.internal

instance DY.DiffieHellman'.Broken.instReachableImpliesInvariantReachability [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] [BytesInvariants] [BytesFunctor.Has SubF] [ExecTraceTypes.Has ExecEntryT] [BytesInvariants.Has invariants] [BytesInvariantsProofs] [ExecTraceTypes.Has Network.ExecEntryT] [ProofTraceTypes.Has ProofEntryT] [ProofTraceTypes.Has Network.ProofEntryT] [TraceInvariant.Has Network.ProofEntryT] [TraceInvariant.Has ProofEntryT] : ReachableImpliesInvariant breakDhPk.reachability