Computationally Sound Symbolic Anonymityof a Ring Signature
Yusuke Kawamoto †Hideki Sakurada ‡Masami Hagiya †† Department of Computer Science, Graduate School of Information Scienceand Technology, University of Tokyo { y k w mt, hagiya } @ is.s.u-tokyo.ac.jp‡ NTT Communication Science Laboratories, NTT Corporation sakurada @ theory.brl.ntt.co.jp

Abstract
This paper investigates the relationship between symbolic and computational
approaches to the analysis of the anonymity of cryptographic protocols. We provide two computational soundness results for a symbolic ring signature in the presence of active adversaries, each corresponding to the unforgeability and signer
anonymity of a ring signature scheme. The first result is the mapping-style soundness: every computational execution trace corresponds to a symbolic execution
trace with overwhelming probability. The second result is the soundness of thesymbolic anonymity of protocols: symbolic indistinguishability implies computational indistinguishability. By employing the mapping-style soundness result,
we obtain the soundness of the symbolic anonymity when the length of execution
traces is bound by a constant independent of the security parameter.
Key words: Formal methods, cryptographic protocols, computational soundness,anonymity.

1 Introduction
Symbolic and computational approaches have developed independently in research related to the security analysis of cryptographic protocols. In the symbolic approach, amessage is abstracted into a symbolic expression, called a Dolev-Yao term [10], and an
adversary can perform only a fixed set of operations on Dolev-Yao terms. The symbolic
analysis of cryptographic protocols assumes perfectly secure cryptographic schemes.
On the other hand, in the computational approach, a message is a bit string and an adversary is a probabilistic polynomial-time (PPT) Turing machine. The computational
analysis of cryptographic protocols is based on computational complexity theory.
In recent years, many researches have related these two approaches [2, 1, 14] to obtain computational soundness results, whereby symbolic security proofs imply strong
security guarantees based on computational complexity theory. The soundness resultsin the previous studies are divided into two categories: mapping-style soundness andindistinguishability-based soundness.
The former category of studies [14, 9, 8, 16, 4] has shown that every computational execution trace corresponds to a symbolic execution trace with overwhelming
probability. This kind of soundness results provides a computational guarantee for thesymbolic analysis of unforgeability and authenticity, which are expressed as nondeducibility in symbolic models. However, it cannot fully deal with anonymity, which isexpressed as indistinguishability. The latter category of studies [2, 12, 3, 11, 13] hasproven that symbolic indistinguishability implies computational indistinguishability.
This indistinguishability-based soundness can deal with anonymity, but is not suited to
unforgeability or authenticity.
This paper provides computational soundness results for both the symbolic nondeducibility and indistinguishability of a ring signature scheme [15, 6, 17]. A ring signature scheme is a digital signature scheme that enables an agent to produce a signature ofa message that identifies a group of possible signers but hides the actual signer. Since
it needs to satisfy both unforgeability and signer anonymity, we combine a mappingstyle soundness result with an indistinguishability-based soundness result. Althoughmany computational soundness results have been obtained for various cryptographic
schemes, no previous studies have dealt with the computational soundness of a symbolic ring signature, which requires both categories of soundness results. For the sakeof brevity, we do not deal with other cryptographic schemes whose soundness results
have been provided in previous studies.
To obtain the computational soundness result, we first extend the symbolic model
presented in [9, 8] to deal with the symbolic nondeducibility of a ring signature, andprove the mapping-style soundness of the model. Next, we introduce a symbolic indistinguishability into the model, and prove its computational soundness by employing
the mapping-style soundness. Here, our indistinguishability-based soundness result is
limited to a case where the length of execution traces is bound by a constant independent of the security parameter. However, this is the first step in our investigation of thecomputationally sound symbolic anonymity of a ring signature, and we will extend ourwork to more practical cases by using the technique presented in [7].
The organization of this paper is as follows. Section 2 presents the definitions of aring signature scheme and its computational security. Section 3 introduces a symbolicmodel, and Section 4 describes a concrete model. Section 5 provides a mapping-stylesoundness result, and Section 6 presents the soundness of symbolic anonymity. The
final section summarizes our work and discusses our future research.

2 Ring SignatureThis section briefly reviews the definition of a ring signature scheme and its security
notions. Hereafter we denote the set { 1, 2, · · · , n } by [n].

2.1 Ring Signature Scheme
A ring signature scheme [15] enables an agent to produce a digital signature of a message that identifies a group of possible signers but hides the actual signer. In thescheme, a real signer can produce a signature by using his own private signing key
and a set of public verification keys of possible signers. We describe the definition of aring signature scheme as follows.
Definition 1 A ring signature scheme is a triple (G, S, V) consisting of the following
three algorithms:• a key generation algorithm G that takes a security parameter 1η and a randomness
rgen , and outputs a private signing key and a public verification key pair (sk, vk).

• a signing algorithm S that takes a signing key sk, a set L of verification keys
that includes the key corresponding to sk, a message m, and a randomness r, andoutputs the signature of m using sk, L, and r.
• a verification algorithm V that takes a set L of verification keys and two bit
strings m and σ, and outputs 1 if σ is a valid signature of m using L, or 0
otherwise.
These algorithms must satisfy V(L, m, S(sk, L, m, r)) = 1, and messages must be
easily recovered from their signatures.
We assume that an adversary can add to L any verification keys possibly including
fake verification keys, which may not have the corresponding signing keys or cannot
generate signatures. We also assume that each public verification key is bound to theidentity of its owner by a certificate authority, so that the owner of the verification key
can be identified.

