Examples.SignedDHKEM.Proof

source

class DY.Example.SignedDHKEM.HasProofTrace extends DY.Example.SignedDHKEM.HasExecTrace :

Type 1

bytesFunc : BytesFunctor
bytesFunc0 : BytesFunctor.Has Random.SubF
bytesFunc1 : BytesFunctor.Has Literal.SubF
bytesFunc2 : BytesFunctor.Has Concat.SubF
bytesFunc3 : BytesFunctor.Has Hash.SubF
bytesFunc4 : BytesFunctor.Has Signature'.SubF
bytesFunc5 : BytesFunctor.Has DiffieHellman'.SubF
bytesFunc6 : BytesFunctor.Has KEM.SubF
bytesLen : BytesLength
bytesLen0 : BytesLength.Has Random.SubF.length
bytesLen1 : BytesLength.Has Literal.SubF.length
bytesLen2 : BytesLength.Has Concat.SubF.length
bytesLen3 : BytesLength.Has Hash.SubF.length
bytesLen4 : BytesLength.Has Signature'.SubF.length
bytesLen5 : BytesLength.Has DiffieHellman'.SubF.length
bytesLen6 : BytesLength.Has KEM.SubF.length
att : AttackerKnowledge
att0 : AttackerKnowledge.Has Random.attackerKnowledge
att1 : AttackerKnowledge.Has Literal.attackerKnowledge
att2 : AttackerKnowledge.Has Concat.attackerKnowledge
att3 : AttackerKnowledge.Has Hash.attackerKnowledge
att4 : AttackerKnowledge.Has Signature'.attackerKnowledge
att5 : AttackerKnowledge.Has DiffieHellman'.attackerKnowledge
att6 : AttackerKnowledge.Has KEM.attackerKnowledge
traceExec : ExecTraceTypes
traceExec0 : ExecTraceTypes.Has Network.ExecEntryT
traceExec1 : ExecTraceTypes.Has Random.ExecEntryT
traceExec2 : ExecTraceTypes.Has (ProtocolEvent.ExecEntryT SignedDHKEMEvent)
traceExec3 : ExecTraceTypes.Has (PersistentLocalState.CompromisableState.ExecEntryT ClientInitiateDHState)
traceExec4 : ExecTraceTypes.Has (PersistentLocalState.CompromisableState.ExecEntryT ClientInitiateKEMState)
traceExec5 : ExecTraceTypes.Has (PersistentLocalState.CompromisableState.ExecEntryT ClientFinishState)
traceExec6 : ExecTraceTypes.Has (PersistentLocalState.CompromisableState.ExecEntryT ServerFinishState)
traceExec7 : ExecTraceTypes.Has (LongTermKeys.ExecEntryT "SignedDHKEM PKI")
traceExec8 : ExecTraceTypes.Has KEM.Broken.ExecEntryT
traceExec9 : ExecTraceTypes.Has DiffieHellman'.Broken.ExecEntryT
traceExec10 : ExecTraceTypes.Has Signature'.Broken.ExecEntryT
attBase : BaseAttackerKnowledge
traceProof : ProofTraceTypes
traceProof0 : ProofTraceTypes.Has Network.ProofEntryT
traceProof1 : ProofTraceTypes.Has Random.ProofEntryT
traceProof2 : ProofTraceTypes.Has (ProtocolEvent.ProofEntryT SignedDHKEMEvent)
traceProof3 : ProofTraceTypes.Has (PersistentLocalState.CompromisableState.ProofEntryT ClientInitiateDHState)
traceProof4 : ProofTraceTypes.Has (PersistentLocalState.CompromisableState.ProofEntryT ClientInitiateKEMState)
traceProof5 : ProofTraceTypes.Has (PersistentLocalState.CompromisableState.ProofEntryT ClientFinishState)
traceProof6 : ProofTraceTypes.Has (PersistentLocalState.CompromisableState.ProofEntryT ServerFinishState)
traceProof7 : ProofTraceTypes.Has (LongTermKeys.ProofEntryT "SignedDHKEM PKI")
traceProof8 : ProofTraceTypes.Has KEM.Broken.ProofEntryT
traceProof9 : ProofTraceTypes.Has DiffieHellman'.Broken.ProofEntryT
traceProof10 : ProofTraceTypes.Has Signature'.Broken.ProofEntryT

Instances

source

def DY.Example.SignedDHKEM.clientDhLabel [HasProofTrace] (me : Participant) (xPk : Bytes) :

Label

Equations

