This talk describes details of a formal analysis of the MUTE system for anonymous file-sharing. We built pi-calculus models of a node that is innocent of sharing files, a node that is guilty of file-sharing and of the network environment. We then tested to see if an attacker can distinguish between a connection to a guilty node and a connection to an innocent node. A "weak bi-simulation" between every guilty network and an innocent network would be required to show possible innocence. We found that such a bi-simulation cannot exist. The point at which the bi-simulation failed lead directly to a previously undiscovered attack on MUTE. We describe a fix for the MUTE system that involves using authentication keys as the nodes' pseudo identities and give details of its addition to the MUTE system.

If time permits I will also discuss "A Framework for Automatically Checking Anonymity with mCRL" which is joint work with Simona Orzan, Jun Pang, Muhammad Torabi Dashti.