2.2 Security Definitions of a Ring Signature Scheme
The ring signature scheme defined above should satisfy two notions of security: unforgeability and anonymity. Although many definitions of security notions have been
proposed, we employ the definitions found in [6, 17].
First, we introduce an oracle O given to the adversary.
Definition 2 We define an oracle O that satisfies the following conditions.
• If O receives a signing query sign(i, L, m) for an agent i, a set L of verification
keys, and a message m, then it produces the signature of m using i’s private
signing key ski , L, and some fresh randomness r, and returns it to the adversary.
• If O receives a corruption query corrupt(i) for an agent i, then it returns i’s private
signing key ski to the adversary.
To prove the soundness result, we assume that the adversary sends corruption queries
to O before sending signing queries. We will take account of dynamic corruptions infuture work.
Next, we define the existential unforgeability of the ring signature scheme against
adaptive chosen message and public key attacks with insider corruptions [6].
Definition 3 A ring signature scheme (G, S, V) is existentially unforgeable if the advantage AdvEUF
defined below is negligible in every security parameter η for every PPTA
adversary A having access to the oracle O.
AdvEUFA (η) = Pr[(sk1 , vk1 ), · · · , (skn , vkn ) ← G(1η );Lleg :=(vk1 , · · · , vkn );(L, m, σ) := AO (1η , Lleg ) :V(L, m, σ) = 1, L ⊆ Lleg ,A has not queried corrupt(i) to O for any i with vki ∈ L, andA has not queried sign(i, L, m) to O for any i with vki ∈ L]

Note that the definition of existentially unforgeability does not prevent a PPT adversary from producing a signature of a message m using a randomness R from anothersignature of the same message m using another randomness R′ .
Finally, we define the basic anonymity of the ring signature scheme against adaptive
chosen message and chosen public key attacks [6, 17].

Definition 4 A ring signature scheme (G, S, V) is basically anonymous if the advantage AdvANO
defined below is negligible in every security parameter η for every PPTA
adversary A having access to the oracle O.
AdvANO(η) = Pr[ (sk1 , vk1 ), · · · , (skn , vkn ) ← G(1η );A
Lleg :=(vk1 , · · · , vkn );(i0 , i1 , L, m, ω) := AO (1η , Lleg );(vki0 , vki1 ∈ L ∩ Lleg , i0 , i1 )ηr ← C .r ;b ← { 0, 1 };σ := S(skib , L, m, r);b′ := AO (ω, σ) :b′ = b and A has not queried corrupt(i0 ) or corrupt(i1 ) to O ] − 21
where ω is an internal state of A, and Cη .r is the set of all the bit strings for randomness.

3 Symbolic Model
This section defines a symbolic model, which is an extension of the Dolev-Yao model
presented in [9, 8]. There are two kinds of parties: agents and an active and adaptive
adversary. Agents follow a protocol without deviation, and can run multiple sessionsof the protocol simultaneously. Agents are divided into honest agents and corrupted
agents, who give their private signing keys to the adversary before executing protocols.

3.1 Terms
We define the following sets of atomic symbols, which are mutually exclusive:• a set AG of agent identity symbols,• a set Garbage of garbage message symbols,• a set Nonceag of nonce symbols of agents,• a set Nonceadv of nonce symbols of the adversary,• a set Randag of randomness symbols of agents, and• a set Randadv of randomness symbols of the adversary.
Let Nonce = Nonceag ∪ Nonceadv and Rand = Randag ∪ Randadv . Intuitively, arandomness symbol denotes the random coin used to generate a signature. Let Atom =AG ∪ Garbage ∪ Nonce ∪ Rand.
Using these atomic symbols, a term is constructed from a signing key sk( ), a
verification key vk( ), a pairing ⟨ , ⟩, and a ring signing [ ] , as follows:
Term ∋ m ::= a | g | n | sk(a) | vk(a) | vk(g) | ⟨m, m⟩ | [ m ]Rsk(a), VK(G)

where a ∈ AG, g ∈ Garbage, n ∈ Nonce, R ∈ Rand, and VK(G) = { vk(x) | x ∈ G } forG ⊆ AG ∪ Garbage with |G ∩ AG| ≥ 2.
The term sk(a) denotes the legitimate signing key of an agent a ∈ AG, the termvk(a) denotes the legitimate verification key of an agent a ∈ AG, and the term vk(g)for g ∈ Garbage denotes a fake verification key that looks like a legitimate one.
The term ⟨m1 , m2 ⟩ denotes the concatenation of two messages m1 and m2 . The term
[ m ]Rsk(a), VK(G) denotes the signature of a message m by using a signing key sk(a), a setof verification keys VK(G), and a randomness R. Note that VK(G) may contain fakeverification keys.

φ⊢m

m∈φ

φ ⊢ a, vk(a)a ∈ AGφ ⊢ g, vk(g)φ ⊢ vk(x1 ), · · · , φ ⊢ vk(xn ) G = { x1 , · · · , xn } ⊆ AG∪Garbage,|G ∩ AG| ≥ 2
φ ⊢ VK(G)φ ⊢ m0 φ ⊢ m1
φ ⊢ ⟨m0 , m1 ⟩φ ⊢ ⟨m0 , m1 ⟩i = 0, 1
φ ⊢ miφ ⊢ sk(a) φ ⊢ VK(G) φ ⊢ m R ∈ Rand,
vk(a) ∈ VK(G)φ ⊢ [ m ]Rsk(a), VK(G)g ∈ Garbage

φ ⊢ [ m ]Rsk(a), VK(G)φ⊢mφ ⊢ [ m ]Rsk(a), VK(G)′φ ⊢ [ m ]Rsk(a), VK(G)φ ⊢ [ m ]Rsk(a), VK(G)φ ⊢ [ m ]Rsk(b), VK(G)R′ ∈ Randvk(b) ∈ VK(G)Figure 1: The adversary’s deduction rules.
We define the following subsets of Term: SKey, VKey, Pair, and Sign, each denoting the set of all terms starting with sk( ), vk( ), ⟨ , ⟩, and [ ] , , respectively. Let
VKeyList be the set { VK(G) | G ⊆ AG ∪ Garbage, |G ∩ AG| ≥ 2 }. We sometimes referto these sets as types.
We use terms with variables to describe protocols. We introduce the following
infinite sets of variables: X.a, X.g, X.n, X.r, X.p, X.s, and X.L each denoting the setof all variables of the type AG, Garbage, Nonce, Rand, Pair, Sign, and VKeyList,
respectively. Let X = X.a ∪ X.g ∪ X.n ∪ X.r ∪ X.p ∪ X.s ∪ X.L.
To represent agents’ messages, we define the set ATerm(X) of agent terms:
X.r
ATerm(X) ∋ m ::= X | vk(X ′ ) | ⟨m, m⟩ | [ m ]sk(A), X.L

