This chapter is from the book
This chapter is from the book
This chapter is from the book
3.5 Anonymity
Anonymity is concerned with protecting the identity of agents with respect to particular events or messages. In this case, unlike secrecy, the messages themselves need not be protected, only their association with particular agents. Hence it is natural to model events in the system as consisting of two components: the identity of the agent performing that event, and the content itself. For anonymity, we consider events of the form a.x, where a is the identity of the agent and x is the content of the event.
An anonymity protocol will be designed to achieve some kind of transaction or exchange of messages without revealing the identity of some or all of the participants. This means not only that the name of the participants should not appear directly, but also that the identities of the participants should not be deducible from the information that is available. The threat is often considered to be more passive than for secrecy and authentication: that agents are not actively working to subvert the protocol, but are simply observing the occurrence of events and making deductions about the participants. Thus an anonymity protocol will generally be over a fairly reliable medium. However, such protocols can also be analyzed in the presence of stronger threats or a more unreliable medium (which might misdeliver messages for example) to see if their anonymity properties still hold.
The principle of anonymity is that a data item that could have originated from one agent could equally have originated from any other (perhaps any other from some given set of users). Hence we wish our definition to capture the notion that any message of the form i.x could equally well have been of the form j.x. If the set Anonusers consists of the set of all users whose identities should be masked by the system in providing anonymity, then the set of messages we wish to confuse for a given piece of information x is given by the set A:
)
Rather than deal directly with the identity of users, we can capture anonymity by requiring that whenever any event from the set A occurs, it could equally well have been any other event. In terms of agent identity and content, this means that if an observer has access only to the content of the message then it is not possible to deduce the identity of the agent associated with it.
A protocol described as a CSP system P will provide anonymity on the set A if any arbitrary permutation pA of the events in A, applied pointwise to all of the traces of the system, does not alter the set of possible traces of the system. This means that the other events from A that can appear in the trace are independent of the identity of the agent performing events from A. If A is of the form above (a set of possible users associated with a piece of information) then permutations will correspond to permutations on agents.
Anonymity is often relative to particular observers or particular viewpoints. In other words, anonymity is provided in cases where an observer has access only to certain kinds of information, and might not be provided in cases where more information is available. For example, a donation to a charity or a political party would be anonymous if the only information available is details of the amounts of money passing through particular accounts, but might not be anonymous if all details of particular transactions are available.
In general, an observer does not have complete access to all the events occurring in a system, but has only limited or no direct access to some events. The events that an observer has access to could be captured as another set B.
It is an immediate requirement for anonymity that A ∩ B = ∅. If an observer has direct access to the very events that we wish to mask, then it will always be possible to tell some events in A (in particular, those also in B) from some others.
The events that are not in B are those events that the observer does not have direct access to. From the point of view of modelling the system in order to analyze for anonymity, the events other than A and B should be abstracted, since the system to be analyzed for anonymity should encapsulate the information available to the observer.
If C is the set of events that are to be abstracted from P, then the system to be analyzed is AbsC(P), where AbsC is an abstraction mechanism such as hiding, masking, or renaming. This situation is pictured in Figure 3.9. In each case the requirement will be to check for any arbitrary permutation on A, lifted to apply to events and thus to traces, that
)
)
Figure 3.9. Analyzing P for anonymity
The dining cryptographers
We will consider the toy example of the dining cryptographers protocol. This is concerned with a situation in which three cryptographers share a meal. At the end of the meal, each of them is secretly informed by their organization whether or not she is paying. Either at most one is paying, or else the organization is itself picking up the bill.
The cryptographers would like to know whether it is one of them who is paying, or whether it is their organization that is paying; but they also wish to retain anonymity concerning the identity of the payer if it is one of them. They will use the following protocol to achieve this.
They each toss a coin, which is made visible to them and their right-hand neighbour. Each cryptographer then examines the two coins that they can see. There are two possible announcements that can be made by each cryptographer: that the coins agree, or that they disagree. If a cryptographer is not paying then she will say that they agree if the results on the coins are the same, and that they disagree if the results differ; a paying cryptographer will say the opposite.
If the number of ‘disagree’ announcements is even, then the organization is paying. If the number is odd, then one of the cryptographers is paying. The two cryptographers not paying will not be able to identify the payer from the information they have available.
The protocol is modelled in CSP as the parallel combination of cryptographers and coins, and a master process dictating who pays, as illustrated in Figure 3.10. The events of the form pays.i and notpays.i are the instructions from the organization concerning payment. Events of the form look.i.j.x model cryptographer i reading value x from coin j. The channels out.i are used for the cryptographers to make their declaration.
)
Figure 3.10. Components of the protocol
The Master process nondeterministically chooses either to pay, or one of the cryptographers to pay.
)
Each cryptographer process follows the protocol. This is described in CSP as follows:
)
Each coin is modelled as a choice between reading heads and reading tails:
)
The master either sends a pay message to one of the cryptographers and a do-not-pay to the other two or a do-not-pay message to all of them.
The system is constructed from the cryptographers and coins, which are two collections of independent processes.
)
They must synchronize on the events representing the examination of coins and the Master decides who is paying.
)
It is also possible to provide a parametric description of the system for an arbitrary number n of cryptographers; but automatic verification via model-checking will be possible only once a particular n is chosen.
Analysis
There are a number of parameters that dictate the precise form of anonymity available to the dining cryptographers:
-
the events A for which anonymity is provided;
-
the events B of the system that can be observed;
-
the way the remaining events Σ \ (A ∪ B) are abstracted.
If anonymity is to be provided with respect to the environment of Meal (for example, an observer on another table), then the set A for anonymity to be provided is simply {pays.i | 0 ≤ i ≤ 2}: the observer should not be able to distinguish the paying cryptographer from the others. Such an observer should only see the publicly announced values on out: occurrences of the notpays and look events should be abstracted. In this situation, the parameters are as follows:
-
A = {| pays |}
-
B = {| out |}
-
the remaining events will be hidden: this means that the observer does not even know whether and how often these events occur.
The system under consideration will be
)
and the question of anonymity will be whether or not
)
for an arbitrary permutation pA.
It might be plausible to expect that look events can be observed, simply requiring that the particular values associated with them are abstracted. In this case a renaming abstraction is more appropriate, using the following alphabet renaming:
)
The system flook(Meal) allows the occurrence of user i inspecting coin j to be observed, but abstracts the information given by the coin. If this form of abstraction is instead used (with notpays events remaining completely hidden) then the equivalence to be checked for anonymity is
)
The cryptographers themselves are privy to more information than an outsider watching the protocol running. They have access to the values of coins, and also they know whether they themselves are paying or not. In principle this additional information might be enough to break anonymity, and indeed anonymity on the set A is trivially not provided, since cryptographer i can distinguish pays.i from pays.j for some other j: pays.i is in both A and B.
In this case, the requirement is that anonymity is provided for each cryptographer against the other two. In other words, if a particular cryptographer is paying then each of the other two should not know whether it is her or the third cryptographer. From the point of view of each cryptographer, this means that the other two pays events should be indistinguishable.
Since the situation is symmetric, we will consider anonymity with respect to cryptographer 0. In this case we have the following parameters defining the anonymity property. A is the set of events that must be indistinguishable, and B is the set of events that are available to cryptographer 0:
-
A = {pays.1, pays.2}
-
B = {pays.0, notpays.0} ∪ {| look.0 |} ∪ {| out |}
-
C = Σ \ (A ∪ B)
There is in fact only one permutation pA to consider: swapping pays.1 and pays.2. The equivalence to check is that
)
This equivalence holds, and hence the protocol is correct.
The threat model considered above is benign: the participants all behave as they should, and we consider whether this allows any information to leak out. However, we may also consider situations where attempts are made to subvert the protocol. For example, a cryptographer might have access to the value on the third coin. This can be captured by allowing the cryptographer access to one of the look events at that third coin. For example the set B that cryptographer 0 has access to might include events of the form look.2.2.
In this case anonymity is lost. In the configuration
-
A = {pays.1, pays.2}
-
B = {pays.0, notpays.0} ∪ {| look.0, look.2.2 |} ∪ {| out |}
-
C =Σ\(A∪B)
we find that
is a trace of Meal \ C but that it is not a trace of pA(Meal \ C). In other words, heads on all three coins are observed and so out.2.disagree is consistent with pays.2. However, it is not consistent with pays.1:ifpays.2 is replaced by pays.1 then the rest of the trace is not consistent with that change. This means that the rest of the trace contains enough information to distinguish pays.1 from pays.2, and hence break the anonymity required for cryptographers 1 and 2.
It is instructive to consider this example when look.2.2 is not available. In this case we have
as the equivalent trace of Meal \ C. But now this is also a trace of pA(Meal \ C): the rest of the trace is consistent with pays.1, since the value of Coin(2) could be tails, leading to out.2.disagree. If the value of Coin(2) is not available then anonymity is again obtained.
)
)