class DY.Example.SignedDHKEM.HasExecBytes : 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

structure DY.Example.SignedDHKEM.ClientMessage [HasExecBytes] : Type

• xPk : Bytes
• zPk : Bytes

structure DY.Example.SignedDHKEM.ServerMessage [HasExecBytes] : Type

• yPk : Bytes
• ct : Bytes
• sig : Bytes

structure DY.Example.SignedDHKEM.SigInput [HasExecBytes] : Type

• xPk : Bytes
• yPk : Bytes
• zPk : Bytes
• ct : Bytes

structure DY.Example.SignedDHKEM.ClientInitiateDHState [HasExecBytes] : Type

• xPk : Bytes
• xSk : Bytes

structure DY.Example.SignedDHKEM.ClientInitiateKEMState [HasExecBytes] : Type

• zPk : Bytes
• zSk : Bytes

structure DY.Example.SignedDHKEM.ClientFinishState [HasExecBytes] : Type

• xPk : Bytes
• zPk : Bytes
• kC : Bytes

structure DY.Example.SignedDHKEM.ServerFinishState [HasExecBytes] : Type

• xPk : Bytes
• yPk : Bytes
• zPk : Bytes
• kS : Bytes

inductive DY.Example.SignedDHKEM.SignedDHKEMEvent [HasExecBytes] : Type

• ClientInitiateEvent [HasExecBytes] (client : Participant) (xPk zPk : Bytes) : SignedDHKEMEvent
• ServerFinishEvent [HasExecBytes] (server : Participant) (xPk yPk zPk kS : Bytes) : SignedDHKEMEvent
• ClientFinishEvent [HasExecBytes] (client server : Participant) (xPk yPk zPk kC : Bytes) : SignedDHKEMEvent

@[instance_reducible]

instance DY.Example.SignedDHKEM.instDecidableEqSignedDHKEMEvent {inst✝ : HasExecBytes} : DecidableEq SignedDHKEMEvent

Equations

• DY.Example.SignedDHKEM.instDecidableEqSignedDHKEMEvent = DY.Example.SignedDHKEM.instDecidableEqSignedDHKEMEvent.decEq

def DY.Example.SignedDHKEM.instDecidableEqSignedDHKEMEvent.decEq {inst✝ : HasExecBytes} (x✝ x✝¹ : SignedDHKEMEvent) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance DY.Example.SignedDHKEM.instParseableSerializeableClientMessage [HasExecBytes] : Comparse.ParseableSerializeable ClientMessage

Equations

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

theorem DY.Example.SignedDHKEM.ClientMessage.IsWellFormed_eq [HasExecBytes] {τ : Sort u_1} (pre : Bytes → τ → Prop) [Comparse.BytesCompatibleTracePred pre] (x : ClientMessage) (tr : τ) : Comparse.IsWellFormed pre x tr = (pre x.xPk tr ∧ pre x.zPk tr)

@[instance_reducible]

instance DY.Example.SignedDHKEM.instParseableSerializeableServerMessage [HasExecBytes] : Comparse.ParseableSerializeable ServerMessage

Equations

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

theorem DY.Example.SignedDHKEM.ServerMessage.IsWellFormed_eq [HasExecBytes] {τ : Sort u_1} (pre : Bytes → τ → Prop) [Comparse.BytesCompatibleTracePred pre] (x : ServerMessage) (tr : τ) : Comparse.IsWellFormed pre x tr = (pre x.yPk tr ∧ pre x.ct tr ∧ pre x.sig tr)

@[instance_reducible]

instance DY.Example.SignedDHKEM.instParseableSerializeableSigInput [HasExecBytes] : Comparse.ParseableSerializeable SigInput

Equations

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

theorem DY.Example.SignedDHKEM.SigInput.IsWellFormed_eq [HasExecBytes] {τ : Sort u_1} (pre : Bytes → τ → Prop) [Comparse.BytesCompatibleTracePred pre] (x : SigInput) (tr : τ) : Comparse.IsWellFormed pre x tr = (pre x.xPk tr ∧ pre x.yPk tr ∧ pre x.zPk tr ∧ pre x.ct tr)

@[instance_reducible]

instance DY.Example.SignedDHKEM.instParseableSerializeableClientInitiateDHState [HasExecBytes] : Comparse.ParseableSerializeable ClientInitiateDHState

Equations

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

theorem DY.Example.SignedDHKEM.ClientInitiateDHState.IsWellFormed_eq [HasExecBytes] {τ : Sort u_1} (pre : Bytes → τ → Prop) [Comparse.BytesCompatibleTracePred pre] (x : ClientInitiateDHState) (tr : τ) : Comparse.IsWellFormed pre x tr = (pre x.xPk tr ∧ pre x.xSk tr)

@[instance_reducible]

instance DY.Example.SignedDHKEM.instParseableSerializeableClientInitiateKEMState [HasExecBytes] : Comparse.ParseableSerializeable ClientInitiateKEMState

Equations

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

