A Formal Approach to Designing Anonymous Software

Many Internet services and protocols should guarantee anonymity; for example, an electronic voting system should guarantee to prevent the disclosure of who voted for which candidate. However, a methodology for designing software that preserves anonymity has not yet been established. In the field of software engineering, it is well known that software correctness can be verified with a formal method. Following the formal method approach, this paper introduces an anonymity proof technique. By finding a condition called an anonymous simulation, we prove the anonymity of communication software. Our approach can deal with both eavesdroppers and stronger adversaries. This paper also demonstrates a formal verification of communication software. We employ Crowds, which is an implementation of an anonymous router, and verify the anonymity. After describing Crowds in a formal specification language, we prove its anonymity with a theorem proven In this verification, we employ a formal verification tool called IOA-Toolkit.