Probabilistic Anonymity and Admissible Schedulers

TL;DR

This paper introduces a refined model of schedulers in security protocols, called admissible schedulers, which better represent realistic adversaries by limiting their knowledge, and proposes a formal definition and proof technique for anonymity based on this model.

Contribution

It defines admissible schedulers that restrict adversarial power and develops a new formal framework for proving anonymity in security protocols.

Findings

Admissible schedulers depend only on visible past behavior.

A new formal definition of anonymity based on independence of user identities.

A proof technique involving behavior exchange without detection.

Abstract

When studying safety properties of (formal) protocol models, it is customary to view the scheduler as an adversary: an entity trying to falsify the safety property. We show that in the context of security protocols, and in particular of anonymizing protocols, this gives the adversary too much power; for instance, the contents of encrypted messages and internal computations by the parties should be considered invisible to the adversary. We restrict the class of schedulers to a class of admissible schedulers which better model adversarial behaviour. These admissible schedulers base their decision solely on the past behaviour of the system that is visible to the adversary. Using this, we propose a definition of anonymity: for all admissible schedulers the identity of the users and the observations of the adversary are independent stochastic variables. We also develop a proof technique for typical cases that can be used to proof anonymity: a system is anonymous if it is possible to `exchange' the behaviour of two users without the adversary `noticing'.