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

theorem DY.Example.SignedDHKEM.client_secrecy {time : Nat} (client server : Participant) (xPk yPk zPk k : Bytes) (tr : ExecTrace) : Trace.Reachable reachability tr → k.AttackerKnows tr → Trace.EventLoggedAt (SignedDHKEMEvent.ClientFinishEvent client server xPk yPk zPk k) time tr → have tr_before := Trace.prefix tr time; (∃ (spk : Bytes), LongTermKeys.LongTermKeyCompromised "SignedDHKEM PKI" server spk tr_before ∨ Signature'.Broken.ThisVkHasBeenBroken spk tr_before) ∨ (ClientEphemeralDHStateCompromised client xPk tr ∨ DiffieHellman'.Broken.ThisDhPkHasBeenBroken xPk tr ∨ DiffieHellman'.Broken.ThisDhPkHasBeenBroken yPk tr) ∧ (ClientEphemeralKEMStateCompromised client zPk tr ∨ KEM.Broken.ThisKemPkHasBeenBroken zPk tr) ∨ ServerEphemeralStateCompromised server xPk yPk zPk tr