def DY.Example.MerkleTree.honestAttacker : Traceful Unit

Equations

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

theorem DY.Example.MerkleTree.honestAttacker_properties : have tr := (honestAttacker.run Trace.nil).snd.val; Trace.Reachable reachability tr ∧ ∃ (t1 : Nat), ∃ (t2 : Nat), ∃ (msg : Bytes), t1 < t2 ∧ Trace.EventLoggedAt (TheEvent.ServerAuthenticated "Bob" msg) t1 tr ∧ Trace.EventLoggedAt (TheEvent.ClientAccept "Bob" msg) t2 tr

def DY.Example.MerkleTree.compromiseSigKeyAttacker : Traceful Unit

Equations

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

theorem DY.Example.MerkleTree.compromiseSigKeyAttacker_properties : have tr := (compromiseSigKeyAttacker.run Trace.nil).snd.val; Trace.Reachable reachability tr ∧ ∃ (t1 : Nat), ∃ (element : Bytes), Trace.EventLoggedAt (TheEvent.ClientAccept "Bob" element) t1 tr ∧ ∀ (t2 : Nat), ¬Trace.EventLoggedAt (TheEvent.ServerAuthenticated "Bob" element) t2 tr