Computationally Sound Formalization of
Rerandomizable RCCA Secure Encryption
Yusuke Kawamoto1 Hideki Sakurada2 Masami Hagiya1
1

Department of Computer Science, Graduate School of Information Science and Technology,
University of Tokyo,
7-3-1 Hongo, Bunkyo-ku, Tokyo 113-0033, JAPAN{ y k w mt, hagiya } at is.s.u-tokyo.ac.jp
2
NTT Communication Science Laboratories, NTT Corporation
3-1, Morinosato Wakamiya, Atsugi-shi, Kanagawa 243-0198, JAPANsakurada attheory.brl.ntt.co.jp

Abstract. Rerandomizing ciphertexts plays an important role in protecting privacy in security protocols such as mixnets. We investigate the relationship between formal and computational approaches to the analysis of the security protocols using a rerandomizable encryption scheme. We introduce a new methodof dealing with composed randomnesses in an Abadi-Rogaway-style pattern, formalize a rerandomizable RCCA secure encryption scheme, and prove its computational soundness.

1

Introduction

Formal and computational approaches have developed separately in research related tothe analysis of security protocols. In the formal approach, a cryptographic message isabstracted into a symbol, called a Dolev-Yao term, and an adversary can only performseveral algebraic operations on Dolev-Yao terms [11]. The formal analysis of security
protocols is based on the assumption that cryptography is perfectly secure. On the other
hand, in the computational approach, a message is a bit string and an adversary is a
probabilistic polynomial-time (PPT) algorithm. The computational analysis of security
protocols deals with the probability of the adversary performing a successful attackfrom a complexity-theory perspective.
These two approaches have advantages and disadvantages. Although the formal approach is simpler and amenable to automation, it is based on the unrealistically strong
assumption as regards cryptography. While the analysis in the computational approach
employs more realistic models, it is very diﬃcult and prone to errors.
In recent years, many researches have related these two approaches [2,1,18]. They
define a function, called an encoding, that maps a Dolev-Yao term to a probability
distribution over bit strings, and prove the soundness theorem, which claims that theformal equivalence of Dolev-Yao terms implies the computational indistinguishabilityof the encodings of the terms. This theorem guarantees that the analysis of security
protocols in the formal approach is also valid from the viewpoint of the computational
approach.

Most of the previous studies related to soundness theorems have dealt with cryptographic primitives with relatively strong computational security, such as IND-CCA2
public key encryption [18], EUF-CMA digital signature [10], and oracle hashing [12].
Although there has been a lot of work on the formal analysis of the security protocols
with more complex primitives such as homomorphic encryption [8], their soundness
theorems have not been proved.
As a first step to obtaining soundness results for more complex message algebras,
we deal with a rerandomizable encryption scheme, which is an encryption scheme witha re-encryption operation that replaces the randomness used in a ciphertext with another without decrypting the ciphertext. Although the randomness used in a probabilistic encryption enables an adversary to observe the occurrences of the same ciphertext,
rerandomizing ciphertexts prevents the adversary from tracing them. For this reason, there-encryption operation plays an important role in protecting privacy in some security
protocols such as mixnet [13].
We propose a new formalization of a rerandomizable encryption scheme using
Abadi-Rogaway-style formal patterns [2,15], and prove its computational soundness
by using the IND-RCCA security [6] of the rerandomizable encryption scheme and therandomness-preserving property of the randomness composition.
In the formalization, we introduce a new method of dealing with composed randomnesses, because the re-encryption operation follows the composition of the randomnesses used in probabilistic encryptions/re-encryptions. Although some studies explicitly represent the randomnesses of probabilistic encryptions in an Abadi-Rogawaystyle pattern [12,7,9], they do not deal with the composition of randomnesses. We extend Herzog’s formalization [15] to explicitly represent composed randomnesses by amultiset of randomness symbols in an Abadi-Rogaway-style pattern. Due to this, patterns are expressive enough to describe the indistinguishability of a ciphertext from its
rerandomization. In addition, we provide a new definition of a renaming of a multiset of randomness symbols that enables us to deal with composed randomnesses. To
obtain the soundness result, we deal only with acyclic terms satisfying the freshness
assumption, which restricts the usage of honest participants’ randomnesses.
In the soundness theorem, we claim that if patterns cannot be distinguished by the
Dolev-Yao adversary, then their computational encodings cannot be distinguished by
any PPT adversary with access to a decryption oracle. Here, the decryption oracle represents a certain aspect of an active and adaptive adversary. Since the computational indistinguishability introduced in this paper is an extension of Herzog’s Abadi-Rogaway
public-key indistinguishability [15] to IND-RCCA security, the PPT adversary in ourmodel is not fully active or adaptive. For example, the adversary’s nonces and randomnesses are fixed in advance and not adaptive.
The organization of this paper is as follows. Section 2 defines the formal model
employed to analyze the security protocols using rerandomizable encryption schemes.
Section 3 introduces a computational rerandomizable encryption scheme, and its computational security definitions. Section 4 defines an encoding that maps patterns to distributions over bit strings. Section 5 introduces Abadi-Rogaway RCCA indistinguishability, and proves the soundness theorem. The final section summarizes our work anddiscusses areas for future research.

2Formal Model

This section introduces the message algebra used to formalize and analyze the protocols
that employs rerandomizable encryption schemes.
2.1 Dolev-Yao Model
Our formal model is an extension of the Dolev-Yao model presented in [15]. A message
is abstracted into a term from an appropriate algebra, called a Dolev-Yao term [11],and parties are restricted to performing only pairing, encryption, decryption, and reencryption operations. There are two kinds of parties: honest participants and an active
and adaptive adversary. The honest participants follow a protocol without deviation,and can run multiple sessions of the protocol simultaneously.
The communications between parties are under the control of the adversary. In thesame way as in [15], we model the adversary as the communication channel, and assume
that the adversary can record, delete, replay, and reorder messages. Each execution of a
protocol is defined as an alternating finite sequence of the adversary’s messages qi andhonest participants’ messages ri : r0 , q1 , r1 , q2 , · · · , rn−1 , qn , rn . We assume that theadversary receives the initial knowledge r0 before executing the protocol, and that eachadversary’s message qi must be derivable from r0 , r1 , · · · , ri−1 , nonces, and randomnesses. Although the analysis of a security protocol in this model must take account of
all non-deterministic choices of the adversary’s messages, we do not present an analysis
method in the model.
This Dolev-Yao model is explained in detail in [15], and here we concentrate on
providing a formalization of a rerandomizable encryption scheme.
2.2 Terms
We define the following sets of atomic symbols, which are mutually exclusive:– a set Const of constants, denoting plaintexts of messages for example,– a set Kpub of public key symbols,– a set Ksec of secret key symbols,– a set Nonce of nonce symbols, and– a set Rand of randomness symbols, denoting the randomnesses used in encryption.
We denote the secret key corresponding to a public key k pub by k pub , and the publickey corresponding to a secret key k sec by k sec . Let Kadv ⊆ Ksec be a finite set of the secretkeys of subverted participants.
Let Nonceuni be a set of the nonce symbols of honest participants, Nonceadv be a setof the nonce symbols of the adversary, and Nonce = Nonceuni ∪ Nonceadv .
Let Randuni be a set of the randomness symbols denoting uniform randomnesses
used only in honest participants’ probabilistic encryptions, Randadv be a set of therandomness symbols used in the adversary’s probabilistic encryptions, and Rand =Randuni ∪ Randadv . For a set X, let FMulti(X) be the set of all the non-empty finite
multisets of X’s elements. Let X1 ⊎ X2 be the disjoint union of two multisets X1 and X2 .

