Documentation

Examples.ACME.WithoutDEO.Proof

class DY.Example.ACME.WithoutDEO.HasExecBytesWithoutDEO :

bytesFunc : BytesFunctor
bytesFunc0 : BytesFunctor.Has Random.SubF
bytesFunc1 : BytesFunctor.Has Literal.SubF
bytesFunc2 : BytesFunctor.Has Concat.SubF
bytesFunc3 : BytesFunctor.Has Signature.SubF
bytesLen : BytesLength
bytesLen0 : BytesLength.Has Random.SubF.length
bytesLen1 : BytesLength.Has Literal.SubF.length
bytesLen2 : BytesLength.Has Concat.SubF.length
bytesLen3 : BytesLength.Has Signature.SubF.length
att : AttackerKnowledge
att0 : AttackerKnowledge.Has Random.attackerKnowledge
att1 : AttackerKnowledge.Has Literal.attackerKnowledge
att2 : AttackerKnowledge.Has Concat.attackerKnowledge
att3 : AttackerKnowledge.Has Signature.attackerKnowledge

Instances

@[instance_reducible]

instance DY.Example.ACME.WithoutDEO.instHasExecBytesOfHasExecBytesWithoutDEO [HasExecBytesWithoutDEO] :

Equations

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

class DY.Example.ACME.WithoutDEO.HasExecTraceWithoutDEO extends DY.Example.ACME.WithoutDEO.HasExecBytesWithoutDEO :

bytesFunc : BytesFunctor
bytesFunc0 : BytesFunctor.Has Random.SubF
bytesFunc1 : BytesFunctor.Has Literal.SubF
bytesFunc2 : BytesFunctor.Has Concat.SubF
bytesFunc3 : BytesFunctor.Has Signature.SubF
bytesLen : BytesLength
bytesLen0 : BytesLength.Has Random.SubF.length
bytesLen1 : BytesLength.Has Literal.SubF.length
bytesLen2 : BytesLength.Has Concat.SubF.length
bytesLen3 : BytesLength.Has Signature.SubF.length
att : AttackerKnowledge
att0 : AttackerKnowledge.Has Random.attackerKnowledge
att1 : AttackerKnowledge.Has Literal.attackerKnowledge
att2 : AttackerKnowledge.Has Concat.attackerKnowledge
att3 : AttackerKnowledge.Has Signature.attackerKnowledge
traceExec : ExecTraceTypes
traceExec0 : ExecTraceTypes.Has Network.ExecEntryT
traceExec1 : ExecTraceTypes.Has Random.ExecEntryT
traceExec2 : ExecTraceTypes.Has (ProtocolEvent.ExecEntryT ACMEEvent)
traceExec3 : ExecTraceTypes.Has (PersistentLocalState.CompromisableState.ExecEntryT OwnerKeyState)
traceExec4 : ExecTraceTypes.Has (PersistentLocalState.CompromisableState.ExecEntryT OwnerAddressState)
traceExec5 : ExecTraceTypes.Has (PersistentLocalState.CompromisableState.ExecEntryT LetsEncryptPendingChallengeState)
traceExec6 : ExecTraceTypes.Has (PersistentGlobalState.CompromisableState.ExecEntryT DNSEntry)
traceExec7 : ExecTraceTypes.Has (LongTermKeys.ExecEntryT "ACME PKI")
attBase : BaseAttackerKnowledge

Instances

@[instance_reducible]

instance DY.Example.ACME.WithoutDEO.instHasExecTraceOfHasExecTraceWithoutDEO [HasExecTraceWithoutDEO] :

Equations

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

class DY.Example.ACME.WithoutDEO.HasProofTrace extends DY.Example.ACME.WithoutDEO.HasExecTraceWithoutDEO :