where X ∈ X.a ∪ X.n ∪ X.p ∪ X.s, X ′ ∈ X.a ∪ X.g, A ∈ X.a, X.r ∈ X.r, and X.L ∈ X.L.
By using agent terms in ATerm(X), we describe protocols where agents do not try
to construct ill-formed messages using garbage messages, or to send signing keys or
randomnesses as plaintexts. Note that we do not need symbols in AG ∪ Nonce ∪ Rand in
the definition of ATerm(X), because we assign a term to each variable of X.a ∪ X.n ∪ X.r
occurring in a session of the protocol execution defined below when the session iscreated. In later sections, we use variables Ai ∈ X.a, X.nAj i ∈ X.n, X.rAj i ∈ X.r, andLij ∈ X.L to describe agents’ messages.

3.2 Deduction Rules
We introduce deduction rules in Figure 1 to restrict the behavior of the adversary inthe symbolic setting. In the deduction rules, a set φ of terms represents the adversary’s knowledge of messages. These rules are standard [9] except for ring signatures.
The rule for deriving [ m ]Rsk(b), VK(G) from [ m ]Rsk(a), VK(G) expresses that the definitionof existential unforgeability does not prevent the adversary from producing an agent
b’s signature of a message m from another agent a’s signature of m when a, b ∈ G.
′
The rule for deriving [ m ]Rsk(a), VK(G) from [ m ]Rsk(a), VK(G) expresses that the definition ofexistential unforgeability does not prevent the adversary from rerandomizing a signature, i.e., replacing a randomness used to produce a signature by another randomness.
Although these rules are too strong for us to obtain a computational completeness ofsymbolic nondeducibility, they allow us to obtain a computational soundness result in
Section 5.

3.3 Symbolic Execution Model
We introduce roles to define a symbolic execution model. Our definition is standard
and similar to that in [9, 8]. Hereafter we denote the domain of a function f by dom( f ).
A k-party protocol Π is a function that maps each i ∈ [k] to a role tree Π(i). A role
tree Π(i) for an agent Ai ∈ X.a is a finite ordered edge-labeled tree where each edge islabeled by an agent rule (l, r) consisting of l ∈ ATerm(X) and r ∈ ATerm(X) ∪ { ⊥ },where the symbol ⊥ represents the abort of the protocol Π. Here, l and r represent messages sent from the adversary to the agent Ai and from Ai to the adversary, respectively.
If Ai sends ⊥ to the adversary, then the execution of the protocol Π stops. We denote
the root node of a role tree by ε. In an execution of a protocol Π, each agent Ai stands
at a node of his role tree Π(i). We assume that the number of children of each node ineach role tree is independent of the security parameter η introduced in Section 4.
A symbolic execution trace of a k-party protocol Π is a finite sequence of global
states with the restrictions given below. A global state is a triple (SId, f, φ) consistingof a finite set SId of session ids, a function f that maps each session id in SId to thecurrent local state of the corresponding session, and the set φ of terms representing
the current adversary’s knowledge. A local state of a session sid ∈ SId is a quadruple(i, σ, p, (a1 , · · · , ak )) where i ∈ [k] is the index of the role tree Π(i), σ is a partial
function from X to Term, p is a node in the role tree Π(i), each a j ∈ AG is the agent
carrying out the session sid, and σ(A j ) = a j holds for each j ∈ [k].
The partial function σ : X → Term is updated in the execution of the protocol Π.
Let p be a node in the role tree Π(i). Now, if the agent ai receives a term m at p, thenai produces a term m′ as follows. Until ai outputs some term, each agent rule thatlabels an outgoing edge of the node p is applied to m in order from the left-most ruleto the right-most rule. Given an agent rule (l, r), m is matched against lσ. If m andlσ match, we denote the matcher by η. Then, the agent produces the output m′ := rση,and follows the edge to the child node, where σ is updated to ση. Note that m′ does
not contain a variable, because of the conditions introduced below. If m and lσ do notmatch, the next agent rule is applied. If there is no rule (l, r) such that m and lσ match,then the agent outputs no term and σ remains unchanged. We describe the restriction
to the role tree at the end of this section.
To define transitions between global states, we introduce some notations. We denote distinct nonces by na, j, s ∈ Nonceag with a ∈ AG and j, s ∈ IN, and distinct
randomnesses by ra, j, s ∈ Randag with a ∈ AG, j ∈ Randag , and s ∈ IN. Let τa, s be afunction that maps each j ∈ Randag to ra, j, s . For a term t ∈ ATerm(X), we write tτa, s
to denote the term obtained from t by replacing every occurrence of j ∈ Randag in twith τa, s ( j) simultaneously.
The initial global state is qI = (∅, ∅, Nonceadv ). We allow three kinds of transitions
between global states: corrupt, new, and send.
• The adversary can specify a set of agents and obtain their private signing keys
corrupt(a1 , ··· , al )before the execution of the protocol: qI −−−−−−−−−−−−→ (∅, ∅, Nonceadv ∪ CSKey )where CSKey = { sk(ai ) | i ∈ [l] }.
• The adversary can initiate a new session for an agent Ai and specify the sets ofnew(i, a1 , ··· , ak , VK(G1i ), ··· , VK(Gmi ))verification keys used to produce ring signatures: (SId, f, φ) −−−−−−−−−−−−−−−−−−−−−−−−−→′′(SId′ , f ′ , φ) where VK(G1i ), · · · , VK(Gmi ) ∈ VKeyList, and SId and f are defined as follows.
– Let SId′ be the set SId ∪ { sid } for the new session sid = |SId| + 1.