Using these atomic symbols, a term is constructed from a pairing ⟨ , ⟩, encryption{| |} , and re-encryption (| |) operations as follows:
Term ∋ m ::= c | k pub | k sec | n | R | ⟨m, m⟩ | {| m |}Rkpub | (| m |)Rkpub ,where c ∈ Const, k pub ∈ Kpub , k sec ∈ Ksec , n ∈ Nonce, and a non-empty finite multiset
R ∈ FMulti(Rand). Here the multiset R denotes the randomness composed of all the
randomnesses in R. We assume that the value of the composition of the randomnesses
in R is uniquely determined.
A term of the form ⟨m1 , m2 ⟩ denotes the pair of two messages m1 and m2 . A termof the form {| m |}Rkpub denotes the encryption of a message m by a public key k pub and a′composed randomness R. For example, {| m |}kR⊎R
denotes the encryption of a message
pub
m by a public key k pub and the randomness composed of R and R′ . A term of the form(| m |)Rkpub denotes the re-encryption of a ciphertext m by a public key k pub and a composed

randomness R. We sometimes abbreviate {| m |}{k rpub} and (| m |)k{ rpub} as {| m |}rk pub and (| m |)rk pub ,respectively. We can derive a term m from {| m |}Rkpub by decrypting {| m |}Rkpub using thecorresponding secret key k pub .

2.3 Patterns
This section defines a pattern pattern(m, T ) for a term m and a set T ⊆ K sec . The
intuitive meaning of a pattern pattern(m, T ) is the bit string distribution associated withm from the viewpoint of the formal adversary with access to the secret keys T .
First, we introduce the type trees of terms [17,15]. We abuse the notation anduse a type symbol as an atomic symbol of the same type. The type tree type(m) of
a term m is defined as follows: type(c) = Const if c ∈ Const, type(k pub ) = Kpub
if k pub ∈ Kpub , type(k sec ) = Ksec if k sec ∈ Ksec , type(n) = Nonce if n ∈ Nonce,type(R) = FMulti(Rand) if R ∈ FMulti(Rand), type(⟨ m1 , m2 ⟩) = ⟨ type(m1 ), type(m2 ) ⟩,type({| m |}Rkpub ) = {| type(m) |}KFMulti(Rand), and type((| m |)Rkpub ) = (| type(m) |)FMulti(Rand). For exKpub
pub
ample, type(⟨ c, {| n |}Rkpub ⟩) = ⟨ Const, {| Nonce |}FMulti(Rand)⟩ holds.
K pub
Next, we define the undecryptable ciphertext symbol {| type(m) |}k pub for each ciphertext {| m |}Rkpub to introduce the pattern representing the distribution of the ciphertext thatR

the adversary cannot decrypt. Intuitively, {| type(m) |}k pub denotes a random message fromwhich the adversary cannot distinguish the ciphertext {| m |}Rkpub when R ∩ Randuni , ∅Rholds. The notation {| type(m) |}k pub implies that the encryption {| m |}Rkpub reveals the publicR

key k pub and the length of the plaintext m. The set R of randomness symbols in {| type(m) |}k pub
is used to analyze the relations between probability distributions.
Finally, we define the pattern associated with a term.
R

Definition 1. A set Pattern of patterns is defined by:
Pattern ∋ m ::= c | k pub | k sec | n | R | ⟨m, m⟩ | {| m |}Rkpub | (| m |)Rkpub | {| type(m) |}Rk

pub,

where c ∈ Const, k pub ∈ Kpub , k sec ∈ Ksec , n ∈ Nonce, and a non-empty finite multiset
R ∈ FMulti(Rand).

