TY - RPRT

T1 - Alpha-Beta Privacy

AU - Mödersheim, Sebastian Alexander

AU - Viganò, Luca

PY - 2018

Y1 - 2018

N2 - The formal speciﬁcation of privacy goals in symbolic protocol models has proved to be not quite trivial so far. The most widely used approach in formal methods is based on the static equivalence of frames in the applied pi-calculus, basically asking whether or not the intruder is able to distinguish two given worlds. But then a subtle question emerges: how can we be sure that we have speciﬁed all pairs of worlds to properly reﬂect our intuitive privacy goal? To address this problem, we introduce in this paper a novel and declarative way to specify privacy goals, called (α,β)-privacy. This new approach is based on specifying two formulae α and β in ﬁrst-order logic with Herbrand universes, where α reﬂects the intentionally released information and β includes the actual cryptographic (“technical”) messages the intruder can see. Then (α,β)-privacy means that the intruder cannot derive any “non-technical” statement from β that he cannot derive from α already. We describe by a variety of examples how this notion can be used in practice. Even though (α,β)-privacy does not directly contain a notion of distinguishing between worlds, there is a close relationship to static equivalence of frames that we investigate formally. This allows us to justify (and criticize) the speciﬁcations that are currently used in veriﬁcation tools, and obtain a decision procedure for a large fragment of (α,β)-privacy

AB - The formal speciﬁcation of privacy goals in symbolic protocol models has proved to be not quite trivial so far. The most widely used approach in formal methods is based on the static equivalence of frames in the applied pi-calculus, basically asking whether or not the intruder is able to distinguish two given worlds. But then a subtle question emerges: how can we be sure that we have speciﬁed all pairs of worlds to properly reﬂect our intuitive privacy goal? To address this problem, we introduce in this paper a novel and declarative way to specify privacy goals, called (α,β)-privacy. This new approach is based on specifying two formulae α and β in ﬁrst-order logic with Herbrand universes, where α reﬂects the intentionally released information and β includes the actual cryptographic (“technical”) messages the intruder can see. Then (α,β)-privacy means that the intruder cannot derive any “non-technical” statement from β that he cannot derive from α already. We describe by a variety of examples how this notion can be used in practice. Even though (α,β)-privacy does not directly contain a notion of distinguishing between worlds, there is a close relationship to static equivalence of frames that we investigate formally. This allows us to justify (and criticize) the speciﬁcations that are currently used in veriﬁcation tools, and obtain a decision procedure for a large fragment of (α,β)-privacy

U2 - 10.1145/3289255

DO - 10.1145/3289255

M3 - Report

T3 - DTU Compute Technical Report-2018

BT - Alpha-Beta Privacy

PB - DTU Compute

ER -