theorem DY.Example.SignedDHKEM.ClientInitiateKEMState.IsWellFormed_eq [HasExecBytes] {τ : Sort u_1} (pre : Bytes → τ → Prop) [Comparse.BytesCompatibleTracePred pre] (x : ClientInitiateKEMState) (tr : τ) : Comparse.IsWellFormed pre x tr = (pre x.zPk tr ∧ pre x.zSk tr)

@[instance_reducible]

instance DY.Example.SignedDHKEM.instParseableSerializeableClientFinishState [HasExecBytes] : Comparse.ParseableSerializeable ClientFinishState

Equations

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

theorem DY.Example.SignedDHKEM.ClientFinishState.IsWellFormed_eq [HasExecBytes] {τ : Sort u_1} (pre : Bytes → τ → Prop) [Comparse.BytesCompatibleTracePred pre] (x : ClientFinishState) (tr : τ) : Comparse.IsWellFormed pre x tr = (pre x.xPk tr ∧ pre x.zPk tr ∧ pre x.kC tr)

@[instance_reducible]

instance DY.Example.SignedDHKEM.instParseableSerializeableServerFinishState [HasExecBytes] : Comparse.ParseableSerializeable ServerFinishState

Equations

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

theorem DY.Example.SignedDHKEM.ServerFinishState.IsWellFormed_eq [HasExecBytes] {τ : Sort u_1} (pre : Bytes → τ → Prop) [Comparse.BytesCompatibleTracePred pre] (x : ServerFinishState) (tr : τ) : Comparse.IsWellFormed pre x tr = (pre x.xPk tr ∧ pre x.yPk tr ∧ pre x.zPk tr ∧ pre x.kS tr)

class DY.Example.SignedDHKEM.HasExecTraceextends DY.Example.SignedDHKEM.HasExecBytes : 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

@[instance_reducible]

instance DY.Example.SignedDHKEM.instExecConfigVkBytes [HasExecTrace] : LongTermKeys.ExecConfig "SignedDHKEM PKI" Signature'.vk

Equations

• DY.Example.SignedDHKEM.instExecConfigVkBytes = { }

def DY.Example.SignedDHKEM.Client.initiate [HasExecTrace] (me : Participant) : Traceful (Nat × Nat × Nat)

Equations

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

def DY.Example.SignedDHKEM.Server.receive [HasExecTrace] (me : Participant) (skHandle msgHandle : Nat) : Traceful (Nat × Nat)

Equations

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

def DY.Example.SignedDHKEM.Client.finish [HasExecTrace] (me server : Participant) (pkHandle msgHandle dhStHandle kemStHandle : Nat) : Traceful Nat

Equations

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

def DY.Example.SignedDHKEM.ClientInitiateDHState.compromise [HasExecTrace] (stHandle : Nat) : Traceful Nat

Equations

• DY.Example.SignedDHKEM.ClientInitiateDHState.compromise stHandle = DY.PersistentLocalState.compromise DY.Example.SignedDHKEM.ClientInitiateDHState stHandle

def DY.Example.SignedDHKEM.ClientInitiateKEMState.compromise [HasExecTrace] (stHandle : Nat) : Traceful Nat

Equations

• DY.Example.SignedDHKEM.ClientInitiateKEMState.compromise stHandle = DY.PersistentLocalState.compromise DY.Example.SignedDHKEM.ClientInitiateKEMState stHandle

def DY.Example.SignedDHKEM.ClientFinishState.compromise [HasExecTrace] (stHandle : Nat) : Traceful Nat

Equations

• DY.Example.SignedDHKEM.ClientFinishState.compromise stHandle = DY.PersistentLocalState.compromise DY.Example.SignedDHKEM.ClientFinishState stHandle

def DY.Example.SignedDHKEM.ServerFinishState.compromise [HasExecTrace] (stHandle : Nat) : Traceful Nat

Equations

• DY.Example.SignedDHKEM.ServerFinishState.compromise stHandle = DY.PersistentLocalState.compromise DY.Example.SignedDHKEM.ServerFinishState stHandle

def DY.Example.SignedDHKEM.ClientEphemeralDHStateCompromised [HasExecTrace] (me : Participant) (xPk : Bytes) (tr : ExecTrace) : Prop

Equations

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

theorem DY.Example.SignedDHKEM.ClientEphemeralDHStateCompromised_le [HasExecTrace] (me : Participant) (xPk : Bytes) (tr1 tr2 : ExecTrace) : tr1 ≤ tr2 → ClientEphemeralDHStateCompromised me xPk tr1 → ClientEphemeralDHStateCompromised me xPk tr2

def DY.Example.SignedDHKEM.ClientEphemeralKEMStateCompromised [HasExecTrace] (me : Participant) (zPk : Bytes) (tr : ExecTrace) : Prop

Equations

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