– Let f ′ be the function that satisfies f ′ (sid′ ) = f (sid′ ) for every sid′ ∈ SId
and f ′ (sid) = (i, σ, ε, (a1 , · · · , ak )) where dom(σ) = { A j | j ∈ [k] } ∪{ X.nAj i | j ∈ IN } ∪ { X.rAj i | j ∈ Randag } ∪ { Lij | j ∈ [m] }, σ(A j ) = a j foreach j ∈ [k], σ(X.nAj i ) = nai , j, sid for each j ∈ IN, σ(X.rAj i ) = rai , j, sid foreach j ∈ Randag , and σ(Lij ) = VK(Gij ) for each Lij ∈ X.L with j ∈ [m]. If avariable L ∈ X.L satisfying L , Lij for each j ∈ [m] occurs in the agent Ai ’srole tree Π(i), then the adversary cannot create the new session sid.
send(sid, m)• The adversary can send messages: (SId, f, φ) −−−−−−−−→ (SId, f ′ , φ′ ) where sid
is a tuple (sid1 , · · · , sidv ) of elements in SId with v ≥ 2, m ∈ Term, φ ⊢ m,
and f ′ and φ′ are defined as follows. The function f ′ initially satisfies f ′ (sid′ ) =f (sid′ ) for every sid′ ∈ SId. In this transition, the term m is first sent to thesession sid1 . For each u ∈ [v − 1], if m is not received by sidu , then it is sent tosidu+1 . For a session sidu ∈ sid, suppose that f (sidu ) = (i, σ, p, (a1 , · · · , ak ))and ((l1 , r1 ), · · · , (lh , rh )) are the labels of edges leaving p in this order.
– If there does not exist j such that m and l j σ match, then we have φ′ = φ,and m is sent to the session sidu+1 . If m is not received by any sessions insid, then the adversary receives nothing.
– Otherwise, let j be minimal such that m and l j σ match. Let θ be thematcher. Then, we update f ′ to obtain f ′ (sid) = (i, σθ, p j , (a1 , · · · , ak ))and φ′ = φ ∪ { r j τai , sid σθ } where p j is the j-th child node of p. Here,the adversary receives the message r j τai , sid σθ, but does not learn which
session he receives it from. Thus, this transition represents an anonymous
communication.
The set of symbolic execution traces for a protocol Π is denoted by Exec s (Π).
We introduce the following restrictions on role trees. For a node p , ε in therole tree Π(i), let Rules≤p be the sequence of agent rules with which the edges on thepath from the root node ε to p are labeled. We write Rulesl≤p and Rulesr≤p to denote thesequence of the left/right-hand side of the rules Rules≤p , respectively. If p , ε holds, wewrite rulep or (rulelp , rulerp ) to denote the agent rule with which the edge leading to p islabeled. Let K pi = { sk(Ai ) }∪{ A j | j ∈ [k] }∪{ X.nAj i | j ∈ IN }∪{ Lij | j ∈ [m] }∪Rulesl≤p .
For each node p , ε in the role tree Π(i), we require the following conditions.
X.rrl
1. If a term of the form [ t ]sk(A), X.L occurs in rulep , then either it occurs in Rules≤p ,or A = Ai holds and X.r ∈ X.r never occurs in Rulesl≤p or Rulesr≤p .
2. For every A ∈ X.a, if sk(A) occurs in Rulesl≤p , then A , A j holds for j , i
X.rand A occurs in Rulesl≤p at most once in a term of the form [ t ]sk(A), X.L for somet ∈ ATerm(X), X.r ∈ X.r, and X.L ∈ X.L.
X.r
3. Every X.r ∈ X.r occurs in Rulesl≤p at most once in a term of the form [ t ]sk(A), X.L
for some t ∈ ATerm(X), A ∈ X.a, and X.L ∈ X.L.
4. For every variable X ∈ X \ X.a ∪ X.n ∪ X.r, if X occurs in rulerp , X occurs in
Rulesl≤p .
5. We have K pi ⊢ rulerp .
Intuitively, the first condition prescribes that no agent can forge another agent’s signature, and that each agent should always use a fresh randomness when he produces asignature. The second condition prescribes that agents cannot break signer anonymity.
The third condition prescribes that agents cannot recognize the diﬀerent signaturesproduced using the same randomness. Note that we can describe the protocols where
agents recognize the same signatures, because we can use variables in X.s. The last two
conditions prescribe that each agent can produce terms only from previously received
terms.

4 Concrete Model
This section defines a concrete model similar to that in [9, 8].
In the concrete model, bit strings are tagged with type tags, and the adversary caneﬃciently recognize the following types of bit strings: agent ids, nonces, randomnesses, garbages, signing keys, verification keys, pairs, signatures, and a set of verification keys including at least two legitimate verification keys. These concrete types
are denoted by Cη .a, Cη .n, Cη .r, Cη .g, Cη .sk, Cη .vk, Cη .p, Cη .s, and Cη .L, respectively,
where η is a security parameter. We denote the set of all bit strings by Cη .
A concrete execution trace of a k-party protocol Π is a finite sequence of concrete
global states with the restrictions presented below. A concrete global state is a pair(SId, g) consisting of a finite set SId of session ids, and a function g that maps eachsession id in SId to the current concrete local state of the corresponding session. A
concrete local state of a session sid ∈ SId is a quadruple (i, ρ, p, (a1 , · · · , ak )) wherei ∈ [k] is the index of the role tree Π(i), ρ is a partial function from X to Cη , p is anode in the role tree Π(i), each a j ∈ Cη .a is the agent carrying out the session sid, andρ(A j ) = a j holds for each j ∈ [k]. The partial function ρ : X → Cη is updated in theconcrete execution of the protocol Π in the same way as in the definition of the partial
function σ : X → Term in the symbolic model except that ρ assigns bit strings insteadof terms.
In a concrete execution of a protocol Π, agents and an active and adaptive adversary
A are probabilistic polynomial time (PPT) Turing machines with respect to the security parameter η, and if one of the machines reaches the computation bounds then theexecution of Π stops. The sequence of all random coins used by agents and the oracle
O is denoted by RΠ , and the sequence of all random coins used by the adversary A isdenoted by RA . If RΠ and RA are fixed, then the concrete execution trace is uniquelydetermined, and is written as ExeccΠ(RΠ ), A(RA ) (η).
In the concrete model, we fix a ring signature scheme (G, S, V). Let Lleg be a setof all legitimate verification keys that is initially empty and available to the adversary.
Whenever a verification key is generated by running G(1η , RΠ ), it is added to Lleg .
We define transitions between concrete global states in ExeccΠ(RΠ ), A(RA ) (η) as follows. The initial concrete global state is qI = (∅, ∅). We allow three kinds of transitions
between concrete global states: corrupt, new, and send.
• The adversary can specify a set of agents and obtain their private signing keys
corrupt(a1 , ··· , al )before the execution of the protocol: qI −−−−−−−−−−−−→ qI where a1 , · · · , al ∈Cη .a. Then, the signing and verification keys are generated for the agents byrunning G(1η , RΠ ), and are given to the adversary A.
• The adversary can initiate a new session for an agent Ai and specify the sets ofnew(i, a1 , ··· , ak , L1i , ··· , Lmi )verification keys used to produce ring signatures: (SId, g) −−−−−−−−−−−−−−−−−−−→
η′′(SId′ , g′ ) where i ∈ [k], a1 , · · · , ak ∈ Cη .a, L1i , · · · , Lm
i ∈ C .L and SId and g
are defined as follows.
– Let SId′ be the set SId ∪ { sid } for the new session sid = |SId| + 1.