Definition 2. For k pub ∈ K pub , let Reenckpub be the minimum set of terms recursively
defined by:– {| m |}Rkpub ∈ Reenckpub holds for any m ∈ Term and any R ∈ FMulti(Rand).
– If mre ∈ Reenck pub holds, then (| mre |)Rkpub ∈ Reenck pub holds for any R ∈ FMulti(Rand).
Note that each m ∈ Reenck pub is generated by repeated encryption/re-encryption operations using the same public key k pub .
Definition 3. For a set T ⊆ K sec , let T be the set { k sec | k sec ∈ T }. For m ∈ Term andT ⊆ K sec , we define the sets F(m, T ) and Gi (m, T ) of all the secret keys that the formal
adversary can learn from m using the secret keys in T and Gi−1 (m, T ), respectively.
– F(m, T ) = T (if m ∈ Const ∪ K pub ∪ Nonce ∪ FMulti(Rand))– F(k sec , T ) = { k sec } ∪ T– F(⟨m1 , m2 ⟩, T ) =( F(m1 , T ) ∪ F(m2 , T )F(m, T ) (if k pub ∈ T or R ∈ FMulti(Randadv ))– F({| m |}Rkpub , T ) =T(otherwise)′ R⊎R′,T ) (if R ∈ FMulti(Rand) \ FMulti(Randadv ),
F({|
m
|
}

k pub


′



and m = {| m′ |}Rk pub holds for m′ ∈ Term






and R′ ∈ FMulti(Rand))



R
R⊎R′
′
– F((| m |)k pub , T ) = 
F((| m |)k pub , T ) (if R ∈ FMulti(Rand) \ FMulti(Randadv ),


′



and m = (| m′ |)Rk pub holds for m′ ∈ Reenckpub






and R′ ∈ FMulti(Rand)) F(m, T )(otherwise)– G0 (m, T ) = T– Gi (m, T ) = F(m, Gi−1 (m, T ))We define the function recoverable : Term × P(K sec ) → P(K sec ) that maps a term m anda set T ⊆ K sec to the set of all the secret key symbols recoverable from m by using T .
– recoverable(m, T ) = G|m| (m, T )We define the function pat : Term × P(K sec ) → Pattern that maps a term t and a set
T ⊆ K sec to t’s pattern with respect to T .
– pat(m, T ) = m (if m ∈ Const ∪ K pub ∪ K sec ∪ Nonce ∪ FMulti(Rand))– pat(⟨m1 , m2 ⟩, T ) =⟨pat(m1 , T ), pat(m2 , T )⟩R
(if k pub ∈ T or R ∈ FMulti(Randadv )) {| pat(m, T ) |}k pub– pat({| m |}Rkpub , T ) = R{|
type(m)
|
}

k pub

(otherwise)′ R⊎R′
pat({|
m
|
}
,
T
)
(if
R ∈ FMulti(Rand) \ FMulti(Randadv ),

k pub


′



and m = {| m′ |}Rk pub holds for m′ ∈ Term





and R′ ∈ FMulti(Rand))




R
′ R⊎R′
pat((| m |)k pub , T ) (if R ∈ FMulti(Rand) \ FMulti(Randadv ),– pat((| m |)k pub , T ) = 


′



and m = (| m′ |)Rk pub holds for m′ ∈ Reenckpub






and R′ ∈ FMulti(Rand)) (| pat(m, T ) |)R(otherwise)k pub

Let pattern : Term × P(K sec ) → Pattern be the function defined by:pattern(m, T ) = pat(m, recoverable(m, T )).

In the above definition, pattern(m, T ) represents the information that the formal
adversary can obtain from the message m using the decryption keys in T . We assume
that the formal adversary can see any messages encrypted using a non-uniform randomness. We also assume that he can see the message c in a re-encryption (| c |)Rkpub if
c is not a valid encryption using k pub . In addition, the above definition reflects that the′re-encryption of a ciphertext {| m |}Rk pub by the same public key k pub and a randomness R′
produces the ciphertext {| m |}kR⊎R
using the randomness composed of R and R′ .
pub
2.4 Acyclicity and Freshness Assumption
First, we introduce a subterm relation. Given a term m, the set SubTerm of all thesubterms of m is recursively defined as follows: SubTerm(m) = {m} if m ∈ Const ∪Kpub ∪ Ksec ∪ Nonce ∪ Rand, SubTerm(m) = {m} ∪ SubTerm(m1 ) ∪ SubTerm(m2 ) if
m = ⟨m1 , m2 ⟩, and SubTerm(m) = {m} ∪ SubTerm(m′ ) if m = {| m′ |}Rkpub or m = (| m′ |)Rkpub .
For two term m and m′ , we write m′ ⊑ m if m′ ∈ SubTerm(m).
Next, we define the acyclicity of terms in a similar way to that in [2,12].
Definition 4. A secret key symbol k encrypts a secret key symbol k′ in a term m if{| m′ |}Rk ⊑ m and k′ ⊑ m′ hold for some R ∈ FMulti(Rand). A term is acyclic if there isno sequence k1 , k2 , · · · , kn , kn+1 = k1 of secret key symbols such that ki encrypts ki+1
in m for each 1 ≤ i ≤ n.
The acyclicity of terms is necessary for us to obtain the soundness theorem.
Then, we define the independence of a uniform randomness symbol.
Definition 5. A uniform randomness symbol r ∈ Randuni is independent in a set S ofterms if there exist a unique multiset R ∈ FMulti(Rand) such that– r ∈ R holds,– R occurs in some m ∈ S , and– r < R′ holds for every R′ ∈ FMulti(Rand) occurring in some m′ ∈ S with R′ , R.
r ∈ Randuni is independent in a term m if it is independent in { m }.
Intuitively, if an independent randomness r ∈ Randuni is used in an honest participant’s probabilistic encryption/re-encryption, then it is not used in another encryption/rre-encryption. For example, let S be the set { {| c1 |}rk1 , {| c1 |}k{ r1 , r2 } , {| c2 |}rk3 , (| {| c2 |}rk3 |)k4 } for
r1 , r2 , r3 , r4 ∈ Randuni . While r2 , r3 , and r4 are independent in S , r1 is not independent.
Finally, we introduce the following freshness assumption.
Definition 6. A multiset R ∈ FMulti(Rand) encrypts a term m′ in a term m if {| m′ |}Rkpub ⊑m holds for some public key symbol k pub . A multiset R ∈ FMulti(Rand) re-encrypts
a term m′ in a term m if (| m′ |)Rkpub ⊑ m holds for some public key symbol k pub . A
term m satisfies the freshness assumption if it holds that for each R ∈ FMulti(Rand) \FMulti(Randadv ) occurring in m, there exist– a unique term m′ such that every occurrence of R encrypts/re-encrypts m′ in m, and– a uniform randomness symbol r ∈ R ∩ Randuni independent in m.
Intuitively, the former condition represents the fact that

– no honest participant uses the same composed randomness R to encrypt/re-encrypt
another message, and that– no honest participant uses the randomnesses in Randuni except when employing
them as the randomnesses in probabilistic encryptions/re-encryptions, that is, no
uniform randomness symbols in Randuni are used as plaintexts or keys in m.
The latter condition represents the fact that– every randomness R used in an honest participant’s encryption/re-encryption iscomposed of at least one independent and uniform randomness r which he neveruses in another encryption/re-encryption.
For example, for c1 , c2 ∈ Const, k ∈ K pub , r1 , r2 ∈ Randuni and radv ∈ Randadv ,the following four terms do not satisfy the freshness assumption: ⟨{| c1 |}k{ r1 } , {| c2 |}{k r1 } ⟩,{| r1 |}{k r2 } , ⟨{| c1 |}{k r1 } , {| c1 |}{k r1 , r2 } ⟩, and ⟨{| c1 |}{k r1 } , {| c1 |}{k r1 , radv } ⟩. If two multisets R, R′ ∈FMulti(Rand) with R ( R′ occur in a term m, then m does not satisfy the freshness
assumption. Note that the freshness assumption allows honest participants to copy any
ciphertexts.
Hereafter, we deal only with acyclic terms that satisfy the freshness assumption.
2.5 Observational EquivalenceThis section defines the renaming of patterns and the observational equivalence ofterms.
First, we introduce several notations and the renaming for atomic symbols.
Definition 7. Given T ⊆ K sec , let AtomT = (Kpub \ T ) ∪ (Ksec \ T ) ∪ Nonceuni ∪(FMulti(Rand) \ FMulti(Randadv )). Given P ∈ Pattern, let AtomT (P) be the following set:
{ P′ ∈ AtomT | P′ occurs in P }.
Definition 8. Given P ∈ Pattern and T ⊆ K sec , a function σ is a renaming for theatomic symbols in P except for T if it is a type-preserving injection from AtomT (P) to
AtomT such that σ(k) = k′ if and only if σ(k) = k′ for any k, k′ ∈ K pub \ T .
Next, we define the renaming of a pattern.
Definition 9. Given a pattern P ∈ Pattern and a renaming σ for the atomic symbols in
P except for T ⊆ K sec , we write σ̃ P to represent the pattern obtained by replacing eachoccurrence of Q ∈ AtomT (P) in P with σ(Q).
Finally, we define the observational equivalence of terms.
Definition 10. Two terms m and m′ are observationally equivalent, written as m  m′ ,if there exists a renaming σ for the atomic symbols in pattern(m′ , Kadv ) except for Kadv
such that pattern(m, Kadv ) = σ̃ pattern(m′ , Kadv ).
Example 1. Let k, k1 , k2 ∈ Kpub \ Kadv and r1 , r2 ∈ Randuni .
– {| m |}{k r1 }  {| m |}{k r1 , r2 }  (| {| m |}rk1 |)rk2
This represents the fact that the re-encryption operation using the same public key
k and a uniform randomness r2 does not change the probability distribution. Notethat we can prove this by employing a renaming σ satisfying σ({ r1 , r2 }) = { r1 }.

– {| m |}rk1  {| m |}rk2 but ⟨{| m |}rk1 , {| m |}rk1 ⟩  ⟨{| m |}rk1 , {| m |}rk2 ⟩This represents the fact that the formal adversary can recognize the repetition of thesame ciphertext bit strings. Note that no renaming σ satisfies both σ({ r1 }) = { r1 }and σ({ r2 }) = { r1 }. In general, our observational equivalence of patterns can deal
with the relations of probability distributions unlike [2], because of our definitionof the renaming.
r– {| m |}rk1  {| m |}{k radv , r1 }  (| {| m |}rkadv |)k1 (radv ∈ Randadv )This represents the fact that the re-encryption of the adversary’s ciphertext {| m |}rkadv
using a uniform randomness r1 produces a uniformly random ciphertext. Note that
there exists a renaming σ satisfying σ({ radv , r1 }) = { r1 }.
– ⟨{| m |}rk1 , {| m |}rk2 ⟩  ⟨{| m |}rk1 , (| {| m |}rk1 |)rkadv ⟩ (radv ∈ Randadv )This represents the fact that the adversary can recognize the re-encryption using theadversary’s randomness radv because he has performed the re-encryption. Note thatr1
r2
we have pattern(⟨{| m |}rk1 , {| m |}rk2 ⟩, ∅) = ⟨{| type(m) |}k , {| type(m) |}k ⟩ but pattern(⟨{| m |}rk1 ,r1
r1 radv(| {| m |}rk1 |)rkadv ⟩, ∅) = ⟨{| type(m) |}k , (| {| type(m) |}k |)k ⟩.
– ⟨{| m |}rk11 , {| m |}rk21 ⟩  ⟨{| m |}rk11 , {| m |}rk22 ⟩This represents the fact that the formal rerandomizable encryption schemes in thispaper do not satisfy receiver anonymity [19], i.e., the key-privacy [4] or which-key
concealing [2] of rerandomizable encryption schemes.

3

Computational Model

This section introduces the notion of computational indistinguishability, a computational rerandomizable encryption scheme, and its security definitions.
3.1 Preliminaries
In a computational setting, messages are bit strings and adversaries are probabilistic
polynomial-time (PPT) algorithms that input and output bit strings. We denote the setof all bit strings by String, and the length of a bit string x by |x|. The computational
security of cryptographic schemes is defined in terms of the notion of a probability
ensemble over bit strings, which is a sequence {Dη }η of probability distributions Dηover bit strings indexed by a security parameter η.
We use the following indistinguishability of probability ensembles as a security
definition in the computational setting. We write d ← Dη to indicate that d is sampledfrom a probability distribution Dη , and write Pr[d ← Dη : E] for the probability of anevent E when d is sampled from Dη . We abuse the notation and write d ← X to indicatethat d is sampled from the uniform distribution on a set X. A function f from integers
to real numbers is negligible in a security parameter η if for every c > 0 there exists an
integer ηc such that f (η) ≤ η−c holds for any η ≥ ηc .
Definition 11. Two probability ensembles {Dη }η and {D′ η }η are computationally indistinguishable with respect to an oracle O, written Dη ≈O D′ η if for every PPT adversary A,
Pr[d ← Dη : AO(·) (d, η) = 1] − Pr[d′ ← D′ η : AO(·) (d′ , η) = 1]
is negligible in η.

In the above definition, we assume that the PPT adversary A can send a polynomial
number of queries to the oracle O.
3.2 Rerandomizable Encryption Scheme
We consider a rerandomizable encryption scheme where everyone can re-encrypt a ciphertext using a public key and a randomness. It is left to our future work to deal withmore complex rerandomizable encryption schemes using re-encryption keys generated
from secret keys, such as the proxy re-encryption scheme proposed in [5].
Let Param be a set of security parameters, PubKey be a set of computational public keys, SecKey be a set of computational secret keys, Plaintext be a set of computational plaintexts, and Random be a set of random bit strings used in encryptions andre-encryptions. Let ⊥ be the special bit string representing the failures of encryptions,decryptions, and re-encryptions. We denote the secret key corresponding to a public key
pk by pk, and the public key corresponding to a secret key sk by sk.
Definition 12. A computational rerandomizable encryption scheme is a quintuple (G,E, D, R, CMP) consisting of the following five algorithms:– a key generation algorithm G : Param × Random → PubKey × SecKey that outputs,
given a security parameter η and a randomness r, a public key and secret key pair
(pk, sk).
– an encryption algorithm E : PubKey×String×Random → Cipher∪{⊥} that outputs,
given a public key pk, a bit string x, and a randomness r, the encryption of x using
pk and r, or the failure message ⊥.
– a decryption algorithm D : SecKey × String → Plaintext ∪ {⊥} that outputs, given
a secret key sk and a bit string x, the decryption of x using sk, or the failure message ⊥.
– a re-encryption algorithm R : PubKey × String × Random → Cipher ∪ {⊥} that
outputs, given a public key pk, a bit string x, and a randomness r, the re-encryptionof x using r, or the failure message ⊥.
– a randomness-composition algorithm CMP : FMulti(Random) → Random that
outputs the composition of a given finite multiset of randomnesses. We assume
that the bit string representing the composition of a multiset of randomnesses is
uniquely determined if the multiset is fixed.
We assume that the lengths of the outputs from these algorithms depend only on thoseof the inputs. These algorithms satisfy the following properties for any pk ∈ PubKey,
sk = pk, any r, r′ ∈ Random, any R1 , R2 , R3 ∈ FMulti(Random), and any x ∈ String.
(x (if x ∈ Plaintext)– D(sk, E(pk, x, r)) =⊥ (otherwise)– R(pk, E(pk, x, r), r′ ) = E(pk, x, CMP({ r, r′ }))– CMP(CMP(R1 ⊎ R2 ) ⊎ R3 ) = CMP(R1 ⊎ CMP(R2 ⊎ R3 ))To obtain soundness results for the schemes such that the composition of a multiset of
randomnesses is not uniquely determined, it is suﬃcient to use sequences of randomness symbols instead of multisets of randomness symbols.

3.3 Security Definitions of Rerandomizable Encryption Schemes
We define the IND-RCCA security of the rerandomizable encryption scheme.
Definition 13. Let η be a security parameter and RE = (G, E, D, R, CMP) be a rerandomizable encryption scheme. For a PPT adversary A, we define the advantage AdvRCCA
RE, A
as follows:
RCCA
AdvRE, A (η) = Pr [ (pk, sk) ← G(η);(m0 , m1 ) ← AD1 (·) (pk);(m0 , m1 and |m0 | = |m1 |)wherer ← Random;b ← { 0, 1 };c := E(pk, mb , r);b′ ← AD2 (·) (c) :b′ = b] − 12 ,(D(sk, x) (D(sk, x) , m0 , m1 )D1 (x) = D(sk, x) and D2 (x) =test(otherwise)

A rerandomizable encryption scheme RE is IND-RCCA secure if the advantage AdvRCCA
RE, A
is negligible in η for every PPT adversary A.
The notion “RCCA”, or Replayable CCA, was proposed by Canetti et al. [6] as arelaxation of CCA2 security. Although this security is strictly weaker than CCA2, it isbelieved to be a necessary and suﬃcient formalization of “secure encryption” from theapplicational point of view [3]. Groth [14] first proposed a rerandomizable encryption
scheme satisfying a weaker form of RCCA security, and another scheme satisfying
RCCA security in the generic groups model. Prabhakaran and Rosulek [19] improved
this rerandomizable scheme to achieve RCCA security in a standard model, and Xue
and Feng [21] proposed a more eﬃcient scheme that also achieves receiver anonymity.
There are notions similar to IND-RCCA: “benign malleability” [20], “loose ciphertextunforgeability” [16], and “generalized CCA security” [3].
Finally, we define the notion of randomness-preserving composition, because INDRCCA security cannot describe the security property whereby the re-encryption algorithm R fully rerandomizes input ciphertexts.
Definition 14. Let η be a security parameter and RE = (G, E, D, R, CMP) be arerandomizable encryption scheme. The randomness composition algorithm CMP is
randomness-preserving if it holds for every r, r0 , r1 ∈ Random that1.
2.

Pr[x0 ← Random : CMP({ x0 , r }) = r1 ] = Pr[x0 ← Random : x0 = r1 ]Pr[x0 ← Random : x0 = r0 ∧ CMP({ x0 , r }) = r1 ]= Pr[x0 ← Random : x0 = r0 ] · Pr[x0 ← Random : CMP({ x0 , r }) = r1 ].

By Lemma 1 of [21], if CMP is randomness-preserving, then RE is perfectly rerandomizable [19], which is a security notion of the re-encryption operation R.

4

Encoding

This section introduces an encoding that maps patterns to distributions over bit strings.
The definition of the encoding is standard [2,12], but we take the composed randomness
into account.
First, we define the set of the symbols that should be encoded using random bit
strings.
Definition 15. For a term/pattern m, let RS (m) be the set of atomic symbols:
RS (m) = { m′ ∈ K pub ∪ Nonce | m′ occurs in m } ∪ { k sec | k sec ∈ K sec , k sec occurs in m }∪ { r ∈ R | R ∈ FMulti(Rand), R occurs in m }.
S
For a set S of terms/patterns, let RS (S ) be the set m∈S RS (m).
Next, we define the set Coinsℓ of functions each of which encodes the randomness
used to encode key/nonce/random symbols.
Definition 16. For a set X of atomic symbols, let Coinsℓ (X) be the set: { t : X → { 0, 1 }ℓ }.
Each function t ∈ Coinsℓ (RS (m)) maps each key/nonce/randomness symbol x in m to arandom bit string used to encode x. For example, for a public key symbol k pub occurringin m, t(k pub ) is the random bit string that is used to generate the public key bit string
denoted by k pub . Hereafter we sometimes omit the length ℓ from the notation when ℓ isa polynomial in the security parameter η such that t ∈ Coinsℓ (X) is suﬃcient to encode
all the key/nonce/randomness symbols in X.
Then, we define the algorithms used in the encoding of terms/patterns. Let RE =(G, E, D, R, CMP) be a rerandomizable encryption scheme. We use G to encode public and secret key symbols, E to encode encryptions, R to encode re-encryptions, and
CMP to encode a set of randomness symbols. We also use the following algorithms.
Definition 17. – A constant encoder C is a deterministic algorithm that outputs afixed bit string corresponding to a given constant c in Const.
– A nonce encoder N is an algorithm that outputs, given a randomness t(n) for somen ∈ Nonce, a bit string uniformly and randomly selected from { 0, 1 } poly(η) , wherepoly(η) is a fixed polynomial in η.
– A type encoder T is an algorithm that outputs a fixed bit string of the same length
as the encoding of the term m for an input type(m), such as an all-zero string of thesame length.
– A nonce distribution Dnonce is an algorithm that outputs, given a random bit string,a bit string used as the adversary’s nonce.
– A randomness distribution Drand is an algorithm that outputs, given a random bit
string, a bit string used as the adversary’s randomness for probabilistic encryptions
and re-encryptions.
We assume that each of these algorithms outputs bit strings of the same length for inputsof the same length. Let I = ⟨RE, C, N, T , Dnonce , Drand ⟩.
Finally, we define the encoding of terms/patterns. We abuse the notations and use⟨ ·, · ⟩ to represent the concatenation of bit strings. Let fst and snd be the two algorithms
that map a concatenation of bit strings to the first and second component, respectively.

Definition 18. Let e be a function from some set dom(e) of terms/patterns to bit strings,
η be a security parameter, and t ∈ Coins(RS (m) \ dom(e)). The encoding [[ m ]]e,η, tI of aterm/pattern m is recursively defined as follows:
if m ∈ Dom(e),then[[ m ]]e,η, tI = e(m)else[[ c ]]e,η, tI = ⟨C(c), “Const”⟩[[ k pub ]]e,η, tI = ⟨fst(G(η, t(k pub ))), “PubKey”⟩[[ k sec ]]e,η, tI = ⟨snd(G(η, t(k sec ))), “SecKey”⟩(⟨Dnonce (N(η, t(n))), “Nonce”⟩ (if n ∈ Nonceadv )e, t[[ n ]]η, I =⟨N(η, t(n)), “Nonce”⟩(otherwise)(⟨Drand (t(r)), “Rand”⟩ (if r ∈ Randadv )[[ { r } ]]e,η, tI =⟨t(r), “Rand”⟩(otherwise)[[ R ]]e,η, tI = ⟨CMP({ fst([[ { r } ]]e,η, tI ) | r ∈ R }), “Rand”⟩[[ ⟨m1 , m2 ⟩ ]]e,η, tI = ⟨⟨[[ m1 ]]e,η, tI , [[ m2 ]]e,η, tI ⟩, “pair”⟩[[ {| m |}Rk ]]e,η, tI = ⟨E(fst([[ k ]]e,η, tI ), [[ m ]]e,η, tI , fst([[ R ]]e,η, tI )), fst([[ k ]]e,η, tI ), “enc”⟩[[ (| m |)Rk ]]e,η, tI = ⟨R(fst([[ k ]]e,η, tI ), fst([[ m ]]e,η, tI ), fst([[ R ]]e,η, tI )), fst([[ k ]]e,η, tI ), “enc”⟩[[ {| type(m) |}k ]]e,η, tI = ⟨E(fst([[ k ]]e,η, tI ), T (type(m)), fst([[ R ]]e,η, tI )), fst([[ k ]]e,η, tI ), “enc”⟩
R

where c ∈ Const, k pub ∈ Kpub , k sec ∈ Ksec , n ∈ Nonce, and r ∈ Rand, R ∈ FMulti(Rand).
For any pattern m and any security parameter η, the encoding [[ m ]]eη, I is the probability
distribution { t ← Coins(RS (m) \ dom(e)) : [[ m ]]e,η, tI }. We omit e when dom(e) = ∅.
When Dom(e) = { x1 , x2 , · · · , xn } and yi = e(xi ) for each 1 ≤ i ≤ n, we sometimes
write [x1 7→ y1 , x2 7→ y2 , · · · , xn 7→ yn ] instead of e. Hereafter we omit I from thenotations, and abbreviate [[ { r } ]]e,η, tI as [[ r ]]e,η t .
In the above definition, each encoding is followed by a type tag representing one of the
bit string types “Const”, “PubKey”, “SecKey”, “Nonce”, or “Random” and the bit string
operation types “pair” and “enc”. The algorithm fst is used to remove type tags, and weomit fst for readability hereafter. A ciphertext bit string contains the public key used togenerate the ciphertext. We introduce the algorithm PK that outputs the public key pk
from a given encryption using pk. PK satisfies the equation: PK(⟨E([[ k ]]e,η t , [[ m ]]e,η t ,[[ R ]]e,η t ), [[ k ]]e,η t , “enc”⟩) = [[ k ]]e,η t .
Note that [[ m ]]e,η t is a unique bit string, because t ∈ Coins(RS (m) \ dom(e)) determines all the randomnesses in m.

5

Soundness

5.1 Abadi-Rogaway Indistinguishability
First, we define a function undecτ that maps a bit string to a set of undecryptable bit
strings. Intuitively, given an encoding µ of a term M and a set τ of encodings of a set

T ⊆ K sec , x ∈ undecτ (µ) is an encoding of an undecryptable message in pattern(M, T ).
Definition 19. Let µ be a bit string, and τ be a set of computational secret keys. Let
undecτ be the algorithm defined in Fig. 1.
algorithm undecτ (µ)
Set B, B′ :={ µ };do
B := B′ ;B′ := ∅;
for each b ∈ B
if b = ⟨b1 , b2 , “pair”⟩
then B′ := B′ ∪ { b1 , b2 };if b = ⟨c, PK(c), “enc”⟩ and ⟨PK(c), “PubKey”⟩ ∈ τthen B′ := B′ ∪ { D(PK(c), c) };if b = ⟨c, PK(c), “enc”⟩ and ⟨PK(c), “SecKey”⟩ ∈ τthen B′ := B′ ∪ { D(PK(c), c) };otherwiseB′ := B′ ∪ { b };while B′ , B;
return B′ ;Fig. 1. Algorithm undecτ .
Roughly speaking, undecτ (µ) is the set of all the challenge ciphertexts, and is used to
specify the ciphertexts that cannot be decrypted by the decryption oracle in Definition 21.
Next, we define the set forbidη, t (M, T ) of bit strings that is used in the oracle ofDefinition 21.
Definition 20. Let M ∈ Term and T ⊆ K sec . Let forbidη, t (M, T ) be the set:()
y ∈ undec[[ T ]]tη ([[ M ]]tη ),,⟨pk, D(pk, y)⟩, ⟨pk, Type(D(pk, y))⟩pk = PK(y)where Type is the algorithm defined by Type([[ m ]]tη ) = T (type(m)) for every m ∈ Term.
Finally, we define a computational indistinguishability between the two probability
distributions each encoding a term. This indistinguishability is defined in the presenceof an active and adaptive PPT adversaryA, and is almost the same as that in [15] except′
for the definition of the oracle Oη,M,t M , T .
Definition 21. Let η be any security parameter, T be any finite set of secret key symbols, and M and M ′ be any two acyclic terms satisfying the freshness assumption andM  M ′ . A rerandomizable encryption scheme RE provides Abadi-Rogaway RCCA
indistinguishability if for every PPT adversary A, it holds that[[ M ]]η ≈OM, M′ , T [[ M ′ ]]η ,η, tthat is, the advantage AdvAR−RCCA
defined below is negligible in η.
RE, A
M, M ′ , T

AdvAR−RCCA(η) = Pr[t ← Coins(M), d ← [[ M ]]tη : AOη, t
RE, A
′

′

(·, ·)(d, η) = 1]

M, M ′ , TOη,(·, ·)t− Pr[t ← Coins(M ), d ← [[ M(d, η) = 1]

D(pk, x) (if either





(i) pk ∈ [[ K ]]tη for some K ∈ T , or






(ii) (a) pk ∈ [[ K ]]tη for some K ∈ Kpub \ T ,





′

(b) ⟨pk, D(pk, x)⟩ < forbid η,t (M, T ),,T
Oη,M,M(pk, x) = 
t


and






(c) ⟨pk, D(pk, x)⟩ < forbid η,t (M ′ , T ))





⊥
(if
pk
< [[ K ]]tη for any K ∈ Kpub )




test
(otherwise)]]tη : A

In this definition, the adversary A can learn some relations
between plaintexts and′their encryptions by having access to the oracle Oη,M,t M , T . As opposed to the access to
D1 andD2 in Definition 13, the adversary A needs to send a public key pk to the oracle′
Oη,M,t M , T to specify the corresponding secret key pk used for the decryption, because
two messages M, M ′ , and their patterns can be thought of as many possible diﬀerent
challenge ciphertexts′ under many possible diﬀerent keys.
The oracle Oη,M,t M , T is similar to that in [15] except that the two sets forbidη, t (M, T )′and forbidη, t (M ′ , T ) are used to determine whether or not Oη,M,t M , T returns the decryp′tion of x to the adversary A. The challenge ciphertexts that the oracle Oη,M,t M , T should notdecrypt are those encryptions that the decryption oracle D2 is not allowed to decrypt in
the IND-RCCA game. They are either undecryptable ciphertexts E(pk, m, r) derivablefrom [[ M ]]tη or [[ M ′ ]]tη , or the corresponding encryptions E(pk, Type(m), r). Therefore,
forbidη, t (M, T ) ∪ forbidη, t (M ′ , T ) specifies the set of all the challenge ciphertexts that′
Oη,M,t M , T should not decrypt.
5.2 Soundness of Formal Rerandomizable Encryption
We obtain the following soundness theorem.
Theorem 1. Let RE be an IND-RCCA secure rerandomizable encryption scheme witha randomness-preserving composition CMP. For any two acyclic terms M and M ′satisfying the freshness assumption, M  M ′ implies [[ M ]]η ≈OM, M′ , Kadv [[ M ′ ]]η .
η, tProof. By Lemmas 1 and 2 presented below, we have the following equation for somerenaming σ for the atomic symbols in pattern(M ′ , Kadv ) except for Kadv .
[[ M ]]η ≈ OM, M′ , Kadv [[ pattern(M, Kadv ) ]]η = [[ σ̃ pattern(M ′ , Kadv ) ]]η
η, t= [[ pattern(M ′ , Kadv ) ]]η ≈ OM, M′ , Kadv [[ M ′ ]]η .
η, t

′



Lemma 1. Let M and M be any two acyclic terms satisfying the freshness assumption,
and T be any finite set of secret key symbols. Let RE = (G, E, D, R, CMP) be an
IND-RCCA secure rerandomizable encryption scheme where CMP is randomnesspreserving. Then we have [[ M ]]η ≈OM, M′ , T [[ pattern(M, T ) ]]η .
η, t

′

Proof. Suppose that there exists a PPT adversary A with access to Oη,M,t M , T who candistinguish between samples from [[ M ]]η and [[ pattern(M, T ) ]]η . Then we derive acontradiction by using a hybrid argument similar to [2,15]. Between the two rows M
and pattern(M, T ), we create a new row for each encryption/re-encryption, so that twoconsecutive rows diﬀer only in one of the following cases:′′

R(1) a single re-encryption (| (| P |)RK |)K being replaced with (| P |)R⊎R
for P ∈ ReencK ,KR ∈ FMulti(Rand) \ FMulti(Randadv ), and R′ ∈ FMulti(Rand),′ R′(2) a single re-encryption (| {| P |}RK |)K being replaced with {| P |}R⊎R
for R ∈ FMulti(Rand)\K
FMulti(Randadv ) and R′ ∈ FMulti(Rand),R(3) a single encryption {| P |}RK being replaced with {| type(P) |}K for R ∈ FMulti(Rand) \FMulti(Randadv ) and K ∈ K pub \ T .
Because of the definition of patterns, we obtain a sequence of rows: M = M0 , M1 , · · · ,Mi , Mi+1 , · · · , Mn = pattern(M, T ) where for each 0 ≤ i < n, Mi and Mi+1 are identical
except for one of the above cases. Unlike [2,15], it is necessary to consider cases (1)and (2) that deal with re-encryption patterns. Furthermore, in case (3) we take accountof the condition with the randomnesses of probabilistic encryptions.
Example 2. For example, let M be the following sequence of terms, and T be the following set for c ∈ Const, k1 , k2 , k3 , k4 ∈ K pub , and R1 , R2 , R3 , R4 , R5 , R6 ∈ Randuni .
R1

R4 R3

1

4

M = {| c |}Rk22 , {| {| c |}Rk22 , {| c |}Rk36 , k3 |}k , (| (| {| c |}Rk45 |)k |)T = { k1 }k4Here we have omitted parentheses for readability. We obtain the secret key symbols:
recoverable(M, T ) = { k1 , k3 }.
We obtain the sequence of rows M = M0 , M1 , M2 , M3 , M4 , M5 = pattern(M, T ).
R4 R3

R1

M0 = {| c |}Rk22 , {| {| c |}Rk22 , {| c |}Rk36 , k3 |}k , (| (| {| c |}Rk45 |)k |)1

R{| Const |}k 2

M1 = 

2

R{| Const |}k 2
2

M2 = 

R{| Const |}k 2
2

M3 = 

R{| Const |}k 2

M4 = 

2

R{| Const |}k 2

M5 = 

2,{| {| c |}Rk22 ,, {| 
, {| 

{| c |}Rk36 ,R{| Const |}k 2
2

R{| Const |}k 2
2

R, {| 

{| Const |}k 2, {| 

{| Const |}k 2

2

R

2

,

k3 |}k ,{| c |}Rk36 ,,{| c |}Rk36 ,,{| c |}Rk36 ,,R1{| c |}Rk36 ,

1

4 k4
R3
R5 R4
(| (| {| c |}k4 |)k |)4 k(3) k2

4

R1

R4 R3

k3 |}k ,(| (| {| c |}Rk45 |)k |)4 k

R1

R3 ⊎R4(| {| c |}Rk45 |)k4

1

k3 |}k ,1

4R1

k3 |}k , {| c |}Rk43 ⊎R4 ⊎R5
1

R1

R ⊎R4 ⊎R5{| Const |}k 3

k3 |}k , (3) k2(1) k4(2) k4(3) k44

1

Since A can distinguish between [[ M0 ]]η and [[ Mn ]]η , there exist two consecutive
rows Mi and Mi+1 such that A can distinguish between [[ Mi ]]η and [[ Mi+1 ]]η . Fix Mi
and Mi+1 . Then the two rows Mi and Mi+1 are the same except for one of the above
three cases (1) - (3). In each case, we derive a contradiction.

(1) Consider the first case: Mi and Mi+1 are the same except that a re-encryption′ R′(| (| P |)RK |)K in Mi is replaced with (| P |)R⊎R
in Mi+1 for P ∈ ReencK . Since P ∈ ReencKKholds, we obtain the following equation for every t ∈ Coins(RS (Mi )):R([[ K ]]tη , R([[ K ]]tη , [[ P ]]tη , [[ R′ ]]tη ), [[ R ]]tη ) = R([[ K ]]tη , [[ P ]]tη , CMP([[ R ]]tη ⊎ [[ R′ ]]tη )Therefore, we have [[ Mi ]]η = [[ Mi+1 ]]η , which contradicts the assumption that A candistinguish [[ Mi ]]η and [[ Mi+1 ]]η .
(2) Consider the second case: Mi and Mi+1 are the same except that a re-encryption′ R′(| {| P |}RK |)K in Mi is replaced with {| P |}R⊎R
in Mi+1 . We have the following equation forK
every t ∈ Coins(RS (Mi )):R([[ K ]]tη , E([[ K ]]tη , [[ P ]]tη , [[ R′ ]]tη ), [[ R ]]tη ) = E([[ K ]]tη , [[ P ]]tη , CMP([[ R ]]tη ⊎ [[ R′ ]]tη )Therefore, we obtain [[ Mi ]]η = [[ Mi+1 ]]η , which contradicts the assumption that A candistinguish [[ Mi ]]η and [[ Mi+1 ]]η .
(3) Consider the third case: Mi and Mi+1 are the same except that an encrypted message
R{| P |}RK in Mi is replaced with {| type(P) |}K in Mi+1 for R ∈ FMulti(Rand) \ FMulti(Randadv )and K ∈ K pub \ T .
Now we construct an adversary A0 that breaks the IND-RCCA security of the rerandomizable encryption scheme RE. The definition of A0 is presented in Figs. 2 and 3.
Let (pk, sk) be a pair consisting of a public key and a secret key generated using
the key generation algorithm G. Because of the freshness assumption in Definition 6,
we can take a randomness symbol r0 ∈ R ∩ Randuni such that r0 < R′ holds for everyR′ ∈ FMulti(Rand) occurring in Mi with R′ , R. Note that r0 does not occur in P.
Assume that x0 ← Random. We treat pk and x0 as the encoding of the public key
symbol K and the randomness symbol r0 , respectively.
A0D1 ( · ) (pk)t ← Coins(RS (Mi ) \ { K, r0 });→⟨pk, “PubKey′′ ⟩], t
m0 :=[[ P ]][K7;η
m1 := T (type(P));
return (m0 , m1 );Fig. 2. The behavior of A0 on input pk.

A0D2 ( · ) (c)s :=[[ Mi ]]e,η t ;Mi[, Mi+1 , T

b′ ← AOη, treturn b′ ;(pk, · )(s, η);

Fig. 3. The behavior of A0 on input c.

In Fig. 2, A0 receives the public key pk and generates two bit strings m0 and m1 of
the same length. D1 is the decryption oracle defined in Definition 13.
Then assume that b ← { 0, 1 }, x := CMP({ x0 } ⊎ { [[ r′ ]]tη | r′ ∈ R \ { r0 } }), andc := E(pk, mb , x). Since CMP is randomness-preserving and x0 is selected independently and uniformly, x is also independent and uniform. Therefore, we can use x as therandomness of the probabilistic encryption generating the challenge ciphertext c in the
IND-RCCA game.
In Fig. 3, A0 receives the ciphertext c and guesses b by invoking the adversary A
as a subroutine. Let e be the function [{| P |}RK 7→ ⟨c, pk, “enc”⟩, K 7→ ⟨pk, “PubKey”⟩],
and s be the bit string [[ Mi ]]e,η t . The adversary A receives s from A0 , and answers whichof the two distributions [[ Mi ]]η and [[ Mi+1 ]]η s is sampled from. Note that we have theequations:n t ← Coins(RS (Mi ) \ { K, r0 }), b := 0,o: [[ Mi ]]e,η t = [[ Mi ]]η

n t ← Coins(RS (Mi ) \ { K, r0 }), b := 1,o: [[ Mi ]]e,η t = [[ Mi+1 ]]η

pk ← fst(G(η)), x0 ← Randompk ← fst(G(η)), x0 ← Random

Here, e depends on the bit b, which was used to produce the challenge ciphertext
c := E(pk, mb , x). Since A can distinguish between [[ Mi ]]η and [[ Mi+1 ]]η with nonnegligible probability, A0 can guess the bit b with non-negligible probability by receiving b′ from A. Hence, A0 breaks the IND-RCCA security. This contradicts the assumption.
′
There remains a problem with the oracle Oη,M,t M , T . Recall that A uses the ora′
cle Oη,M,t M , T defined in Definition 21. Since the definition of IND-RCCA security allows
M, M ′ , T
A to use only the decryption oracles D and D , we consider an algorithm O[
0

1

η, t

2

′

that uses only D2 and simulates the oracle Oη,M,t M , T . We assume that the adversary A′
M, M ′ , T
uses the algorithm O[
presented in Fig. 4, instead of the oracle O M, M , T . Note
η, t

η, t

that A can eﬃciently decide ⟨pk, D2 (x)⟩ ∈ forbidη, t (M, T ) ∪ forbidη, t (M ′ , T ) by computing forbidden1D2 ( · ) ([[ M ]]tη , [[ M ′ ]]tη , D2 (x), [[ T ]]tη ) in Fig. 5, and ⟨pk′ , D(sk′ , x)⟩ ∈forbidη, t (M, T )∪forbidη, t (M ′ , T ) by computing forbidden2([[ M ]]tη , [[ M ′ ]]tη , D(sk′ , x),[[ T ]]tη , sk′ ) in Fig. 6.
D (·)
M, M ′ , T 2
algorithm forbidden1D2 ( · ) (s1 , s2 , µ, τ)algorithm O[(pk, x)η, tt
Set F := ∅if pk , [[ k pub0 ]]η
for each y ∈ undecτ (s1 ) ∪ undecτ (s2 )for any k pub0 ∈ Kpub
F := F ∪ { D2 (y) };then return ⊥;if µ ∈ F
else if k pub0 = K
then return “yes”;
then if ⟨pk, D2 (x)⟩ ∈ forbidη,t (M, T )else return “no”;
or ⟨pk, D2 (x)⟩ ∈ forbidη,t (M ′ , T )then return test;
Fig. 5. Algorithm forbidden1D2 ( · ) .
else return D2 (x);else (pk′ , sk′ ) := G(η, t(k pub0 ));algorithm forbidden2(s1 , s2 , µ, τ, sk′ )if k pub0 ∈ T
Set F := ∅then return D(sk′ , x);
for each y ∈ undecτ (s1 ) ∪ undecτ (s2 )else if ⟨pk′ , D(sk′ , x)⟩ ∈ forbidη,t (M, T )F := F ∪ { D(sk′ , y) };or ⟨pk′ , D(sk′ , x)⟩ ∈ forbidη,t (M ′ , T ) if µ ∈ Fthen return test;
then return “yes”;
else return D(sk′ , x);else return “no”;

D (·)[
M, M ′ , T 2
Fig. 4. Algorithm Oη,.
tFig. 6. Algorithm forbidden2.

Lemma 2. Let RE = (G, E, D, R, CMP) be an IND-RCCA secure rerandomizableencryption scheme where CMP is randomness-preserving. Let M be any acyclic term
satisfying the freshness assumption, and T be any set of secret key symbols. Let σ be arenaming for the atomic symbols in pattern(M, T ) except for T such that σ̃ pattern(M, T )= pattern(M ′ , T ) for some acyclic term M ′ satisfying the freshness assumption. Then
we have [[ σ̃ pattern(M, T ) ]]η = [[ pattern(M, T ) ]]η .
Proof. Given a term/pattern Q, let X(Q) = { R ∈ FMulti(Rand) \ FMulti(Randadv ) |R occurs in Q }. Let P = pattern(M, T ). Let σ|X(P) be the renaming for the atomic symbols in P such that σ|X(P) (R) = σ(R) if R ∈ X(P) and σ|X(P) (Q) = Q otherwise. Let
σ|AtomT (P)\X(P) be the renaming for the atomic symbols in P such that σ|AtomT (P)\X(P) (R)= R if R ∈ X(P) and σ|AtomT (P)\X(P) (Q) = σ(Q) otherwise. Clearly, we have [[ σ̃ P ]]η =[[ σ̃|AtomT (P)\X(P) σ̃|X(P) P ]]η and [[ σ̃|AtomT (P)\X(P) σ̃|X(P) P ]]η = [[ σ̃|X(P) P ]]η . Hence, it issuﬃcient to prove [[ σ̃|X(P) P ]]η = [[ P ]]η .
Let t ∈ Coins(RS ({ M } ∪ T )). Since M satisfies the freshness assumption, for eachR̃ ∈ X(M), there exists a uniform randomness symbol r̃ ∈ R̃∩Randuni that is independent
in M. Therefore, [[ r̃ ]]tη is a random bit string independently and uniformly selected from
Random. Since CMP is randomness-preserving, for each R̃ ∈ X(M), the randomness[[ R̃ ]]tη composed of [[ r̃ ]]tη is also independent and uniform.
Let R1 , R2 , · · · , Rn be all the distinct finite multisets of randomness symbols in
X(P). It is immediate from Definition 3 that for every 1 ≤ i ≤ n, there exist some R̃i1 ,
R̃i2 , · · · , R̃ik ∈ FMulti(Rand) occurring in M for k ≥ 1 such that Ri = R̃i1 ⊎ R̃i2 ⊎· · ·⊎ R̃ik ,
R̃i

R̃i2

R̃ik

a term of the form (| · · · (| {| m |}k 1 |)k · · · |)k occurs in M, and R̃ik ∈ X(P). Since CMP is
randomness-preserving and [[ R̃ik ]]tη is independent and uniform, [[ R̃i ]]tη = CMP([[ R̃i1 ⊎
R̃i2 ⊎ · · · ⊎ R̃ik−1 ]]tη , [[ R̃ik ]]tη ) is also independent and uniform.
On the other hand, since σ|X(P) is injective, σ|X(P) (R1 ), σ|X(P) (R2 ), · · · , σ|X(P) (Rn )are all the distinct multisets of randomness symbols in X(σ̃|X(P) P). Then, [[ σ|X(P) (Ri ) ]]tηis independent and uniform, because σ̃|X(P) P is also the pattern of some term satisfying
the freshness assumption.
Since both [[ σ|X(P) (Ri ) ]]tη and [[ Ri ]]tη are independent bit strings uniformly distributed on Random for any 1 ≤ i ≤ n, we obtain [[ σ̃|X(P) P ]]η = [[ P ]]η .

5.3 Example: Analysis of Simple Re-encryption Mixnet
We present an example of an analysis of a security protocol in our model.
Example 3. Consider a simple re-encryption mixnet protocol in which there are twohonest senders X1 and X2 , an honest mixnet server Y, and a formal adversary A. We
assume that they all have a public key k pub ∈ K pub , and that only Y has the corresponding
secret key k pub .
First, each Xi encrypts a message ci ∈ Const using k pub and a uniformly selected randomness ri ∈ Randuni . Next, each Xi sends the ciphertext {| ci |}rkipub to the server Y. Then,Y receives the two ciphertexts and re-encrypts them using the same public key k pub and′uniformly selected randomnesses r′ 1 , r′ 2 ∈ Randuni . Finally, Y outputs (| {| c1 |}rk1pub |)r 1
k pub

′

and (| {| c2 |}rk2pub |)r 2 in a random order.
k pub

The sequence of the honest participants’ messages in this protocol is either M or M ′ .
r′r′|) 3−iM = {| c1 |}rk1pub , {| c2 |}rk2pub , (| {| ci |}rkipub |) i , (| {| c3−i |}rk3−i
pub
M

′

= {| c2 |}rk2pub ,{| c1 |}rk1pub ,

k pub

k pub

r′
r
(| {| c j |}k jpub |) j ,
k pub

r′
r
(| {| c3− j |}k3−pubj |) 3− jk pubNote that M and M ′ are acyclic and satisfy the freshness assumption. For these twosequences of terms M and M ′ , we obtain the following two patterns.
r{| Const |}k1

pattern(M, ∅) = pubr{| Const |}k2

pattern(M ′ , ∅) = pubr{| Const |}k2

, 

pub

r

{| Const |}k1

, 

pub

{ r , r′ i }{| Const |}k i

, 

pub

{ r j , r′ j }{| Const |}k

, 

pub

{r

{| Const |}k 3−i

, 

, 

, r′ 3−i }pub{ r3− j , r′ 3− j }{| Const |}kpub

Since the uniform randomness symbols r1 , r2 , r1′ , and r2′ are independent in M ′ , there
exists a renaming σ such that σ({ r j , r′ j }) = { ri , r′ i }, σ({ r3− j , r′ 3− j }) = { r3−i , r′ 3−i },and σ({ ri }) = { r3−i } for i, j = 1, 2. Then we obtain pattern(M, ∅) = σ̃ pattern(M ′ , ∅),that is, M  M ′ .
Assume that the rerandomizable encryption scheme used in this protocol satisfies IND-RCCA security and the randomness-preserving property. Let η be a security parameter, and [[ · ]]η be the encoding that uses the scheme. Since M and M ′ areacyclic and satisfy the freshness assumption, it follows from Theorem 1 that we obtain[[ M ]]η ≈OM, M′ , ∅ [[ M ′ ]]η . This implies that no active and adaptive PPT adversary canη, tidentify the sender of each plaintext ci . Hence, we obtain sender anonymity with thissimple re-encryption mixnet protocol in the computational sense.

6

Conclusion

We proposed a new formalization of a rerandomizable encryption scheme by using
Abadi-Rogaway-style formal patterns, and proved its computational soundness by using
IND-RCCA security and the randomness-preserving property. In the formalization, we
introduced a new method for dealing with composed randomnesses.
Our method of defining patterns using multisets is not limited to the formalizationof rerandomizable encryption schemes. We believe it is also useful in order to provide acomputationally sound formalization of other cryptographic primitives, such as threshold cryptography and blind signature.

Acknowledgments
We thank Gergei Bana and the members of the Computing Theory Research Group at
NTT for their helpful suggestions. We also thank the reviewers for useful comments.

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, 2001.
2. M. Abadi and P. Rogaway. Reconciling two views of cryptography (the computationalsoundness of formal encryption). Journal of Cryptology, 15(2):103 – 127, 2002.
3. J. H. An, Y. Dodis, and T. Rabin. On the security of joint signature and encryption. In Theory
and Application of Cryptographic Techniques, pages 83–107, 2002.
4. M. Bellare, A. Boldyreva, A. Desai, and D. Pointcheval. Key-privacy in public-key encryption. In ASIACRYPT ’01: Proceedings of the 7th International Conference on the Theory
and Application of Cryptology and Information Security, pages 566–582, 2001.

5. R. Canetti and S. Hohenberger. Chosen-ciphertext secure proxy re-encryption. In CCS ’07:
Proceedings of the 14th ACM Conference on Computer and Communications Security, pages
185–194. ACM, 2007.
6. R. Canetti, H. Krawczyk, and J. B. Nielsen. Relaxing chosen-ciphertext security. In
CRYPTO, pages 565–582, 2003.
7. H. Comon-Lundh. Soundness of abstract cryptography lecture notes, 2007. Available at
http://www.lsv.ens-cachan.fr/˜comon/Soundness/.
8. V. Cortier, S. Delaune, and P. Lafourcade. A survey of algebraic properties used in cryptographic protocols. JCS, 14(1):1–43, 2006.
9. V. Cortier, S. Kremer, R. Küsters, and B. Warinschi. Computationally sound symbolic secrecy in the presence of hash functions. In FSTTCS, pages 176–187, 2006.
10. V. Cortier and B. Warinschi. Computationally sound, automated proofs for security protocols. In ESOP 2005, pages 157–171, 2005.
11. D. Dolev and A. Yao. On the security of public key protocols. IEEE Transactions on
Information Theory, 29(2):198–207, 1983.
12. F. D. Garcia and P. van Rossum. Sound computational interpretation of symbolic hashes
in the standard model. In Advances in Information and Computer Security. International
Workshop on Security (IWSEC 2006), pages 33–47, 2006.
13. P. Golle, M. Jakobsson, A. Juels, and P. F. Syverson. Universal re-encryption for mixnets. In
CT-RSA, pages 163–178, 2004.
14. J. Groth. Rerandomizable and replayable adaptive chosen ciphertext attack secure cryptosystems. In TCC, pages 152–170, 2004.
15. J. Herzog. A computational interpretation of Dolev-Yao adversaries. Theoretical Computer
Science, 340(1):57–81, 2005.
16. H. Krawczyk. The order of encryption and authentication for protecting communications(or: How secure is SSL?). In CRYPTO, pages 310–331, 2001.
17. D. Micciancio and S. Panjwani. Adaptive security of symbolic encryption. In TCC 2005,
pages 169–187, 2005.
18. D. Micciancio and B. Warinschi. Soundness of formal encryption in the presence of active
adversaries. In TCC 2004, pages 133–151, 2004.
19. M. Prabhakaran and M. Rosulek. Rerandomizable RCCA encryption. In CRYPTO, pages
517–534, 2007.
20. V. Shoup. A proposal for an ISO standard for public key encryption. Input for Committee
ISO/IEC JTC 1/SC 27, 2001.
21. R. Xue and D. Feng. Toward practical anonymous rerandomizable RCCA secure encryptions. In ICICS, pages 239–253, 2007.