theorem DY.Example.SignedDHKEM.ClientEphemeralKEMStateCompromised_le [HasExecTrace] (me : Participant) (zPk : Bytes) (tr1 tr2 : ExecTrace) : tr1 ≤ tr2 → ClientEphemeralKEMStateCompromised me zPk tr1 → ClientEphemeralKEMStateCompromised me zPk tr2

def DY.Example.SignedDHKEM.ServerEphemeralStateCompromised [HasExecTrace] (me : Participant) (xPk yPk zPk : Bytes) (tr : ExecTrace) : Prop

Equations

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

theorem DY.Example.SignedDHKEM.ServerEphemeralStateCompromised_le [HasExecTrace] (me : Participant) (xPk yPk zPk : Bytes) (tr1 tr2 : ExecTrace) : tr1 ≤ tr2 → ServerEphemeralStateCompromised me xPk yPk zPk tr1 → ServerEphemeralStateCompromised me xPk yPk zPk tr2

def DY.Example.SignedDHKEM.Client.initiate.reachability [HasExecTrace] : ReachabilityConfig

Equations

• DY.Example.SignedDHKEM.Client.initiate.reachability = DY.ReachabilityConfig.make fun (me : DY.Participant) => DY.Example.SignedDHKEM.Client.initiate me

def DY.Example.SignedDHKEM.Server.receive.reachability [HasExecTrace] : ReachabilityConfig

Equations

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

def DY.Example.SignedDHKEM.Client.finish.reachability [HasExecTrace] : ReachabilityConfig

Equations

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

def DY.Example.SignedDHKEM.ClientInitiateDHState.compromise.reachability [HasExecTrace] : ReachabilityConfig

Equations

• DY.Example.SignedDHKEM.ClientInitiateDHState.compromise.reachability = DY.ReachabilityConfig.make fun (stHandle : Nat) => DY.Example.SignedDHKEM.ClientInitiateDHState.compromise stHandle

def DY.Example.SignedDHKEM.ClientInitiateKEMState.compromise.reachability [HasExecTrace] : ReachabilityConfig

Equations

• DY.Example.SignedDHKEM.ClientInitiateKEMState.compromise.reachability = DY.ReachabilityConfig.make fun (stHandle : Nat) => DY.Example.SignedDHKEM.ClientInitiateKEMState.compromise stHandle

def DY.Example.SignedDHKEM.ServerFinishState.compromise.reachability [HasExecTrace] : ReachabilityConfig

Equations

• DY.Example.SignedDHKEM.ServerFinishState.compromise.reachability = DY.ReachabilityConfig.make fun (stHandle : Nat) => DY.Example.SignedDHKEM.ServerFinishState.compromise stHandle

def DY.Example.SignedDHKEM.ClientFinishState.compromise.reachability [HasExecTrace] : ReachabilityConfig

Equations

• DY.Example.SignedDHKEM.ClientFinishState.compromise.reachability = DY.ReachabilityConfig.make fun (stHandle : Nat) => DY.Example.SignedDHKEM.ClientFinishState.compromise stHandle

def DY.Example.SignedDHKEM.reachability.internal [HasExecTrace] : Fin 12 → ReachabilityConfig

Equations

• DY.Example.SignedDHKEM.reachability.internal 0 = DY.Network.reachability
• DY.Example.SignedDHKEM.reachability.internal 1 = DY.LongTermKeys.reachability "SignedDHKEM PKI"
• DY.Example.SignedDHKEM.reachability.internal 2 = DY.Example.SignedDHKEM.Client.initiate.reachability
• DY.Example.SignedDHKEM.reachability.internal 3 = DY.Example.SignedDHKEM.Server.receive.reachability
• DY.Example.SignedDHKEM.reachability.internal 4 = DY.Example.SignedDHKEM.Client.finish.reachability
• DY.Example.SignedDHKEM.reachability.internal 5 = DY.Example.SignedDHKEM.ClientInitiateDHState.compromise.reachability
• DY.Example.SignedDHKEM.reachability.internal 6 = DY.Example.SignedDHKEM.ClientInitiateKEMState.compromise.reachability
• DY.Example.SignedDHKEM.reachability.internal 7 = DY.Example.SignedDHKEM.ClientFinishState.compromise.reachability
• DY.Example.SignedDHKEM.reachability.internal 8 = DY.Example.SignedDHKEM.ServerFinishState.compromise.reachability
• DY.Example.SignedDHKEM.reachability.internal 9 = DY.KEM.Broken.breakKemPk.reachability
• DY.Example.SignedDHKEM.reachability.internal 10 = DY.DiffieHellman'.Broken.breakDhPk.reachability
• DY.Example.SignedDHKEM.reachability.internal 11 = DY.Signature'.Broken.breakVk.reachability
• DY.Example.SignedDHKEM.reachability.internal ⟨n.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ, isLt⟩ = ⋯.elim

@[instance_reducible]

def DY.Example.SignedDHKEM.reachability [HasExecTrace] : ReachabilityConfig

Equations

• DY.Example.SignedDHKEM.reachability = DY.ReachabilityConfig.combine DY.Example.SignedDHKEM.reachability.internal