Computational Soundness of Indistinguishability
Properties without Computable Parsing
Hubert Comon-Lundh1 , Masami Hagiya2 , Yusuke Kawamoto1 , andHideki Sakurada3
LSV, CNRS, ENS Cachan and INRIA, France⋆
2
University of Tokyo, Japan
3
NTT Communication Science Laboratories, NTT Corporation, Japan
1

Abstract. We provide a symbolic model for protocols using public-key
encryption and hash function, and prove that this model is computationally sound: if there is an attack in the computational world, then there
is an attack in the symbolic (abstract) model. Our original contribution
is that we deal with the security properties, such as anonymity, whichcannot be described using a single execution trace, while considering an
unbounded number of sessions of the protocols in the presence of active
and adaptive adversaries. Our soundness proof is diﬀerent from all existing studies in that it does not require a computable parsing function
from bit strings to terms. This allows us to deal with more cryptographic
primitives, such as a preimage-resistant and collision-resistant hash function whose input may have diﬀerent lengths.

1

Introduction

There are two main approaches to the analysis of protocol security. The ﬁrst
considers an attacker modeled as a probabilistic polynomial-time (PPT) interactive Turing machine (ITM) and a protocol is an unbounded number of copiesof ITMs. The attacker is assumed to control the network and can schedule thecommunications and send fake messages. The security property is deﬁned as an
indistinguishability game: the protocol is secure if, for any attacker A, the probability that A gets an advantage in this game is negligible. A typical example isthe anonymity property, by which an attacker should not be able to distinguishbetween two networks in one of which identities have been switched. The diﬃculty with such computational security notions lies in the problem of obtaining
detailed proofs: they are in general unmanageable, and cannot be veriﬁed byautomatic tools.
The second approach relies on a formal model: bit strings are abstracted
by formal expressions (terms), the attacker is any formal process, and security
properties, such as anonymity, can be expressed by the observational equivalenceof processes. This model is much simpler: there is no coin tossing, no complexity
bounds, and the attacker is given only a ﬁxed set of primitive operations (the⋆This work has been supporter by the ANR project ProSe.

function symbols in the term algebra). Therefore it is not surprising that security
proofs become much simpler and can sometimes be automatized. However, thedrawback is that we might miss some attacks because the model might be too
abstract.
Starting with work of Abadi and Rogaway [2] and Backes, Pﬁtzmann andWaidner [4], there have been several results showing the computational soundness of the formal models: we do not miss any attacks when considering theabstract model, provided that the security primitives satisfy certain properties;
for instance IND-CPA or IND-CCA in the case of encryption. Such results avoid
the weaknesses of both approaches to security.
In their original work, Abadi and Rogaway only considered symmetric encryption and a passive attacker with some other minor restrictions. This has been
extended in a number of directions. For instance, Backes et al. consider active attackers and several cryptographic primitives and show simulatability theorems,
which imply the computational soundness of some formal model [4,6]. There arealso several other soundness results, typically for some trace properties [13,9]
and, more recently, for equivalence properties [7].
In the present work, we show a soundness result for active attackers andpublic-key encryption and hash functions as cryptographic primitives. Our result
extends the previous work in the following respects:
1. In addition to security properties that can be checked on each trace, i.e., eachindividual sequence of events, we consider equivalence properties. Therefore,
our work does not ﬁt into the general framework of [3], which only considers
trace properties. Actually, we need rather diﬀerent proof techniques, such astree oracles and tree transformations. The only previous results concerning
equivalence properties in the presence of active attackers are [7], in which
only symmetric encryption and a particular class of processes is considered,and [12], in which only a ﬁxed number of protocol instances is considered.
We do not assume here any bound on the number of protocol instances.
2. Our soundness proof does not use a computable parsing function from bit
strings to terms. This is a major diﬀerence from all existing studies on computational soundness. It allows us to deal with a preimage-resistant andcollision-resistant hash function whose input may have diﬀerent lengths, forwhich the soundness of process calculi cannot be obtained by [7]’s proof
technique with the computable parsing function, as we detail later.
3. Unlike [7], we do not restrict ourselves to the so-called “simple processes”.
Simple processes are parallel compositions of replicated processes that are
just ﬁnite sequences of inputs/outputs and tests, without conditional branching. We consider here a larger fragment of the applied π-calculus of [1]: weallow negative tests and non-trivial processes in both branches of conditional, as well as arbitrary replications. We keep however two important
restrictions. First we assume that the processes are determinate: every copyof a process has ﬁrst to generate communication channels and disclose them.
In this way, the attacker can schedule to which copy of a process a message issent. Furthermore, we do not allow private communication channels. Consid-

