All rights are reserved and copyright of this manuscript belongs to the authors.
This manuscript has been published without reviewing and editing as received
from the authors: posting the manuscript to SCIS 2006 does not prevent future
submissions to any journals or conferences with proceedings.

SCIS 2006
The 2006 Symposium on
Cryptography and Information Security
Hiroshima, Japan, Jan. 17-20, 2006
The Institute of Electronics,
Information and Communication Engineers

Role Interchangeability and Verification of Electronic Voting
Ken Mano ∗Yoshinobu Kawabe ∗Hideki Sakurada ∗Yasuyuki Tsukada ∗Abstract— We propose a new information-hiding property called role interchangeability. We specify
the property in multiagent systems, and describe its relationship with known anonymity and privacy
properties. Then a method is presented to prove role interchangeability of a protocol described as an
automaton. As a case study, we apply our method to the formal veriﬁcation of the FOO electronic
voting protocol.
Keywords: security protocol, formal veriﬁcation, electronic voting, anonymity, privacy.

1

Introduction

We propose a new information-hiding property calledrole interchangeability and present its theoretical foundation. Role interchangeability means that any two
agents could interchange their roles, that is, the actions
they performed.
We have two objectives, the ﬁrst of which is to ﬁll thegap between logic and computation in the formal veriﬁcation of anonymity and privacy. Epistemic logics andformal computation models have been two classical approaches to such veriﬁcation. However, the relationshipbetween them hasn’t been fully studied. Researches
have recently been undertaken on “bridging” the gap[4, 5]. However, these results cannot be directly applied to the veriﬁcation of electronic voting. To verify
practical protocols, it is needed to make this “bridge”
wider, and we achieve this by formalizing role interchangeability in multiagent systems and by providing
a simulation proof method for the property.
Our second objective is to reveal the duality between
anonymity and privacy. There have been some researches on the formal speciﬁcation and veriﬁcation ofprivacy [1, 5]. However, as far as we know, every known
formal deﬁnition of privacy depends on some speciﬁc
problem and so is not general enough. In fact, it isdiﬃcult to provide such a formal and general deﬁnition
since casual meaning of privacy includes various issues.
In this paper, we deﬁne privacy as some kind of dual ofanonymity. Moreover, we show that exploiting this duality is useful for deriving anonymity and privacy fromrole interchangeability.
This paper is organized as follows. In Section 2, we
introduce role interchangeability and show its properties. We specify role interchangeability in multiagent
systems [4] and show that it derives various known anonymity properties under appropriate conditions. We
then present a duality property that is useful for deriving privacy. In Section 3 we show a way to prove role interchangeability. First we introduce the ω-compatibilityof an interpreted system with a set of traces. Based∗NTT Communication Science Laboratories, NTT Corporation. 3-1 Morinosato Wakamiya Atsugi-shi Kanagawa, 2430198 Japan.

on this, role interchangeability is characterized by theexistence of role-interchange functions on traces. We
then present a simulation proof method to prove theexistence of role-interchange functions for a given automaton. In order to examine the applicability of theveriﬁcation method, in Section 4 we prove the anonymity and privacy of a practical electronic voting protocol.
The protocol is described as an automaton and shownto have role-interchange functions.

2

Specification by Multiagent Systems

We specify role interchangeability and present its
properties in multiagent systems, which is a modal logic
system with operator Ki to represent the knowledge ofagent i. Notions and terminologies are borrowed from
[4].
2.1

Role Interchangeability

Let I be the set of all agents, and A be the set of
all agent actions. We assume i, i , i1 , i2 , . . . range overagents while a, a , a1 , a2 , . . . range over agent actions.
Following [4], we use the formula θ(i, a) to represent“agent i has performed an agent action a, or will perform a in the future”1 .
Definition 2.1 Set A of agent actions is role interchangeable with respect to agent j in the interpreted
system I if the following holds for any i, i ∈ I anda, a ∈ A:
I |= (θ(i, a) ∧ θ(i , a )) ⇒ Pj [θ(i , a) ∧ θ(i, a )],where Pj φ is an abbreviation of ¬Kj ¬φ, meaning that“agent j thinks that φ is possible”.
Role interchangeability means that, as far as agent j
is concerned, any two agents could interchange theirroles, that is, the actions they performed.
We compare this property with a series of anonymity
properties appearing in [4].
1 An agent action in this paper is simply called an ‘action’ in[4]. We changed the terminology since we must distinguishthe actions of agents from those of automata appearing in thenext section.