bytesFunc : BytesFunctor
bytesFunc0 : BytesFunctor.Has Random.SubF
bytesFunc1 : BytesFunctor.Has Literal.SubF
bytesFunc2 : BytesFunctor.Has Concat.SubF
bytesFunc3 : BytesFunctor.Has Signature.SubF
bytesLen : BytesLength
bytesLen0 : BytesLength.Has Random.SubF.length
bytesLen1 : BytesLength.Has Literal.SubF.length
bytesLen2 : BytesLength.Has Concat.SubF.length
bytesLen3 : BytesLength.Has Signature.SubF.length
att : AttackerKnowledge
att0 : AttackerKnowledge.Has Random.attackerKnowledge
att1 : AttackerKnowledge.Has Literal.attackerKnowledge
att2 : AttackerKnowledge.Has Concat.attackerKnowledge
att3 : AttackerKnowledge.Has Signature.attackerKnowledge
traceExec : ExecTraceTypes
traceExec0 : ExecTraceTypes.Has Network.ExecEntryT
traceExec1 : ExecTraceTypes.Has Random.ExecEntryT
traceExec2 : ExecTraceTypes.Has (ProtocolEvent.ExecEntryT ACMEEvent)
traceExec3 : ExecTraceTypes.Has (PersistentLocalState.CompromisableState.ExecEntryT OwnerKeyState)
traceExec4 : ExecTraceTypes.Has (PersistentLocalState.CompromisableState.ExecEntryT OwnerAddressState)
traceExec5 : ExecTraceTypes.Has (PersistentLocalState.CompromisableState.ExecEntryT LetsEncryptPendingChallengeState)
traceExec6 : ExecTraceTypes.Has (PersistentGlobalState.CompromisableState.ExecEntryT DNSEntry)
traceExec7 : ExecTraceTypes.Has (LongTermKeys.ExecEntryT "ACME PKI")
attBase : BaseAttackerKnowledge
traceProof : ProofTraceTypes
traceProof0 : ProofTraceTypes.Has Network.ProofEntryT
traceProof1 : ProofTraceTypes.Has Random.ProofEntryT
traceProof2 : ProofTraceTypes.Has (ProtocolEvent.ProofEntryT ACMEEvent)
traceProof3 : ProofTraceTypes.Has (PersistentLocalState.CompromisableState.ProofEntryT OwnerKeyState)
traceProof4 : ProofTraceTypes.Has (PersistentLocalState.CompromisableState.ProofEntryT OwnerAddressState)
traceProof5 : ProofTraceTypes.Has (PersistentLocalState.CompromisableState.ProofEntryT LetsEncryptPendingChallengeState)
traceProof6 : ProofTraceTypes.Has (PersistentGlobalState.CompromisableState.ProofEntryT DNSEntry)
traceProof7 : ProofTraceTypes.Has (LongTermKeys.ProofEntryT "ACME PKI")

Instances

@[instance_reducible]

instance DY.Example.ACME.WithoutDEO.instSignPred [HasProofTrace] :

Signature.SignPred

Equations

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

instance DY.Example.ACME.WithoutDEO.instSignPredProof_examples [HasProofTrace] [BytesInvariants] :

Signature.SignPredProof

class DY.Example.ACME.WithoutDEO.HasBytesInvariants extends DY.Example.ACME.WithoutDEO.HasProofTrace :

Instances

def DY.Example.ACME.WithoutDEO.sigAcmeUsage [HasBytesInvariants] :

Equations

DY.Example.ACME.WithoutDEO.sigAcmeUsage = { type := "SigKey", tag := "ACME PKI", data := none }

Instances For

@[instance_reducible]

instance DY.Example.ACME.WithoutDEO.OwnerKeyStateInv [HasBytesInvariants] :

PersistentLocalState.CompromisableLocalStateInv OwnerKeyState

Equations

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

theorem DY.Example.ACME.WithoutDEO.OwnerKeyStateInv_imp_Invariant [HasBytesInvariants] (participant : Participant) (st : OwnerKeyState) (tr : ProofTrace) :

PersistentLocalState.LocalStateInv.invariant participant st tr → st.oSk.Invariant tr

@[instance_reducible]

instance DY.Example.ACME.WithoutDEO.OwnerAddressStateInv [HasBytesInvariants] :

PersistentLocalState.CompromisableLocalStateInv OwnerAddressState

Equations

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

@[instance_reducible]

instance DY.Example.ACME.WithoutDEO.LetsEncryptPendingChallengeStateInv [HasBytesInvariants] :

PersistentLocalState.CompromisableLocalStateInv LetsEncryptPendingChallengeState

Equations

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

theorem DY.Example.ACME.WithoutDEO.LetsEncryptPendingChallengeStateInv_imp_Invariant [HasBytesInvariants] (participant : Participant) (st : LetsEncryptPendingChallengeState) (tr : ProofTrace) :

PersistentLocalState.LocalStateInv.invariant participant st tr → st.token.Invariant tr

@[instance_reducible]

instance DY.Example.ACME.WithoutDEO.DNSEntryInv [HasBytesInvariants] :

PersistentGlobalState.CompromisableGlobalStateInv DNSEntry

Equations

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

@[instance_reducible]

instance DY.Example.ACME.WithoutDEO.instProofConfigSigAcmeUsageLabel [HasBytesInvariants] :

LongTermKeys.ProofConfig "ACME PKI" (fun (x : Participant) => sigAcmeUsage) (LongTermKeys.label "ACME PKI")

Equations

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

@[instance_reducible]

instance DY.Example.ACME.WithoutDEO.SignedDHEventInv [HasBytesInvariants] :

ProtocolEvent.EventInv ACMEEvent

Equations

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

class DY.Example.ACME.WithoutDEO.HasTraceInvariant extends DY.Example.ACME.WithoutDEO.HasBytesInvariants :

Instances

instance DY.Example.ACME.WithoutDEO.Owner.generateKeyPair.proof [HasTraceInvariant] (owner : Participant) :

HoareTriple (Owner.generateKeyPair owner) (fun (x : ProofTrace) => True) fun (x : Nat × Nat) (x_1 : ProofTrace) => True

