The use of a formal method is a promising approach to developing reliable computer programs. This paper presents a formal method for anonymity, which is an important security property of communication protocols with regard to a user's identity. When verifying the anonymity of security protocols, we need to consider the presence of adversaries. To formalize stronger adversaries, we introduce an adversary model for simulation-based anonymity proof. This paper also demonstrates the formal verification of a communication protocol. We employ Crowds, which is an implementation of an anonymous router, and verify its anonymity. After describing Crowds in a formal specification language, we prove its anonymity with a theorem prover.

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. To prove trace anonymity, which is an extension of the formulation of anonymity by Schneider and Sidiropoulos, this paper presents an inductive method based on backward anonymous simulations. We show that the existence of an image-finite backward anonymous simulation implies trace anonymity. We also demonstrate the anonymity verification of an e-voting protocol (the FOO protocol) with our backward anonymous simulation technique. When proving the trace anonymity, this paper employs a computer-assisted verification tool based on a theorem prover.

We present a mathematical formulation of a trust metric using a quality and quantity pair. Under a certain assumption, we regard trust as an additive value and define the soundness of a trust computation as not to exceed the total sum. Moreover, we point out the importance of not only soundness of each computed trust but also the stability of the trust computation procedure against changes in trust value assignment. In this setting, we define trust composition operators. We also propose a trust computation protocol and prove its soundness and stability using the operators.