theorem DY.Example.SignedDH.client_auth (client server : Participant) (xPk yPk k : Bytes) (time : Nat) (tr : ExecTrace) : Trace.Reachable reachability tr → Trace.EventLoggedAt (SignedDHEvent.ClientFinishEvent client server xPk yPk k) time tr → have tr_before := Trace.prefix tr time; Trace.EventLogged (SignedDHEvent.ServerFinishEvent server xPk yPk k) tr_before ∨ ∃ (spk : Bytes), LongTermKeys.LongTermKeyCompromised "SignedDH PKI" server spk tr_before

theorem DY.Example.SignedDH.client_secrecy {time : Nat} (client server : Participant) (xPk yPk k : Bytes) (tr : ExecTrace) : Trace.Reachable reachability tr → k.AttackerKnows tr → Trace.EventLoggedAt (SignedDHEvent.ClientFinishEvent client server xPk yPk k) time tr → have tr_before := Trace.prefix tr time; (∃ (spk : Bytes), LongTermKeys.LongTermKeyCompromised "SignedDH PKI" server spk tr_before) ∨ ClientEphemeralStateCompromised client xPk tr ∨ ServerEphemeralStateCompromised server yPk tr