Documentation

Examples.ACME.WithDEO.Attack

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