– Let g′ be the function that satisfies g′ (sid′ ) = g(sid′ ) for every sid′ ∈ SId
and g′ (sid) = (i, ρ, ε, (a1 , · · · , ak )) where dom(ρ) = { A j | j ∈ [k] } ∪{ X.nAj i | j ∈ IN } ∪ { X.rAj i | j ∈ Randag } ∪ { Lij | j ∈ [m] }, ρ(A j ) = a j forRΠRΠeach j ∈ [k], ρ(X.nAj i ) ←−− Cη .n for each j ∈ IN, ρ(X.rAj i ) ←−− Cη .r for eachj ∈ Randag , and ρ(Lij ) = Lij for each Lij ∈ X.L with j ∈ [m]. If a variable
L ∈ X.L satisfying L , Lij for each j ∈ [m] occurs in the agent Ai ’s role tree
Π(i), then the adversary A cannot create the new session sid.
As a result of this transition, each a j ’s signing and verification keys are generated
if they have not been produced yet, and all the verification keys are given to A.
send(sid, m)• The adversary can send messages: (SId, g) −−−−−−−−→ (SId, g′ ) where sid is atuple (sid1 , · · · , sidv ) of elements in SId with v ≥ 2, m ∈ Cη , and g′ is defined asfollows. The function g′ initially satisfies g′ (sid′ ) = g(sid′ ) for every sid′ ∈ SId.
In this transition, the term m is first sent to the session sid1 . For each u ∈ [v − 1],
if m is not received by sidu , then it is sent to sidu+1 . For a session sidu ∈ sid,
suppose that g(sid) = (i, ρ, p, (a1 , · · · , ak )) and ((l1 , r1 ), · · · , (lh , rh )) are thelabels of edges leaving p in this order.
– If there does not exist j such that m and l j ρ match, then m is sent to thesession sidu+1 . If m is not received by any sessions in sid, then the adversary
A receives nothing.
– Otherwise, let j be minimal such that m and l j ρ match. Let θ be the matcher.
Then, we update g′ to obtain g′ (sid) = (i, ρ′ , p j , (a1 , · · · , ak )) and theagent ai outputs the bit string corresponding to r j τai , sid ρ′ where ρ′ = ρθand p j is the j-th child node of p. Although the adversary A receives thebit string, he does not learn which session he receives it from.
Matching l j ρ against m is performed recursively on the structure of l j .
– If l j ∈ X, and the types of l j and m match, then∗ if ρ(l j ) = m, then ρ′ = ρ,∗ if ρ(l j ) is not defined, then ρ′ (X) = ρ(X) for every X , l j and ρ′ (l j ) = m.
– If l j = vk(X ′ ) for some X ′ ∈ X.a∪X.g, and m is a legitimate/fake verification
key, then l j ρ is matched against m. If the matcher θ exists, then ρ′ = ρθ.
– If l j = ⟨l j1 , l j2 ⟩ and m is the pair consisting of m1 and m2 , then l j1 ρ ismatched against m1 . If the matcher θ1 exists, then l j2 ρθ1 is matched against
m2 . If the matcher θ2 exists, then ρ′ = ρθ1 θ2 .
– If l j = [ lm′ ]lskR (A), lL and m is a signature of m′ using a set L of verification
keys, then lm′ ρ is matched against m′ . If the matcher θ1 exists, then lL ρθ1
is matched against L. If the matcher θ2 exists, then ρ′ = ρθ1 θ2 . Note thatsk(A) and lR do not occur as terms in r j .
– Otherwise, the matching fails.

5 Computational Soundness of Nondeducibility
This section provides a mapping-style computational soundness result for the above
symbolic execution model.

First, we define a partial function c that maps each term to a bit string, and a concrete instantiation of a symbolic execution trace in the same way as in [9, 8].
Definition 5 Let t s = (SId1s , f1 , φ1 ), · · · , (SIdns , fn , φn ) be a symbolic execution trace,and tc = (SIdc1 , g1 ), · · · , (SIdcn , gn ) be a concrete execution trace. The trace tc is aconcrete instantiation of t s with an injective partial mapping c : Term → Cη , written ast s ≼c tc , if for every ℓ ∈ [n], it holds that
• SIdℓs = SIdcℓ , and• for every sid ∈ SIdℓs , if fℓ (sid) = (isid , σsid , psid , (a1 , · · · , an )) and gℓ (sid) =( jsid , ρsid , qsid , (a1 , · · · , an )), then isid = jsid , ρsid = cσsid , and psid = qsid .
The trace tc is a concrete instantiation of t s , written as t s ≼ tc , if there exists an injective
partial mapping c : Term → Cη that satisfies t s ≼c tc .
Next, we provide a mapping-style computational soundness result.
Theorem 1 Let Π be a protocol. If a ring signature scheme (G, S, V) satisfies existential unforgeability, then for any PPT adversary A,
Pr[ ∃ t s ∈ Exec s (Π) | t s ≼ ExeccΠ(RΠ ), A(RA ) (η) ] ≥ 1 − νA (η)
where the probability is over the choice (RΠ , RA ) ← { 0, 1 } pA (η) × { 0, 1 }qA (η) , and νA
is a function that is negligible in η.
We use the following lemma to prove Theorem 1.
Lemma 1 Let C = CSKey ∪ Nonceadv , φ′ ⊆ Term \ C, φ = φ′ ∪ C, m ∈ Term,∪
Nonceag (m) = { n ∈ Nonceag | n ⊑ m }, and Nonceag (φ′ ) = m′ ∈φ′ Nonceag (m′ ). If
φ 0 m, then either
1. there exists a term [ t ]Rsk(a), VK(G) with sk(a′ ) < CSKey for any a′ ∈ G ∩ AG such′that we have [ t ]Rsk(a), VK(G) ⊑ m and [ t ]Rsk(a′ ), VK(G) @ m′ for every R′ ∈ Rand,′′
every a ∈ G ∩ AG, and every m ∈ φ,
2. there exists sk(a) < CSKey that occurs in m in a form other than [ t ]Rsk(a), VK(G) , or
3. Nonceag (m) \ Nonceag (φ′ ) , ∅ holds.
Proof of Theorem 1 (Overview).
two steps.

