Second FME Lucas Award to Syverson and Stubblebine

The FME Lucas Award goes to Paul F. Syverson and Stuart G. Stubblebine for their paper

Group principals and the formalisation of anonymity

published at the First World Congress on Formal Methods (FM’99).

Paul F. Syverson receives the Lucas Award

The FME Awards Committee motivated its decision as follows:

Syverson and Stubblebine’s paper introduces a reasoning approach for anonymity protocols and anonymity services. The paper has been widely cited and is an important contribution to the theory and practice of formal methods in a significant application area that is of increasing importance: security.

The goal of the protocols studied in this paper is to provide some type of anonymity; that is, to hide some fact about a principal or set of principals from some adversary. The authors demonstrate that certain security specifications, such as anonymity and authentication, are most appropriately expressed in terms of the knowledge (or lack of it) of protocol participants and intruders. These security properties are not easily expressed in terms of events that did or did not happen along a single run of the protocol. Instead, they are perhaps best articulated in terms of the knowledge and beliefs of the participants. The authors developed an epistemic language and associated logic for describing and reasoning about an adversary’s view of a set of suspected principals. Epistemic logic is the logic of knowledge and belief, and by providing a way of modelling complicated scenarios involving groups of agents, it provides insight into the properties of individual agents who know facts in a security-sensitive context.

This work is widely applicable and has been useful for characterising security properties relating to anonymity and privacy. It is especially important for users of electronic commerce, where many protocols have emerged for protecting the anonymity of individual users, general Internet communications, commercial transactions, web-based communications, email, and electronic cash. The contribution is in formally representing and analysing privacy in such protocols. Their epistemic characterisation of anonymity properties was entirely novel. Epistemic logic today is one of just three different frameworks for analysing anonymity. An important consequence of this paper’s foundational work on axiomatising the concept of anonymity in an epistemic logic is that it has contributed to other well-founded theoretical approaches employing epistemic logic in a security setting.

The paper is available here.

Author: Einar Broch Johnsen