ering such private channels would require to consider timing attacks, or (forinstance) to assume that an attacker cannot distinguish between terminating
and non-terminating processes, as investigated in [15].
4. We included hash functions in our set of primitives in order to illustrate theusefulness of dropping the parsing assumptions. Previous (positive) resultson the computational soundness of hash functions either assume stronger
properties of the hash functions than the standard preimage-resistance andcollision-resistance ([5,11,10,8]), or they assume that all plaintexts have thesame size ([5]). In any case, all these studies do not consider both an active attacker and indistinguishability properties. On the other hand, we assume that the hash function is only applied to nonces (possibly of diﬀerent
lengths).
5. Finally, we observe that the ability of the computational attacker to observe
the length of bit strings cannot be soundly represented using a (reasonable)
symbolic length function. Up to our knowledge, this problem has never been
considered in the papers on computational soundness. We propose here a new
solution where each plaintext term is associated with a label representing its
expected length in the symbolic model, and protocols accept only input of
expected length in the computational model. This is a reasonable assumptionthat can be easily implemented.
Our proof relies on ideas that are similar to [7]: each process is associatedwith a computation tree, which records all possible executions of the process. The
observational equivalence between two processes implies some labeled bisimilarity between the computation trees. Computation trees are used as tree oracles in
the computational model. The computational indistinguishability between two
processes is then equivalent to that between the two tree oracles. The proof
proceeds by successive transformations of the computation trees, in such a waythat the attacker wins a game (may distinguish the tree oracles) iﬀ he wins
the game against the transformed trees. Eventually, the computation trees are
simple enough: it is straightforward that the attacker cannot win.
There are however important diﬀerences between our work and [7], which wesummarize now. Without computable parsing, we cannot rely on the same notionof computation trees as in [7]; in [7], when the attacker submits a bit string to thetree oracle, the bit string is parsed into a term and the branch of the computation
tree labeled with this term is then taken. In this paper, we consider symbolic
computation trees, in which all term labels that satisfy the same conditions aregathered together: now the computation trees are ﬁnitely branching and theedges are labeled with formulas rather than terms. The formulas are evaluatedon the attacker’s input, whether in the computational or in the symbolic model.
In addition, since the formulas are arbitrary Boolean combinations of atomic
formulas, we may allow arbitrary conditional branching (which is not the casein [7]).
Symbolic computation trees however introduce new diﬃculties, since the previous transformations are no longer valid. We need therefore additional trans-formations, as well as a partial unraveling of the computation tree.
We also diﬀer from [7] in three other respects:
1. We consider hash functions (in the standard model), whose inputs may havediﬀerent structures (we use two diﬀerent constructors for nonces of diﬀerent
lengths): this is an example where we cannot assume a computable parsing
function. On the other hand, the impossibility result of [5] shows that the
BRISM/UC results cannot be extended to hash functions in the standard
model, when the plaintexts may have diﬀerent structures; the BRISM framework relies on the existence of a computable parsing function, allowing totranslate bit strings into terms.
2. The soundness of indistinguishability requires a symbolic length function:
we need to provide the symbolic attacker with a capability to distinguishterms, whose implementations are bit strings of diﬀerent lengths. This isdiﬃcult because, for instance, a pair ⟨u, u⟩ and a ciphertext {u}rek(k) may
or not have the same length, depending on the security parameter, while
a symbolic length function cannot depend on a security parameter; should⟨u, u⟩ and {u}rek(k) get the same symbolic length or not ? A symbolic length
function is hardly sound with respect to the computational length.
The solution adopted in [7] is to assume that the length of any cryptographic
primitive applied to some arguments is a homogeneous function of the lengths
of its arguments. Typically, in case of a linear function, the length |[[⟨u, v⟩]]η |of the computational interpretation of a pair, with respect to the security
parameter η must be α × |[[u]]η | + β × |[[v]]η | + γ × η. Then, by induction, we
may factor out η from the length of the interpretation of any term and get(in)equalities on lengths, independently of η.
This is a strong restriction on the implementation since, for instance, thepairing operation does not have a constant overhead; it depends linearly on
the security parameter.
We propose another solution here, relying on labels, that is more realistic:
messages received by honest agents do have expected lengths. Such an expected length is represented by a symbolic label such that two identical labels
yield the same computational length of messages in an honest execution. On
the computational side, we assume that the honest agents check the lengthsof messages that they receive or encrypt, which is easy to implement, sothat the actual length matches the expected one. It turns out that these assumptions, together with some weak length-regularity of the cryptographic
primitives, are suﬃcient for the soundness result, as we show in this paper.
3. [7] uses a trace mapping property, whose use in the indistinguishability games
is unclear. We formalize a new transformation of computation trees, in which
computational traces that do not have a symbolic counterpart yield a failurenode.
We do not have the space to present here the result in detail, which willappear as a research report. We sketch our symbolic model in Section 2, emphasizing the unusual components. Similarly, we sketch our computational interpre-tation in Section 3 and ﬁnally sketch the main steps of the proofs of our main
result in Section 4.

2

The symbolic model

2.1

Terms

We rely on a variant of the applied π-calculus [1]. Terms are built from names(out of a set N ), variables (out of a set X ), the constructor function symbols
FuncC = {n1 ( ), n2 ( ), ⟨ , ⟩ , h( ), ek( ), dk( ), cert( ), { } } and the destructor
function symbols FuncD = {π1 ( ), π2 ( ), dec( , )}. Let F = FuncC∪FuncD. n1 ( )and n2 ( ) are two constructor symbols for nonces. They can get only names asarguments. They are intended to produce names of diﬀerent lengths. cert( ) isa constructor for public keys certiﬁcates, h( ) is a hash function symbol andek( ), dk( ) are intended to represent encryption and decryption keys, respectively. These two symbols can only take names as arguments.
All the function symbols are available to the attacker, except for cert( ). Termis the set of ground terms built on these function symbols, the names and a set of
constants Const. Term(X ) are the terms that may additionally contain variablesfrom X . Constructor terms are terms that do not contain symbols from FuncD.
For any expression or set of expressions S, Var(S) is the set of variables occurring
free in S.
The function symbols satisfy the equations of Fig. 1. In these equations,

π1 (⟨x, y⟩) = x
π2 (⟨x, y⟩) = ydec({x}rek(k) , dk(k)) = x if k, r ∈ Name

Fig. 1. Equational speciﬁcation of the algebra