DY.Example.SignedDHKEM.clientDhLabel me xPk = { isCorrupt := fun (tr : DY.ExecTrace) => DY.Example.SignedDHKEM.ClientEphemeralDHStateCompromised me xPk tr, isCorruptLater := ⋯ }

Instances For

source

def DY.Example.SignedDHKEM.clientKemLabel [HasProofTrace] (me : Participant) (zPk : Bytes) :

Label

Equations

DY.Example.SignedDHKEM.clientKemLabel me zPk = { isCorrupt := fun (tr : DY.ExecTrace) => DY.Example.SignedDHKEM.ClientEphemeralKEMStateCompromised me zPk tr, isCorruptLater := ⋯ }

Instances For

source

def DY.Example.SignedDHKEM.serverLabel [HasProofTrace] (me : Participant) (xPk yPk zPk : Bytes) :

Label

Equations

DY.Example.SignedDHKEM.serverLabel me xPk yPk zPk = { isCorrupt := fun (tr : DY.ExecTrace) => DY.Example.SignedDHKEM.ServerEphemeralStateCompromised me xPk yPk zPk tr, isCorruptLater := ⋯ }

Instances For

source

structure DY.Example.SignedDHKEM.LongTermKeyUsage :

Type

principal : Participant

Instances For

source

@[instance_reducible]

instance DY.Example.SignedDHKEM.instParseableSerializeableLongTermKeyUsage [HasProofTrace] :

Comparse.ParseableSerializeable LongTermKeyUsage

Equations

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

source

def DY.Example.SignedDHKEM.mkLongTermUsage [HasProofTrace] (me : Participant) :

Usage

Equations

DY.Example.SignedDHKEM.mkLongTermUsage me = { type := "SigKey", tag := "SignedDHKEM PKI", data := some (DY.Comparse.serialize { principal := me }) }

Instances For

source

theorem DY.Example.SignedDHKEM.mkLongTermUsage_inj [HasProofTrace] :

Function.Injective mkLongTermUsage

source

@[instance_reducible]

instance DY.Example.SignedDHKEM.SignedDHKEMSignPred [HasProofTrace] :

Signature'.SignPred

Equations

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

source

class DY.Example.SignedDHKEM.HasBytesInvariants extends DY.Example.SignedDHKEM.HasProofTrace :

Type 1

Instances

source

@[instance_reducible]

instance DY.Example.SignedDHKEM.ClientInitiateDHStateInv [HasBytesInvariants] :

PersistentLocalState.CompromisableLocalStateInv ClientInitiateDHState

Equations

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

source

theorem DY.Example.SignedDHKEM.ClientInitiateDHStateInv_imp_Invariant [HasBytesInvariants] {tr : ProofTrace} (participant : Participant) (st : ClientInitiateDHState) :

PersistentLocalState.LocalStateInv.invariant participant st tr → st.xSk.Invariant tr ∧ st.xPk.Invariant tr

source

@[instance_reducible]

instance DY.Example.SignedDHKEM.ClientInitiateKEMStateInv [HasBytesInvariants] :

PersistentLocalState.CompromisableLocalStateInv ClientInitiateKEMState

Equations

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

source

theorem DY.Example.SignedDHKEM.ClientInitiateKEMStateInv_imp_Invariant [HasBytesInvariants] {tr : ProofTrace} (participant : Participant) (st : ClientInitiateKEMState) :

PersistentLocalState.LocalStateInv.invariant participant st tr → st.zSk.Invariant tr ∧ st.zPk.Invariant tr

source

@[instance_reducible]

instance DY.Example.SignedDHKEM.ClientFinishStateInv [HasBytesInvariants] :

PersistentLocalState.CompromisableLocalStateInv ClientFinishState

Equations

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

source

@[instance_reducible]

instance DY.Example.SignedDHKEM.ServerFinishStateInv [HasBytesInvariants] :

PersistentLocalState.CompromisableLocalStateInv ServerFinishState

Equations

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

source

def DY.Example.SignedDHKEM.mkLongTermLabel [HasBytesInvariants] (p : Participant) (vk : Bytes) :

Label

Equations

