=Paper=
{{Paper
|id=Vol-1816/paper-03
|storemode=property
|title=Analysing Privacy Analyses
|pdfUrl=https://ceur-ws.org/Vol-1816/paper-03.pdf
|volume=Vol-1816
|authors=Giampaolo Bella,Denis Butin,Hugo Jonker
|dblpUrl=https://dblp.org/rec/conf/itasec/BellaBJ17
}}
==Analysing Privacy Analyses==
https://ceur-ws.org/Vol-1816/paper-03.pdf
In Proceedings of the First Italian Conference on Cybersecurity (ITASEC17), Venice, Italy.
Copyright c 2017 for this paper by its authors. Copying permitted for private and academic purposes.
Analysing Privacy Analyses
Giampaolo Bella1 , Denis Butin2 , and Hugo Jonker3,4
1
Dipartimento di Matematica e Informatica, Università di Catania, Italy
2
TU Darmstadt, Germany
3
Open University of the Netherlands, Heerlen, The Netherlands
4
Radboud University, Nijmegen, The Netherlands
giamp@dmi.unict.it, dbutin@cdc.informatik.tu-darmstadt.de, hugo.jonker@ou.nl
Abstract
The debate on people’s right to privacy and on the meaning of privacy is ongoing worldwide, for
example in Europe over the newly adopted General Data Protection Regulation. By contrast, works in
the area of formal e-voting privacy analysis, which aim at assessing the privacy preservation of a target
e-voting system by means of mathematical rigour, appear to have reached a well-known plateau. This
plateau is called indistinguishability. However, also other works look at privacy from a formal standpoint,
though on different grounds. Notable ones are unlinkability and minimal information disclosure. This
paper provides a contrastive argument about the three mentioned approaches by discussing the intuition
behind each of them and by assessing their respective pros and cons. The ultimate aim is to revamp the
privacy debate also at the level of formal analysis.
1 Introduction
The newly adopted EU General Data Protection Regulation 2016/679 enshrines privacy as a
fundamental human right, and the international debate that was revolving around its definition
has now shifted to the consequences of the new regulation for concrete data processing scenarios.
In particular, Article 35 promotes “safeguards, security measures and mechanisms to ensure the
protection of personal data”, and e-voting was explicitly included in the Article 29 Working
Group’s 2016–2018 work programme [2].
We believe that such a debate on mechanisms to ensure privacy, in particular in the context
of e-voting, must be accompanied by an appropriate debate also at the level of the formal
methods that can be used. This paper tackles the three best-known approaches to formal privacy
analysis — indistinguishability, unlinkability and minimal information disclosure — puts them
into perspective, introduces informal scenarios to comprehend them and provides a contrastive
debate to evaluate them.
2 Privacy as Indistinguishability
Kremer and Ryan [14] introduced the modelling of voter privacy and related properties in the
applied pi calculus [1], a security protocol modelling language. The applied pi calculus models
security protocols as concurrent, interacting processes. The initial idea of seeing voter privacy as
observational equivalence (but not specifically in the applied pi calculus) was introduced a decade
earlier [21]. In this more recent approach, cryptographic primitives are supported by the applied
pi calculus through the definition of new equational theories, which are equivalence relations over
terms. For example, the equational theory used to model the fundamental principle of symmetric
cryptography is written as dec(enc(x, k), k) = x. Considering two voters, their formalisation
reflects whether an outsider can distinguish between two scenarios that are identical, except for
19
the fact that the voters’ votes are swapped. Cryptography is seen as a perfect black box, and
the Dolev-Yao model is used, that is the attacker is omnipotent except for the fact that she
cannot decrypt without the adequate key.
2.1 Intuition
The notion behind the formalism of indistinguishability is that an even stronger property than
the confidentiality of a certain voter’s vote is proven: an outsider may not even detect that
votes were cast differently at all. The gist of this approach is a representation of voter privacy
as observational equivalence between processes. A voter casting a vote is represented as a
process. A security protocol verification software, ProVerif [5], is used to partially mechanise
proof techniques for observational equivalence.
Delaune, Kremer and Ryan [9] studied voter privacy, receipt-freeness and coercion-resistance
using observational equivalence for all three of these privacy-type properties. Their formalisation
can be summed up as follows. Voter privacy holds if an outsider cannot obtain information
allowing him to distinguish between two situations in which voters’ votes are swapped. Receipt-
freeness holds if an outsider cannot distinguish between the following two situations involving,
again, two voters: (1) the targeted voter votes as instructed, and the other voter votes differently;
(2) the targeted voter does not vote as instructed, but the other voter votes as per the instruction
(even though it was not addressed to him). Coercion-resistance is defined similarly, but the
outsider communicates with the targeted voter during the vote, and can instruct the voter to
send crafted messages.
The last two of these properties feature a fundamental difference with voter privacy, because
they involve the concept of inability of proof (by the voter, and for the benefit of the attacker,
regarding the cast vote). The remainder of our discussion on the indistinguishability approach
focuses solely on a discussion of the voter privacy property.
2.2 Machinery
Focusing on the prime example of voter privacy (the weakest property of the tree listed above),
some formalism must be introduced so it can be expressed in the applied pi calculus:
• {r/s} represents an active substitution, replacing the variable s with the term r.
• Processes are described using names, which represent atomic data such as a named
communication channel. We omit their operational semantics here for space reasons.
• S is an evaluation context, defined as a special voting process with holes instead of two
voter processes.
• f v(A) is the set of free variables of A. f n(A) is the set of free names of A. bn(A) is the
set of bound names of A.
• The relation → is called internal reduction and is a relation on extended processes satisfying
a number of rules we omit here. The relation →α , built on top of →, allows labelled
operations, e.g. α can be the name of an input, the output of a channel name or a basic
variable.
• The relation ≈l is called labelled bisimilarity. It is defined as the largest symmetric relation
R on closed extended processes such that if A R B, then (i) A ≈l B and (ii) if A → A0 ,
then B →∗ B 0 and A0 R B 0 for some B 0 and (iii) if A →α A0 and f v(α) ⊆ dom(A) and
bn(α) ∩f n(B) = ∅, then B →∗ →α →∗ B 0 and A0 R B 0 for some B 0 .
20
The notion of frames, based on extended processes, accounts for the knowledge that processes
leak to the environment. Processes may behave differently while still yielding identical frames.
2.3 Findings
With the machinery we just described in place, voter privacy is then defined to hold if the
following is true for all possible votes a and b:
Theorem 1 (Voter privacy as labelled bisimilarity in the indistinguishability approach).
S[VA {a/v} | VB {b/v}] ≈l S[VA {b/v} | VB {a/v}]
In other words, two processes differing only by swapped votes a and b between two (honest)
voters VA and VB are observationally equivalent. As seen here, in practice, the indistinguishability
approach uses labelled bisimilarity rather than observational equivalence. Since these two
relations are known to coincide, the choice of labelled bisimilarity is purely technical — proofs
become simpler.
In the framework by Delaune, Kremer and Ryan [9], election officials can be specified as
corrupt or honest. Some protocols can be shown to enforce voter privacy in this formalism
even with corrupt officials, but not all. As a consequence, statements about voter privacy for
protocols are only meaningful if assumptions about the honesty of election officials are made
explicit. In the aforementioned paper [9], three e-voting protocols are analysed within the
proposed framework: the FOO protocol [11], a later protocol by Okamoto using homomorphic
encryption [19] and a simplified version of a vote & go protocol with mixnet randomisation by
Lee et al. [16].
The intuitive implication chain from coercion-resistance to voter privacy via receipt-freeness
is formally shown to hold.
3 Privacy as Unlinkability
Unlinkability as an approach towards a formal encoding of privacy was abstractly discussed
by Langer et al. [15] in the context of electronic voting and was given a semantics precisely in
terms of indistinguishability. A practical specification in a formal language was advanced by
Butin et al. [8] in particular to handle voter privacy. The latter is reviewed and discussed below
to an unprecedented level of detail.
3.1 Intuition
The idea of using unlinkability to model voter privacy is inspired by a real-world scenario, which
can be demonstrated as follows. An attacker sits in her mobile laboratory in her van, just outside
the polling station of an electronic election. She intercepts the data cable between the site and
the local hub, hence she captures the entire election traffic and analyses it. She observes when a
specific voter enters the site, so she can guess reasonably well what portion of network traffic
corresponds to the vote of that voter. If she manages to distil out a vote, namely a candidate
identifier, from that traffic portion, then she has violated the privacy of that voter.
It can be imagined that the attacker will collect relevant message components such as names
and keys from the traffic using all means at her disposal, such as splitting concatenated messages
and decrypting ciphertexts using the keys that she has. If the analyst’s aim is to study how well
the protocol is designed to protect the votes, then it can be assumed that encryption cannot
21
be broken; however, the intertwining of cryptographic weaknesses and protocol design flaws is
currently being studied in other contexts [3, 6]. Arguably, the attacker will also check whether
the components obtained from various messages in the traffic have something in common and, if
so, will meaningfully relate the messages. We next show how this threat model can be formalised.
3.2 Machinery
Unlinkability can be defined on an inductive protocol model, which can be built using the
Inductive Method. This is briefly reviewed here, and only the details of unlinkability are given.
The method is to use Higher-Order Logics to specify a security protocol as an inductive definition
and then leverage the induction principle to prove properties of the model. The method was
introduced by Paulson [20] and fully fleshed out by Bella [4]. Full mechanisation is achieved
with the support of the Isabelle/HOL interactive theorem prover [23]. A Dolev-Yao attacker is
also specified as the agent called Spy, who can intercept, break down and recompose messages
at will but not break encryption. Cryptography is therefore assumed to work perfectly, so that
a ciphertext can be opened only if the corresponding encryption key is available.
The formal protocol model is the set of all possible traces of the given protocol, each trace
being a list of protocol events. Two main functions are knows and analz. The former expresses
all messages that an agent can learn from a trace, and the latter extracts all components of a
given set of messages by means of decomposition of clear-texts and decryption of ciphertexts
using available keys. Although we omit their full definitions for brevity, we observe that the set
analz(knows Spy evs) expresses all message components, such as keys and nonces, that the Spy
can derive from a trace evs. This set is crucial both in traditional work to express secrecy and
below to build the machinery for unlinkability.
Three protocol events are modelled, respectively Says for sending a message to specific
recipient, Gets for receiving a message, and Notes for noting down a message for future use.
Here is a trace admitted in the model of an imaginary voting protocol:
[ Says Spy O (Crypt (priSK V ) (Agent vote)), Gets O (Crypt (priSK V ) (Agent vote)),
Says V 0 O (Crypt (priSK V ) (Agent vote 0 )), Says V O (Crypt (priSK V ) (Agent vote)) ]
Traces are built in reverse order, so the first event here sees voter V cast vote vote in a signed
form with the election official O; then voter V 0 casts vote vote 0; then the official receives the
first vote; finally the Spy replays the first vote casting message. Note that the correspondence
between receiving a message and sending it can be interleaved with other events, that a sent
message is not necessarily received, and that the Spy may intercept all traffic and reuse it.
The unlinkability approach rests on the notion of an association, namely a link, which is
simply a set of elements of type msg; therefore, an association has type msg set. A fundamental
operator is aanalz:
primrec aanalz :: agent ⇒ event list ⇒ msg set set where
aanalz_Nil: aanalz A [] = {}
| aanalz_Cons:
aanalz A (ev # evs) =
(if A = Spy then
(case ev of
Says A 0 B X ⇒
(if A 0 ∈ bad then aanalz Spy evs
else if isAnms X
22
then insert ({Agent B} ∪ (analzplus {X } (analz(knows Spy evs))))
(aanalz Spy evs)
else insert ({Agent B} ∪ {Agent A 0 } ∪
(analzplus {X } (analz(knows Spy evs)))) (aanalz Spy evs))
| Gets A 0 X ⇒ aanalz Spy evs
| Notes A 0 X ⇒ aanalz Spy evs)
else aanalz A evs)
It takes parameters of type agent and event list, returning one of type msg set set. It therefore
captures the set of associations that a given agent can build by observing a trace. The base case
of the primitive recursive definition is obvious; the recursive case is less so. It can be seen that
only the Spy can build associations, as the symbolic evaluation of the current event ev cancels
that event out for other agents, and the last line concludes so. The Spy builds associations only
if the current event is a Says one: this is sound because received messages were also sent, and
because notes are intended as off-line records.
The definition specifies further cases. If the sender in the Says event is an accomplice of the
Spy’s, namely it belongs to the set bad, then also in this case the evaluation cancels the current
event out because the Spy’s goal is to violate the privacy of agents who do not collude with her.
The next distinction is on whether the current message, which is X in the definition, was sent
over an anonymous channel or not, as declared by the predicate isAnms, whose definition we
omit. If the message is anonymously sent, then the current set of associations aanalz Spy evs is
extended with a new association {Agent B} ∪ (analzplus {X } (analz(knows Spy evs))). This
association features the recipient B along with all components that the Spy can extract from
the current message using her entire knowledge gained from the current trace. The operator
analzplus, whose definition we omit, takes precisely two parameters: a message to break down as
much as possible using keys derived from a set of messages. This is where the set analz(knows
Spy evs) mentioned above comes into play. Therefore, analzplus models the forcing of a message
in all possible ways except for cryptanalysis.
The only remaining case has the current message as not anonymous. The association that is
extracted is the same as the previous case’s but also contains the identity of the sender, here A 0.
Modelling unlinkability requires another important operator, asynth:
inductive_set
asynth :: msg set set ⇒ msg set set
for as :: msg set set where
asynth_Build [intro]: [[a1 ∈ as; a2 ∈ as; m ∈ a1 ; m ∈ a2 ; m 6= Agent Adm; m 6= Agent Col]]
=⇒ a1 ∪ a2 ∈ asynth as
It can be seen how this operator transforms a set of associations in another one, namely by
merging two associations as a new one provided that they have an element in common. Another
requirement is that the common element is not an obvious one for the protocol, such as the
officials Adm and Col. This operator models the attacker’s ability to compare the associations
deriving from different messages and combine them meaningfully, namely when they intersect.
A voting protocol might protect voter privacy by distributing the link between a voter and his
vote over several messages, so asynth empowers the attacker against that.
3.3 Findings
The ultimate aim of the machinery defined above is to build the set asynth (aanalz Spy evs).
It is the set of all possible associations that the Spy can build by observing (the messages
23
circulated on) the trace evs. It contains vast and, from a malicious perspective especially,
valuable information. Therefore, given a generic association drawn from that set, the analyst
will assess whether that association may contain a voter and his vote. If this is not the case, the
informal conclusion will be that the protocol preserves voter privacy.
For example, the main theorem about voter privacy on the FOO protocol [8] is the following:
Theorem 2 (foo_V_privacy_asynth).
[[Says V Adm {|Agent V , Crypt (priSK V ) (Crypt b (Crypt c (Nonce Nv)))|} ∈ set evs;
a ∈ (asynth (aanalz Spy evs));
Nonce Nv ∈ a; V ∈ / bad; V 6= Adm; V 6= Col; evs ∈ foo]] =⇒ Agent V ∈
/ a
The theorem premises bind the main elements. They state that the main event whereby a
generic voter V casts his vote, here formalised as nonce Nv, appears in a generic trace evs of
the protocol model foo. They also specify that the voter is neither of the protocol authorities,
the administrator Adm and the collector Col. Most importantly, they state an association a
that the Spy can derive as just discussed, and assert that V ’s vote belongs to that association.
The theorem concludes that the voter does not belong to the association instead. The proof is
omitted because out of the scope of this paper.
There is no notion of a vote belonging to a specific voter, namely no function that associates
a vote to the voter who cast it. Although this would be easy to define, the conclusion of the
theorem as it stands is more generic, hence stronger: no vote can be associated to any voter.
4 Privacy as Minimal Information Disclosure
Privacy has also been studied in the area of statistical databases. A trend in this field is to
quantify privacy, e.g. k-anonymity [22], `-diversity [17], and differential privacy [10]. Similar
notions are rare in the domain of formal protocol analysis, though examples exist in the field of
voting [12, 13]. The advantage of quantifying privacy is that this can capture privacy loss and
thus be used to analyse the minimal information disclosure inherent in a system.
4.1 Intuition
Like unlinkability, using minimal information disclosure to model privacy is inspired by privacy
in voting. In most countries, elections are divided into districts, and each district has one or
more polling stations where voters assigned to that polling station can cast their vote. It is
common to announce the result of each polling station individually, to ensure a measure of
verifiability. Remark that this reveals information about how a voter could have voted: suppose
a candidate received zero votes in polling station A and some votes in polling station B, then
the privacy of voters that were to vote in polling station A is less than that of the voters of
polling station B.
A traditional indistinguishability approach would find all voters in A distinguishable from
voters in B, but find that (barring further information) voters within one polling station are
indistinguishable. However, how much privacy is lost remains unclear. This is what minimal
information disclosure aims to capture: how much privacy does a subject have.
4.2 Machinery
Minimal information disclosure models the system under analysis as a labelled transition system
induced by a normal process algebra. The underlying notion on which privacy is build is trace
24
indistinguishability of two traces. Two traces t, t0 are considered indistinguishable if there exists
a reinterpretation ρ under which the intruder-observed part of the traces are equal, formally:
t ∼ t0 ≡ ∃ ρ : observation(t) = ρ(observation(t 0 )) ∧ KIt = ρ(KIt ).
0
Reinterpretations are an intruder’s “guess” of what happened in the trace — assigning values
to variables such as keys, nonces, encrypted terms, etc. Naturally, these must be consistent,
that is, everywhere where two terms t, t0 can be distinguished, their reinterpretations ρ(t), ρ(t0 )
must also be distinguishable.
Even if two reinterpretations are consistent, they may be distinguishable, such as when they
lead to different outcomes. For example, in a voting system every voter chooses a candidate.
We can model this as a mapping γ : V → C, where V represents the set of voters and C the set
of candidates. The specific mapping used determines the result. So, two mappings γa , γb are
indistinguishable for the intruder, notation γa ' γb , if and only if:
∀ t ∈ Traces(Votsys(γa )) : ∃ t0 ∈ Traces(Votsys(γb )) : t ∼ t0 ∧
∀ t ∈ Traces(Votsys(γb )) : ∃ t0 ∈ Traces(Votsys(γa )) : t ∼ t0 .
To determine how much privacy is left to a user of the system, we construct a choice group.
The choice group consists of all choices for user-actions that are indistinguishable from other
choices for the intruder. For the example of a voting system Votsys, the choice group of a given
mapping γa for a given voter v is the set of all candidates γb (v) a voter could have chosen, which
the intruder could not distinguish from the actual mapping γa . This is expressed as:
cgv (VotSys, γa ) = {γb (v) | γb ' γa }.
To determine the minimal information disclosure for a user, we determine her choice group.
The size of the choice group quantifies the privacy of a given user – which we can compare
to the number of all possible choices (the size of the set of candidates). By extending the
intruder model to include collaboration with the intruder, we can compare privacy of coerced
and non-coerced users. We consider whole-sale (a priori and a posteriori) knowledge sharing
and collaborating on information sent over private communication channels. The latter can
involve merely sharing what the user sends (via an action is(term)) or even letting the intruder
construct such terms (via action sequence is(vars(term)) · ir(newterm)).
Collaborating users are modelled via a process transformation (introducing the above actions)
on regular user processes. Privacy of such collaborating users can now be compared to non-
collaborating users by determining, for each, the choice group and comparing their sizes.
4.3 Findings
The above machinery provides a quantified model of privacy. Consider, for example, the FOO
protocol. Informally, a voter must have some minimum amount of privacy if an attacker can
interpret his vote in at least two ways. In terms of the framework: the voter’s choice group
must contain at least two elements. Of course, this is not possible if the result is unanimous or
if there’s only one voter. Hence, the theorem requires the existence of at least two voters who
vote differently:
Theorem 3 (privacy of FOO92). Suppose |V| > 1 and |C| > 1. Then, for all γa for which
∃ va, vb ∈ V : γa (va) 6= γa (vb), we have ∀ v ∈ V : |cg v (FOO, γ1 )| > 1.
25
5 Analysis
Privacy as Indistinguishability Indistinguishability conveniently supports privacy-type
properties stronger than mere voter privacy: receipt-freeness and coercion-resistance can also be
tackled by this approach, albeit the degree of supported mechanisation may vary.
Generally speaking, a major drawback of the indistinguishability approach using the applied
pi calculus is that voter privacy proofs cannot be entirely mechanised, namely the necessary
proofs are only partially supported in the ProVerif protocol verification tool. ProVerif can
generally check static equivalences, but not full observational equivalence. Depending on the
cryptographic primitives used in an e-voting protocol, the equational theories necessary to
include them in the framework may be beyond the scope of ProVerif mechanisation, to the point
that even static equivalence may not always be checked by the software. The Okamoto protocol
was a traditional example in which ProVerif could not prove voter privacy [19]; however, this
particular limitation has been overcome only recently [7].
Also, the threat model hard-coded in ProVerif overestimates the standard Dolev-Yao threat
model, hence it may signal attacks that the human analyst realises not to be so. Therefore,
despite the tool itself is automatic, the amount of human intervention required is not negligible.
Privacy as Unlinkability We believe that one of the major strengths of this approach is
that it is intuitive. It also resembles the investigator’s approach on a crime scene, of finding
a clue such as the size of a footprint and then reducing the set of suspects from everyone to
only those wearing that size. And the inductive references modelled by asynth represent the
additional deductions that the investigator may build.
A weakness could be that aanalz does not extract the sender’s identity over anonymous
channels. One may argue that the attacker derives the sender’s identity from the out-of-band,
for example by observing who enters a voting site. This criticism would be easy to address by
removing the innermost if-then-else of aanalz so as to always extract the sender’s identity.
It could also be observed that asynth only takes a single step of synthesis between associations
that intersect. Its premises mention two associations that are drawn from the original set of
associations termed as and not from the inductive set asynth as. On one hand, this may not
be considered a serious weakness until there is evidence that protocols vastly appeal to the
technique of distributing crucial associations over several protocol messages; on the other hand,
porting the current proofs over the generalised definition is yet to be achieved.
Privacy as Minimal Information Disclosure The main strength of minimal information
disclosure is that it enables one to reason about privacy in situations where there is more than
one class of subjects. Whether this distinction is made by physical means (e.g. geographically,
such as with voting precincts), based on attributes (e.g. age) or through yet different means, the
existence of different classes need not imply a complete loss of privacy.
Currently, the main drawback of this approach is the specific focus of the current machinery.
Minimal information disclosure was originally conceived for the domain of vote privacy, and the
underlying mechanism is tailored to that specific domain. Secondly, the approach inherently
requires one to know a priori what privacy-affecting information will be available to the attacker.
In voting, this is the result — public information. In other areas, it will not always be clear.
For example, a few years ago top secret documents were leaked to journalists. It was not clear
whether this act was a breach of trust or a breach of security, that is whether it was done by
someone with appropriate security clearance or by someone without, until Edward Snowden
(holding appropriate clearance) revealed his involvement.
26
5.1 Comparison
The minimal information disclosure approach to privacy is inherently finer-grained than the other
two. Definitive boolean claims about privacy may seem intrinsically simplistic if interpreted in
a real-world context. However, both indistinguishability and unlinkability enjoy stronger tool
support and hence are more easily applicable to additional case studies.
As for tool support, ProVerif offers full automation to indistinguishability while Isabelle
is not fully automatic and requires human directions over the proof argument. However, also
automatic tools generally require human effort to ensure termination and meaningful outputs,
and ProVerif makes no exception when used intensively for a privacy assessment.
The unlinkability approach has other shortcomings [18]. One is that aanalz does not extract
the identity of the agent who signs a digital signature; thus, if a voting protocol prescribes
the voter to sign his vote and submit the outcome, this pair voter-vote would not appear in
the set of all possible associations asynth(aanalz Spy evs), whereas the voter privacy of this
protocol would not be met by means of indistinguishability. A similar conclusion would apply
to a protocol that allowed an attacker to learn that two voters cast the same vote.
This does not mean that unlinkability is weaker than indistinguishability. The two short-
comings affect the implementation of the unlinkability concept outlined above (§3) and not the
concept itself. They can easily be resolved by having aanalz also extract the signer’s identity and
by proving an additional theorem that no pair of voters appear in any meaningful association
along with a vote. The unlinkability concept was in fact informally given [8, 15] to abstractly
mean that the voter could not be linked to his vote from the malicious observation of a trace; it
was then prototypically implemented via aanalz, asynth and corresponding theorems, which in
fact could be extended or amended. It seems to be the opposite with the indistinguishability
concept: it was precisely coined after a given formal definition in terms of labelled bisimilarity
(Theorem 1, §2).
By contrast, an informal argument can be advanced to conclude that the two concepts are
equivalent. It can be outlined as follows. Unlinkability implies indistinguishability because
the former tackles general associations between any voter and any votes. Therefore, proving
unlinkability implies that the attacker cannot see any of the associations (that a voter cast
a specific vote, and another vote cast another vote) which premise the indistinguishability
conclusion. So, that conclusion trivially holds (because its premises are falsified). It is also the
case that indistinguishability implies unlinkability because “linkability of the vote to the voter
states that a run [. . . , v, . . . , ω(v), . . .] is distinguishable from a run where the vote was cast by
another voter [. . . , v 0 , . . . , ω(v), . . .]” [15].
6 Conclusions
This paper reviewed the three main approaches to conduct formal privacy analysis in the context
of e-voting. Due to space limitations, a full account on the related work was impossible, hence
only those works that were barely sufficient to support the arguments were discussed.
Indistinguishability is unequivocally the most widespread and best developed approach, and
its tool support is improving. Unlinkability seems to be an equivalent concept, but its currently
available implementation, though promising, is weaker than the implementation of the other
approach by means of labelled bisimilarity. Orthogonally to both, minimal information disclosure
is a promising and highly detailed approach whose tool support is worthy of development.
27
References
[1] M. Abadi and C. Fournet. Mobile values, new names, and secure communication. In POPL 2001,
pages 104–115. ACM, 2001.
[2] Article 29 Data Protection Working Party. Work programme 2016–2018 (WP235), 2016.
[3] M. Backes, B. Pfitzmann, and M. Waidner. Formal Methods and Cryptography. In FM 2006,
volume 4085 of LNCS, pages 612–616. Springer, 2006.
[4] G. Bella. Formal Correctness of Security Protocols. Information Security and Cryptography.
Springer, 2007.
[5] B. Blanchet. An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. In CSFW-14,
pages 82–96. IEEE Computer Society, 2001.
[6] B. Blanchet. A Computationally Sound Mechanized Prover for Security Protocols. IEEE Trans.
Dependable Sec. Comput., 5(4):193–207, 2008.
[7] B. Blanchet and B. Smyth. Automated Reasoning for Equivalences in the Applied Pi Calculus
with Barriers. In CSF 2016, pages 310–324. IEEE Computer Society, 2016.
[8] D. Butin, D. Gray, and G. Bella. Towards Verifying Voter Privacy through Unlinkability. In ESSoS
2013, volume 7781 of LNCS, pages 91–106. Springer, 2013.
[9] S. Delaune, S. Kremer, and M. Ryan. Verifying Privacy-Type Properties of Electronic Voting
Protocols: A Taster. In Towards Trustworthy Elections, New Directions in Electronic Voting,
volume 6000 of LNCS, pages 289–309. Springer, 2010.
[10] C. Dwork. Differential Privacy. In ICALP 2006, volume 4052 of LNCS, pages 1–12. Springer, 2006.
[11] A. Fujioka, T. Okamoto, and K. Ohta. A Practical Secret Voting Scheme for Large Scale Elections.
In AUSCRYPT ’92, volume 718 of LNCS, pages 244–251. Springer, 1992.
[12] H. Jonker, S. Mauw, and J. Pang. A formal framework for quantifying voter-controlled privacy. J.
Algorithms, 64(2-3):89–105, 2009.
[13] H. Jonker and J. Pang. Bulletin Boards in Voting Systems: Modelling and Measuring Privacy. In
ARES 2011, pages 294–300. IEEE Computer Society, 2011.
[14] S. Kremer and M. Ryan. Analysis of an Electronic Voting Protocol in the Applied Pi Calculus. In
ESOP 2005, volume 3444 of LNCS, pages 186–200. Springer, 2005.
[15] L. Langer, H. Jonker, and W. Pieters. Anonymity and Verifiability in Voting: Understanding
(Un)Linkability. In ICICS 2010, volume 6476 of LNCS, pages 296–310. Springer, 2010.
[16] B. Lee, C. Boyd, E. Dawson, K. Kim, J. Yang, and S. Yoo. Providing Receipt-Freeness in
Mixnet-Based Voting Protocols. In ICISC 2003, volume 2971 of LNCS, pages 245–258. Springer,
2003.
[17] A. Machanavajjhala, D. Kifer, J. Gehrke, and M. Venkitasubramaniam. l-diversity: Privacy beyond
k-anonymity. ACM Transactions on Knowledge Discovery from Data (TKDD), 1(1):3, 2007.
[18] A. Marcedone. Indistinguishability vs Unlinkability: defining voter privacy in an electronic protocol,
2014. Università di Catania, unpublished.
[19] T. Okamoto. An electronic voting scheme. In IFIP World Conference on IT Tools, pages 21–30,
1996.
[20] L. C. Paulson. The Inductive Approach to Verifying Cryptographic Protocols. Journal of Computer
Security, 6(1-2):85–128, 1998.
[21] S. Schneider and A. Sidiropoulos. CSP and Anonymity. In ESORICS 96, volume 1146 of LNCS,
pages 198–218. Springer, 1996.
[22] L. Sweeney. k-anonymity: A model for protecting privacy. International Journal of Uncertainty,
Fuzziness and Knowledge-Based Systems, 10(05):557–570, 2002.
[23] M. Wenzel, L. C. Paulson, and T. Nipkow. The Isabelle Framework. In TPHOLs 2008, volume
5170 of LNCS, pages 33–38. Springer, 2008.
28