the variables x, y range over any ground constructor term. This corresponds toa “call-by-value” interpretation of the destructors. In other words, the implementation is strict: if an argument of a destructor is not a constructor term, wecannot apply these equations to cancel the destructor. The set of equations is inﬁnite, as there are symbols k, r, r′ that range over all possible names. Then, Termmight be seen as a quotient algebra with respect to the congruence generated
by the equations of Fig. 1. We ambiguously keep the same notation Term andTerm(X ) for the quotients. Term is then a F-algebra: morphisms and ﬁrst-order
structures are deﬁned as usual, referring to this quotient structure.
We orient all equations of Fig. 1 from left to right. This yields an inﬁnite
convergent term rewriting system on terms. The normal form of u is written
as u ↓.

A labeled term is either a term or a symbolic expression obtained from aterm by labeling some of its subterms with labels in Label. More formally, theset LTerm of labeled terms is deﬁned by:
LTerm ::= Term | F(LTerm, · · · , LTerm) | Term:Label | F(LTerm, · · · , LTerm):Label⟨⟩′′′For instance, { n1 (r), n2 (r′ ):ln2 :l1 }rek(k) and {h(n1 (r):ln1 ):l2 }rek(k) are labeledterms. Intuitively, u:l represents a message whose length is expected to be l inan honest protocol execution.
The rewrite rules of Fig. 1 can only be applied to unlabeled instances of thevariables; when we rewrite a labeled term, the labels of the rule instances are
implicitly removed. In this way, we keep the conﬂuence and termination of therewrite system and rewriting a labeled term yields a labeled term (for instance,
we do not get u:l:l′ ).
2.2

Predicates, conditions, frames and static equivalence

Predicates are used either in honest processes, in order to check properties of the
input terms, or by the attacker, in order to distinguish sequences of terms. We
consider the following predicate symbols: M , EQ, EK , IsEK ,IsN 1 , IsN 2 , PL,
and HL, whose (informal) meaning is as follows. M (u) holds on ground terms usuch that u ↓ is a constructor term. EQ is the strict equality predicate: EQ(u, v)
implies u ↓= v ↓ and M (u) and M (v). EK holds on a ciphertext {u}wv and apublic key ek(k) when v = ek(k). IsEK is true on pairs of an encryption key anda certiﬁcate of that key. IsN 1 holds on terms n1 (r) with r ∈ Name and IsN 2 holds
on terms n2 (r) with r ∈ Name. PL holds on two ciphertexts whose plaintexts
have the same expected length, i.e. the same label. HL holds on two hash values
whose plaintexts have the same label. A condition is a Boolean combination of
atomic formulas. Examples of predicate interpretations are given in Example 1.
The frames usually record the messages that have been sent. Since we consider symbolic executions, we need to extend the classical deﬁnition to message
templates that may contain variable. A frame is an an expression νy.νn.σ where
y is a ﬁnite set of variables, n is a ﬁnite set of names, σ is a substitution froma ﬁnite set of variables dom(σ) into Term(X ) such that y ∩ dom(σ) = ∅, andVar(codom(σ)) ∩ dom(σ) = ∅.
Given a frame ϕ, we write σϕ the associated substitution, bn(ϕ) is the associated sequence of bound names n and bv(ϕ) is the associated sequence of boundvariables y. A ground frame ϕ is a frame such that Var(codom(σϕ )) = ∅. We
recall here the deﬁnition of symbolic indistinguishability between ground frames(for general frames, this notion will be directly deﬁned on computation trees).
Definition 1. Two ground frames ϕ1 and ϕ2 are statically equivalent, which is
written as ϕ1 ∼ ϕ2 , if dom(σϕ1 ) = dom(σϕ2 ) and for any terms u and v suchthat cert does not occur in u, v, Var(u) ∪ Var(v) ⊆ dom(σϕ1 ) and (fn(u) ∪ fn(v)) ∩(bn(ϕ1 ) ∪ bn(ϕ2 )) = ∅, we have the following:– For each PR ∈ {M , IsEK , IsN 1 , IsN 2 }, M |= PR(uσϕ1 ↓) iﬀ M |= PR(uσϕ2 ↓).

– For each PR ∈ {EQ, EK , PL, HL}, M |= PR(uσϕ1 ↓, vσϕ1 ↓) iﬀ M |=PR(uσϕ2 ↓, vσϕ2 ↓).
Example 1. In the examples, we omit the variables of the domains of σϕ : they
are always x1 , . . . , xn where n is the length of the frame.
1. νr. n1 (r) ∼ νr′ . n1 (r′ ), while νr. n1 (r) ̸∼ νr′ . n2 (r′ ), since M |= IsN 1 (n1 (r))
and M ̸|= IsN 1 (n2 (r)).
′
2. νr. {b: l}rek(a) ∼ νr. {c: l′ }rek(a) iﬀ l = l′ , since M |= PL({b: l}rek(a) , {b′ : l}rek(a) )′and M |= PL({c:l′ }rek(a) , {b′ : l}rek(a) ) iﬀ l = l′ . In this example, the recipe
u is reduced to the variable x1 and the recipe v is the ground (labeled)′term {b′ : l}rek(a) .
3. νa, r. {b: l}rek(a) , dk(a) ̸∼ νa, r. {c: l}rek(a) , dk(a) if b, c ∈ N and a, b, c, r are
pairwise distinct. It suﬃces to consider u = dec(x1 , x2 ), v = b: M |=EQ(uσϕ1 ↓, v) while M ̸|= EQ(uσϕ2 ↓, v).
′′
4. νa, a′ , r, r′ . {b: l}rek(a) , {b: l}rek(a) , ek(a) ̸∼ νa, a′ , r, r′ . {b: l}rek(a) , {b: l}rek(a′ ) , ek(a)using EK .
2.3

Processes

Processes are built as in the applied π-calculus [1], using the predicates andfunction symbols of the previous section. We do not recall here the syntax andthe basic deﬁnitions. Let us explain the communication rule.
c(x: l).P ∥ c(u: l).Q→