Definition 2.2 Agent action a, performed by agent i,
is minimally anonymous with respect to agent j in theinterpreted system I if I |= ¬Kj [θ(i, a)].
Agent action a, performed by agent i, is totally anonymous with respect to j  in the interpreted system I if
I |= θ(i, a) ⇒Pj [θ(i , a)].
i =jIntuitively, minimal anonymity means agent j neverknows that action a is performed by agent i, while total anonymity means, from j’s viewpoint, a could havebeen performed by anybody in the system except j itself.
Basically, role interchangeability and the above anonymities are incomparable. However, minimal anonymity is derived from role interchangeability by assuming
certain conditions:
Theorem 2.3 Assume the following conditions holdfor i ∈ I and a ∈ A.
 
1. I |= θ(i, a) ⇒[i = i ∧ θ(i , a )]2. I |=

i=i

i ∈I a ∈A¬[θ(i, a) ∧ θ(i , a)]

If A is role interchangeable in I with respect to j, thenaction a performed by agent i is minimally anonymous
as well.
Below is another version of anonymity that generalizes total anonymity so that an anonymity set IA ⊆ I
can be used instead of I.
Definition 2.4 Agent action a, performed by agent i,
is anonymous up to IA ⊆ I with respect to j if
Pj [θ(i , a)].
I |= θ(i, a) ⇒i ∈IAFor an appropriate IA , anonymity up to IA follows fromrole interchangeability.
Theorem 2.5 Let IA be the set of agents that perform
an agent action in all runs in I, that is, the set{i ∈ I | ∀ (r, m) ∈ R(I) ∃a ∈ A (I, r, m) |= θ(i, a)}.
If A is role interchangeable in I, then agent action a ∈A performed by i ∈ I is anonymous up to IA .
Corollary 2.6 Suppose that any agent in I performs
an agent action in A. If A is role interchangeable inI, then agent action a performed by i is totally anonymous.
2.2

Duality and Privacy

Here, we present some duality properties with respect to θ. Let us consider duality to replace I with
A, A with I, and θ with θ satisfying ∀i ∈ I ∀a ∈A θ (a, i) ⇔ θ(i, a). The formula θ (a, i) is read as“agent action a has been performed, or will be performed in the future by an agent i”, so this is the duality of the passive voice.
Then, both role interchangeability and minimal anonymity are equivalent to its dual. Thus, for deriving minimal anonymity from role interchangeability, we
can assume conditions 1’ and 2’ below instead of 1 and
2 in Theorem 2.3.

1’. I |= θ(i, a) ⇒2’. I |=


a=a





a ∈A i ∈I[a = a ∧ θ(i , a )]¬[θ(i, a) ∧ θ(i, a )]Suppose A = {vote(1), . . . , vote(cmax)}, where cmax
is a natural number. Assume that the intended interpretation of θ(i, vote(j)) is that voter i voted for candidate j. Then, condition 2 means that no two votersvote for the same candidate, which is quite unnatural
as regards voting. On the other hand, 2’ is a much
more adequate condition, namely that a voter does notvote for two candidates. Although this adequacy depends on the interpretation, the example shows that
this duality is useful in terms of obtaining appropriate
premises for the problem.
Let us next consider anonymity up to IA . This time
it is not equivalent to its dual, but the dual itself seems
to be an interesting information-hiding property:
Pj [θ(i, a )],I |= θ(i, a) ⇒a ∈AI

where AI ⊆ A. This property intuitively means thatagent i could have performed any agent action in AI ,and can be thought of as a privacy of i. In otherwords, hiding who performs the agent action is anonymity while hiding what is performed by the agent isprivacy. Thus we call it privacy up to AI . Formally,
agent i performing agent action a is private up to AI
with respect to j if the above condition holds. The
following is the dual of Theorem 2.5.
Theorem 2.7 Let AI be the set of agent actions thatis performed by an agent in all runs in I, that is, theset {a ∈ A | ∀ (r, m) ∈ R(I) ∃i ∈ I (I, r, m) |= θ(i, a)}.
Then, if A is role interchangeable in I, then agent i ∈ I
performing a ∈ A is private up to AI .