DY.Example.SignedDHKEM.mkLongTermLabel p vk = (DY.LongTermKeys.label "SignedDHKEM PKI" p vk).join (DY.Signature'.Broken.label vk)

Instances For

source

@[instance_reducible]

instance DY.Example.SignedDHKEM.instProofConfigMkLongTermUsageMkLongTermLabel [HasBytesInvariants] :

LongTermKeys.ProofConfig "SignedDHKEM PKI" mkLongTermUsage mkLongTermLabel

Equations

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

source

@[instance_reducible]

instance DY.Example.SignedDHKEM.SignedDHKEMEventInv [HasBytesInvariants] :

ProtocolEvent.EventInv SignedDHKEMEvent

Equations

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

source

class DY.Example.SignedDHKEM.HasTraceInvariant extends DY.Example.SignedDHKEM.HasBytesInvariants :

Type 1

Instances

source

instance DY.Example.SignedDHKEM.Client.initiate.proof [HasTraceInvariant] (me : Participant) :

HoareTriple (initiate me) (fun (x : ProofTrace) => True) fun (x : Nat × Nat × Nat) (x_1 : ProofTrace) => True

source

instance DY.Example.SignedDHKEM.instHoareTriplePureBytesConcatAndInvariantEqLabelLabelMeet_examples [HasTraceInvariant] (lhs rhs : Bytes) :

HoareTriplePure (Concat.concat lhs rhs) (fun (tr : ProofTrace) => lhs.Invariant tr ∧ rhs.Invariant tr) fun (res : Bytes) (tr : ProofTrace) => res.Invariant tr ∧ res.label tr = (lhs.label tr).meet (rhs.label tr)

source

instance DY.Example.SignedDHKEM.Server.receive.proof [HasTraceInvariant] (me : Participant) (skHandle msgHandle : Nat) :

HoareTriple (receive me skHandle msgHandle) (fun (x : ProofTrace) => True) fun (x : Nat × Nat) (x_1 : ProofTrace) => True

source

instance DY.Example.SignedDHKEM.Client.finish.proof [HasTraceInvariant] (me server : Participant) (pkHandle msgHandle dhStHandle kemStHandle : Nat) :

HoareTriple (finish me server pkHandle msgHandle dhStHandle kemStHandle) (fun (x : ProofTrace) => True) fun (x : Nat) (x_1 : ProofTrace) => True

source

instance DY.Example.SignedDHKEM.ClientInitiateDHState.compromise.proof [HasTraceInvariant] (stHandle : Nat) :

HoareTriple (compromise stHandle) (fun (x : ProofTrace) => True) fun (x : Nat) (x_1 : ProofTrace) => True

source

instance DY.Example.SignedDHKEM.ClientInitiateKEMState.compromise.proof [HasTraceInvariant] (stHandle : Nat) :

HoareTriple (compromise stHandle) (fun (x : ProofTrace) => True) fun (x : Nat) (x_1 : ProofTrace) => True

source

instance DY.Example.SignedDHKEM.ClientFinishState.compromise.proof [HasTraceInvariant] (stHandle : Nat) :

HoareTriple (compromise stHandle) (fun (x : ProofTrace) => True) fun (x : Nat) (x_1 : ProofTrace) => True

source

instance DY.Example.SignedDHKEM.ServerFinishState.compromise.proof [HasTraceInvariant] (stHandle : Nat) :

HoareTriple (compromise stHandle) (fun (x : ProofTrace) => True) fun (x : Nat) (x_1 : ProofTrace) => True

source

instance DY.Example.SignedDHKEM.instReachableImpliesInvariantReachability [HasTraceInvariant] :

ReachableImpliesInvariant Client.initiate.reachability

source

instance DY.Example.SignedDHKEM.instReachableImpliesInvariantReachability_1 [HasTraceInvariant] :

ReachableImpliesInvariant Server.receive.reachability

source

instance DY.Example.SignedDHKEM.instReachableImpliesInvariantReachability_2 [HasTraceInvariant] :

ReachableImpliesInvariant Client.finish.reachability

source

instance DY.Example.SignedDHKEM.instReachableImpliesInvariantReachability_3 [HasTraceInvariant] :

ReachableImpliesInvariant ClientInitiateDHState.compromise.reachability

source

instance DY.Example.SignedDHKEM.instReachableImpliesInvariantReachability_4 [HasTraceInvariant] :

ReachableImpliesInvariant ClientInitiateKEMState.compromise.reachability

source

instance DY.Example.SignedDHKEM.instReachableImpliesInvariantReachability_5 [HasTraceInvariant] :

ReachableImpliesInvariant ClientFinishState.compromise.reachability

source

instance DY.Example.SignedDHKEM.instReachableImpliesInvariantReachability_6 [HasTraceInvariant] :

ReachableImpliesInvariant ServerFinishState.compromise.reachability