def DY.Example.SignedDHKEM.honestAttacker : Traceful Unit

Equations

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

theorem DY.Example.SignedDHKEM.honestAttacker_properties : have tr := (honestAttacker.run Trace.nil).snd.val; Trace.Reachable reachability tr ∧ ∃ (t1 : Nat), ∃ (t2 : Nat), ∃ (xPk : Bytes), ∃ (yPk : Bytes), ∃ (zPk : Bytes), ∃ (k : Bytes), t1 < t2 ∧ Trace.EventLoggedAt (SignedDHKEMEvent.ServerFinishEvent "Bob" xPk yPk zPk k) t1 tr ∧ Trace.EventLoggedAt (SignedDHKEMEvent.ClientFinishEvent "Alice" "Bob" xPk yPk zPk k) t2 tr

def DY.Example.SignedDHKEM.breakDhAndKemAttacker : Traceful Unit

Equations

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

theorem DY.Example.SignedDHKEM.breakDhAndKemAttacker_properties : have tr := (breakDhAndKemAttacker.run Trace.nil).snd.val; Trace.Reachable reachability tr ∧ ∃ (t1 : Nat), ∃ (xPk : Bytes), ∃ (yPk : Bytes), ∃ (zPk : Bytes), ∃ (k : Bytes), Trace.EventLoggedAt (SignedDHKEMEvent.ClientFinishEvent "Alice" "Bob" xPk yPk zPk k) t1 tr ∧ k.AttackerKnows tr

def DY.Example.SignedDHKEM.breakSigKeyAttacker : Traceful Unit

Equations

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

theorem DY.Example.SignedDHKEM.breakSigKeyAttacker_properties : have tr := (breakSigKeyAttacker.run Trace.nil).snd.val; Trace.Reachable reachability tr ∧ ∃ (t1 : Nat), ∃ (xPk : Bytes), ∃ (yPk : Bytes), ∃ (zPk : Bytes), ∃ (k : Bytes), Trace.EventLoggedAt (SignedDHKEMEvent.ClientFinishEvent "Alice" "Bob" xPk yPk zPk k) t1 tr ∧ k.AttackerKnows tr