The proof is similar to [9, 8], and is divided into

STEP I. First, we associate each concrete execution trace with a symbolic execution
trace. By fixing the security parameter η and the random coins RΠ and RA , we can generate all agent identities, garbage messages, nonces, signing keys, and randomnesses.
Hence, we obtain a unique concrete execution trace tc = ExeccΠ(RΠ ), A(RA ) (η). Then, it issuﬃcient to show that tc is an instantiation of a symbolic execution trace t s , i.e., t s ≼ tc .
We can construct the symbolic execution trace t s and the function parse that maps each
bit string occurring in tc to a term occurring in t s . This step is similar to that in [9, 8].
If a bit string does not have one of the types defined above, and has not been parsed
previously, then we map it to a fresh garbage message symbol in Garbage.

STEP II. Next, we show that with overwhelming probability, the symbolic execution
trace t s constructed above satisfies t s ∈ Exec s (Π), that is, t s is a Dolev-Yao trace. We
assume that in the ℓ-th step of t s , t s has already been proven to be a Dolev-Yao trace.
For some set φ′ℓ with φ′ℓ ∩ C = ∅, let φℓ = φ′ℓ ∪ C be the adversary’s knowledge inthe ℓ-th step of t s . Then, it is suﬃcient to prove that for each send(sid, m) transition
made by the PPT adversary A in the (ℓ + 1)-th step of the concrete execution trace tc ,the adversary makes the query send(sid, parse(m)) in the symbolic execution trace t s ,and we have φℓ ⊢ parse(m) with overwhelming probability. To prove this, we assume
that φℓ 0 parse(m) holds with non-negligible probability, and derive a contradiction to
a computational security such as the unforgeability of the ring signature scheme. By
using Lemma 1, we divide this proof into three cases corresponding to the conditionsof Lemma 1.
In the first case, there exists a term [ t ]Rsk(a), VK(G) with sk(a′ ) < CSKey for any a′ ∈′G ∩ AG such that we have [ t ]Rsk(a), VK(G) ⊑ parse(m) and [ t ]Rsk(a′ ), VK(G) @ m′ for everyR′ ∈ Rand, a′ ∈ G ∩ AG, and m′ ∈ φ. Then, we construct an adversary B that uses A
as a subroutine maintaining the global states of the concrete execution and playing therole of the agents in the execution. By using the oracle O defined in Definition 2, theadversary B parses the queries made by A and sends the answers to A. Since B simulates the execution of protocols on behalf of the agents, A makes a query send(sid, m)
where m contains a ring signature of a message m′′ such that no ring signatures of m′′
have appeared previously. Then, the adversary B outputs the ring signature and stops.
Hence, B breaks the existential unforgeability of the ring signature scheme.
In the second case, there exists sk(a) < CSKey that occurs in parse(m) in a form otherthan [ t ]Rsk(a), VK(G) . Then, the PPT adversary A can obtain the signing key corresponding to sk(a). Therefore, we can construct an adversary that breaks the unforgeability of
the ring signature scheme by using the signing key.
In the last case, we have Nonceag (parse(m)) \ Nonceag (φ′ℓ ) , ∅. Then, the PPTadversary A can produce an agent’s nonce independent of the messages that A has
received.
Finally, we mention the computational soundness of a ring signature scheme thatsatisfies strong existential unforgeability 1 . To prove the mapping-style soundness theorem similar to Theorem 1, it is suﬃcient to remove the deduction rule shown in Fig′ure 1 that allows the adversary to produce [ m ]Rsk(a), VK(G) from [ m ]Rsk(a), VK(G) for any
R′ ∈ Rand.

6 Computational Soundness of Indistinguishability
The mapping-style soundness result in Theorem 1 is insuﬃcient as regards the signer
anonymity of the ring signature scheme. In fact, in the proof of Theorem 1, we did notneed to use any computational security notion with respect to the signer anonymityof the ring signature scheme. This is because our symbolic model could not deal
with indistinguishability-based properties, including signer anonymity, in the deduction rules shown in Figure 1. To deal with signer anonymity in our model, we introduce
a symbolic indistinguishability relation and prove its computational soundness.
1 The strong existential unforgeability of a ring signature scheme [17] forbids anyone to produce a ring
signature of a message m using a randomness R from another signature of m using another randomness R′ .

6.1 Symbolic Indistinguishability
First, we introduce a set Pattern of symbolic patterns as follows:
Pattern ∋ m ::= a | g | n | sk(a) | vk(a) | vk(g) | ⟨m, m⟩ | [ m ]Rsk(a), VK(G) | [ m ]Rsk(G ), VK(G)

