Documentation

Examples.SignedDH.Proof

class DY.Example.SignedDH.HasProofTraceextends DY.Example.SignedDH.HasExecTrace :

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
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
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
traceExec : ExecTraceTypes
traceExec0 : ExecTraceTypes.Has Network.ExecEntryT
traceExec1 : ExecTraceTypes.Has Random.ExecEntryT
traceExec2 : ExecTraceTypes.Has (ProtocolEvent.ExecEntryT SignedDHEvent)
traceExec3 : ExecTraceTypes.Has (PersistentLocalState.CompromisableState.ExecEntryT ClientInitiateState)
traceExec4 : ExecTraceTypes.Has (PersistentLocalState.CompromisableState.ExecEntryT ClientFinishState)
traceExec5 : ExecTraceTypes.Has (PersistentLocalState.CompromisableState.ExecEntryT ServerFinishState)
traceExec6 : ExecTraceTypes.Has (LongTermKeys.ExecEntryT "SignedDH PKI")
attBase : BaseAttackerKnowledge
traceProof : ProofTraceTypes
traceProof0 : ProofTraceTypes.Has Network.ProofEntryT
traceProof1 : ProofTraceTypes.Has Random.ProofEntryT
traceProof2 : ProofTraceTypes.Has (ProtocolEvent.ProofEntryT SignedDHEvent)
traceProof3 : ProofTraceTypes.Has (PersistentLocalState.CompromisableState.ProofEntryT ClientInitiateState)
traceProof4 : ProofTraceTypes.Has (PersistentLocalState.CompromisableState.ProofEntryT ClientFinishState)
traceProof5 : ProofTraceTypes.Has (PersistentLocalState.CompromisableState.ProofEntryT ServerFinishState)
traceProof6 : ProofTraceTypes.Has (LongTermKeys.ProofEntryT "SignedDH PKI")

Instances

def DY.Example.SignedDH.clientLabel [HasProofTrace] (me : Participant) (xPk : Bytes) :

Equations

DY.Example.SignedDH.clientLabel me xPk = { isCorrupt := fun (tr : DY.ExecTrace) => DY.Example.SignedDH.ClientEphemeralStateCompromised me xPk tr, isCorruptLater := ⋯ }

Instances For

def DY.Example.SignedDH.serverLabel [HasProofTrace] (me : Participant) (yPk : Bytes) :

Equations

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

Instances For

structure DY.Example.SignedDH.LongTermKeyUsage :

principal : Participant

Instances For

@[instance_reducible]

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

Comparse.ParseableSerializeable LongTermKeyUsage

Equations

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

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

Equations

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

Instances For

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

Function.Injective mkLongTermUsage

@[instance_reducible]

instance DY.Example.SignedDH.SignedDHSignPred [HasProofTrace] :

Signature.SignPred

Equations

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

class DY.Example.SignedDH.HasBytesInvariantsextends DY.Example.SignedDH.HasProofTrace :

Instances

@[instance_reducible]

instance DY.Example.SignedDH.ClientInitiateStateInv [HasBytesInvariants] :

PersistentLocalState.CompromisableLocalStateInv ClientInitiateState

Equations

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

theorem DY.Example.SignedDH.ClientInitiateStateInv_imp_Invariant [HasBytesInvariants] {tr : ProofTrace} (participant : Participant) (st : ClientInitiateState) :

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

@[instance_reducible]

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

PersistentLocalState.CompromisableLocalStateInv ClientFinishState

Equations

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

@[instance_reducible]

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

PersistentLocalState.CompromisableLocalStateInv ServerFinishState

Equations

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

@[instance_reducible]

instance DY.Example.SignedDH.instProofConfigMkLongTermUsageLabel [HasBytesInvariants] :

LongTermKeys.ProofConfig "SignedDH PKI" mkLongTermUsage (LongTermKeys.label "SignedDH PKI")

Equations

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

@[instance_reducible]

instance DY.Example.SignedDH.SignedDHEventInv [HasBytesInvariants] :

ProtocolEvent.EventInv SignedDHEvent

Equations

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

class DY.Example.SignedDH.HasTraceInvariantextends DY.Example.SignedDH.HasBytesInvariants :

Instances

instance DY.Example.SignedDH.Client.initiate.spec [HasTraceInvariant] (me : Participant) :

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

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

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

instance DY.Example.SignedDH.Client.finish.spec [HasTraceInvariant] (me server : Participant) (pkHandle msgHandle stHandle : Nat) :

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

instance DY.Example.SignedDH.ClientInitiateState.compromise.spec [HasTraceInvariant] (stHandle : Nat) :

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

instance DY.Example.SignedDH.ClientFinishState.compromise.spec [HasTraceInvariant] (stHandle : Nat) :

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

instance DY.Example.SignedDH.ServerFinishState.compromise.spec [HasTraceInvariant] (stHandle : Nat) :

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

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

ReachableImpliesInvariant Client.initiate.reachability

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

ReachableImpliesInvariant Server.receive.reachability

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

ReachableImpliesInvariant Client.finish.reachability

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

ReachableImpliesInvariant ClientInitiateState.compromise.reachability

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

ReachableImpliesInvariant ClientFinishState.compromise.reachability

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

ReachableImpliesInvariant ServerFinishState.compromise.reachability