We report on a case study in which the OTS/CafeOBJ method is used to formalize and verify trace anonymity property of distributed systems. In this case study, the property of trace anonymity is formalized with the trace notations of observational transition systems (OTSs), and CafeOBJ language/system is used as an interactive theorem prover to verify that systems satisfy such property. The work presented in the paper follows the approach proposed in [3], in which I/O automaton and Larch prover are employed for handling trace anonymity.
['Weiqiang Kong', 'Kazuhiro Ogata', 'Jian Cheng', 'Kokichi Futatsugi']
Trace anonymity in the OTS/CafeOBJ method