On Backward-Style Verification for Timed Anonymity of Security Protocols

Trace anonymity is an extension of the formulation of anonymity by Schneider and Sidiropoulos. To prove the trace anonymity of infinite-state or unbounded systems, we have introduced proof techniques in which we find a binary relation called an anonymous simulation. There are two sorts of anonymous simulation methods a forward-style method and a backward-style method. In our previous work, we discussed a proof technique for the anonymity of real-time systems, and the approach was based on the forward-style method. In this study, we concentrate on the backward-style method, and we discuss how to prove the timed anonymity.