class DY.Example.SignedDH.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
• 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

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

• xPk : Bytes

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

• yPk : Bytes
• sig : Bytes

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

• xPk : Bytes
• yPk : Bytes

structure DY.Example.SignedDH.ClientInitiateState [HasExecBytes] : Type

• xPk : Bytes
• xSk : Bytes

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

• xPk : Bytes
• kC : Bytes

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

• yPk : Bytes
• kS : Bytes

inductive DY.Example.SignedDH.SignedDHEvent [HasExecBytes] : Type

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

def DY.Example.SignedDH.instDecidableEqSignedDHEvent.decEq {inst✝ : HasExecBytes} (x✝ x✝¹ : SignedDHEvent) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance DY.Example.SignedDH.instDecidableEqSignedDHEvent {inst✝ : HasExecBytes} : DecidableEq SignedDHEvent

Equations

• DY.Example.SignedDH.instDecidableEqSignedDHEvent = DY.Example.SignedDH.instDecidableEqSignedDHEvent.decEq

@[instance_reducible]

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

Equations

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

theorem DY.Example.SignedDH.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

@[instance_reducible]

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

Equations

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

theorem DY.Example.SignedDH.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.sig tr)

@[instance_reducible]

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

Equations

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

theorem DY.Example.SignedDH.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)

@[instance_reducible]

instance DY.Example.SignedDH.instParseableSerializeableClientInitiateState [HasExecBytes] : Comparse.ParseableSerializeable ClientInitiateState

Equations

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

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

@[instance_reducible]

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

Equations

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

theorem DY.Example.SignedDH.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.kC tr)

@[instance_reducible]

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

Equations

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

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

class DY.Example.SignedDH.HasExecTrace extends DY.Example.SignedDH.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
• 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

@[instance_reducible]

instance DY.Example.SignedDH.instExecConfigVkBytes_examples [HasExecTrace] : LongTermKeys.ExecConfig "SignedDH PKI" Signature.vk

Equations

• DY.Example.SignedDH.instExecConfigVkBytes_examples = { }

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

Equations

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

def DY.Example.SignedDH.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.SignedDH.Client.finish [HasExecTrace] (me server : Participant) (pkHandle msgHandle stHandle : Nat) : Traceful Nat

Equations

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

def DY.Example.SignedDH.ClientInitiateState.compromise [HasExecTrace] (stHandle : Nat) : Traceful Nat

Equations

• DY.Example.SignedDH.ClientInitiateState.compromise stHandle = DY.PersistentLocalState.compromise DY.Example.SignedDH.ClientInitiateState stHandle

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

Equations

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

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

Equations

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

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

Equations

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

theorem DY.Example.SignedDH.ClientEphemeralStateCompromised_le [HasExecTrace] (me : Participant) (xPk : Bytes) (tr1 tr2 : ExecTrace) : tr1 ≤ tr2 → ClientEphemeralStateCompromised me xPk tr1 → ClientEphemeralStateCompromised me xPk tr2

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

Equations

• DY.Example.SignedDH.ServerEphemeralStateCompromised me yPk tr = ∃ (kS : DY.Bytes), DY.PersistentLocalState.LocalStateCompromised me { yPk := yPk, kS := kS } tr

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

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

Equations

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

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

Equations

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

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

Equations

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

def DY.Example.SignedDH.ClientInitiateState.compromise.reachability [HasExecTrace] : ReachabilityConfig

Equations

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

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

Equations

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

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

Equations

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

@[instance_reducible]

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

Equations

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

def DY.Example.SignedDH.reachability.internal [HasExecTrace] : Fin 8 → ReachabilityConfig

Equations

• DY.Example.SignedDH.reachability.internal 0 = DY.Network.reachability
• DY.Example.SignedDH.reachability.internal 1 = DY.LongTermKeys.reachability "SignedDH PKI"
• DY.Example.SignedDH.reachability.internal 2 = DY.Example.SignedDH.Client.initiate.reachability
• DY.Example.SignedDH.reachability.internal 3 = DY.Example.SignedDH.Server.receive.reachability
• DY.Example.SignedDH.reachability.internal 4 = DY.Example.SignedDH.Client.finish.reachability
• DY.Example.SignedDH.reachability.internal 5 = DY.Example.SignedDH.ClientInitiateState.compromise.reachability
• DY.Example.SignedDH.reachability.internal 6 = DY.Example.SignedDH.ClientFinishState.compromise.reachability
• DY.Example.SignedDH.reachability.internal 7 = DY.Example.SignedDH.ServerFinishState.compromise.reachability
• DY.Example.SignedDH.reachability.internal ⟨n.succ.succ.succ.succ.succ.succ.succ.succ, isLt⟩ = ⋯.elim