3

Verification by Automata

3.1

ω-Compatibility and Role-Interchange
Function

ω-compatibility is a variant of the compatibility introduced by Halpern and O’Neill to characterize anonymity up to IA by strong anonymity [9] for CSP. Our
notion modiﬁes the original by introducing a view function. Moreover, the original notion implicitly assumes
ﬁniteness of trace length while our notion does not.
Let I be the set of all agents and A be the set of allagent actions as in the previous section. Σ is the setof all trace actions (or actions, simply). Let ΣI,A ={i.a | i ∈ I, a ∈ A} and suppose ΣI,A ⊆ Σ. A ﬁnite
or inﬁnite sequence of actions in Σ is called a traceon Σ. An action i.a ∈ ΣI,A is an “imaginary” action
to make a trace reﬂect the fact that θ(i, a) holds in thecorresponding run. Thus, such actions are not intended
to be observed directly.
Then we deﬁne a notion of view function. Let α bea fresh constant that represents an “invisible” action.
Definition 3.1 Let fV be a function whose domain isΣ. If fV satisﬁes the following property, it is called aview function:∀x ∈ ΣI,A fV (x) = α.

The domain of a view function is homomorphically extended to traces and sets of traces.
We can use a view function to represent the abilityof the observer. For instance, let send(σk (data)) bean action to send message σk (data) encrypted with asecret key k that only the sender knows. Then, using a
fresh constant envelop, the invisibility of the encrypted
message can be modeled by deﬁning the view function
as ∀x fV (send(σk (x))) = send(envelop).
In the following, we suppose the existence of two special agents: the environment e and the observer o. A
preﬁx of a trace t of length n is denoted by t|n. For
convenience, for a trace t of length less than n we deﬁnet|n = t.
Definition 3.2 Let fV be a view function. We saythat a system R is ω-compatible with a set T of traces
via a view function fV if the following two conditions
hold:
1. for every run r ∈ R, there is a trace t ∈ Tsuch that for every time m, t|m = re (m) andfV (t|m) = ro (m), and
2. for every trace t ∈ T , there is a run r ∈ R suchthat for every time m, re (m) = t|m and ro (m) =fV (t|m).
Moreover, an interpreted system I = (R, π) is ω-compatible with T if R is ω-compatible with T and if(I, r, m) |= θ(i, a) whenever the action i.a is in the
trace re (m ) for some m .
Then we introduce the role-interchange functions ofa trace set. The existence of the functions characterizes
the role interchangeability of the system ω-compatible
with the set.

An automaton is a quadruple consists of sets of states,
actions, initial states and transitions. Unlike a usual
deﬁnition, we do not use a set of ﬁnal states since
it is not important for describing the system behavior. A transition is a triple (s, δ, s ) of states s, s andδ

action δ, and is also written as s → s . Let S =(States, Actions, Start, T rans) be an automaton.
An execution of S is a ﬁnite or inﬁnite alternating
sequence s0 , δ1 , s1 , δ2 , s2 , . . . of states and actions thatsatisfy s0 ∈ Start and (si , δi+1 , si+1 ) ∈ T rans for every
i . The set of all executions of S is denoted by execs(S).
The sequence obtained by removing all states from an
execution e is called a trace of e, denoted by trace(e).
We write traces(S) instead of trace(execs(S)).
In the second condition of a role-interchange function, agents i and i are assumed to perform actions in
ΣI,A in a given trace. The following is the notion that
corresponds to the assumption for executions.
Definition 3.5 Let i and i be arbitrary distinct agents.
An execution is called coexistable for i and i if there
are agent actions a and a such that i.a and i .a appear
in the execution. A state in a coexistable execution for
i and i is called a coexistable state for i and i .
Then we present a method for constructing role-interchange functions by the stepwise simulation of executions.
Definition 3.6 (Agent-exchange function on coexistablestates) Let S be an automaton, I be the set of allagents, A be the set of all agent actions, and fV be
a view function. An agent exchange function gi,i of
S with respect to distinct agents i, i ∈ I via fV is afunction on states that satisfy the following conditions
for any coexistable states s, s for i and i :• For any a ∈ A, sgi,i (s ).

