Documentation

Examples.ACME.WithoutDEO.SanityChecks

source
def DY.Example.ACME.WithoutDEO.honestAttacker :
Traceful Unit
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem DY.Example.ACME.WithoutDEO.honestAttacker_properties :
    have tr := (honestAttacker.run Trace.nil).snd.val; Trace.Reachable reachability tr ∧ ∃ (t1 : Nat), ∃ (t2 : Nat), ∃ (oPk : Bytes), t1 < t2 ∧ Trace.EventLoggedAt (ACMEEvent.OwnerRegisterAddress "example.com" oPk) t1 tr ∧ Trace.EventLoggedAt (ACMEEvent.LetsEncryptAcceptAddress "example.com" oPk) t2 tr