Formal Verification of e-Reputation Protocols

Reputation systems are often useful in large online communities in which most of the users are unknown to each other. They are good tools to force the users to act in truthfulness way. However, for a reputation system to work effectively users have to be willing to provide rates. In order to incentivize the users to provide honest rates, a reputation system have to ensure their privacy and anonymity. Users are also concerned about verifying the correctness of the reputation score. In the applied pi-calculus, we define a formal framework and several fundamental privacy, authentication, and verifiability properties suitable for the security analysis of e-reputation protocols. As proof of concept, using ProVerif, we analyze a simple additive decentralized reputation protocol proposed to ensure rate privacy if all users are honest.