P {x 7→ u} ∥ {x 7→ u} ∥ Q

If a process c(x: l).P is ready to receive a message on the channel c and anotherprocess is ready to emit the message u on channel c and if the two messages havethe same label, then the network moves to a conﬁguration in which x is replacedwith u in P . The active substitution {x 7→ u} is kept (as a local memory of P ).
While the attacker’s processes are arbitrary processes (the attacker may relabel the terms as he wishes), protocols are speciﬁed as combinations of basic
processes, using replication, name generation and parallel composition.
The basic processes are built using name generation, conditionals and sequences of input/output actions. We assume that all inputs are labeled variables.
This is not a restriction, since the attacker may re-label the terms. We assume
that all occurrences of plaintexts (of either ciphertexts or hashes) in the basic
processes are labeled, and that before sending a message s the process always
checks M (s). This forbids sending ill-formed messages (or forwarding ill-formed
message). Since, according to our semantics, ill-formed messages do not pass any
test, the eﬀect of message forwarding (moving the control point of some process)can be achieved with a well-formed message. We believe that this assumption is
not a restriction.
The main restriction, with respect to the full applied π-calculus is that, eachtime a process is replicated, it must start with the generation of communication
channels that are disclosed and then used as input/output channels. This ensuresthe determinacy of processes: when the attacker sends a message on a channelc, there is at most one basic process that is able to receive a message on c.
Example 2. This is a simple process that ﬁrst generates two channel names anddisclose them, hence can be later replicated.
B(a, b, c, d) = νx, y. νiin , iout , r. c(x: l).c(⟨iin , iout ⟩).
iin (y: l). if EQ(π1 (dec(y, dk(a)))), b) ∧ M (π2 (dec(y, dk(a)))) ∧ IsEK (ek(b))
then iout ({π2 (dec(y, dk(a))): l′ }rek(b) )else iout ({d: l′ }rek(b) )Example 3. The following is an example of a protocol.
)((νa)(νb)(νd) ! (νx) (νc1 , c2 ) c(x: l) c(⟨c1 , c2 ⟩) (! B(a, b, c1 , d))∥ !B(b, a, c2 , d))
The attacker, using the public channel c, may send a signal, which will giveback fresh channel names c1 , c2 . This allows to get a copy of the (outermost)
replicated process. Each of these channel names may then be used to request a
copy of the corresponding instance of B.
Protocols may also include an initial setting, in which, for instance, some
private keys are disclosed (static corruption).
We assume a number of (reasonable) properties of the protocols:– Two occurrences of the same variable have the same label.
– The random seed r used in honest encryption terms { }r only occur in thatterms and the random seed k used for honest (i.e., certiﬁed) keys ek(k) anddk(k), are not used for any other purpose.
– Encryption keys with their certiﬁcates are sent to the attacker whenever they
are generated.
– Only correct encryption keys are used for encryption (for unknown keys,
IsEK is checked before encryption). This rules out the problem of keys thatare forged by the attacker.
– Only hash values of nonces are produced by the protocols: for unknown
plaintexts s, the protocol checks IsN 1 (s) ∨ IsN 2 (s) before hashing.
– There is no dynamic corruption: the protocols only disclose decryption key
at the beginning of the execution.
– There is no key cycle: a key hierarchy ensures that the attacker cannot force
the protocol to produce a cycle involving non-corrupted keys.
Finally, two processes P and Q are observationally equivalent, which we write
P ∼ Q if, as usual, there is no context C such that C[P ] may emit on a channel
a while C[Q] cannot (or the converse).

3

Computational interpretation

3.1

Computational interpretation of terms and predicate symbols

Each function symbol f is associated with a function [[f ]] from bit strings to bit
strings that can be computed in deterministic polynomial time. These interpretations are assumed to satisfy the equations of Fig. 1, hence the set of bit strings

