theorem DY.Example.MerkleTree.client_authentication (server : Participant) (element : Bytes) (time : Nat) (tr : ExecTrace) : Trace.Reachable reachability tr → Trace.EventLoggedAt (TheEvent.ClientAccept server element) time tr → have tr_before := Trace.prefix tr time; Trace.EventLogged (TheEvent.ServerAuthenticated server element) tr_before ∨ ∃ (spk : Bytes), LongTermKeys.LongTermKeyCompromised "MerkleTree PKI" server spk tr_before