Measuring Anonymity with Plausibilistic Entropy

To prove that a certain protocol provides a certain security property (e.g. anonymity) one must first formally define that property in the context of a logical framework capable of expressing the relevant aspects of that protocol and then perform the actual inference steps (preferably automatically). After the qualitative aspect of the property is successfully addressed the next issue is the strength of the property - how to express it quantitatively so that it can be compared both to some business requirements and to other implementing protocols. The framework that we build upon is the MAS epistemic logic introduced by Halpern and O´Neill in their approach for defining anonymity both possibilistically and probabilistically. Our contribution employs the highly general plausibilistic approach in order to provide a numeric measure for anonymity that can also be extended to other properties as well. We propose a formula for calculating a particular kind of entropy suited for characterising partially ordered sets used to define plausibility measures and, on top of it, a quantitative definition for anonymity. We believe that the theory presented here is capable of filling the gap between the very general qualitative definition of anonymity and the information intensive probabilistic approach that might not always be applicable.