has a structure of F-algebra. Let SS be a set of mappings from Name to {0, 1}∗ .
Given τ ∈ SS, for any ground term u, [[u]]τ is the unique extension of τ into a
homomorphism of F-algebra. If u is a term with variables X and θ is a mappingfrom X into {0, 1}∗ , [[u]]θ,τ is deﬁned in a similar way. The interpretation of labeled terms is deﬁned by ignoring the labels. Labels themselves are interpreted
as natural numbers. The security parameter is the minimal length of τ (r) forr ∈ Name.
In addition, we assume the following properties of the computational interpretation:– The ranges of constructor function symbols are disjoint and disjoint fromthe interpretation of names. This assumption is necessary for a soundness
result. However, we do not assume that the range of a function symbol iscomputable.
– We assume the following properties on lengths of the computational interpretation of names and nonces.
• For each b = 1, 2 and any r, r′ ∈ Name, [[nb (r)]]τ = [[nb (r′ )]]τ , and that[[n1 (r)]]τ < [[n2 (r)]]τ < |[[r]]τ |.
• When τ is uniformly drawn (which we will assume in what follows), thedistribution of [[nb (r)]]τ is uniform and covers all bit strings of the length|[[nb (r)]]τ |.
• [[n1 (r)]]τ and [[n2 (r)]]τ are polynomial in the security parameter η.
Thanks to the assumptions, for instance, the lengths of keys are diﬀerent
from those of nonces in the computational model.
– We assume a weak notion of length regularity: Let u: l be any labeled term
occurring in a protocol such that y1 : l1 , y2 : l2 , . . . , yn : ln are all variables
occurring in u. For any computational interpretation τ of names as bit
strings, if terms v1 , v2 , . . . , vn satisfy |[[vi ]]τ | = [[li ]]τ for i = 1, 2, . . . , n, then[[u {y1 7→ v1 , y2 7→ v2 , · · · , yn 7→ vn }]]τ = [[l]]τ .
– For each PR ∈ {M , IsEK } and any term u,• M |= PR(u) iﬀ [[PR]]([[u]]τ ) = 1 holds for any τ ∈ SS, and• M |= ¬PR(u) iﬀ [[PR]]([[u]]τ ) = 0 holds for any τ ∈ SS.
Note that this does not imply anything on the interpretation of PR on a bit
string that is not the interpretation of any term.
– For each PR ∈ {IsN 1 , IsN 2 } and any bit string m, [[PR]](m) = 1 iﬀ there
are u ∈ Term and τ ∈ SS such that m = [[u]]τ and M |= PR(u). For instance,
we can implement [[IsN b ]](m) by checking whether the length of m is [[lnb ]]τ
or not.
– For any bit string m and any name k,• if [[M ]]([[πi ]](m)) = 1 for i = 1, 2, then [[M ]]([[dec]](m, [[dk(k)]]τ )) = 0,
• if [[M ]]([[dec]](m, [[dk(k)]]τ )) = 1, then[[M ]]([[dec]](m, [[dk(k ′ )]]τ )) = 0 for
any name k ′ such that [[dk(k)]]τ ̸= [[dk(k ′ )]]τ ,• for any m ∈ {0, 1}∗ and any m′ ∈ {0, 1}∗ \ {[[dk(k)]]τ : τ ∈ SS},[[M ]]([[dec]](m, m′ ) = 0.

These assumptions cover the case where m is not the computational interpretation of any term. They can be ensured, for instance, by assuming thatthe decryption of a ciphertext with a wrong key returns an error. The previous work on computational soundness has implemented this by appending
each ciphertext with the encryption key used to produce the ciphertext.
– The implementation is strict: For any f ∈ F and any bit string m, [[M ]](m) =0 implies [[M ]]([[f ]](· · · m · · ·)) = 0. For instance, [[M ]]([[{u}rek(k) ]]τ ) = 0 when′u = dec({s}rek(k) , dk(k ′ )).
– For any two terms u, v, [[EQ]]([[u]]τ , [[v]]τ ) = 1 iﬀ [[M ]]([[u]]τ ) = [[M ]]([[v]]τ ) = 1
and [[u]]τ = [[v]]τ .
For a computational soundness result, we assume nothing on the computational interpretation of the predicates EK , PL, HL, which may (not) be available
to a computational attacker.
3.2

Interactive Turing machines

The processes are interpreted as interactive Turing machines, which we do notrecall here. Let us only highlight the speciﬁcs of our model.
The model of the network includes a store that records the IDs (interpretation of channel names) associated with each process. This allows us to consider
nested replications: the attacker may refer to a given replicated process in a
deterministic way using such channel IDs.
More importantly, each basic process, upon receiving a message on a channelc, checks that the length of the input bit string matches the expected length. It
proceeds only there is a match: the machine in state c(x: l).B may move to thestate B only if the content of its input tape has length [[l]].
Definition 2. Two protocols P and Q are computationally indistinguishable,
which we write P ≈ Q, if, for any attacker’s machine A,|Pr [τ : [[P ]]τ ∥A = 1] − Pr [τ : [[Q]]τ ∥A = 1]|
is negligible in the security parameter.
3.3

Cryptographic assumptions

We assume the public-key encryption scheme to be IND-CCA2 and the hashfunction to be preimage-resistant and collision-resistant. For instance, preimageresistance is stated as follows.
Given a security parameter η, a hash function [14] is a deterministic algorithm
H that, given a key k ∈ KH and a bit string m ∈ MH , outputs a hash value of mby k, whose length only depends on η (not on m), where KH is a key space and′MH is a message space such that m′ ∈ MH implies {0, 1}|m | ⊆ MH , and thateach bit string in MH is so long that it cannot be guessed by the attacker (i.e.

there is a polynomial p such that η ≤ p(min{|m| | m ∈ MH })). H is preimageresistant if the following probability is negligible in η for any PPT attacker A
and any ℓ such that {0, 1}ℓ ⊆ MH :Pr[ k ← KH ; s ← {0, 1}ℓ ; m := H(k, s) ; s′ ← A(1η , k, m) : H(k, s′ ) = m ].
$$We also assume the following (which are necessary for the soundness result):– The key certiﬁcates cannot be forged with a non-negligible probability.
– The length of a pair is longer than (or equal to) the sum of the lengths of
its two components.
– The length of a ciphertext is strictly longer than the length of the corresponding plaintext.
– The length of a hash value (of a nonce) is strictly smaller than the length of
the nonce. This rules out identities such as h(n) = n that could, otherwise,
occur with a non-negligible probability.

4

The main result

Our main result states that we captured all distinguishing capabilities of a computational attacker in a symbolic model:
Theorem 1. Let P and Q be two protocols. If P ∼ Q, then P ≈ Q.
The rest of the paper is devoted to the sketch of the proof of this result. First
we express the problem as the equivalent problem “tP ∼ tQ implies tP ≈ tQ ”
where tP is a computation tree that represents all possible execution sequences(see Section 4.1). Unlike [7], these trees have a ﬁnite outdegree, which is independent of the security parameter.
Next, we perform successive transformations T of the computation trees,transforming the problem into “T (tP ) ∼ T (tQ ) implies T (tP ) ≈ T (tQ )”. The
computation trees T (tP ) are no longer the computation trees of processes andthat is why we use the detour through computation trees. Let us consider someof these transformations in more details.
1. The ﬁrst transformation aims at ensuring more properties of the computation
trees and therefore enables the next step: we partially unravel the computation trees, unfolding some conditions (see Section 4.2). This transformation
may yield computation trees whose branching degree depends on the security parameter. The diﬃculty lies in proving that they are still polynomiallysimulatable.
2. The second transformation is a classical one: thanks to the absence of key
cycles, following the ordering on keys, we may replace plaintexts of encryptions by uncorrupted keys with a constant of the same length as the plaintext(see Section 4.3). This step requires the IND-CCA2 property of the publickey encryption scheme. After this step, t ∼ t′ iﬀ the total unravelings U (t)and U (t′ ) of t and t′ respectively (which are inﬁnitely branching trees) are
identical up to renaming, which we write U (t) ≃ U (t′ ).

3. The third transformation rules out coincidences (see Section 4.4): in the
resulting computation tree, the conditions explicitly state that two distinct
names are distinct and that two hash values of distinct terms are distinct.
Though this is trivial in the symbolic model, it may happen by chance inthe computational one. We also need here to rely on collision-resistance ofthe hash function.
4. The fourth transformation rules out guesses made in advance (see Section 4.5): in the resulting computation tree, the conditions state explicitlythat a random term that has not been produced yet, cannot be computed.
This is more tricky than it looks, and relies in particular on the assumptionthat the length of a pair is longer than the sum of the lengths of its components. It also rules out the computation of a nonce from its hash value,
thanks to preimage-resistance.
After these transformations, we can conclude that t ≈ t′ , thanks to a trace
mapping property (see Section 4.6).
4.1

Computation trees

A computation tree is a ﬁnitely branching tree whose nodes are labeled withpairs consisting a process (a state) and a frame and whose each edge is labeledwith a variable, a channel name and a condition. For any node of a computation
tree, given a variable x and a channel name c, the disjunction of all the conditions
Φ such that (x, c, Φ) labels some edge departing from the node is a tautology
and any two such conditions cannot be satisﬁed together.
We may associate a computation tree to any protocol: Roughly speaking, if aprocess P0 ∥Q is structurally equivalent to (νn)(c(x: l).P1 ∥Q) and (νm)(P0 ∥Q, ϕ)x,c,Φ

is labeling a node, we add an edge (νm) (P0 ∥Q, ϕ) −−−→ (νm, n)(P2 ∥Q, ϕ ⊎ ϕ′ )if there is a (sequence of) test Φ in P1 , whose satisfaction yields the output of ϕ′and the remaining process P2 .4 Any symbolic trace (i.e., any sequence of triples(x, c, s) where x is a variable, c is a channel name and s is a ground term) thatcan be produced by an attacker process corresponds to an instance θ of a pathin the process computation tree, such that, at any step as above, there is a termu such that uσϕ θ ↓= xθ (in other words, xθ is deducible from the corresponding
instance of the frame).
Given a sample τ , each computation tree t is also associated with a tree
oracle Ot,τ : when the oracle is queried with a bit string m, a variable x anda channel ID [[c]]τ , it evaluates (in the computational model) the conditions
departing from the root node and associated with (x, c). Exactly one of them is
x,c,Φ

satisﬁed: this corresponds to an edge t −−−→ t′ . Then the oracle replies sending
the computational interpretation of the frame labeling the root of t′ and thenbehaves as Ot′ ,τ . Two tree oracles are indistinguishable if no polynomial time
4

The names that are bound in front of the state/frame cannot be renamed, unlessthey are renamed in the whole subtree.

attacker can guess with a signiﬁcant advantage which of the two oracles he isinteracting with.
Example 4. The computation tree of the protocol P = νiin , iout , r, k. cB (x). c¯B (⟨iin ,iout ⟩). B is shown in Fig. 2 where n̄ = iin , iout , r, k and B is the following basic
process:iin (y).if EQ(π1 (y), n1 (r))
then if M (dec(π2 (y), dk(k)))
then iout (dec(π2 (y), dk(k))).0
else 0else 0.
P, [ ]
x, cB , ⊤(ν n̄) B, [⟨iin , iout ⟩]Py, iin , EQ(π1 (y), n (r))∧
 ZPPPZ
PP y, iin , ¬EQ(π1 (y), n1 (r))
M (dec(π2 (y), dk(k)))

Z

PP

1

Z
PP
y, iin , EQ(π1 (y), n (r))∧
PPZ¬M (dec(π2 (y), dk(k)))Z

P
1




(ν n̄) 0, [⟨iin , iout ⟩ , dec(π2 (y), dk(k))]

ZPP(ν n̄) 0, [⟨iin , iout ⟩] (ν n̄) 0, [⟨iin , iout ⟩]Fig. 2. Example of a computation tree

4.2

Partial unraveling

The goal is to replace plaintexts with ﬁxed bit strings, thanks to IND-CCA2.
However, in some cases, it would not be correct, because the terms occurring in
the frames or the conditions may contain variables. For instance in dec({u: l}rx ,y), we may replace u with a ﬁxed term of expected length l only if the instance ofthe term does not contain a redex, in other words unless x = ek(k) and y = dk(k)for some name k. The basic idea is to narrow these terms, which may require to
split the conditions, depending on whether there is a key generated so far suchthat x = ek(k) and y = dk(k).
We prove that we can unravel a computation tree, in such a way that theresulting tree is both computationally and symbolically indistinguishable fromthe original tree and such that any occurrence of an encryption/decryption issafe: either the key is explicitly an encryption/decryption key that has been
generated before, or the condition implies that this is not the case. Furthermore,
we prove that the tree oracle can still be simulated in polynomial time.
For example, let us consider the computation tree t1 shown in Fig. 3 that has
only one subtree t2 . For brevity, the states and the bindings are omitted from
Fig. 3.

h(s: l)y1 , ⊤
1h(s: l), {s: l}rek(k)y2 , ¬EQ(y1 , dec(y2 , dk(k)))







Z
Z y2 , EQ(y1 , dec(y2 , dk(k)))
Z
Z
Z
Z
Z

t3

t4

Fig. 3. Example of a computation tree t1

The partial unraveling Uek (t1 ) of t1 is shown in Fig. 4. In Uek (t1 ), the edge fromt2 to t3 is split into the two edges to t30 and t31 such that C0 = ¬EQ(y1 , s) ∧1
1
EQ(y2 , {s: l}rek(k)) and C1 = ¬EQ(y1 , dec(y2 , dk(k))) ∧ ¬EQ(y2 , {s: l}rek(k)). Similarly, the edge from t2 to t4 is split into the edges to t40 and t41 . Then Uek (t1 )is a safe computation tree.
h(s: l)y1 , ⊤
1h(s: l), {s: l}rek(k)BHHy2 , EQ(y1 , dec(y2 , dk(k)))

B HHH∧¬EQ(y2 , {s: l}r1 )y2 , C 0  ek(k)HHB , s)
 y2 , EQ(y
1
H

B
r1
H


∧EQ(y
HH

B 2 , {s: l}ek(k) )y2 , C1

H

B

t30

t31

t40

t41

Fig. 4. The partial unraveling Uek (t1 ) of t1

4.3

Replacing plaintexts

To such safe computation trees, we may apply the pattern function Ω, replacing
each encryption {u: l}rek(k) with {l : l}rek(k) . This yields again a computation
tree which is both symbolically and computationally indistinguishable from theoriginal one, unless we break IND-CCA2.
For example, the tree Ω(Uek (t1 )) is shown in Fig. 5 where C0′ = ¬EQ(y1 , s) ∧1
1
EQ(y2 , {l : l}rek(k)) and C1′ = ¬EQ(y1 , dec(y2 , dk(k))) ∧ ¬EQ(y2 , {l : l}rek(k)).
r1Note that the plaintext s inside the ciphertext {s: l}ek(k) is replaced with theconstant l , whose expected length l is the same as s.
After this step, t ∼ t′ iﬀ the total unravelings of t and t′ respectively (which
are inﬁnitely branching trees) are identical up to renaming.

h(s: l)y1 , ⊤
1h(s: l), {l : l}rek(k)BHHy2 , EQ(y1 , dec(y2 , dk(k)))

HH
r1

B
′

2 , {l : l}ek(k) )H∧¬EQ(yy2 , C 0  BHy2 , EQ(y1 , s)
H

B
r1 H

∧EQ(y
2 , {l : l}ek(k) ) H′
BHHy2 , C1H
BΩ(t30 )Ω(t31 )Ω(t40 )Ω(t41 )

Fig. 5. Ω(Uek (t1 ))4.4

Ruling out coincidences

Roughly speaking, we add to any condition Φ, labeling an edge of the computation tree, the conditions ¬EQ(r, r′ ) for distinct names r, r′ , as well as theconditions ¬EQ(h(u), h(v)) for distinct terms h(u), h(v) that appear either inthe current frame or condition. We also add similar constraints for keys. Thisrelies, for instance, on collision-resistance.
4.5

Ruling out predictions

This is a bit more involved: we need to introduce new predicate symbols (for the
purpose of the proof only). For instance, we consider a predicate NP (K, u, v),
which holds, given a substitution σ, if for any destructor context C using decryption keys in K, we have C[u]σ ↓̸= vσ ↓. We may express for instance that,when a name n is generated, if the currently available keys are in K, the lastattacker input x cannot contain anything that depends on n. This is expressedby adding the constraint NP (K, x, n). We use here preimage-resistance of thehash function, expressing that a nonce cannot be guessed from its hash.
h(s: l)HHy1 , NP (K, y1 , s)H y1 , ¬NP (K, y1 , s)H1h(s: l), {l : l}rek(k)

abort


P
HP
@

,
HP

"
"


",  @HP
HP


P
"
HP
 , 
 "
HHPPP

@
abort  " ,
abort
H
@

" ,
H

"
HH
y2 , EQ(y1, s)y@
2 , EQ(y1 , s)" ,,
r1
r1
H

@

∧EQ(y
2 , {l : l}ek(k) )
∧EQ(y
,
{
abort
2
l : l}ek(k)
H)H

,

@

∧¬NP
(K,
y
,
s)
2
∧NP@
(K, y2 , s),H∆(Ω(t30 ))∆(Ω(t31 ))abort

Fig. 6. ∆(Ω(Uek (t1 )))∆(Ω(t40 ))∆(Ω(t41 ))For instance, if we apply the transformation ∆ to Ω(Uek (t1 )), ruling out
predictions, the edge from Ω(Uek (t1 )) to Ω(Uek (t2 )) is split in two by adding
NP (K, y1 , s), which expresses the impossibility of computing the nonce s fromy1 , or ¬NP (K, y1 , s), and the edge from Ω(Uek (t2 )) to Ω(t40 ) is split in two
by adding NP (K, y2 , s) or ¬NP (K, y2 , s), as shown in Fig. 6. We omit detailsof the other edges that are split similarly. ¬NP (K, y1 , s), for instance, implies
EQ(C[y1 ], s) for some destructor context C. Hence the satisfaction of this condition implies the existence of an attacker on the preimage-resistance of the hashfunction; the execution aborts in this case.
4.6

Trace mapping

We show that the conditions resulting from all previous transformations areeither unsatisﬁable or else satisﬁable both in the computational and in the symbolic model. It follows that, for every computational trace, which corresponds toa path in the computation tree and an assignment of variables that satisﬁes all
the conditions along this path, there is also a symbolic trace that corresponds
to the same path. This is what we call trace mapping. It is slightly diﬀerent
from the usual trace mapping, which states that every computational trace isan interpretation of a symbolic trace, with an overwhelming probability. First,
thanks to our previous transformation steps, we get a property with the probability 1 (not with an overwhelming probability only). Next, we do not statethat the computational trace is an interpretation of the symbolic one: we only
state that they satisfy the same conditions. This is suﬃcient to conclude: thanks
to trace mapping, for every sequence of attacker inputs si , if Ot,τ replies thesequence [[ur ]]τ , then there is a sequence of symbolic attacker inputs vi yielding
the sequence ur of symbolic replies of U (t). Now, since U (t) ≃ U (t′ ), there is′also a sequence u′r of replies of U (t′ ) such that, for some τ ′ , [[u′r ]]τ = [[ur ]]τ is thesequence of replies of the oracle Ot′ ,τ ′ on the input sequence si . Hence t ≈ t′ .
(And we do not need [[vi ]]τ = si .)5Conclusion

We managed to get a computational soundness result for observational equivalence, without any parsing assumption. This result holds for a large subset ofthe applied π-calculus. We believe that the same method can be applied to otherprimitives, though, as this proof shows, it might be long and tedious.
However, we learned several lessons from this work. For instance, we attacked the problem of the symbolic length from another angle, using a trade-oﬀ
between computational assumptions and assumptions on the protocols. We also
showed how collision-resistance (resp. preimage-resistance) of hash functions canbe used in soundness proofs. And maybe, more importantly, we identiﬁed several
assumptions that look necessary for soundness results, showing the limitationsof the method.

Acknowledgments
We thank Dominique Unruh and Véronique Cortier for valuable discussions. We
also thank the anonymous reviewers for helpful comments.

References
1. Martı́n Abadi and Cédric Fournet. Mobile values, new names, and secure communication. In Proc. of the 28th ACM Symposium on Principles of Programming
Languages (POPL’01), pages 104–115, 2001.
2. Martı́n Abadi and Phillip Rogaway. Reconciling two views of cryptography (thecomputational soundness of formal encryption). Journal of Cryptology, 15(2):103– 127, 2002.
3. Michael Backes, Dennis Hofheinz, and Dominique Unruh. CoSP: A general framework for computational soundness proofs. Cryptology ePrint Archive, Report
2009/080, 2009. http://eprint.iacr.org/.
4. Michael Backes, Birgit Pﬁtzmann, and Michael Waidner. A composable cryptographic library with nested operations. In Proc. of the 10th ACM Concerence on
Computer and Communications Security (CCS’03), pages 220–230, 2003.
5. Michael Backes, Birgit Pﬁtzmann, and Michael Waidner. Limits of the BRSIM/UC
soundness of Dolev-Yao models with hashes. In Proc. of 11th European Symposium
on Research in Computer Security (ESORICS’06), volume 4189 of Lecture Notes
in Computer Science, pages 404–423, 2006.
6. Michael Backes, Birgit Pﬁtzmann, and Michael Waidner. The reactive simulatability (RSIM) framework for asynchronous systems. Information and Computation,
205(12):1685–1720, 2007.
7. Hubert Comon-Lundh and Véronique Cortier. Computational soundness of observational equivalence. In Proc. of the 15th ACM Conference on Computer andCommunications Security (CCS’08), pages 109–118, 2008.
8. Véronique Cortier, Steve Kremer, Ralf Küsters, and Bogdan Warinschi. Computationally sound symbolic secrecy in the presence of hash functions. In Proceedings ofthe 26th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS’06), volume 4337 of Lecture Notes in Computer Science,
pages 176–187. Springer, 2006.
9. Véronique Cortier and Bogdan Warinschi. Computationally sound, automatedproofs for securityprotocols. In Proc. of 14th European Symposium on Programming(ESOP’05), volume 3444 of Lecture Notes in Computer Science, pages 157–171,
2005.
10. Flavio D. Garcia and Peter van Rossum. Sound and complete computational
interpretation of symbolic hashes in the standard model. Theor. Comput. Sci.,
394(1-2):112–133, 2008.
11. Romain Janvier, Yassine Lakhnech, and Laurent Mazaré. Computational soundness of symbolic analysis for protocols using hash functions. Electr. Notes Theor.
Comput. Sci., 186:121–139, 2007.
12. Yusuke Kawamoto, Hideki Sakurada, and Masami Hagiya. Computationally soundsymbolic anonymity of a ring signature. In Proc. of Joint Workshop on Foundationsof Computer Security, Automated Reasoning for Security Protocol Analysis andIssues in the Theory of Security (FCS-ARSPA-WITS’08), pages 161–175, 2008.

13. Daniele Micciancio and Bogdan Warinschi. Soundness of formal encryption in thepresence of active adversaries. In Proc. of Theory of Cryptography Conference(TCC’04), volume 2951 of Lecture Notes in Computer Science, pages 133–151,
2004.
14. Phillip Rogaway and Thomas Shrimpton. Cryptographic hash-function basics:
Deﬁnitions, implications, and separations for preimage resistance, second-preimage
resistance, and collision resistance. In Proc. of Fast Software Encryption (FSE),
volume 3017 of Lecture Notes in Computer Science, pages 371–388, 2004.
15. Dominique Unruh. Termination-insensitive computational indistinguishability(and applications to computational soundness). In Proc. of the 24th IEEE Computer Security Foundations Symposium (CSF 2011). IEEE Computer Society, June2011.