instance DY.Example.ACME.WithoutDEO.Owner.claimAddress.proof [HasTraceInvariant] (owner : Participant) (address : String) (oSkHandle : Nat) :

HoareTriple (Owner.claimAddress owner address oSkHandle) (fun (x : ProofTrace) => True) fun (x : Nat) (x_1 : ProofTrace) => True

instance DY.Example.ACME.WithoutDEO.LetsEncrypt.initiate.proof [HasTraceInvariant] (server : Participant) (address : String) (skHandle : Nat) :

HoareTriple (LetsEncrypt.initiate server address skHandle) (fun (x : ProofTrace) => True) fun (x : Nat × Nat) (x_1 : ProofTrace) => True

instance DY.Example.ACME.WithoutDEO.Owner.respond.proof [HasTraceInvariant] (owner server : Participant) (msgHandle lePkHandle stHandle : Nat) :

HoareTriple (Owner.respond owner server msgHandle lePkHandle stHandle) (fun (x : ProofTrace) => True) fun (x : Nat × Nat) (x_1 : ProofTrace) => True

theorem DY.Example.ACME.WithoutDEO.instHoareTriplePureGhostBoolUsageVerifyBytesTrueEqOfBytesInvariants_examples [HasTraceInvariant] {skUsg : Usage} [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] (vkey msg sig : Bytes) :

HoareTriplePureGhost (Signature.verify vkey msg sig) skUsg (fun (_tr : ProofTrace) => True) fun (res : Bool) (_tr : ProofTrace) => res = Signature.verify vkey msg sig

theorem DY.Example.ACME.WithoutDEO.verify_implies_signature [HasTraceInvariant] (vkey msg sig : Bytes) :

Signature.verify vkey msg sig = true → ∃ (sk : Bytes ), ∃ (nonce : Bytes ), vkey = Signature.vk sk ∧ sig = Signature.sign sk nonce msg

theorem DY.Example.ACME.WithoutDEO.sign_injective [HasTraceInvariant] (sk1 sk2 nonce1 nonce2 msg1 msg2 : Bytes) :

Signature.sign sk1 nonce1 msg1 = Signature.sign sk2 nonce2 msg2 → sk1 = sk2

instance DY.Example.ACME.WithoutDEO.LetsEncrypt.finish.proof [HasTraceInvariant] (server : Participant) (msgHandle pendingStHandle dnsEntryHandle : Nat) :

HoareTriple (LetsEncrypt.finish server msgHandle pendingStHandle dnsEntryHandle) (fun (x : ProofTrace) => True) fun (x : Unit) (x_1 : ProofTrace) => True

instance DY.Example.ACME.WithoutDEO.OwnerKeyState.compromise.proof [HasTraceInvariant] (stHandle : Nat) :

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

instance DY.Example.ACME.WithoutDEO.OwnerAddressState.compromise.proof [HasTraceInvariant] (stHandle : Nat) :

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

instance DY.Example.ACME.WithoutDEO.LetsEncryptPendingChallengeState.compromise.proof [HasTraceInvariant] (stHandle : Nat) :

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

instance DY.Example.ACME.WithoutDEO.DNSEntry.compromise.proof [HasTraceInvariant] (stHandle : Nat) :

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

instance DY.Example.ACME.WithoutDEO.instReachableImpliesInvariantReachability [HasTraceInvariant] :

ReachableImpliesInvariant Owner.generateKeyPair.reachability

instance DY.Example.ACME.WithoutDEO.instReachableImpliesInvariantReachability_1 [HasTraceInvariant] :

ReachableImpliesInvariant Owner.claimAddress.reachability

instance DY.Example.ACME.WithoutDEO.instReachableImpliesInvariantReachability_2 [HasTraceInvariant] :

ReachableImpliesInvariant LetsEncrypt.initiate.reachability

instance DY.Example.ACME.WithoutDEO.instReachableImpliesInvariantReachability_3 [HasTraceInvariant] :

ReachableImpliesInvariant Owner.respond.reachability

instance DY.Example.ACME.WithoutDEO.instReachableImpliesInvariantReachability_4 [HasTraceInvariant] :

ReachableImpliesInvariant LetsEncrypt.finish.reachability

instance DY.Example.ACME.WithoutDEO.instReachableImpliesInvariantReachability_5 [HasTraceInvariant] :

ReachableImpliesInvariant OwnerKeyState.compromise.reachability

instance DY.Example.ACME.WithoutDEO.instReachableImpliesInvariantReachability_6 [HasTraceInvariant] :

ReachableImpliesInvariant OwnerAddressState.compromise.reachability

instance DY.Example.ACME.WithoutDEO.instReachableImpliesInvariantReachability_7 [HasTraceInvariant] :

ReachableImpliesInvariant LetsEncryptPendingChallengeState.compromise.reachability

instance DY.Example.ACME.WithoutDEO.instReachableImpliesInvariantReachability_8 [HasTraceInvariant] :

ReachableImpliesInvariant DNSEntry.compromise.reachability