Definition 3.3 Let fV be a view function and T be a
set of traces on Σ. Let i, i be any distinct agents, anda, a be any distinct agent actions.
a,a: T → T is called a role-interchange
A function fi,i
function of T with respect to i, i and a, a via fV if thefollowing two conditions hold for any t ∈ T :• For any a ∈ A, sgi,i (s ).

3.2

Simulation Proof Method

Given an automaton formalizing the behavior of asystem, we present a suﬃcient condition for the trace
set of an automaton to have role-interchange functions.
This condition guarantees the existence of a family{fi,i |i, i ∈ I} of role-interchange functions that are
independent of agent actions.

i .a

i .a

i,a

→ s implies gi,i (s)

→
→
δ

δ

a,a
1. fV (t) = fV (fi,i (t)).

Theorem 3.4 Suppose an interpreted system I = (R, π)
is ω-compatible with a set T of traces via a view function fV . Then the set A of agent actions is role intera,achangeable in I if and only if there is a family {fi,i |distinct i, i ∈ I, distinct a, a ∈ A} of role interchange
functions of T via fV .

→ s implies gi,i (s)• For any action δ not of the form i.a or i .a, s →

2. If i.a and i .a appear in t, then i .a and i.a apa,a
pears in fi,i
 (t).

i.as implies there is an action δ  s.t. gi,i (s) →gi,i (s ) and fV (δ) = fV (δ  ).
Theorem 3.7 Let S be an automaton, I be the set of
all agents, and fV be a view function. Suppose there isan agent-exchange function of S with respect to i, i via
fV for any distinct agents i, i ∈ I. Then traces(S) has
a family {fi,i | i, i ∈ I} of role-interchange functions
via fV .

4

Case Study: Electronic Voting

4.1 FOO Protocol
In this section we explain an electronic voting protocol called FOO [3] and present some assumptions forverifying its anonymity and privacy. Formal anonymity veriﬁcations for FOO have been presented in [7]and [6]. We aim at providing a logical foundation forsuch simulation-based veriﬁcations. The model of FOO
involves the following agents: voters V1 , . . . , Vvmax , an