where a ∈ AG, g ∈ Garbage, n ∈ Nonce, R ∈ Rand, VK(G) = { vk(x) | x ∈ G } forG ⊆ AG ∪ Garbage with |G ∩ AG| ≥ 2, and G is a special symbol representing someagent in G. Note that patterns are the same as terms except for those representing thesignatures [ m ]Rsk(G ), VK(G) with signer anonymity.
Next, we associate each term with a pattern.
Definition 6 We define the function pat : Term × P(SKey) → Pattern that maps t ∈Term and KS ⊆ SKey to t’s pattern with respect to KS.
• pat(m, KS) = m (if m ∈ Atom ∪ SKey ∪ VKey)• pat(⟨m1 , m2 ⟩, KS) = ⟨pat(m{ 1 , KS), pat(mR2 , KS)⟩[ pat(m, KS) ]sk(a), VK(G) (if sk(a′ ) ∈ KS for some a′ ∈ G )R• pat([ m ]sk(a), VK(G) , KS) =[ pat(m, KS) ]Rsk(G ), VK(G) (otherwise)
Then, we define a symbolic indistinguishability relation between terms.
Definition 7 An atomic renaming λ is a type-preserving injection from Nonce ∪ Rand
to Nonce ∪ Rand. A renaming λ̃ with respect to an atomic renaming λ is a function
from Pattern to Pattern defined inductively as follows:• λ̃(x) = x (x ∈ AG ∪ Garbage)• λ̃(n) = λ(n) (n ∈ Nonce)• λ̃(sk(a)) = sk(a)• λ̃(vk(x)) = vk(x)• λ̃(⟨t1 , t2 ⟩) = ⟨λ̃(t1 ), λ̃(t2 )⟩λ(R)• λ̃([ t ]Rsk(a), VK(G) ) = [ λ̃(t) ]sk(a), VK(G)λ(R)• λ̃([ t ]Rsk(G ), VK(G) ) = [ λ̃(t) ]sk(G ), VK(G)Definition 8 Two terms m and m′ are symbolically indistinguishable with respect toan atomic renaming λ and a set CSKey of signing key symbols, written as m λ, CSKey m′ ,if we have λ̃(pat(m, CSKey )) = pat(m′ , CSKey ). Two terms m and m′ are symbolicallyindistinguishable, written as m  m′ , if there exist an atomic renaming λ and a set
CSKey of signing key symbols that satisfy m λ, CSKey m′ .
Finally, we define a symbolic indistinguishability relation between symbolic traces.
Definition 9 Two finite symbolic traces t0s and t1s have equivalent transition types underan atomic renaming λ and a set CSKey of signing key symbols if they satisfy the following conditions: If we have CSKey = { a1 , · · · , al }, then the transition corrupt(a1 , · · · , al )takes place both in t0s and t1s . If a transition in t0s is by new(i, a1 , · · · , ak ), the corresponding transition in t1s is by new(i, a1 , · · · , ak ). If a transition in t0s is by send(sid, m0 ),the corresponding transition in t1s is by send(sid, m1 ), where m1 is constructed by thesame derivation as that of m0 except that λ̃ is applied.
Definition 10 Two finite symbolic traces t0s and t1s are symbolically indistinguishable
with respect to an atomic renaming λ and a set CSKey of signing key symbols, written
as t0s λ, CSKey t1s , if t0s and t1s have equivalent transition types under λ and CSKey , andeach term m0 received by the adversary in t0s and the corresponding term m1 in t1s are
symbolically indistinguishable with respect to λ and CSKey , i.e., m0 λ, CSKey m1 . Two
finite symbolic traces t0s and t1s are symbolically indistinguishable, written as t0s  t1s , ifthere exist an atomic renaming λ and a set CSKey of signing key symbols that satisfy
t0s λ, CSKey t1s .

6.2 Computational Soundness of Indistinguishability
First, we define the computational indistinguishability between distributions.
Definition 11 Two probability distributions Dη and D′ η are computationally indistinguishable, written Dη ≈ D′ η , if for every PPT adversary A,
Pr[d ← Dη : A(d, η) = 1] − Pr[d′ ← D′ η : A(d′ , η) = 1]
is negligible in η.
Then, we present a soundness result for computational indistinguishability. Let Π
be a protocol. Let Exec s,≤h (Π) be the set of all symbolic traces each of which is a prefixof a symbolic trace in Exec s (Π) and stops at h or fewer steps. Let Execc,hΠ( · ), A( · ) (η) be
the probability distribution obtained from ExeccΠ( · ), A( · ) (η) such that each concrete tracecin Execc,hΠ( · ), A( · ) (η) is a prefix of a concrete trace in ExecΠ( · ), A( · ) (η) and stops at h steps.
Theorem 2 Let Π1 and Π2 be any two protocols using an existential unforgeable andbasically anonymous ring signature scheme (G, S, V), and h > 0 be a fixed integer
independent of η. Assume that for every symbolic trace t1s ∈ Exec s,≤h (Π1 ), there exists
a symbolic trace t2s ∈ Exec s,≤h (Π2 ) with t1s  t2s , and that for every symbolic tracet2s ∈ Exec s,≤h (Π2 ), there exists a symbolic trace t1s ∈ Exec s,≤h (Π1 ) with t1s  t2s . Then,c,hwe have ExecΠ(η) ≈ Execc,hΠ2 ( · ), A( · ) (η).
1 ( · ), A( · )Proof (Overview). For any PPT adversary A and each 0 ≤ k ≤ h, we define Adv(1, k)
and Adv(2, k) as follows:c
Adv(1, k) = Pr[t1c ← Execc,kΠ1 ( · ), A( · ) (η) : A(t1 , η) = 1]c
Adv(2, k) = Pr[t2c ← Execc,kΠ2 ( · ), A( · ) (η) : A(t2 , η) = 1].

Then, we show by induction on k that Adv(1, k) − Adv(2, k) is negligible in η for any
PPT adversary A. Clearly, we have Adv(1, 0) − Adv(2, 0) = 0. Let 0 ≤ k < h.
Assume that Adv(1, k) − Adv(2, k) is negligible in η. Then, it is suﬃcient to prove that
Adv(1, k + 1) − Adv(2, k + 1) is also negligible in η.
Let Supp be the function that maps a probability distribution to its support. For any
error
PPT adversary A and j = 1, 2, we define Errorc,k( j, k) as follows:Π j ( · ), A( · ) (η) and Adv
{

c,k
s,≤k
s
c
s
ErrorΠ(η) = tc ∈ Supp(Execc,kΠ j ( · ), A( · ) (η)) | t ≼ t holds for no t ∈ ExecΠ j ( · ), A( · ) (η)
j ( · ), A( · )

}

[
]
c,k
c
c
Adverror ( j, k) = Pr tcj ← Execc,kΠ j ( · ), A( · ) (η) : t j ∈ ErrorΠ j ( · ), A( · ) (η) and A(t j , η) = 1 .

We denote the length of a symbolic/concrete trace t by |t|, i.e., t stops at |t| steps. For asymbolic trace t s , we define [[ t s ]]k as follows:[[ t s ]]k = { t′ c | t s ≼ tc and t′ c is a prefix of tc with |t′ c | = k }.
For j = 1, 2, 0 ≤ k ≤ h, and an index set I(k) dependent on k and independent of η, let{ t sj, i | i ∈ I(k) } be a set of symbolic traces that satisfies
Supp(Execc,kΠ j ( · ), A( · ) (η)) =∪[[ t sj, i ]]k ∪ Errorc,kΠ j ( · ), A( · ) (η).

i∈I(k)

We can take I(k) independently of η, because the number of children of each node ineach role tree is independent of η. Here, by assumption, we can assume that t1,s i  t2,s iholds for each i ∈ I(k) without losing generality. For i ∈ I(k), we define Pi ( j, k) andQi ( j, k) by:
[
]
c
s
k
Pi ( j, k) = Pr tcj ← Execc,kΠ j ( · ), A( · ) (η) : t j ∈ [[ t j, i ]]][Qi ( j, k) = Pr tcj ← [[ t sj, i ]]k : A(tcj , η) = 1 .

Then, we haveAdv( j, k + 1) =

∑

]
[
c
s
k+1
and A(tcj , η) = 1 + Adverror ( j, k + 1)
Pr tcj ← Execc,k+1
Π j ( · ), A( · ) (η) : t j ∈ [[ t j, i ]]i∈I(k+1)=∑

Pi ( j, k + 1) · Qi ( j, k + 1) + Adverror ( j, k + 1).

i∈I(k+1)

By the mapping soundness result shown in Theorem 1, Adverror (1, k+1)−Adverror (2, k + 1)
is negligible in η. In addition, we can prove that Qi (1, k + 1) − Qi (2, k + 1) is negligible in η for each i ∈ I(k + 1) by using a hybrid argument similar to [2], because
the ring signature scheme (G, S, V) satisfies basic anonymity. By using the induction
hypothesis that Adv(1, k) − Adv(2, k) is negligible in η, we can prove that for eachi ∈ I(k + 1), Pi (1, k + 1) − Pi (2, k + 1) is negligible in η. Since I(k + 1) is independentof η, Adv(1, k + 1) − Adv(2, k + 1) is negligible in η.


7 Conclusion
We proposed a symbolic model dealing with a ring signature, and presented two kindsof computational soundness results in the presence of active adversaries. The first result
is the mapping-style soundness: every concrete execution trace corresponds to a symbolic execution trace with overwhelming probability. The second result is the soundness of symbolic anonymity: symbolic indistinguishability implies computational indistinguishability.
Our soundness result for symbolic anonymity is limited to a case where the lengthof each trace is a constant independent of the security parameter. However, we willtake account of traces each of whose length depends on the security parameter by using the technique presented in [7]. In addition, we will also employ a more genericapproach [5, 7] to investigate the computationally sound symbolic anonymity of various protocols.

Acknowledgments
We thank Prof. Hubert Comon-Lundh for his helpful comments and suggestions.

References[1] M. Abadi and J. Jürjens. Formal eavesdropping and its computational interpretation. In TACS ’01: Proceedings of the 4th International Symposium on Theoretical Aspects of Computer Software, pages 82–94. Springer-Verlag, 2001.
[2] M. Abadi and P. Rogaway. Reconciling two views of cryptography (the computational soundness of formal encryption). Journal of Cryptology, 15(2):103 – 127,2002.

[3] P. Adao, G. Bana, and A. Scedrov. Computational and information-theoretic
soundness and completeness of formal encryption. In CSFW 2005, pages 170–
184, 2005.
[4] M. Backes and D. Unruh. Computational soundness of symbolic zero-knowledge
proofs against active attackers. In CSF 2008, 2008. To appear. Available at
http://www.infsec.cs.uni-sb.de/˜unruh/.
[5] M. Baudet, V. Cortier, and S. Kremer. Computationally sound implementations ofequational theories against passive adversaries. In ICALP, pages 652–663, 2005.
[6] A. Bender, J. Katz, and R. Morselli. Ring signatures: Stronger definitions, andconstructions without random oracles. In TCC, pages 60–79, 2006.
[7] H. Comon-Lundh and V. Cortier. Computational indistinguishability and observational equivalence. INRIA Research Report RR-6508, INRIA, 2008.
[8] V. Cortier, S. Kremer, R. Küsters, and B. Warinschi. Computationally soundsymbolic secrecy in the presence of hash functions. In FSTTCS, pages 176–187,
2006.
[9] V. Cortier and B. Warinschi. Computationally sound, automated proofs for security protocols. In ESOP 2005, pages 157–171, 2005.
[10] D. Dolev and A. Yao. On the security of public key protocols. IEEE Transactions
on Information Theory, 29(2):198–207, 1983.
[11] F. D. Garcia and P. van Rossum. Sound and complete computational interpretationof symbolic hashes in the standard model. Theoretical Computer Science, 394(1–2):112–133, 2008.
[12] J. Herzog. A computational interpretation of Dolev-Yao adversaries. TheoreticalComputer Science, 340(1):57–81, 2005.
[13] Y. Kawamoto, H. Sakurada, and M. Hagiya. Computationally sound formalization of rerandomizable RCCA secure encryption. In Third Franco-JapaneseComputer Security Workshop, 2008.
[14] D. Micciancio and B. Warinschi. Soundness of formal encryption in the presenceof active adversaries. In TCC 2004, pages 133–151, 2004.
[15] R. L. Rivest, A. Shamir, and Y. Tauman. How to leak a secret. In ASIACRYPT,
pages 552–565, 2001.
[16] H. Sakurada and M. Hagiya. Computationally sound formal blind signature. In
Third Franco-Japanese Computer Security Workshop, 2008.
[17] K. Yoneyama and K. Ohta. Ring signatures: Universally composable definitions
and constructions. IPSJ Digital Courier, 3:571–584, 2007.