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

@[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

@[instance_reducible]

def DY.DiffieHellman.SubF : Type → Type

Equations

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

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

@[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.DhPk.invariants [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] : Bytes.PartialInvariants SubF

Equations

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

theorem DY.DiffieHellman.DhPk.invariantsProofs [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesInvariants] : Bytes.PartialInvariantsProofs invariants

@[simp]

theorem DY.DiffieHellman.dhPk.WellFormed [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesFunctor.Has SubF] [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] [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] [BytesInvariants] [BytesInvariants.Has DhPk.invariants] (sk : Bytes) (tr : ProofTrace) : sk.Invariant 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] [BytesInvariants] [BytesInvariants.Has DhPk.invariants] : Bytes.PartialInvariantsProofs invariants

def DY.DiffieHellman.invariants.internal [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor.Has SubF] (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

@[instance_reducible]

def DY.DiffieHellman.invariants [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor.Has SubF] : 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] [BytesInvariants.Has DhPk.invariants] : Bytes.PartialInvariantsProofs invariants

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

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] [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] [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] [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] [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] [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] [BytesInvariants] [BytesInvariants.Has invariants] (pk sk : Bytes) (tr : ProofTrace) : pk.Invariant tr ∧ sk.Invariant tr → (dh pk sk).Invariant tr

instance DY.DiffieHellman.instHoareTriplePureBytesDhPkInvariantAndEqLabelLabelPub [BytesFunctor] [BytesFunctor.Has SubF] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] [BytesInvariants.Has invariants] (sk : Bytes) : HoareTriplePure (dhPk sk) (fun (tr : ProofTrace) => sk.Invariant tr) fun (res : Bytes) (tr : ProofTrace) => res.Invariant tr ∧ res.label tr = Label.pub

instance DY.DiffieHellman.instHoareTriplePureBytesDhAndInvariantPublishableEqLabelLabelJoinDhSkLabel [BytesFunctor] [BytesFunctor.Has SubF] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] [BytesInvariants.Has invariants] (pk sk : Bytes) : HoareTriplePure (dh pk sk) (fun (tr : ProofTrace) => sk.Invariant 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] [BytesInvariants.Has invariants] : SubAttackerKnowledgeTheorem dhPk.attackerKnowledge

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