administrator Ad, and a collector Co. The administrator
veriﬁes that only eligible voters can cast votes, and thecollector collects and publishes the votes.
We assume that readers are familiar with the properties of basic cryptographic primitives such as a commitment ξ(v, r), a digital signature scheme σx for agent
x, a blind signature scheme σAdwith a blinding factor
χ, formalized by the following equations:ξ −1 (ξ(v, r), r) = v,
−1
σAd
(σAd (m)) = m, σi−1 (σi (m)) = m,(χ(m, b)), b) = σAd (m).
χ−1 (σAd(x) = null.
We also assume σAd
The FOO protocol consists of 3 phases:[phase 1] Voter Vi to vote for vi computes a ballot xi =ξ(vi , ri ) using key ri , and the message ei = χ(xi , bi ).
Then Vi sends the administrator Ad the signed message
σi (ei ) together with his identiﬁer i. Then Ad conﬁrms
the signature and veriﬁes that it is the ﬁrst vote by
an eligible voter. If it passes the tests, Ad replies tovi with the signed message σAd(ei ). At the end of thephase, Ad publishes the list of all authenticated voterswith their blinded ballots.
[phase 2] Vi sends the collector Co the message σAd (xi )obtained by unblinding the reply from Ad via a senderanonymous communication channel such as the mixnet[2]. Then Co conﬁrms the signature of Ad. If it does
not pass the test, Co claims this by showing the badsignature. At the end of the phase, Co publishes thepair (li , σAd (xi )) for every vote that passed the test,
where li is a number unique to each vote.
[phase 3] Vi sends Co the message (li , ri ) again via thesender-anonymous channel. Co checks that ri is a correct key for xi , and counts and announces the voting
result at the end of the phase.
We assume that a voter may abstain from voting, so
we omit the number check of voters found in phase 3of the original protocol. Furthermore, we assume that
only Vi knows bi , which aﬀects the deﬁnition of theview function in the next section.

4.2

Automaton Description of FOO

We describe the behavior of FOO in the preconditioneﬀect style. This style is based on that of I/O-automata
in [8]. Actually the description in this section can bethought of as an I/O-automaton with only output actions.
Conceptually, the system consists of the agents introduced in the previous section together with a special agent called phase manager. Formally, the system is an automaton S whose actions are observed by
the attacker from his viewpoint. A state of S consistsof ﬁelds phase, abuﬀ , line, vbuﬀ , kbuﬀ and voter(i)(i = 1, . . . , vmax), each of which is associated with anagent as shown in Figure 1. The automaton S performs
actions phase2, phase3, auth, ack, etc., andFor simplicity, we assume the following:
1. phase can be referred from anyone at anytime.
Also, each communication between a voter andthe administrator/collector is completed immediately.

2. The attacker is an eavesdropper.
Moreover, all message checks and claim processing are
omitted, and the administrator returns a reply to all
requests without any eligibility check.
Constants, Functions, and Primitive Propositions.
Constants P h, Ad, Co, and natural numbers 1, . . . , vmax
are used to represent the phase manager, the administrator, the collector, and voters 1, . . . , vmax, respectively. Candidates are also represented by natural numbers 1, . . . , cmax, and they are distinguished from voters by the context. For multisets to represent buﬀers,
we use the multiset constructor -:, the empty multiset ∅, the multiset membership ∈, and the functiondelete(x, y) that deletes an occurrence of x in y if any
exist. It is easy to formalize the properties of the data
structure used here by using ﬁrst-order formulae withequations.
States. A state consists of ﬁelds and subﬁelds. Flags
authed, casted, keyed and f inish range over boolean
constants initially f alse, and buﬀers abuﬀ , vbuﬀ andkbuﬀ are multisets initially ∅. Fields and subﬁelds aredesignated using . . For instance, subﬁeld X of ﬁeld
Y in state s is denoted by s.Y.X. The preﬁx s. is often
omitted when the state s is clear from the context.
Actions. Each action other than vote corresponds
to a communication between agents, and has the form
action name(sender, receiver, data1 , data2 , . . .). We
suppose that null receiver means the action corresponds
to a publication. Phase synchronizations are formulated as a publication from the phase manager.
vote(i, j) should be written as i.vote(j) in the notation of Section 3, where I = {1, . . . , vmax} and A ={vote(null), vote(1), . . . , vote(cmax)}. The action reﬂects i’s voting behavior; performing vote(i, j) for j =1, . . . , cmax implies that i voted for j, while vote(i, null)means that i received the voting right from Ad but did
not actually cast a vote.
Transition rules. The transition rules are describedin precondition-eﬀect style as shown in Figure 2. States
are implicit in the description. For instance, the phase2
rule is read as “for any state s, phase2(P h, null) action
is possible when s.phase = 1, and if the action is performed, in the next state s the value of s .phase will
be updated to 2”.
Note that each phase can be shut before all votersﬁnish their actions in the phase. If phase 1 is shut
before voter i performs ack action, then he will notcontinue the following actions. If phase 2 is shut before
i’s pub action, i can then perform only vote(i, null).
4.3

Role-Interchange Function for FOO

The deﬁnition of view function fV reﬂects the assumptions that the observer does not know the blinding
factors voter(i).b and that each voter sends a message
to the collector via the sender-anonymous channel.
Definition 4.1 fV is a view function deﬁned such thatfV (auth(i, Ad, σi (x))) = auth(i, Ad, σi (env(i)))
fV (ack(i, Ad, σAd(x))) = ack(i, Ad, σAd(env(i)))fV (cast(x, Co, svote)) = cast(null, Co, svote)fV (key(x, Co, l, r)) = key(null, Co, l, r)fV (vote(x, y)) = α

To Observer
Actions
Automaton S
phase2phase3Phase Manager
phase

auth
Administrator

ack

abuf f.
.
.

Voter 1

pub

vote

Collector

voter(1)cand, b, r, ...
.
.
.
Voter vmax
voter(vmax)

cast

line

key

vbuf f.
.
.

kbuf fFigure 1: Conceptual model of electronic voting systemphase2(P h, null)
Precondition:phase = 1
Eﬀect:
phase := 2phase3(P h, null)
Precondition:phase = 2
Eﬀect:
phase := 3auth(i, Ad, req)
Precondition:phase = 1 ∧ voter(i).authed = f alse ∧req = σi (voter(i).cand)Eﬀect:
voter(i).authed := true
abuﬀ := pair(i, req) -: abuﬀ
For any Γ,ack(Ad, i, sreq)
Precondition:phase = 1 ∧ pair(i, Γ) ∈ abuf ∧ (σ −1 (Γ))
sreq = σAdiEﬀect:
abuﬀ := delete(pair(i, Γ), abuﬀ )if
voter(i).authed = truethenvoter(i).sreq := sreqﬁcast(i, Co, svote)
Precondition:phase = 2 ∧ voter(i).sreq = null ∧voter(i).casted = f alse ∧svote = χ−1 (voter(i).sreq, voter(i).b)
Eﬀect:
voter(i).casted := true
vbuﬀ := svote -: vbuﬀ

pub(Co, null, l, svote)
Precondition:phase = 2 ∧ svote ∈ vbuﬀ ∧ l = line
Eﬀect:
vbuﬀ := delete(svote, vbuﬀ )line := line + 1
For any θ = 1, . . . , vmax,
if
voter(θ).casted = true ∧svote = χ−1 (voter(θ).sreq, voter(θ).b)
then
voter(θ).line := lﬁkey(i, Co, l, r)Precondition:phase = 3 ∧ voter(i).line = null ∧voter(i).keyed = f alse ∧l = voter(i).line ∧ r = voter(i).rEﬀect:
voter(i).keyed := true
kbuﬀ := pair(l, r) -: kbuﬀ
vote(i, null)
Precondition:phase = 3 ∧ voter(i).sreq = null ∧voter(i).line = null ∧ voter(i).f inish = f alse
Eﬀect:
voter(i).f inish := truevote(i, j)
Precondition:phase = 3 ∧ voter(i).keyed = true ∧voter(i).f inish = f alse ∧−1
 (voter(i).cand), voter(i).b)), voter(i).r)j = ξ −1 (σAd(χ−1 (σAdEﬀect:
voter(i).f inish := true

Figure 2: Transition rules of FOO
and for any other action a than the above, fV (a) = a.
In the rest of this section, suppose i and i are arbitrary voters. For any voter k, k̃ denotes i if k = i , i if
k = i, and k otherwise.
Definition 4.2 The function gi,i is deﬁned as follows:
If s.phase = 1,gi,i (s).phase = s.phasegi,i (s).line = s.line
gi,i (s).vbuﬀ = s.vbuﬀ
gi,i (s).kbuﬀ = s.kbuﬀ
gi,i (s).abuﬀ = exi,i (s.abuﬀ )gi,i (s).voter(k).sreq= null if s.voter(k).sreq = null,(s.voter(k̃).cand) otherwise.
σAdgi,i (s).voter(k).authed = s.voter(k).authed for any
voter k.
gi,i (s).voter(k).ψ = s.voter(k̃).ψ for any other subﬁeld ψ of voter(k) than sreq and authed.
Otherwise, gi,i simply exchanges i’s ﬁelds for thoseof i . Here, exi,i (x) is a multiset obtained by replacing each occurrence of pair(k, σk (s.voter(k).cand)) inx with pair(k, σk (s.voter(k̃).cand)).
The deﬁnition of the agent exchange above depends
on the value of phase because the simulation policy
must be switched during the execution of the protocol.
In phases 2 and 3, i’s behavior can be mimicked by iand vice versa since voters use the sender-anonymous
communication channel for cast and key transitions.

Hence, gi,i simply exchanges the states of i and i inthese phases.
In phase 1, however, i cannot mimic i since thesender-anonymous channel is not used, and so i’s behavior must be mimicked by i himself. Then, we cannot simply exchange subﬁelds authed and sreq between
i and i since these concern the progress in phase 1,
while subﬁelds cand, b, r must be exchanged to maintain consistency with phases 2 and 3. And since thesethree subﬁelds are exchanged, messages accumulated in
abuﬀ (and so the stored value of sreq after the ack action) must be exchanged between i and i . Therefore,
the above deﬁnition follows. Note that the observer
cannot observe the values of cand, r and b of each voter
since the messages in phase 1 are encrypted appropriately. Then we can prove the following theorem.
Theorem 4.3

Privacy: Let AI = {vote(j) | j is a candidate who
wins a vote in t̂}. Then, any voter i who performs vote(j)is private up to AI with respect to o in I.
Note that the above theorem does not claim any anonymity for voters who did not obtain a voting right. In
fact, a voter who did not obtain a voting right cannot
interchange his role with a voter who obtained it since
the observer knows who obtained it and who did not.

5

Conclusion

We formalized role interchangeability in multiagent
systems, and showed how known anonymity and privacy properties are derived from it. We also presented
a simulation proof method for the property. Then weapplied our method to a veriﬁcation of the anonymity
and privacy of the FOO electronic voting protocol. We
are now planning to extend our method to deal withprobabilistic systems.

1. The functions gi,i deﬁned above for all distincti, i ∈ I are agent exchange functions of S withrespect to i, i via fV .

Acknowledgements

2. Any interpreted system that is ω-compatible withtraces(S) is role interchangeable.

We thank Dr. Kiyoshi Shirayanagi and Prof. Masami
Hagiya for helpful discussions.

4.4

Anonymity and Privacy of FOO

Recall that role interchangeability alone does notlead to anonymity or privacy in the sense of Section
2. We need some appropriate premise, which corresponds to a restriction of possible traces. What is anappropriate restriction for this problem?
A natural restriction is to consider only traces of fair
executions with respect to ΣI,A . Here, we say an execution s0 , δ1 , s1 , δ2 , s2 , . . . is fair with respect to ΣI,A if
any action in ΣI,A continuously enabled will eventually
be performed, that is, unless i.a ∈ ΣI,A and an integer
n exist such that i.a is possible in sn and δn = i.a for
all n > n. For instance, a ﬁnite execution is fair inthis sense if and only if there is no possible action from
ΣI,A in the ﬁnal state. Let S be the automaton in Section 4.2. The set of all fair executions of S with respect
to ΣI,A is denoted by f execs(S). We write f traces(S)instead of trace(f execs(S)).
Another natural restriction is to assume trace t̂ was
obtained as the result of the actual execution of voting.
For instance, if the total number of votes in the actual
poll was 100, then we need not be concerned with thepossibility that only one voter participated in the voting. With this assumption we can restrict ourselves tothe traces t that satisfy fV (t) = fV (t̂). We deﬁne therestriction T ↑ft̂ V of trace set T with trace t̂ ∈ T andview function fV as the set {t ∈ T | fV (t) = fV (t̂)}. It
can be shown that this restriction preserves role interchangeability.
Then, we obtain the following veriﬁcation result.
Theorem 4.4 (Anonymity and Privacy of FOO)
Suppose an interpreted system I is ω-compatible withf traces(S) ↑ft̂ V .
Anonymity: Let IA be the set of all voters who obtainthe voting right in t̂. Then, vote(j) performed by i isanonymous up to IA with respect to o in I.

References[1] M. Abadi and C. Fournet. Private authentication.
TCS, 322(3):427–476, 2004.
[2] D. L. Chaum. Untraceable electronic mail, return addresses, and digital pseudonyms. CACM,
24(2):84–90, 1981.
[3] A. Fujioka, T. Okamoto, and K. Ohta. A practicalsecret voting scheme for large scale elections. In
Advances in Cryptography–AUSCRYPT ’92, pages
244–251, 1992. LNCS 718.
[4] J. Y. Halpern and K. R. O’Neill. Anonymity andinformation hiding in multiagent systems. JCS,
13(3):483–514, 2005.
[5] D. Hughes and V. Shmatikov. Information hiding,anonymity and privacy: A modular approach. JCS,
12(1):3–36, 2004.
[6] Y. Kawabe, K. Mano, H. Sakurada, and
Y. Tsukada. Simulation techniques to verify anonymity of security proptocols. In Computer Security Symposium 2005, volume I, pages 43–48, 2005.
In Japanese.
[7] S. Kremer and M. Ryan. Analysis of an electronic
voting protocol in the applied pi calculus. In European Symposium on Programming–ESOP 2005,
pages 186–200, 2005. LNCS 3444.
[8] N. A. Lynch. Distributed Algorithms. Morgan Kaufmann Publishers, 1996.
[9] S. Schneider and A. Sidiropoulos. CSP and anonymity. In Fourth European Symposium on Research in Computer Security (ESORICS 96), pages
198–218, 1996. LNCS 1146.