Computationally Complete Symbolic Attacker and Key
Exchange
Gergei Bana
INRIA, Paris, France
bana@math.upenn.edu

Koji Hasebe
Graduate School of Systems and Information Engineering, University of Tsukuba
Tsukuba, Japan
hasebe@iit.tsukuba.ac.jp

Mitsuhiro Okada
Department of Philosophy, Keio University, Tokyo, Japanmitsu@abelard.flet.keio.ac.jp

ABSTRACTtional implementation that they needed for soundness. But PROGKDM security and the other conditions are necessary only to receive computational guarantees for their symbolic analysis even if
computational security of the analyzed protocol holds without theserequirements. Their strong conditions are imposed on the computational implementation not for the security of the protocol, but forthe soundness of the analysis.
Recently, Bana and Comon-Lundh (BC) presented in [8] a newkind of symbolic attacker. They called it computationally complete symbolic adversary, as it is capable of doing everything thata computational adversary is capable of. They observed that thediscrepancy between symbolic and computational proofs emerges
from the following fact: While the usual computational security
assumptions on the primitives (such as IND-CCA2 security of theencryption) define what the adversary cannot violate (and the security of the protocol is derived from the security of the primitives),
symbolic adversaries are defined by listing all the adversarial capabilities (Dolev-Yao rules). Hence, to adjust the viewpoint of thesymbolic analysis to that of the computational, instead of listing every kind of moves a symbolic adversary is allowed to do, Bana andComon-Lundh list a few rules (axioms) that the symbolic adversary
is not allowed to violate. Anything that does not contradict theseaxioms is allowed for the adversary. Hence, a successful symbolic
attack in their case means that the violation of the security property of the protocol is consistent with the axioms. The axioms thatare introduced must be computationally sound with respect to thecomputational interpretation they defined. Their general soundness
result is the following: Suppose that the computational implementation satisfies a set of axioms. If there is a successful PPT attacker
for which the number of sessions it exploits does not increase indefinitely as the security parameter increases (there is a bound, but
it can be arbitrarily high), then there is also a successful symbolic
adversary complying with the set of axioms.
The difference between the original Dolev-Yao (DY) techniqueand that of BC can be best understood from the following pictures.
In the DY technique, as more and more rules are added, the symbolic adversarial capabilities are increasing, the symbolic adversary
covers more and more of the computational capabilities. However,no-one has been able to come up with rules that properly cover
all possible computational capabilities. As Figure 1 shows, there
are always some computational capabilities that are not covered by
the DY ones. All computational soundness results that use the DY

Recently, Bana and Comon-Lundh [8] introduced the notion ofcomputationally complete symbolic attacker to deliver unconditional computational soundness to symbolic protocol verification.
First we explain the relationship between their technique and Fitting’s embedding of classical logic into S4 [25]. Then, based on
predicates for “key usability”, we provide an axiomatic system intheir framework to handle secure encryption when keys are allowed
to be sent. We examine both IND-CCA2 and KDM-CCA2 encryptions, both symmetric and asymmetric situations. We also consider
INT-CTXT ciphertext integrity. This technique does not require theusual limitations of computational soundness such as the absenceof dynamic corruption, the absence of key-cycles or unambiguous
parsing of bit strings. In particular, if a key-cycle possibly corrupts
CCA2 encryption, our technique delivers an attack. If it does notendanger security, the security proof goes through. We illustrate
how our notions can be applied in protocol proofs.

1.

INTRODUCTION

Approaches to computationally sound automated verification of
security protocols can be divided into two groups. Works in one[3, 22, 4, 18, 26, 21] define symbolic adversaries, and soundness
theorems state that under certain circumstances, if there is no successful symbolic attack, then there is no successful computational
attack either. The other group aims to work directly in the computational model [23, 15, 10, 11, 9]. In this latter case, computationalsoundness means that the properties on which symbolic manipulations are conditioned hold computationally.
The first group, where a symbolic attacker is defined, gives hopethat already existing automated tools may be adopted for computationally sound verification, but these soundness theorems requirelarge sets of assumptions. A number of assumptions, as well as
reasons why they are not realistic are discussed in [19]. Such assumptions are, for example, that bit strings can be unambiguously
parsed into symbolic terms, or, that no key cycles occur, or, that all
keys are honestly generated, or, that there is no dynamic corruption.
Recently, Backes et al. in [2] showed a way to avoid some of these
problems such as key-cycles and badly generated keys, but for thecomputational implementation of the encryption, they needed torequire a very strong notion called PROG-KDM security. Moreover, they still used an entire page to list all the further necessary
conditions (such as unambiguous parsing) limiting the computa1

Add MoreDY RulesComputational Attacker

the general soundness theorem worked only for certain kinds offirst-order formulas, and the non-negligible subsets of the computational execution had to satisfy a certain computability property.
Later, in the online version of their paper [7] they presented improved computational semantics for the disjunction and existential
quantification, and with that they could make the general soundness proof work for any first-order formula. But they still needed
the computability condition on the non-negligible subsets (not an
important limitation though, but not pretty). In this work, we remove this limitation with a trick in the soundness proof.
Bana and Comon-Lundh proved their general soundness theorem
directly from their definitions. This involved showing that althoughcomputational semantics of their compound formulas are not defined as usual in Tarskian semantics, first-order deduction rules andaxioms are valid with respect to their semantics too. As it turns
out, this actually follows from Fitting’s theorem of embedding firstorder logic into first-order S4 [25]. After introducing the basics, we
detail this relationship in the current work, and show how the BC
general soundness theorem follows from Fitting’s theorem.
In order to tackle key exchange, the necessary element to incorporate in the framework is key usability, an idea introduced in [24]for a different framework. This notion is meant to express whether
a properly generated key, at a certain point of the protocol execution, is still usable for secure encryption or whether it has been
compromised. If a decryption key (or just a key in the symmetriccase) is sent in the clear, the encryption key associated to it cannot
be used for secure encryption any more. Or, a key that was sent ina key cycle, may also have lost its capability to encrypt securely if
the encryption scheme is only IND-CCA2 secure. More generally,
keys can also be compromised in more subtle, non-trace fashion.
For overall consistency of notation, instead of key usability weintroduce the opposite, namely key compromise as a predicate. We
define key compromise predicates both for symmetric and asymmetric encryptions, both for IND-CCA2 [13] and KDM-CCA2 [1,16] cases, and also for INT-CTXT [14] ciphertext integrity. Thereis an essential difference from the way key usability was definedin [24], we explain that at our definition. (Furthermore, the axioms in [24] were introduced to work for the Diffie-Hellmann key
exchange, they are not helpful with other protocols.)
Further essential innovations of this paper are predicates representing adversarial derivability (computability) with oracle access.
This makes the axioms simpler than just using derivability as in[6]. Depending on whether IND-CCA2 or KDM-CCA2 oracles areused, and on whether the encryption is symmetric or asymmetric,
we define four such derivability with oracle access predicates.
We introduce axioms and show that they are computationallysound. The axioms are suitable for (but not limited to) inductive
reasoning: if something is uncompromised up-to a point, then certain newly sent messages do not destroy this property. They arealso entirely modular: Introducing further primitives will not destroy the soundness of these axioms, they do not have to be proved
again. If we want to prove a protocol that uses further primitives such as signatures besides encryption, then we only have to
introduce new axioms for the new primitives. For encryption, thecurrent axioms can still be used unchanged. Hence, a library of axioms can be gradually developed by adding more and more axioms.
A nice feature of our new predicates for key usability and derivability with oracles is that we only have a single axiom requiring
CCA2 security of the encryption: the axiom stating that fresh keys
are uncompromised (with respect to CCA2 security). The rest of
the axioms, such as the one expressing that encryption with uncompromised key hides the plaintext, or the one expressing nonmalleability are immediate consequences of the computational se-

Computational
Assumptions
Are Adjusted
to Symbolic
Formulation
Dolev-Yao Attacker

Figure 1: Soundness of the DY Adversary

symbolic adversaries in the end have to impose some significant
limitations on the computational implementation.
In the BC approach, without axioms, the symbolic adversary isallowed to do anything. As axioms are added, the symbolic adversary’s capabilities are decreasing. Their main theorem is that if the

Add
ComputationallySound Axioms

Computational Attacker

Add More
ComputationallySound Axioms

Bana-Comon Attacker

Figure 2: Soundness of the BC Adversary
axioms are computationally sound, the symbolic adversarial capabilities cover all of the computational adversarial capabilities thatuse bounded number of sessions. This is illustrated in Figure 2.
Clearly, if the symbolic adversary is too strong, security of protocols cannot be proven. Therefore, the aim is to create a library of
axioms that are sound and are sufficient to prove actual protocols.
In [6], Bana et al. introduced several modular, computationally sound axioms, and verified secrecy and authentication of the
Needham-Schroeder-Lowe protocol to illustrate that the technique
can indeed be used to verify actual protocols. However, as Backes
et al. have pointed out in [2], the axioms in [6] were not suitable
when decryption keys were sent around in the course of the protocol (under encryptions for example, in a key distribution). The
current work aims to address this problem.
Before we describe this current work in detail, it is worth asking ourselves, does it really make sense to develop a new techniquewhen such tools as CryptoVerif and EasyCrypt exist? However,
EasyCrypt at its current stage is more for proving properties aboutprimitives, such as CCA2 security from hardness assumptions; it
is not suitable for more complex protocols. CryptoVerif is a very
powerful tool for protocol analysis, but if it fails to prove a protocol, other than its developer, it is difficult for a user to know what
to do. The aim of the BC technique is to construct a relatively simple, intuitive system. If we remove the explanations, the axioms
in this paper are just a few lines, perhaps half a page, and most ofthem are trivial. The BC technique is still lightweight compared to
CryptoVerif or EasyCrypt. BC does not use explicit probabilities,
neither game reductions. Proofs are readable to human, convenient
for human interaction if automated. NSL and the and the symmetric Needham-Schroeder protocols were proven by hand, without
any assumption on parsing unambiguity. Available other proofs of
the NSL protocol including the one with CryptoVerif all assume
unambiguous parsing. The NSL proof with this technique reduces
to 2-3 pages with unambiguous parsing. For an initial decidability
result, see Comon et al. [20].

1.1

Our Work

In this paper we tackle the problem of key exchange, but along
the way we also present various other improvements on the original work of Bana and Comon-Lundh. In their original work [8],2

mantics of the derivability and key-compromise predicates.
We emphasize that we introduce axioms for KDM-CCA2 security to be able to analyze protocols for which KDM security is computationally necessary: Unlike [2], in our case, for those protocols
that do not require KDM security for their computational soundness, the use of our IND-CCA2 axioms is sufficient.
After presenting the axioms and their soundness proofs, we lookat three simple examples in Section 11 to illustrate how the axioms
work with special focus on comparing how the IND-CCA2 and the
KDM-CCA2 axioms are applied to key cycles. We show security
in a case when there are no key cycles, then we present a case when
there is a key cycle and the IND-CCA2 axioms provide an attack
while KDM-CCA2 axioms still prove security. Finally we show acase when there is a key cycle, but as it is under another encryption
it does not danger security even in the IND-CCA2 case and the
security proof goes through. We also show that the axioms in [6]without key compromise are not sufficient to treat these examples.
Finally, we present the result of our proof of the Amended Symmetric Needham-Schroeder Protocol. This protocol first distributes
a session key, and then uses the distributed key to share a secret.
Using the IND-CCA2 and INT-CTXT axioms, we proved that the
key is securely distributed, that the shared nonce remains secret,and that agreement and authentication hold. It is posted online at
the first author’s homepage.
The technique of [8] and also this work allows to avoid all restrictions mentioned before on the computational world. Once a
protocol is proven secure in our symbolic model with respect to aset of axioms, then all properties that the computational implementation has to satisfy for computational security are included in theaxioms. Any number of bad keys are allowed to be generated by theadversary; any number of corrupted, uncorrupted, or dynamicallycorrupted parties can be present. As for parsing of bit strings into
terms, previous soundness results relied on unambiguous parsing.
Within this framework, there is no need for such an assumption. We
do not even need the condition that encryptions, pairing are length
regular (i.e. encryption, pairing of inputs that have the same length
output bit strings of the same length).
As long as indistinguishability properties are not concerned, theonly significant restriction remains that the technique is not capable
to detect computational attacks for which the PPT attacker needs
the number of sessions to grow indefinitely as the security parameter increases. (It is the general soundness theorem that requires
bounded number of sessions, not the axioms.) However, the usual
Dolev-Yao technique is not capable of doing this either. (ProVeriffor example is unbounded only in the sense that it works for arbitrary number of sessions, but still, if an attack is found, that,and the corresponding computational attack uses a given numberof sessions independently of the security parameter.) Nevertheless,it would still be nice to have conditions under which the absence of
successful symbolic BC adversaries means that there are no computational attacks even if unbounded number of sessions are allowed.
For example, if only CCA2 encryptions and pairings are used toconstruct messages, we believe that this statement holds. Analysisof this is left for future work.
The contributions of this paper include (i) relating the BC technique to Fitting’s embedding, (ii) syntax and computational semantics of key compromise and derivability with oracle access, (iii) a
library of axioms for symmetric and asymmetric IND-CCA2 andKDM-CCA2 encryptions and INT-CTXT encryptions as well, (iv)soundness result of the axioms, (v) short examples to illustrate how
the axioms are used with an emphasis on key-cycles, (vi) summaryof the verification of the symmetric Needham-Schroeder protocol
with this tool as a proof of concept. (The NSL proof in [6] can also

be done with the current set of axioms the same way as it was done
there, with minor modifications only.)
The paper is organized as follows: In Section 2, we give the intuitive description of our new predicates. In Section 3, we present
our first-order language, which is an extension of that of BC. We
then summarize in Sections 4 and 5 how Bana and Comon treatedthe symbolic and computational executions in [8], define computational semantics, and present the general soundness theorem. In
Section 6, we show how the BC technique is related to Fitting’s embedding of classical logic in S4, and show how the general soundness result of Bana and Comon-Lundh follows from Fitting’s theorem. Section 7 is devoted to the semantics of the new derivability
predicates with oracles and their axioms, and Section 8 is the samefor key usability. In Section 9 we discuss congruence of the equality predicate. In Section 10 we state and prove our soundness theorem for the axioms. In Section 11, we show a few simple examples
of how inconsistency of certain formulas with the axioms can beproven. Finally, in Section 14, we state the result of the verificationof the amended symmetric NS protocol with our tool.
We thank Pedro Adão, Bruno Blanchet, Rohit Chadha, Hubert
Comon and Guillaume Scerri for helpful suggestions and valuable
discussions.

2.

DERIVABILITY, KEY COMPROMISE

The most important new aspect of the symbolic execution in [8]was to replace the DY technique’s fixed definition of what the symbolic adversary can deduce, x1 , ..., xn ` y, with a derivability
predicate1 x1 , ..., xn  y for which the symbolic semantics is not
fixed. Namely, while in the DY technique, x1 , ..., xn ` y meantthat using only the DY rules y can be computed from x1 , ..., xn , inthe BC case x1 , ..., xn y is given some unfixed symbolic interpretation in an abstract model M for which they only require to satisfy
some (computationally sound) axioms. That is, the axioms express
what the symbolic adversary cannot violate. They do imply thatfrom DY deducibility, satisfaction of the derivability predicate follows, for example, {y}K , K  y. But in the BC system these rules
are not what the adversary can at most do, but what it can certainly
at least do (in other words, the adversary is not allowed to be unable
to do it). The idea is that symbolic interpretation of x1 , ..., xn  yshould be at least as powerful as computability of y from x1 , ..., xn
by some probabilistic polynomial time algorithm, and so the only
limitations that we want to put on symbolic satisfaction of  arelimitations that are derived from computational computability.
One of the major innovations we propose here is that axioms become simpler if we allow the use of some oracles for the adversary.
For example, considering IND-CCA2 public key encryption, it isbetter to introduce a new derivability predicate, x1 , ..., xn aic2 ywith the computational semantics meaning that the interpretation ofy can be derived from the interpretation of x1 , ..., xn by a PPT adversary with the help of decryption oracles that decrypt everythingthat are not results of encryptions on the left hand side. Similarly,
for the symmetric case, we can introduce x1 , ..., xn sic2 y meaning that y can be derived from x1 , ..., xn with the help of decryption oracles and encryption oracles. That is, the algorithm trying
to compute y from the x1 , ..., xn is allowed to submit strings tothe oracles for encryption and also for decryption. The decryption
oracle decrypts as long as the submitted string is not an encryption from x1 , ..., xn or an encryption produced by the encryption
1
Note that in [8] Bana and Comon-Lundh denoted this predicate
as x1 , ..., xn ` y although ` is usually reserved for denoting deducibility in a proof system. We find that somewhat confusing, so
we use the notation x1 , ..., xn  y to emphasize that we do notmean some specific deducibility by it, it is a predicate.

3

• t1 , ..., tn Iakc2
K meaning the lhs compromises (with orancle access) secure asymmetric KDM-CCA2 encryption withK
• t1 , ..., tn Iskc2
K meaning the lhs compromises (with oraclenaccess) secure symmetric KDM-CCA2 encryption with K• t1 , ..., tn Iicn K meaning the lhs compromises (with oracle
access) INT-CTXT ciphertext integrity of encryptions withK.

oracle. The encryption oracles here are needed, because the adversary cannot himself do encryptions (he does not know the key), andfor this reason the IND-CCA2 definition for symmetric encryption
allows the submission to the encryption oracle multiple times. In
fact, for uniformity, we allow it for the public case too, as INDCCA2 is equivalent for the case of multiple submissions to encryption oracles [12]. Similarly, we will also define derivation withoracle accessibility for KDM-CCA2 encryptions, which is somewhat more tricky. But encryption oracles using which keys? The
answer is, keys honestly generated by the agents during the execution. We will use the notation Ofor such derivability with O being
either aic2, sic2, akc2, skc2 or nothing, depending on whether wewant asymmetric or symmetric IND-CCA2 oracles, or asymmetricor symmetric KDM-CCA2 oracles, or no oracles. (O is Fraktur O.)
Our next innovation is key compromise for the case when keys
are sent around. We use the notation x1 , ..., xn IO K, where O
again indexes whether we are talking about IND-CCA2, KDMCCA2, symmetric or asymmetric encryption (there is always someoracle here). The intuitive meaning is that K is compromised by
the messages x1 , ..., xn with access to the given oracles. For example, K, x2 IO K. Or, {K}K 0 , K 0 IO K. Or, if x1 , ..., xn OK,
then x1 , ..., xn IO K. But, presumably, if x1 is just the first halfof K, then x1 IO K may still hold, while x1 OK does not. Thatis, while x1 , ..., xn OK clearly implies x1 , ..., xn IO K, the otherway is not necessarily true. Nevertheless the two properties, as we
will see, behave very similarly, so we chose similar notation forthem. We also consider key compromise for INT-CTXT ciphertext
integrity.

3.

We always drop the index n: t1 , ..., tn Ot and t1 , ..., tn IO K.

4.

LANGUAGE

4.1

The core of the framework used in this paper was introduced by
Bana and Comon-Lundh in [8]. Along with our new innovations,
we present a brief summary of the original system of Bana andComon-Lundh as well.

3.1

SYMBOLIC EXECUTION

In case of the Dolev-Yao adversary, derivability predicates would
have fixed interpretations. For example,  holds in case of a DY
adversary, if the right-hand side can be computed from the left-handside with the DY rules. However, for the symbolic execution, theBC technique allows any interpretation of the predicates (including=) that does not contradict some axioms (introduced later).
Accordingly, let M be any first-order structure that interprets thefunction and predicate symbols of the logic. We denote by DM thedomain of interpretation, and by OM , IOM and =M the relations
on DM interpreting O, IO, and = respectively. Given an assignment σ of elements in DM to the free variables of term t, we write[[t]]σM for the interpretation of tσ in M ([[_]]σM is the unique extension of σ into a homomorphism of F-algebras). For any first-orderformula θ, for any first-order structure M over the functions F andpredicates P, and any assignment σ of the free variables of θ inthe domain of M, the satisfaction relation M, σ |= θ is defined as
usual in first-order logic from the satisfaction of predicates.

Protocols

Bana and Comon-Lundh set up their technique to be convenient
for constraint-solving methods as in [17].
Let Q be a set of control states (not necessarily finite). A protocol is a recursive set of tuples((q, n), (q 0 , n, n0 ), hx1 , ..., xm i , x, ψ, s)

Terms, Predicates, Formulas

where q, q 0 ∈ Q, x1 , ..., xm , x are variables (into which agents readmessages from the adversary), n, n0 are disjoint finite sequences ofnames (corresponding to honestly generated items such as keys,
nonces). ψ is some formula corresponding to agent checks on
incoming messages. For example, ψ can be a formula such asdec(x, k) = n, checking whether the input decrypts to a previously generated nonce n. ψ is over the variables {x1 , ..., xm , x},
the names n, the function symbols F without the rest of the names
and handles, and some subset of the predicate symbols P. Finally,s is the output message, when the transition succeeds. s is built
from the variables {x1 , ..., xm , x}, the names n, n0 , and the function symbols F without the rest of the names and handles.

Terms are built out of a set of function symbols F that contains
an unbounded set of names N and an unbounded set of handles
H. Names and handles are constants (zero-arity function symbols).
We use names to denote items honestly generated by agents, whilehandles denote inputs of the adversary. Let X be an unbounded setof variables. A ground term is without variables.
Let P be a set of predicate symbols over terms. We assume herethat P contains the binary predicate = and is used as t1 = t2 andthe following families of of (n + 1)-ary predicates meaning various
sorts of derivability:• t1 , ..., tn n t for derivability of the rhs from the lhs• t1 , ..., tn aic2
t for derivability of the rhs from the lhs withnaccess to IND-CCA2 oracles in asymmetric case• t1 , ..., tn sic2
n t for derivability of the rhs from the lhs withaccess to IND-CCA2 oracles in symmetric case• t1 , ..., tn akc2
t for derivability of the rhs from the lhs withnaccess to KDM-CCA2 oracles in asymmetric case• t1 , ..., tn skc2
t for derivability of the rhs from the lhs withnaccess to KDM-CCA2 oracles in symmetric case

4.2

Execution of a Protocol and Attacks

In applied π-calculus, frames are sequences of terms with namebinders: a frame φ can be written νn. hp1 7→ t1 , ..., pn 7→ tn iwhere p1 , ...pn are place holders that do not occur in t1 , ..., tn and
n is a sequence of names, but we think of a frame simply as a listof terms ht1 , ..., tn i representing the messages that agents have sent
over the network, that is, messages that the adversary has seen. The
names, variables of φ are the names, variables of t1 , ..., tn .
A symbolic state of the network consists of:and the following key compromise predicates:• t1 , ..., tn Iaic2
K meaning the lhs compromises (with oraclenaccess) secure asymmetric IND-CCA2 encryption with K• t1 , ..., tn Isic2n K meaning the lhs compromises (with oracle
access) secure symmetric IND-CCA2 encryption with K• a control state q ∈ Q together with a sequence of names(randomly) generated so far, n1 , ..., nk• a sequence of constants called handles h1 , ..., hn (recording
the attacker’s inputs)4• a ground frame φ (the agents outputs)• a set of closed formulas Θ (all conditions that must be satisfied in order to reach the state).

• Satisfactions of predicates by M, σ, n, φ (depends on M):s– M, σ, n, φ |= t = t0 if M, σ |= t = t0s
– M, σ, n, φ |= φ̂, s1 , ..., sn Ot
if M, σ |= t1 , ..., tm , s1 , ..., sn Ot.
s
– M, σ, n, φ |= φ̂, s1 , ..., sn IO t
if M, σ |= t1 , ..., tm , s1 , ..., sn IO t.

A symbolic transition sequence of a protocol Π is a sequence((q0 , n0 ), ∅, φ0 , ∅) → ... → ((qm , nm ), hh1 , ..., hm i , φm , Θm )if, for every m − 1 ≥ i ≥ 0, there is a transition rule((qi , αi ), (qi+1 , αi+1 ), hx1 , ..., xi i , x, ψ, s)such that n = αi+1 \ αi , φi+1 = (φi , sσi+1 ), ni+1 = (ni , n),Θi+1 = Θi ∪ {φi  hi+1 , ψσi+1 } where σi+1 = {x1 7→ h1 , ...,
xi 7→ hi , x 7→ hi+1 }. If necessary, some renaming of the sequence
αi+1 ensures the freshness of the names n: n ∩ ni = ∅.
Given an interpretation M, a transition sequence of Π((q0 , n0 ), ∅, φ0 , ∅) → ... → ((qm , nm ), hh1 , ..., hm i , φm , Θm )is valid w.r.t. M if, for every m − 1 ≥ i ≥ 0, M |= Θi+1 .
Examples of symbolic executions can be found in [8] and [6].

4.3

• Satisfactions of constraints by M, σ, n, φ are independent of
M and σ so we define them as satisfaction by n, φ:– Handle(h) for h closed term:sn, φ |= Handle(h) if h ∈ H.
– RanGen(s) for s closed term:sn, φ |= RanGen(s) if s ∈ N
and M, σ |= s = n1 ∨ ... ∨ s = nk .
– t v φ̂, where t is closed term:sn, φ |= t v φ̂ if t is a subterm of some ti– t v s1 , ..., sn , where s1 , ..., sn , t are closed terms:sn, φ |= t v s1 , ..., sn if t is a subterm of some si

Symbolic Satisfaction of Formulas• Satisfaction of any FOL formula by M, σ, n, φ:

M modeled, among others, the predicate t1 , ..., tn  t. In executions we also consider a predicate that we write as φ̂, t1 , ..., tn  t.
This is also an n + 1-arity predicate. φ̂ is just a symbol, not anargument, and it represents the frame containing the messages that
protocol agents sent out, that is, the information available from theprotocol to the adversary. We also use a number of different constraints: Handle(h) means h is a handle, RanGen(x) means that x
was honestly, randomly generated (i.e. appears in the n of the control state); x v φ̂ means that x is a subterm of a message sent out byan agent (i.e. listed in the frame φ), x v ~x means x is subterm of ~x.
dK vd φ̂ means dK occurs somewhere other than in a decryption
position dec( , dK) in φ, and dK vd ~x is analogous (dK may also
occur in a decryption position in ~x, but it has to occur elsewheretoo)2 . Similarly, let K ved φ̂ mean that symmetric key K occurs
somewhere other than in an encryption or decryption position (as{|_|}K or sdec( , K)) in φ, and K ved ~x is analogous (K may also
occur in encryption or decryption position in ~x, but it has to occur
elsewhere too). Let us introduce the following abbreviations:– θ1 ∧θ2 , θ1 ∨θ2 , and ¬θ are interpreted as usual in FOL.
– If x is not under a constraint in θ, interpretations of ∀xθ
and ∃xθ are defined as usual in FOL.
– If x occurs under a constraint in θ, thens
∗ M, σ, n, φ |= ∀xθ iff for every ground term t,sM, σ, n, φ |= θ{x 7→ t}s∗ M, σ, n, φ |= ∃xθ iff there is a ground term t,sM, σ, n, φ |= θ{x 7→ t}• Satisfaction at step m:sM, σ, ((q, n), hh1 , ..., hm i , φm , Θ) |= θsiff M, σ, n, φm |= θ.
We say there is a successful symbolic attack against the security
property θ (a first-order formula) of the protocol if there is a model
M and state of an execution ((q, n), hh1 , ..., hm i , φm , Θ) suchsthat M, ((q, n), hh1 , ..., hm i , φm , Θ) |= ¬θ holds, and moreover,M, ((q, n), hh1 , ..., hm i , φm , Θ) also satisfies the computationally sound axioms that we introduce in the rest of the paper. Thisis the same as saying that there is a successful symbolic attack if at
a certain point of some symbolic execution, the axioms, the agent
checks and the negation of the security property are all consistent.

• x v φ̂, ~x ≡ x v φ̂ ∨ x v ~x• fresh(x; φ̂, ~x) ≡ RanGen(x) ∧ x 6v φ̂, ~x• keyfresh(K; φ̂, ~x) for asymmetric key:x
keyfresh(K; φ̂, ~x) ≡ RanGen(K) ∧ dK 6vd φ̂, ~• keyfresh(K; φ̂, ~x) for symmetric key:
keyfresh(K; φ̂, ~x) ≡ RanGen(K) ∧ K 6ved φ̂, ~x• x 4 φ̂, ~x ≡ ∀h(h v x ∧ Handle(h) → φ̂, ~x  h)Wy ∧ xp2 4 φ̂, ~y , xp1 ∧ ...
~x 4 φ̂, ~y ≡p (xp1 4 φ̂, ~E XAMPLE 4.1. We show the beginning of a possible branch inthe symbolic execution of a single session of the NSL protocol.
(q0 , ∅, φ0 , ∅)•∧ xpn 4 φ̂, ~y , xp1 , ..., xpn−1 )(q1, H1, φ1, Θ1 ) (q2, H2, φ2, Θ2 ) (q3 , H3 , φ3 , Θ3 )
-•
-•
-•

where with qjA , qjB counting the states of the A and B, q0 =(q0A , q0B , n0 ), and q1 = (q1A , q0B , n1 ), and q2 = (q1A , q1B , n2 ), andq3 = (q2A , q1B , n3 ) and q4 = (q2A , q2B , n4 ). In other words, weinterleave the actions of A and B, as in an expected execution andassume that the two processes were first activated. Let W denotethe unary predicate that tells if its argument is an agent name.

Where p runs through all permutations of 1, ..., n. Further, for symmetric encryption we also require for x 4 φ̂, ~x that if any R is arandom input of an encryption in φ̂, ~x, x then the only way it canappear in x is within that same encryption.
If M is a first-order model, satisfaction of predicates and consstraints in a symbolic execution (denoted by |= ) is defined recursively: Let n = (n1 , ..., nk ) be a list of names and φ = ht1 , ..., tm i
a list of closed terms. Let σ be a substitution of free variables ofs
the rhs of |= with elements in the domain of M.

• n0 = (),φ0 = hi,Θ0 = ∅• n1 = (KA , KB ),H1 = ∅,
φ1 = hA, B, eKA , eKB i,
Θ1 = ∅• n2 = (KA , KB , N1 , R1 ),H2 = hh1 i,
1
φ2 extends φ1 with {hN1 , Ai}ReKB ,
Θ2 = {φ1  h1 }2
In this paper, we will use the notation {x}ReK and dec(y, dK) for
both symmetric and asymmetric encryptions with random input R,
where in the symmetric case, eK = dK = K. We use {|x|}R
K andsdec(y, K) for symmetric encryption and decryption only.

5

• n3 = (KA , KB , N1 , R1 , N2 , R2 )H3 = hh1 , h2 i,
φ3 extends φ2 with2{hπ1 (dec(h2 , dKB )) , hN2 , Bii}ReK

π2 (dec(h2 ,dKB ))• for all i = 0, ..., m − 1, si = ((qi , ni ), hi , φi , Θi ), φi+1 =(φi , ui ), [[ui ]]τ = b0i+1• for every i = 0, ..., m − 1, there is a configuration γi0 of themachine Mc such that γi `∗M γi0 `∗M γi+1 and γi0 is in asending state, the sending tape containing bi+1 , γi+1 is in a
receiving state, the receiving tape containing b0i+1• for all i = 0, ..., m−1, the bit strings τ , {h1 7→ b1 , ..., hi+1 7→
bi+1 } satisfy all agent checks listed in Θi+1 .

,Θ3 = Θ2 ∪ {φ2  h2 , W (π2 (dec(h2 , dKB )))}
• n4 = (KA , KB , N1 , R1 , N2 , R2 , R3 ),H4 = hh1 , h2 , h3 i,
3φ4 extends φ3 with {π1 (π2 (dec(h3 , dKA )))}ReKB ,Θ4 = Θ3 ∪ {φ3  h3 , π1 (dec(h3 , dKh )) = N1 ,π2 (π2 (dec(h3 , dKA ))) = B},• H5 = hh1 , h2 , h3 , h4 i,
φ5 = φ4 ,Θ5 = Θ4 ∪ {φ4  h4 , dec(h4 , dKB ) = N2 },Here `∗M means what the machine (in whatever model it is defined)
can compute via a sequence of computational steps.

5.2

Let M be a model such that π2 (dec(h2 , dKB )) = A, and h2 =M
R21{hN1 , Ai}ReKB , and h3 =M {hN1 , hN2 , Bii}eKA , and h4 =M
R3{N }eKB , and M is simply the classical Dolev-Yao deduction
relation. Then the execution sequence above is valid w.r.t. M,
and this corresponds to the correct execution of the NSL protocol
between A and B.
E XAMPLE 4.2. Consider again Example 4.1, and a model Mr2
in which N0 , {N1 , N2 , B}ReKA M {N1 , N0 , B}eKA for an honestly generated nonce N0 that can be chosen by the attacker; thetransition sequence of the previous example is also valid w.r.t. thismodel. This however yields an attack, using a malleability property of the encryption scheme. Discarding such attacks requires
some properties of the encryption scheme (for instance IND-CCA).
It can be ruled out by the axioms that we will introduce. From thisexample, we see that unexpected attacks can be found when someassumption is not explicitly stated as an axiom to limit adversarial
capabilities.

5.

COMPUTATIONAL EXECUTION

We now summarize the computational semantics. Short proofsof Theorems 5.2 and 5.3 are in the Section 6 using Fitting’s embedding of classical logic into S4 [25].

5.1

Computational satisfaction of formulas

We recall the computational interpretation of the original predicates, = and  here and the semantics of compound formulas. The
difference between our presentation here and that of [7] is that we
do not assume any computability condition on non-negligible sets
any more, as we apply a trick in the soundness proof that makes it
unnecessary. Interpretations of the new predicates are presented inlater sections.
Let (Ω0 , Σ0 , Prob0 ) be the probability space of infinite fair cointosses, Ω0 being the the set of infinite bit strings, Σ0 the measurable
sets generated by fixing finitely many outcomes, and Prob0 the
probability measure assigning the probabilities to the sets of Σ0 .
For a finite bit string b ∈ {0, 1}∗ of length n, let b̄ ⊂ Ω0 denotethe set of infinite bit strings for which the initial n bits are exactlyb. Let Σf be the set generated by finite unions intersections, andsubtractions of sets of the form b̄ (including Ω). Σ0 is the σ-closureof Σf .
Let Mc be an interactive PPT Turing machine with a special
challenge control state qch . We may regard this machine as an
attacker, who moves to the state qch when he thinks that he isready to break the security property. As usual, the machine takes
the security parameter 1η as an initial input. Mc interacts withthe protocol agents, which are also assumed to be interactive PPTTuring machines, and they respond to the calls of the adversary.
Since once η is fixed, such an execution is probabilistic, and foreach security parameter η, we denote underlying probability spaceby (Ωη , Ση , Probη ), which is just a copy of the (Ω0 , Σ0 , Prob0 )above. We denote the elements of Ωη by ω η . (Actually, the adversary’s random string and the agent random strings are separate,
but as there are finitely many of them, they can be thought to be
on a single string) Each ω η is one particular random string. LetΩ = (Ωη )η∈N . Let τ (ω η ) be the assignment of all fixed bit string
evaluations τ (n) of names given for ω η . For a given n name, we
just use simply n(ω η ) for the bit string τ (ω η )(n).
By a non-negligible set of coins S, we mean S = (S η )η∈N ,where for all η ∈ N, S η ∈ Σηf , and Probη {S η } is non-negligible
function of η. We use the notation S1 ⊆ S2 for S1 = (S1η )η∈N
and S2 = (S2η )η∈N non-negligible sets of coins if for all η ∈ N,
S1η ⊆ S2η . In what follows, S is any such non-negligible set ofcoins. The domain of interpretation D(S) = D is the same for
all S: PPT algorithms that take as input η, read from the randomtape ω η , and output a bit string. (As ω η is infinite coin tosses, thealgorithms of course do not read it all, they terminate in polynomial
time.)We recall the interpretations of = and  from [8]: Let σ be asequence of PPT machines (e.g. one for each free variable xi of θ):
Ax1 , ..., Axn ∈ D. For example, and Ax can be the evaluation of
any name (in which case Ax (η, ω η ) = n(ω η ), or any value for ahandle computed by the adversary, or some more complex object.
Let σ(ω η ) denote the assignments x1 7→ Ax1 (η, ω η ), ..., xn 7→
Axn (η, ω η ). If st(η, ω η ) is a statement, then for any fixed S =(S η )η∈N , instead of “for all η ∈ N and all ω η ∈ S η , st(η, ω η )”,Computational Execution

Following Bana and Comon, we consider a family of computational algebras, parametrized by a security parameter η, in which
each function symbol is interpreted as a polynomially computablefunction on bit strings (that may return an error message). Givena sample τ of names, every ground term t can be interpreted asa bit string [[t]]τ in such a way that [[_]]τ is a homomorphism of
F-algebras (a name n is interpreted as a bit string τ (n)). Moregenerally, if σ is an assignment of the variables of t to bit strings,[[t]]στ is the (unique) extension of τ (on names) and σ (on variables)
as a homomorphism of F-algebras.
Given a set of transition rules, a computational state consists of• a symbolic state s (that is itself a tuple ((q, n), h, φ, Θ))• a sequence of bit strings hb1 , ..., bm i (attacker outputs)• a sequence hb01 , ..., b0m i of bit strings (agents’ outputs)• the configuration γ of the attacker.
Given a PPT interactive Turing machine Mc and a sample τ , asequence of transitions(s0 , ∅, b~00 , γ0 ) → ... → (sm , hb1 , ..., bm i , b01 , ..., b0m , γm )is (computationally) valid with respect to Mc and τ if
• s0 → · · · → sm is a transition sequence of the protocol
6

we simply write “for all ω ∈ S, st(ω)”.

T HEOREM 5.2 (T RACE M APPING ). Let Π be a protocol, s1 →... → sm be a symbolic transition sequence of Π and Mc be aprobabilistic polynomial time interactive Turing machine. If there
is a non-negligible set of coins S such that, for any ω ∈ S, there is asequence of transitions (s0 , b~0 , b~00 , γ0 ) → · · · → (sm , b~m , b~0m , γm )that is computationally valid w.r.t. Mc , τ (ω) and γm is in the chalc
lenge state qch , then for any set of FOL formulas Φ, Mc , Π, S |= Φimplies there is a symbolic model M such that s0 → · · · → sm issa valid symbolic execution w.r.t. M and M, sm |= Φ.

c• For the equality predicate, Mc , Π, S, σ |= t1 = t2 iff there
is a subset S 0 ⊆ S such that S \ S 0 is negligible, and for all
σ(ω)
σ(ω)
ω ∈ S 0 , [[t1 ]]τ (ω) = [[t2 ]]τ (ω) .
c• For the derivability predicate, Mc , Π, S, σ |= φ̂, t1 , ..., tn tif for all non-negligible S 0 ⊆ S, there is a non-negligible
S 00 ⊆ S 0 and a PPT Turing machine A such that for all ω ∈
σ(ω)
σ(ω)
σ(ω)
S 00 , A([[φm(ω) ]]τ (ω) , [[t1 ]]τ (ω) , ..., [[tn ]]τ (ω) , a(ω), r(ω)) =σ(ω)[[t]]τ (ω) where m(ω) is the step at which Mc reached thechallenge state, a(ω) stands for the protocol adversary’s output and r(ω) is some fresh input from the random tape.
• If P is a constraint, ~t are closed terms then Mc , Π, S, σ |=P (~t) iff there is S 0 ⊆ S such that, S\S 0 is negligible, and forall ω ∈ S 0 , the unique valid computation of Π with respect
to Mc , τ (ω) yields a state (((q, n), h, φ, Θ), b, b0 , γ) in thescontrol state qch such that n, φ |= P (~t).

T HEOREM 5.3 (G ENERAL S OUNDNESS ). If there is a successful computational attack such that the number of sessions ofhonest agents are bounded in the security parameter, then there isalso a successful symbolic attack.

5.3

About the fresh r(ω), note we assumed for any non-negligible set
S that S η ⊆ Σηf and not S η ⊆ Ση0 , so there can always be fresh
random bits generated inside S.
Satisfaction of compound formulas are defined the following way.

Equality is a Congruence:• x = x, and the substitutability (congruence) property ofequal terms holds for = and .
Core Axioms for the Derivability Predicate:• Self derivability: φ̂, ~x, x  x• Increasing capabilities: φ̂, ~x  y −→ φ̂, ~x, x  y• Commutativity: If ~x0 is a permutation of ~x, thenφ̂, ~x  y −→ φ̂, ~x0  y• Transitivity of derivability:
φ̂, ~
x~
y ∧ φ̂, ~x, ~y  ~z −→ φ̂, ~x  ~z• Functions are derivable: φ̂, ~x  f (~x)
This axiom is sound as long as functions are interpreted as
PT computable algorithms.
Axioms for Freshly Generated Items:• No telepathy: fresh(x; φ̂) −→ φ̂ 6  x
This axiom is sound as long as RanGen() items are generated
so that they can only be guessed with negligible probability.
A more general version is also possible as
fresh(x; φ̂, ~x) ∧ ~
x 4 φ̂ −→ φ̂, ~x 6 x• Fresh items do not help to compute:fresh(x; φ̂, ~x, y) ∧ ~x, y 4 φ̂ ∧ φ̂, ~x, x  y −→ φ̂, ~xyEquations for the fixed function symbols: For example, forsymmetric encryption sdec({|x|}R
K , K) = x, and for pairing,
π1 (hx, yi) = x; π2 (hx, yi) = y. Function of error is errorf (..., ⊥, ...) = ⊥, etc.

c

• Mc , Π, S, σ |= θ1 ∧ θ2cc
iff Mc , Π, S, σ |= θ1 and Mc , Π, S, σ |= θ2 .
c
• Mc , Π, S, σ |= θ1 ∨ θ2 iff for any S 0 ⊆ S non-negligible,
there is a S 00 ⊆ S 0 non-negligible such thatcceither Mc , Π, S 00 , σ |= θ1 or Mc , Π, S 00 , σ |= θ2 .
c
0c
• M , Π, S, σ |= θ1 → θ2 iff for all S ⊆ S non-negligible,cc
Mc , Π, S 0 , σ |= θ1 implies Mc , Π, S 0 , σ |= θ2cc0• M , Π, S, σ |= ¬θ iff for all S ⊆ S non-negligible,c
Mc , Π, S 0 , σ |6= θcc• M , Π, S, σ |= ∃x.θ iff for any S 0 ⊆ S non-negligible, there
is a S 00 ⊆ S 0 non-negligible and a PT machine Ax such thatc
Mc , Π, S 00 , σ, Ax |= θcc
• M , Π, S, σ |= ∀x.θ iff for any probabilistic polynomial timecmachine Ax , Mc , Π, S, σ, Ax |= θ• If x is a constrained variable, the interpretation of ∃x.θ iscanalogous to the symbolic case: M, Π, S, σ |= ∃x.θ if and0
only if for every non-negligible S ⊆ S there is a nonnegligible S 00 ⊆ S 0 and a ground term t, such that the satisc
faction M, Π, S 00 , σ |= θ{x 7→ t} holds.
• If x is a constrained variable, the interpretation of ∀x.θ iscanalogous to the symbolic case: M, Π, S, σ |= ∀x.θ if andconly if for every ground term t, the satisfaction M, Π, S, σ |=θ{x 7→ t} holds.
cccAxioms for Equality and Derivability

We recall the core axioms presented in [6]. As usual, unquantified variables are universally quantified. Unless noted otherwise,
they are always sound.

6.

THE FITTING CONNECTION

The trace mapping and the general soundness theorems for arbitrary first-order formulas were proven directly from their definitions by an elaborate argument in [7]. We have realized however,that they are rather easy consequences of Fitting’s embedding offirst-order logic into first-order S4 [25]. The non-Tarskian computational semantics of first-order formulas that naturally arouse in
the BC technique turns out to be a special kind of Kripke semantics of first-order S4 composed with Fitting’s embedding of FOL
into first-order S4. We detail this connection here, and show how
trace mapping and general soundness follow from Fitting’s theorem. This section assumes basic familiarity with S4 modal logic
and its first-order extension as well as Kripke semantics.
For any first-order formula θ, consider the Fitting transformation
θ 7→ θ∗ , where θ∗ is a formula of first-order S4, and is definedrecursively as follows:c

Mc , Π |= θ iff Mc , Π, Ω |= θ and Π |= θ if Mc , Π |= θ for every
Mc and qch .
Given a protocol Π, we say that there is a successful computational attack against the security property θ (a first-order formula)of the protocol if there is a an attacker Mc and a non-negligible setccof coins S such that Mc , Π, S |= ¬θ (which is the same as Π |6= θ).
Despite that semantics of the compound formulas is not as usualin first-order logic, we prove in Section 6 that as a consequence ofFitting’s embedding [25] of classical logic into S4, the following
theorems hold.
T HEOREM 5.1 (F ITTING ’ S E MBEDDING ). With the above semantics, first-order deduction rules are sound.

7c• For any atomic formula θ, let θ∗ ≡ 23θ.
• (¬θ)∗ ≡ 2¬θ∗• (θ1 → θ2 )∗ ≡ 2(θ1∗ → θ2∗ )• (θ1 ∧ θ2 )∗ ≡ (θ1∗ ∧ θ2∗ )• (θ1 ∨ θ2 )∗ ≡ 23(θ1∗ ∨ θ2∗ )• (∀xθ)∗ ≡ ∀xθ∗• (∃xθ)∗ ≡ 23∃xθ∗s4That is, Mc , Π, S, σ |= t1 = t2 iff Mc , Π, S, σ |= 23t1 = t2 .
The same is true for constraints. Hence we have this for all atomic
s4
formulas. |= for compound formulas is defined as usual in Kripke
s4
semantics. For example, Mc , Π, S, σ |= θ1 ∨ θ2 if and only if
s4
s4
c
c
M , Π, S, σ |= θ1 or M , Π, S, σ |= θ2 .
cComparing the definition of |= in Section 5.2 for compound
formulas with Fitting’s embedding, for any first-order formula θ,

Fitting in [25] put 23 everywhere and noted that it is redundant infront of the conjunction. It is also easy to check that if the Barcan
formula and its converse (∀x2θ ↔ 2∀xθ) are assumed (that is,when the domain does not change from possible world to possible
world in the Kripke structure), then 23 is also redundant in front of
the universal quantification (as θ∗ ↔ 23θ∗ holds in our definitions
for all θ). In our computational situation the domain is unchanged
as we show below. So in this paper we assume the Barcan formulaand its converse.
Fitting’s theorem says that any formula θ is derivable in firstorder logic if and only if θ∗ it is derivable in S4 with the Barcan
formulas. (Without the Barcan formulas, (∀xθ)∗ ≡ 23∀xθ∗ has
to be written above).
Observe that if we think of non-negligible sets as possible worlds,
and the subset relation as accessibility (that is, if S 0 is accessible
from S iff S 0 ⊆ S), then we can define a computational Kripke
semantics: For our predicates, consider the S4 satisfaction relations4
Mc , Π, S, σ |= that we define almost the same way as the BC comc
putational satisfaction |= of Section 5.2 is defined, except that wedrop the "for all non-negligible S 0 ⊆ S, there is a non-negligible
S 00 ⊆ S 0 " phrase, and replace S 00 with S in the remaining of thedefinition. For example, the satisfaction of derivability becomes:cs4

Mc , Π, S, σ |= θ ⇐⇒ Mc , Π, S, σ |= θ∗ .
For a set of first-order formulas Φ, let Φ∗ mean the set that we getby applying the Fitting transformation to all formulas in Φ. Sinces4with |= , our computational semantics is a special kind of Kripke
s4
semantics, Fitting’s theorem implies that if Mc , Π, S, σ |= Φ∗ holds
s4 ∗
FOL
c
and if Φ `θ, then M , Π, S, σ |= θ . So we also have that ifcc
Mc , Π, S, σ |= Φ holds and if Φ `FOL θ, then Mc , Π, S, σ |= θ.
This is exactly Theorem 5.1.
The Barcan formula and its converse hold, as the domain D does
not depend on the non-negligible sets.
For Theorem 5.2, note that it is assumed in the theorem that forall ω ∈ S the computational execution has the same length m andthe symbolic part of their traces, si agree. Remember that the symbolic states have the transition conditions Θi in them. So at thecchallenge state, we have Mc , Π, S |= Θm ∧ Φ. Note that since on
the traces, si agree, the terms that are in the frame also agree forall trace ω ∈ S. Therefore, φ̂ in the formulas of θm and Φ can be0
replaced by the list of terms in the frames. Let θmand Φ0 denoteccthe formulas we receive this way. Then, M , Π, S |= Θ0m ∧ Φ0 .
s4This is the same as Mc , Π, S |= (Θ0m ∧ Φ0 )∗ , that, by Fitting’s theorem means that Θ0m ∧ Φ0 is first-order satisfiable (because (Θ0m ∧Φ0 )∗ is S4 satisfiable). Hence there is a symbolic model M withs
M |= Θ0m ∧Φ0 . As Θ0m and Φ0 have no frames in them, it is easy tossee from the symbolic satisfaction that M, sm |= Θ0m ∧ Φ0 is alsosatisfied as satisfaction does not depend on the state. Finally, as insm , the frames contain exactly the terms with which we replaceds
φ̂, we can now write them back and receive M, sm |= Θm ∧ Φ.
Which also means that Θm and Φ are first-order consistent.
Finally, for proving Theorem 5.3, consider the following. If there
is a computational attack, that is, if the negation of the security formula θs is computationally satisfied by some Mc , Π, S, then, as
long as only bounded number (in the security parameter) of sessions are allowed, the maximum number of different (with respectto ω) symbolic transitions s1 → · · · → sm does not depend on
the security parameter. Therefore, S can be split (up to negligible
probability) into a fixed number of non-negligible subsets on eachof which s1 → · · · → sm is independent of ω. Pick one, call it S 0 .
Then Mc , Π, S 0 computationally satisfies ¬θs as well as all computationally sound axioms (denote the set by ΦA ), and Θm also:c
Mc , Π, S 0 |= Θm ∧ ΦA ∧ θs . Hence, By Theorem 5.2 there issa symbolic model M such that M, sm |= Θm ∧ ΦA ∧ θs , which
exactly means that there is a symbolic attack.
Note, although by Fitting’s theorem, the first-order deduction
rules are computationally sound, it is not possible in the current
formulation to deduce security properties from the axioms only by
first-order deduction rules and nothing else. The BC technique has
no formulas expressing the transition system, no formulas saying
the agents follow the protocol roles. Explicit time and some axiom
for induction would also be needed as in [9]. These are taken careby the symbolic execution.

s4• For the derivability predicate, Mc , Π, S, σ |= φ̂, t1 , ..., tn tif there is a PPT Turing machine A such that for all ω ∈ S,
σ(ω)
σ(ω)
σ(ω)
σ(ω)
A([[φm(ω) ]]τ (ω), [[t1 ]]τ (ω), ..., [[tn ]]τ (ω), a(ω), r(ω))=[[t]]τ (ω)
cwhere m(ω) is the step at which M reached the challenge
state, a(ω) stands for the protocol adversary’s output andr(ω) is some fresh input from the random string.
s4

For an arbitrary θ first-order S4 formula, Mc , Π, S, σ |= 2θ is des4
fined to hold if and only if Mc , Π, S 0 , σ |= θ holds for all nons4
0cnegligible S ⊆ S, and M , Π, S, σ |= 3θ is defined to hold if ands4
only if Mc , Π, S 0 , σ |= θ holds for some non-negligible S 0 ⊆ S.
Taking θ to be φ̂, t1 , ..., tn  t, and applying 23 to the above definition of S4 satisfaction, we receive the computational satisfaction
cof Bana and Comon-Lundh. That is, Mc , Π, S, σ |= φ̂, t1 , ..., tn ts4
cif and only if M , Π, S, σ |= 23φ̂, t1 , ..., tn  t.
Note also that for the equality predicate and for the constraints,"for all non-negligible S 0 ⊆ S, there is a non-negligible S 00 ⊆ S 0 "can be freely inserted in the definition, as the resulting definition isequivalent with the original: for example, if for all non-negligibleσ(ω)
S 0 ⊆ S, there is a non-negligible S 00 ⊆ S 0 such that [[t1 ]]τ (ω) =σ(ω)[[t2 ]]τ (ω) holds on S 00 , then it also holds up to negligible probability on S, because if there were a non-negligible subset S 0 ⊆ S on
σ(ω)
σ(ω)
which [[t1 ]]τ (ω) 6= [[t2 ]]τ (ω) were true, then this S 0 would not havesome non-negligible subset S 00 on which they are equal, a contradiction. So BC could have defined satisfaction of equality asc• For the equality predicate, Mc , Π, S, σ |= t1 = t2 iff for
all non-negligible S 0 ⊆ S, there is a non-negligible subset
σ(ω)
σ(ω)
S 00 ⊆ S 0 such that for all ω ∈ S 00 , [[t1 ]]τ (ω) = [[t2 ]]τ (ω) .

7.
8

DERIVABILITY WITH ORACLESto depend on a secret nonce. This is necessary for receiving niceaxioms for the KDM case, and we explain the reason at the axioms.
Still, assuming the usual KDM security is enough to prove that an
unsent key is uncompromised with such oracle access. The reason
is that when a KDM attack is constructed from the protocol attack,the KDM attacker has access to the items generated by the honest
agents except for the secret keys and for the random inputs to theencryptions.

Syntax of various types of derivability with oracles was introduced in Section 3. Here we define their computational semantics
and list a number of axioms that are computational sound.

7.1

Computational Semantics of Derivability
with Oracles

Let Osic2 be the following oracle: It first takes a list of honestly
generated keys K and some additional list C of ciphertexts. The oracle can be called for encryption by submitting a string to encryptalong with the encrypting key’s place number in K. The oracle honestly generates the desired encryption, returns the result and adds itto the list C. The oracle can also be called for a decryption again
with specifying the key and providing a ciphertext. If the ciphertext
is not one of those in C, the oracle outputs the decryption. Let Oskc2
take K and C as above, but also τ (L) assignment of bit strings toa finite set of name symbols L. The oracle accepts descriptions offunctions of the names L, the ciphers C and the keys K, into which
he substitutes the corresponding bit strings, computes the function
and then encrypts the result with the specified key and adds it to
C. Decryption works as for Osic2 . Let Oaic2 and Oakc2 be the analogous notions for public key encryption. PPT algorithms with oracleO
access will be written as AO , BO .
s4
The meaning of the definition is that Mc , Π, S, σ |= φ̂, ~x O xO
holds if there is a PPT algorithm A that, for ω ∈ S, receiving the
σ(ω)
σ(ω)
bit strings [[φ̂, ~x]]τ (ω) , it outputs the bit string [[x]]τ (ω) . In the computation AO can request encryption and decryption oracles corresponding to the honest keys, but it will only receive a decryption if
the submitted bit string is not a bit string corresponding to an encryption in φ̂, ~x or a bit string received from the encryption oracle.
Outside S, nothing is required.

7.2

Core Axioms for the Derivability Predicate with Oracles.
• Let SameEnc(~x; ~y ) be the constraint that there is a one-toone correspondence between the honest encryption terms of~x and ~
y such that the corresponding encryption terms areequal (with respect to the equality predicate). Then
SameEnc(~x; ~y) ∧ ~
x, x = ~y , y −→ (φ̂, ~x Ox ↔ φ̂, ~y Oy).
• More oracles help more: If the oracles of O are more power0
ful than the oracles of O0 , then φ̂, ~x O x −→ φ̂, ~x Ox.
O
In particular, φ̂, ~x  x −→ φ̂, ~x  x andφ̂, ~x aic2 x → φ̂, ~x akc2 x and φ̂, ~x sic2 x → φ̂, ~x skc2 x
OO• Increasing capabilities: φ̂, ~x  y −→ φ̂, ~x, x  y• Commutativity: If ~x0 is a permutation of ~x, thenφ̂, ~x Oy −→ φ̂, ~x0 Oy• Transitivity: φ̂, ~x O~y ∧ φ̂, ~x, ~y O~z −→ φ̂, ~x O~z• Decryption Oracles help:
RanGen(K) ∧ φ̂, ~
x y
O

R
∧ ∀xR(y = {x}Rx)eK → {x}eK 6v φ̂, ~D EFINITION 7.1. Semantics of Derivability with Oracles: Let
Mc , Π, S, σ be as before. Let a(ω η ) denote the protocol adversary
output as it reaches the challenge state on the random input ω η ,and let m(ω η ) denote the number of moves till then. We writes4
Mc , Π, S, σ |= φ̂, ~x O x iff there is a PPT Turing machine AO
such that for all ω ∈ S,

σ(ω)
σ(ω)
σ(ω)
AO [[φm(ω) ]]τ (ω) , [[~x]]τ (ω) , a(ω), r(ω) = [[x]]τ (ω)−→ φ̂, ~x Odec(y, dK).
This expresses that if y is computable and is not an encryption in φ̂, ~x, then dec(y, dK) is also computable from thesame items as the decryption oracle can be called. We do nothave to require that y is none of the encryptions done by theoracles, because if they were, then the decryption is known
to the submitter. Again, this follows purely from the definition of O, CCA2 security of the encryption is not required.
This axiom together with the transitivity axiom easily imply

where r(ω) is some fresh (not used for the computation of φ̂, ~x, x)
random input from the random string. On each ω, if the tuple(((q, n), h, φ, Θ), b, b0 , γ) denotes the state yielded by the uniquevalid computation of Π with respect to Mc and τ (ω), then the oracles receive in K all keys (bit strings) corresponding to the keysσ(ω)
in n, and in C all strings of the form [[{z}ReK ]]τ (ω) with R and K

RanGen(K) ∧ φ̂, ~x  y ∧ φ̂, ~x, dec(y, dK)  z
OOR∧ ∀xR(y = {x}Rx) −→ φ̂, ~x Oz.
eK → {x}eK 6v φ̂, ~This replaces the non-malleability axiom of [6] for the derivability predicate. With tiny modifications, it is possible torewrite the NSL proof presented in [6] for using the Opredicate and this simpler axiom instead of the  predicate with
the non-malleability axiom there.
Axioms for Freshly Generated Items. These axioms are soundfor the same reason as the corresponding ones for  were:• No telepathy: fresh(x; φ̂, ~x) ∧ ~
x 4 φ̂ −→ φ̂, ~x 6 Ox(implies no-telepathy axiom without oracles). This is soundas long as RanGen() means generation with negligible guessing probability only.
• Fresh items do not help to compute: fresh(x; φ̂, ~x, y) ∧~
x, y 4 φ̂ ∧ φ̂, ~x, x Oy −→ φ̂, ~
x Oy

s

x. In τ (L), the KDM oracles
names in n, and n, φ |= {z}ReK v φ̂, ~receive all assignments of names in n̄ to bit strings, except (in thesymmetric case), for those that occur as random inputs R to theencryptions in C.
We shorten this asOx) = x,Mc , Π, S, σ ||= AO (φ̂, ~implicitly assuming the algorithm has access to the protocol adversary’s knowledge and to random bits. LetcAxioms for Derivability with Oracles

The following axioms (except for the second and last entry of
the core axioms for derivability predicates) are very similar to theones in Section 5.3, and are just as trivial. The second entry of thecore axioms for derivability predicates with oracles is also triviallycomputationally sound.

s4

Mc , Π, S, σ |= φ̂, ~x Ox iff Mc , Π, S, σ |= 23(φ̂, ~x Ox).
Note that in the KDM case, the submitted functions may depend on
randomly generated items that differ from the secret keys but are
not accessible to the protocol adversary. For example, it is allowed

φ̂, ~x, x Ox is implied by the more oracles help more axiom and theself-derivability axiom of derivability predicate. Also, φ̂, ~x Of (~
x).
9

8.

KEY USABILITY• Or Mc , Π, S, σ ||=Syntax of various types of key usability was introduced in Section 3. Here we define their computational semantics and list a
number of axioms that are computational sound.

8.1

O
AO
x, {x}Rx, {x}R
21 (φ̂, ~eK ) 6= A22 (φ̂, ~eK )and for some (hence for all) R0 fresh random input generated
inside S, Mc , Π, S, σ ||=IND-CCA2 and KDM-CCA2 cases

8.1.1

0

Semantics of IND-CCA2 Key CompromisecRecall from Section 6 that 23 means "there is a non-negligible
S 0 ⊆ S such that for all S 00 ..." Also note that as we required our
non-negligible sets to be in Σf , it is always possible to toss freshcoins inside the non-negligible sets.
Note that while R does not have to be generated inside S, R0
does. In particular, S may actually depend on R, which is essential
for the usability of the axioms, because the non-negligible sets on
which we need to apply the axioms may depend on values of an
encryption, and hence values of R. On the other hand, S is not allowed to depend on R0 , which is essential for proving that a freshly
generated key is not compromised.
Note, in the KDM case, x does not have to be computed fromφ̂, ~x, it could be a secret nonce. This corresponds to the fact that in
the semantics of O in the KDM case (as we noted after the definition) we allowed the functions submitted to the oracles to depend
on such items not known to the protocol adversary.

8.1.2

Core Axioms for the Key Compromise Predicate.
• Let SameEnc(~x; ~y ) be the constraint as before. Then
SameEnc(~x; ~y) ∧ ~
x, x = ~y , y −→ (φ̂, ~x IO x ↔ φ̂, ~y IO y).
O• Derivability implies compromise: φ̂,~x  K−→ φ̂,~x IO K
If K is computable for the adversary, then it is compromised.
Note, this axiom and the self derivability axiom (from 7.2)
imply that φ̂, ~x, K IO K• Increasing capabilities for key compromise:φ̂, ~x IO K −→ φ̂, ~x, x IO K• Commutativity: If ~x0 is a permutation of ~x, thenOφ̂, ~x I K −→ φ̂, ~x0 IO K
• Transitivity: φ̂, ~x O~y ∧ φ̂, ~x, ~y IO K −→ φ̂, ~x IO K
The intuitive reason is very clear: ~y just contains extra information, that can be computed from φ̂, ~x, so it is not actuallyneeded in the compromise. This, and the functions are derivable axiom imply φ̂, ~x, f (~x) IO K −→ φ̂, ~x IO K. With
the increasing capabilities axiom, we get φ̂, f (~x) IO K −→O
φ̂, ~x I K. We refer to these as function application.
• Uncompromised keys securely encrypt:• R is generated honestly, statistically independently of the inO(φ̂, ~x) andterpretations of φ̂, ~
x, AO
1
c
• Either M , Π, S, σ ||=O
AO
x, {AOx)}Rx, {AOx)}R
21 (ϕ, ~1 (ϕ, ~
eK ) = A22 (ϕ, ~1 (ϕ, ~eK )and for some (hence for all) R0 fresh random input generated
inside S, Mc , Π, S, σ ||=
O

0

O
AO
x, {0|A1 (ϕ,~x)| }R
x, {0|A1 (ϕ,~x)| }R
21 (ϕ, ~eK ) 6= A22 (ϕ, ~eK )• Or Mc , Π, S, σ ||=O
AO
x, {AOx)}Rx, {AOx)}R
21 (φ̂, ~1 (φ̂, ~eK ) 6= A22 (φ̂, ~1 (φ̂, ~eK )and for some (hence for all) R0 fresh random input generated
inside S, Mc , Π, S, σ ||=O

0O

Axioms for CCA2 Key Compromise

We now present the axioms for key compromise. First the coreaxioms for which soundness does not need CCA2 security.

D EFINITION 8.1 (K EY C OMPROMISE ). The define the relas4s4
x 64
tion Mc , Π, S, σ |= φ̂, ~x IO K to hold if either Mc , Π, S, σ |= ~Oφ̂ ∨ ¬RanGen(K), or there are R, PPT algorithms AO
21 , A22 , andAO
1 (in the IND case) or x (in the KDM case) such that:In the the IND case0s4

Let Mc , Π, S, σ |= φ̂, ~x IO x iff Mc , Π, S, σ |= 23(φ̂, ~x IO x).

The idea of key usability is that a key has been uncompromised,that is, it can be used for safe encryption. To match the computability predicate, we define the negation of it, that is, key compromise.
The intuitive meaning of φ̂, ~x IO K is that φ̂, ~x compromises thekey (with oracles) and it cannot be used for safe encryption any
more.
The first thought here would be to define the compromise so thatfrom φ̂, ~x, an x can be computed such that the encryption of x andof 0|x| are computationally distinguishable. However, the majordifficulty here (and the major difference from [24]) is that we haveto define our notion for any S. Computational distinguishability on
an arbitrary set has no meaning: even in the usual CCA2 game with
CCA2 secure encryption, there can be non-negligible sets of coins
defined on which the CCA2 attacker returns 1 if the real bit stringis encrypted, while 1 with probability 1/2 if the 0’s are encrypted;
it is very easy to find sets like this.
What we came up with is a notion of observational inequivalence: encryptions of x and 0|x| have to be observationally inequivalent on S, where PPT algorithms with oracle access provide thecontexts and equality on S provides the equivalence.

O

0

O
AO
x, {0|x| }Rx, {0|x| }R
21 (φ̂, ~eK ) = A22 (φ̂, ~
eK )

0

O
x, {0|A1 (φ̂,~x)| }RAO
x, {0|A1 (φ̂,~x)| }R
21 (φ̂, ~eK ) = A22 (φ̂, ~eK )– If O is either aic2 or sic2, thenIn the KDM case

RanGen(K) ∧ fresh(R; φ̂, ~x, x, y, K)O∧ ~x, x, y 4 φ̂ ∧ φ̂, ~x, {x}ReK  y• R is generated honestly, statistically independently of the inc
terpretations of φ̂, ~x, x, and Mc , Π, S, σ |= x 4 φ̂, ~x andc• Either M , Π, S, σ ||=−→ φ̂, ~x, x IO K ∨ φ̂, ~x OyThis formula means that if the key is uncompromised,that is, φ̂, ~x, x 6 IOK, then {x}ReK cannot help in deriving y. In other words, if it is possible to derive ywith {x}ReK , then it is also possible to derive it without{x}ReK . The freshness and random generation conditions ensure that {x}ReK is indeed a good encryptionOx, {x}Rx, {x}RAOeK ) = A22 (φ̂, ~eK )21 (φ̂, ~and for some (hence for all) R0 fresh random input generated
inside S, Mc , Π, S, σ ||=
0

0

O
AO
x, {0|x| }Rx, {0|x| }R
21 (φ̂, ~eK ) 6= A22 (φ̂, ~
eK )

10

eK
(e.g. {N }N
eK or {N }eK are not good), and also thatRy cannot depend on {x}ReK (e.g. y = {x}eK is notgood). Moreover, ~x, x, y 4 φ̂ ensures that handles inthese terms are given values the adversary can compute(otherwise e.g. taken x = h, the handle h cannot be
dK if dK was never sent, and it cannot be R either).
This formula is completely analogous to the secrecy axiom in [6] but dK v φ̂, ~x, x there is replaced now with
φ̂, ~x, x Iaic2 K as we can now allow dK to appear
inside a secure encryption for example.
– If O is either akc2 or skc2, then

• Axioms for Freshly Generated Items.
– Fresh keys are not compromised: The intuition of thisaxiom is that if K is fresh, then it can be used for secure
encryption: keyfresh(K; φ̂, ~x)∧ ~x 4 φ̂ −→ φ̂, ~x 6 IOK
This axiom is sound if the encryption for which K isgenerated (correctly) is CCA2 secure. Depending on
which O is in the axiom, the encryption needs to havethe corresponding level of security. This is the only axiom where the security of the encryption is necessary.
The reader may wonder that proving the KDM case,what happens to the variables not known to the protocol adversary in the submitted functions as the standard
KDM encryption oracle only fills in the gaps of keys,
not other unknown items. However, in a KDM attack
created by the failure of the axiom, the attacker simulates the protocol, and all honestly generated items except for the keys and random inputs to the encryptionsin question are available to him.
– Fresh items do not compromise: they were generated
independently and as they have not been sent out, they
have not had a chance to compromise other items:
fresh(x; φ̂, ~x, y) ∧ ~x, y 4 φ̂ ∧ φ̂, ~x, x IO y → φ̂, ~x IO yRanGen(K) ∧ fresh(R; φ̂, ~x, x, y, K)O∧ ~x, x, y 4 φ̂ ∧ φ̂, ~x, {x}ReK  y−→ φ̂, ~x IO K ∨ φ̂, ~x Oy
The difference here from the axiom for IND-CCA2 security is that in φ̂, ~x IO K now there is no x. This
corresponds to the fact that the encrypted message x isallowed to contain the decryption key, or it may leak itsomehow together with φ̂, ~x. For more, see Section 11.
It may be surprising however that these core axioms do not
require any security of the encryption. It is purely a consequence of the definition of key compromise and derivability
predicates. (The axiom that requires CCA2 security is the
fresh keys are uncompromised axiom later.)Here we want to allow x to be any secret thing, such as anonce, so only x 4 φ̂ was assumed. That is why in the KDM
definition of key compromise we needed to allow functions
depending on such secret items to be submitted to the encryption oracles in the semantics of Oand IO.
• Encryptions with uncompromised keys do not compromise:

8.2
8.2.1

Mc ,Π, S, σ ||= sdec(AOsic2(φ̂, ~x), K) 6= ⊥sic2x) is not equal any of the outputs
And on S, the output of AO (φ̂, ~of the encryption oracles, and it is not any of the bit strings corresponding to the honest encryptions in φ̂, ~x. Letcs4
icccx I x iff M , Π, S, σ |= 23(φ̂, ~x Iic x).
M , Π, S, σ |= φ̂, ~0

RanGen(K) ∧ RanGen(K ) ∧ fresh(R; φ̂, ~x, x, K, K )O∧ ~x, x 4 φ̂ ∧ φ̂, ~x, {x}ReK 0 I K−→ φ̂, ~x, x IO K 0 ∨ φ̂, ~x IO KThe reason for using oracle Osic2 is that the definition of INT-CTXT
security [14] allows the use of encryption and decryption oracles.

That is, if φ̂, ~x, {x}ReK 0 compromised K, then either K
0is already compromised without {x}ReK 0 , or K was al-

8.2.2

ready compromised by φ̂, ~x, x. Note that this includes
x, the encrypted term. This means that x itself (withφ̂, ~x) should not compromise K 0 if we want {x}ReK 0 tobe safe. This is the generalization of that key cycles
may compromise CCA2 encryption. In Section 11 wewill see how this axiom deals with key cycles.
– KDM-CCA2 case. If O is akc2 or skc2, then0

Semantics of Ciphertext Integrity

D EFINITION 8.2. We define INT-CTXT compromise as: We says4s4that Mc , Π, S, σ |= φ̂, ~x Iic K, if and only if Mc , Π, S, σ |= ~x 64
O sic2φ̂ ∨ ¬RanGen(K), or there is a PPT algorithm A, with– IND-CCA2 case. If O is either aic2 or sic2, then0

Ciphertext Integrity

Axioms for Ciphertext Integrity Key Compromise• Let SameEnc(~x; ~y ) be the constraint as before. Then
SameEnc(~x; ~y) ∧ ~
x,x = ~
y ,y −→ (φ̂, ~x Iic x ↔ φ̂, ~y Iic y).
• Derivability implies compromise: φ̂, ~x K −→ φ̂, ~x Iic K
• Increasing capabilities for key compromise:φ̂, ~x Iic K −→ φ̂, ~x, x Iic K• Commutativity: If ~x0 is a permutation of ~x, thenφ̂, ~x Iic K −→ φ̂, ~x0 Iic K.
• Transitivity: φ̂, ~x~y ∧ φ̂, ~x, ~y Iic K −→ φ̂, ~x Iic K
• Uncompromised key’s encryption cannot be faked:

0x, x, K, K )RanGen(K) ∧ RanGen(K ) ∧ fresh(R; φ̂, ~O∧ ~x, x 4 φ̂ ∧ φ̂, ~x, {x}ReK 0 I K−→ φ̂, ~x IO K 0 ∨ φ̂, ~x IO K
This is basically the same as the previous one, except
again that φ̂, ~x I K 0 does not contain x.

RanGen(K) ∧ φ̂, ~x  y ∧ dec(y, dK) 6= ⊥R
∧ ∀xR(y = {x}Rx) −→ φ̂, ~x Iic KeK → {x}eK 6v φ̂, ~Again, soundness of these axioms follow directly from thedefinition of key usability, and it does not depend on what
encryption is used.
In the above formulas, K and K 0 could be allowed to encrypt
different kinds of encryptions, not necessarily the same, we
just did not want to overload our formulas.

This means the adversary cannot compute a y which decrypts
to something meaningful. This is exactly what we need fromthe INT-CTXT property, namely, that the encryption cannot
be faked. Again, soundness of this axiom does not need INTCTXT encryption, it is immediate from our semantics.

11• Encryptions with uncompromised keys do not compromise:

Note, unlike for general soundness (Theorem 5.3), here the number of sessions in the computational execution does not have to bebounded in the security parameter.
We detail the proofs in the IND case, the KDM case is sketched,details will be included in the long version.

– For the IND case, we have
00

RanGen(K) ∧ RanGen(K ) ∧ fresh(R; φ̂, ~x, x, K, K )ic∧ ~x, x 4 φ̂ ∧ φ̂, ~x, {|x|}R
K0 I KP ROOF. As the soundness proofs of the axioms for derivability
with oracles are essentially the same as the soundness proofs for
key compromise below, we skip that and focus on key compromise.

−→ φ̂, ~x, x Isic2 K 0 ∨ φ̂, ~x Iic K
– For the KDM case, we have
00

RanGen(K) ∧ RanGen(K ) ∧ fresh(R; φ̂, ~x, x, K, K )ic∧ ~x, x 4 φ̂ ∧ φ̂, ~x, {|x|}R
K0 I K• Substitutability of equal terms: The reason is that according
to the definition of key compromise, compromise of the itemon the right hand side of IOonly depends on the bit string thatis associated to the term there, and not on the structure of theterm. This is in contrast with the left hand side. The notionthat anything can be submitted to the decryption oracle thatis not an encryption on the left clearly depends on the term
structure on the left, so we have to make sure that in ~x and ~ythe same encryption values occur.
• Derivability implies compromise: Soundness of this axiom
is rather trivial, but we write it out for clarity. In order toshow that in any protocol execution and n.n. set S, we havec
Mc , Π, S |= ∀~xK(φ̂, ~x OK −→ φ̂, ~x IO K), by the computational semantics we have to show that for any evaluation
σ of the variables, and for any S 0 ⊆ S non-negligible set,ccMc , Π, S 0 , σ |= φ̂, ~x OK implies Mc , Π, S 0 , σ |= φ̂, ~
x IO
c
c
0
O
K. So suppose M , Π, S , σ |= φ̂, ~x  K holds. To showcx IO K, let us take any n.n. S 00 ⊆ S 0 . By
Mc , Π, S 0 , σ |= φ̂, ~cx OK, there is a n.n. S 000 ⊆ S 00 and an
Mc , Π, S 0 , σ |= φ̂, ~O
OO
algorithm B
such that Mc , Π, S 000 , σ ||= BO (φ̂, ~x) =O
K. We can chose A1 in the IND definition of key compromise, and x in the KDM definition, simply to be a random
bit string r(ω) of length η. AO
21 can take the key and decryptη
its third input. AO
22 can be chosen to be identically 0 . If thethird input is the encryption of r(ω) then r(ω) is received afO
ter the decryption, so the output of AO
21 and A22 differ overwhelmingly. On the other hand, if it is the encryption 0|r(ω)| ,O
then the outputs of AO
21 and A22 always agree. So by the defc
inition of key compromise, Mc , Π, S 0 , σ |= φ̂, ~x IO K holds
000
00
as there is such an S for all S .
• Increasing capabilities for key compromise: If φ̂, ~x IO KO
holds, there are A1 , R, etc in the definition of key compromise. The same items are good for φ̂, ~x, x0 IO K, ignoringx0 .
• Commutativity: Trivial, the definition of key compromise isinvariant under the change of the order of the list ~x.
c• Transitivity: For any S, assuming Mc , Π, S, σ |= φ̂, ~
x O
c
c
O
~
y and M , Π, S, σ |= φ̂, ~x, ~y I K, we have to show thatc
Mc , Π, S, σ |= φ̂, ~x IO K. Take an arbitrary S 0 ⊆ S. Byc
Mc , Π, S, σ |= φ̂, ~x O ~
y , there is a S 00 ⊆ S 0 and an AOcalgorithm such that M , Π, S 00 , σ ||= AO (φ̂, ~x) = ~
y . Byc
Mc , Π, S, σ |= φ̂, ~x, ~y IO K, there is a S 000 ⊆ S 00 such thatfor this S 000 , the conditions in the definition of key compromise (in place of S 00 ) hold. Also, we have Mc , Π, S 000 , σ ||=AO (φ̂, ~x) = ~
y . So in the key compromise definition appliedcx, ~y IO K, the algoto the satisfaction Mc , Π, S, σ |= φ̂, ~OOOrithms A1 , A21 and A22 can run AO as a subroutine to compute ~y , so they do not need it as an input. Since there is such ac
S 000 ⊆ S 0 for all S 0 ⊆ S, we have Mc , Π, S, σ |= φ̂, ~x IO K.

−→ φ̂, ~x Iskc2 K 0 ∨ φ̂, ~x Iic K
Soundness of these follow from the compromise definitions.
• Fresh keys are not INT-CTXT compromised if encryption is
INT-CTXT secure:– keyfresh(K; φ̂) −→ φ̂ 6 Iic K. The intuition of this axiom is that if the encryption is INT-CTXT secure and if
K is fresh, then the adversary cannot fake encryptions
with this key.
• Fresh items do not compromise: fresh(x; φ̂, ~x, K) ∧ ~x 4
φ̂ ∧ φ̂, ~x, x Iic K −→ φ̂, ~x Iic K

9.

ON CONGRUENCE OF EQUALITY

Note that the semantics of the equality predicate = is not defined as identity in the domain. In fact, on the left-hand sides of thepredicates Oand IO, equal terms cannot be freely substituted. Thismight cause problems with decidability, the result in [20] heavily
builds on the fact that  is invariant under substitution with respect to equal terms. There is, however a solution if we observethat CCA2 security implies that encryptions cannot be faked: for
CCA2 secure encryption schemes, we can define the semantics ofφ̂, ~x Ox such that only those ciphers are not decrypted by the decryption oracles that are necessary for the computation of [[φ̂, ~x]].
Here, when we say an encryption is necessary, we mean the encryption cannot be omitted and the number of encryptions reduced bythis in the process computing [[φ̂, ~x]]. The reason we did not define
our predicates this way is that we did not want the well-definednessof our predicates depend on whether the encryption satisfies CCA2
security. But if the encryption does satisfy CCA2 security, then O
and IOcan be defined in the above way and all axioms that we havelisted are also valid for those new definitions, and on the top of it,= would be a congruence relation.
The symmetric Needham-Schroeder protocol proof as well as
the NSL proof work either way, and we believe this issue does notmake a big difference in protocol proofs in general. But for automation, the two definitions might make a big difference.

10.

SOUNDNESS OF AXIOMST HEOREM 10.1 (S OUNDNESS ). With the computational interpretations of derivability and key compromise predicates, the axioms are computationally sound. For the "fresh keys are not compromised", it is necessary that the implementation of the encryption satisfies the corresponding (symmetric or asymmetric, IND or
KDM-CCA2 security, or INT-CTXT ciphertext integrity). Soundness of the other axioms do not require that. Furthermore, the notelepathy axiom requires that freshly generated items are guessable
only with negligible probability.
12• Secrecy of CCA2 encryption: For the IND case, we havein the form of such a function. The only items in x that areneither function symbols nor names generated thus far are
new names and handles. But new names can be generated
by the submitter, and handles were computed by the adversary from sent messages earlier, the handles of which wereagain computed earlier from earlier messages. So ultimately,
all handles were computed by earlier names and functions,so they can be submitted to the oracle as functions of earlier
names. The rest of the proof is exactly the same.
• Next, we have to show that encryptions with uncompromised
keys do not compromise. Note again in the proof below that
we do not need CCA2 security of the encryption, we only
need the definition of key compromise. Instead of the original formula, we show the following in the IND-CCA2 case:

RanGen(K) ∧ fresh(R; φ̂, ~x, x, y, K)O∧ ~x, x, y 4 φ̂ ∧ φ̂, ~x, {x}ReK  y−→ φ̂, ~x, x IO K ∨ φ̂, ~x Oywhere O is either aic2 or sic2. Soundness of this follows
easily from our definition of key compromise and derivability with oracle access. Note that CCA2 security of the encryption is not needed in the following argument: We moveφ̂, ~x Oy to the premise, it becomes φ̂, ~x 6 Oy. Let us denoteby θ the premise received this way:θ ≡ RanGen(K) ∧ fresh(R; φ̂, ~x, x, y, K)O∧ ~x, x, y 4 φ̂ ∧ φ̂, ~x, {x}Rx OyeK  y ∧ φ̂, ~0

O∧~x, x 4 φ̂ ∧ φ̂, ~x, {x}Rx, x 6 IOK 0
eK 0 I K ∧ φ̂, ~We have to show that for any σ evaluation of free variablescand S non-negligible set, if Mc , Π, S, σ |= θ holds, thenccOM , Π, S, σ |= φ̂, ~x, x I K is also satisfied. So supposecc
Mc , Π, S, σ |= θ. For Mc , Π, S, σ |= φ̂, ~x, x IO K, takec0c
any non-negligible set S ⊆ S. As M , Π, S, σ |= θ implies
c
c
0
R
O
that M , Π, S , σ |= φ̂, ~x, {x}eK  y by the semantics ofOcompound formulas (one conjunct in θ is φ̂, ~x, {x}ReK y, and the property is preserved under taking subsets), forsuch an S 0 , by the definition of derivability, there is a nonnegligible subset S 00 ⊆ S 0 and an algorithm AO such thatOO
be theMc , Π, S 00 , σ ||= AO (φ̂, ~x, {x}ReK ) = y. Let B
algorithm that takes φ̂, ~x, x as input, submits x to its en0Oon
cryption oracle to receive {x}ReK , and then applies A
0R(φ̂, ~x, {x}eK ). As this was y with non-negligible probability for R, it is also y with non-negligible probability for
R0 , because y does not depend on either of them, and because the random inputs of the algorithms are required to be
fresh. Hence R0 is just as good an independent item as R
was. So there is a S 000 ⊆ S 00 such that Mc , Π, S 000 , σ ||=0
OO
AO (φ̂, ~x, {x}R
, weeK ) = y, and by the definition of B
c000
OO
also have M , Π, S , σ ||= B (φ̂, ~x, x) = y. Therefore,
0
OO
Mc , Π, S 000 , σ ||= AO (φ̂, ~x, {x}R(φ̂, ~
x, x) =
eK ) = B
y. Now observe that since x was PPT generated, for any
non-negligible S, there must be a length function `(η) suchthat the probability that |x| = `(η) is non-negligible on S.
00
OO(φ̂, ~
x, x) = yThis, means that AO (φ̂, ~x, {0|x| }ReK ) = B
cannot hold on any non-negligible subset of S 000 , because if
00
it did, then AO (φ̂, ~x, {0` }ReK ) = y would also hold nonc000
negligible in S contradicting Mc , Π, S, σ |= φ̂, ~x 6 Oy. So,−→ φ̂, ~x IO K.
We have to show that for all S non-negligible sets and σevaluations of variables, if Mc , Π, S, σ satisfies the premise,then it satisfies the conclusion as well. So let us suppose itcsatisfies the premise. We want to conclude Mc , Π, S, σ |=Oφ̂, ~x I K. Following the definition of key compromise,take any subset S 0 ⊆ S. By the definition of key comproc
Omise applied to Mc , Π, S, σ |= φ̂, ~x, {x}ReK 0 I K, thereOO
are S 00 ⊆ S 0 , R0 , R1 AO
,
A
and
A
such
that,
taking the1
21
22
first possibility,
Mc , Π, S 00 , σ ||=R1O
AOx, {x}Rx, {x}R
21 (φ̂, ~eK 0 , {A1 (φ̂, ~eK 0 )}eK ))

(1)

R1
O
x, {x}R= AO
x, {x}R
22 (φ̂, ~eK 0 )}eK )).
eK 0 , {A1 (φ̂, ~but
Mc , Π, S 00 , σ ||=
O

R0

R

x,{x}eK 0 )||A1 (φ̂,~}eK1 ))
AO
x, {x}R
21 (φ̂, ~eK 0 , {0x,{x}R)||AO
1 (φ̂,~
eK 0

6= AOx, {x}R
22 (φ̂, ~eK 0 , {0(2)R0}eK1 )).

cx, x 6 IOK 0 , from Equation 5, we have
By Mc , Π, S 00 , σ |= φ̂, ~that there is an R0 , and a subset (by restricting R0 ) S 000 ⊆ S 00
such that
Mc , Π, S 000 , σ ||=
0

0

O
R1
x, {0|x| }RAO
x, {0|x| }R
21 (φ̂, ~eK 0 , {A1 (φ̂, ~eK 0 )}eK ))

(3)

0
0
O
R1
x, {0|x| }R= AO
x, {0|x| }R
22 (φ̂, ~eK 0 , {A1 (φ̂, ~eK 0 )}eK )).

O

O
Mc , Π, S 000 , σ ||= AO (φ̂, ~x, {x}R(φ̂, ~
x, x),
eK ) = B

Equation 6 still holds on S 000 and for all R10 , as R10 and R0c
are independent. By Mc, Π, S 000 , σ |= φ̂, ~x, x 6 IOK 0 , from00
Equation 6, we get that there is an R , a subset S 0000 ⊆ S 000
just by restricting R00 , such that

but
00

0

RanGen(K) ∧ RanGen(K ) ∧ fresh(R; φ̂, ~x, x, K, K )OO
Mc , Π, S 000 , σ ||= AO (φ̂, ~x, {0|x| }R(φ̂, ~
x, x),
eK ) 6= Bcwhich means Mc , Π, S, σ |= φ̂, ~x, x IO K.
The argument for the KDM case is completely analogous, exc
cept that from the satisfaction of the same Mc , Π, S 00 , σ |= θ,cOc00
we have to derive M , Π, S , σ |= φ̂, ~x I K there. ThisO
means that the analogous BO in the KDM case is not allowed to use x as an input, so it cannot submit x to the encryption oracle. Instead, in the definition of key compromisefor the KDM case we allowed the algorithms to use the encryptions functions of items depending on the names generated that far. Hence x 4 φ̂ can be submitted to the oracle

Mc , Π, S 0000 , σ ||=00O|A1 (φ̂,~x,{0AOx, {0|x| }R
21 (φ̂, ~eK 0 , {000

6= AO
x, {0|x| }R
22 (φ̂, ~eK 0 , {0|x| R00}eK 0 )|

0

}R
eK ))

00
|AO
x,{0|x| }R)|
1 (φ̂,~
eK 0

(4)
0

}R
eK )),

still for all R0 . Again, there is a length function `(η) suchthat the probability that |x| = `(η) is non-negligible on S 0000 .
Let the subset of S 0000 on which they are equal be S 00000 . Since0` is easily computable, we get that there are algorithms AO
3 ,13

Let the subset of S 0000 on which they are equal be S 00000 . Since0` is easily computable, we get that there are x000 4 φ̂, ~x andOalgorithms AO
41 and A42 such thatO
AO
41 and A42 such that

Mc , Π, S 00000 , σ ||=O
1
1
AO
x, {AOx)}Rx, {AOx)}R
41 (φ̂, ~3 (φ̂, ~3 (φ̂, ~eK ) = A42 (φ̂, ~eK ))Mc , Π, S 00000 , σ ||=butcM , Π, S

00000

O
1
1
AO
x, {x000 }Rx, {x000 }R
41 (φ̂, ~eK ) = A42 (φ̂, ~eK )), σ ||=

but

O
O
R0
R0
AO
x, {0|A3 (φ̂,~x)| }eK1 ) 6= AO
x, {0|A3 (φ̂,~x)| }eK1 )).
41(φ̂, ~42(φ̂, ~Mc , Π, S 00000 , σ ||=cThis exactly means that Mc , Π, S, σ |= φ̂, ~x IO K. If weswitch = and 6=, we receive the proof of the other case of
key compromise.
Here too, the KDM case is proven entirely analogously, but
we write the details out for more clarity: We have to show0AOx, {0|x41 (φ̂, ~

0
000
R0
| R1
}eK ) 6= AO
x, {0|x | }eK1 )).
42 (φ̂, ~cThis exactly means that Mc , Π, S, σ |= φ̂, ~x IO K. If weswitch = and 6=, we receive the proof of the other case of
key compromise.
• Fresh keys are not compromised: It is here where IND-CCA2
or KDM-CCA2 security of the encryption is used. Let us firstconsider the IND-CCA2 case. We define our CCA2 attacker
against the CCA2 oracle that allows multiple submissions forencryptions, which is equivalent with the original definition[12]. Let us consider the IND-CCA2 case. What we haveto prove is that if Mc , Π, S, σ satisfies freshness of key K,cthen Mc , Π, S, σ |= φ̂, ~x IO K leads to a CCA2 attack to theccencryption. Let M , Π, S, σ |= φ̂, ~x IO K hold. That is, for
000every S ⊆ S, there are S ⊆ S 0 , etc. such that (consider
the first case),

0

RanGen(K) ∧ RanGen(K ) ∧ fresh(R; φ̂, ~x, x, K, K )O∧ ~x, x 4 φ̂ ∧ φ̂, ~x, {x}Rx 6 IOK 0
eK 0 I K ∧ φ̂, ~−→ φ̂, ~x IO K.
We have to show that for all S non-negligible sets and σevaluations of variables, if Mc , Π, S, σ satisfies the premise,then it satisfies the conclusion as well. So let us suppose itcsatisfies the premise. We want to conclude Mc , Π, S, σ |=Oφ̂, ~x I K. Following the definition of key compromise,take any subset S 0 ⊆ S. By the definition of key comproc
Omise applied to Mc , Π, S, σ |= φ̂, ~x, {x}ReK 0 I K, there
00
0
0
0
O
O
are S ⊆ S , R , R1 x , A21 and A22 such that, taking thefirst possibility,

Mc , Π, S 00 , σ ||= AO
x, {AOx)}R
21 (φ̂, ~1 (φ̂, ~
eK )

(9)

= AO
x, {AOx)}R
22 (φ̂, ~1 (φ̂, ~eK )andMc , Π, S 00 , σ ||=0 R1AOx, {x}R
21 (φ̂, ~eK 0 , {x }eK ))O

for all fresh R0 . Note that here we continue the convention
that for easier readability, we drop notating the computational interpretations of φ̂, ~x, R, etc. Of course, the algorithms act on the computational interpretations and not on thesymbolic terms. Note further that keyfresh(K; φ̂, ~x) ∧ ~
x 4 φ̂
means the decryption key or any function of it was never usedin φ̂, ~x (except for decrypting, and in case of symmetric keys
encrypting). What the CCA2 attacker has to do is to simulate
the protocol execution such that

Mc , Π, S 00 , σ ||=
0

R0

(6)

0
|x0 | R1
6= AOx, {x}R}eK )).
22 (φ̂, ~eK 0 , {0cBy Mc , Π, S 00 , σ |= φ̂, ~x 6 IOK 0 , from Equation 5, we have0that there is an R , and a subset (by restricting R0 ) S 000 ⊆ S 00
such that– except for K, the CCA2 attacker generates all otherkeys– encryptions (except for that of AOx)) with K are
1 (φ̂, ~done by requesting the encryption oracle (in case ofasymmetric encryptions, the adversary can also compute them himself)– the attacker keeps a table recording which encryption
belongs to which plaintext– decryptions of ciphertexts provided by the encryption
oracle are done by looking it up in the table– decryptions of strings not provided by the oracle aredone by submitting to the decryption oracle– when the challenge state is reached, the interpretationsof ~x and AOx) are computed
1 (φ̂, ~O– A1 (φ̂, ~x) is submitted to the encryption oracle alongwith a string of 0’s of the same length. Let c0 denote theencryption that is received from the oracle. Note thatthe adversary does not know if this is the encryption ofAOx) or of the 0’s.
1 (φ̂, ~Mc , Π, S 000 , σ ||=
0

00 R1
AO
x, {0|x| }R
21 (φ̂, ~eK 0 , {x }eK ))

(7)

0
00 R1
= AO
x, {0|x| }R
22 (φ̂, ~eK 0 , {x }eK ))0where x00 4 φ̂, ~x, {0|x| }R
eK 0 is received from x by com0R
puting the handles in it using {0|x| }R
eK 0 instead of {x}eK 0 .
Equation 6 still holds on S 000 and for all R10 , as R10 and R0 arec
independent. By Mc, Π, S 000 , σ |= φ̂, ~x 6 IOK 0 , from Equa00
tion 6, we get that there is an R , a subset S 0000 ⊆ S 000 justby restricting R00 , such that
Mc , Π, S 0000 , σ ||=00

0|x | RAO
x, {0|x| }R}eK ))
21 (φ̂, ~eK 0 , {0

(10)

O
0
6= AO
x, {0|A1 (φ̂,~x)| }R
22 (φ̂, ~
eK )

but

|x |
AO
x, {x}R}eK1 ))
21 (φ̂, ~eK 0 , {00Mc , Π, S 00 , σ ||= AO
x, {0|A1 (φ̂,~x)| }R
21 (φ̂, ~
eK )

(5)

0 R1
= AO
x, {x}R
22 (φ̂, ~eK 0 , {x }eK )).

00

000

(8)

00
|x00 | R0
6= AO
x, {0|x| }R}eK )),22 (φ̂, ~eK 0 , {0still for all R0 . Again, there is a length function `(η) suchthat the probability that |x| = `(η) is non-negligible on S 0000 .
14O– apply AOx, c0 .
21 and A22 to φ̂, ~– because of (9) and (10) on S 00 , if the correct bit string
was encrypted, the two computations are equal, and if
the 0’s were encrypted, the two are different.

for all i = 1, ..., µ, (that is, CASE 1 happens when the 0’s
are encrypted in the CCA2 attack). Suppose now the internal
bit is 0. Then, on {0} × Sµ0 , according to our setup of the
CCA2 attacker, he outputs 1, giving the wrong guess. Thatis, the output of ACCA2 is 1 on {0} × Sµ0 . On {0} × (Ω \ Sµ0 ),ACCA2 tosses a coin, so the probabilities there balance out.
The advantage of the attacker is essentially the difference ofthe probabilities of Sµ1 and Sµ0 :However, the attacker does not necessarily know when he isinside S 00 and when outside. Outside S 00 the attacker cannot be sure that equality means the correct encryption wasencrypted. To overcome this problem, we finish the above
CCA2 attack the following way. Let µ(η) be a function (inthe security parameter) of natural numbers.

Adv(ACCA2 ) =11
1 = · Prob{b = b0 |b = 1} − + Prob{b = b0 |b = 0} −
2
2
2
1 
1
1
0
1
= · Prob{Sµ } · Prob{b = b |b = 1 ∧ Sµ } −
2
2
1
1
0
1
+ Prob{Ω \ Sµ } · Prob{b = b |b = 1 ∧ Ω \ Sµ
}−
2
1
0
0
0
+ Prob{Sµ } · Prob{b = b |b = 1 ∧ Sµ } −
2
1 
0
0
+ Prob{Ω \ Sµ
} · Prob{b = b0 |b = 1 ∧ Ω \ Sµ
}−
2
1
1
1
1 
1
1
}· 1−
−
= · Prob{Sµ+ Prob{Ω \ Sµ
}·
2
2
2
2
1
1
1 
0
0
}· 0−
+ Prob{Sµ}·−+ Prob{Ω \ Sµ
2
2
2

1 
1
0
= · Prob{Sµ } − Prob{Sµ }4O– the adversary submits pairs of 0|A1 (φ̂,~x)| for encryption µ times. Let ci denote (i = 1, ..., µ) the encryptions received back from the oracle. Note thattheseO
encryptions are known to be encryptions of 0|A1 (φ̂,~x)|O– applies AO
x, ci
21 and A22 on all of φ̂, ~O– CASE 1: if A21 (φ̂, ~x, c0 ) = AO
x, c0 ) but
22 (φ̂, ~AO
x, ci ) 6= AO
x, ci ) for all i = 1, ..., µ, then21 (φ̂, ~22 (φ̂, ~the CCA2 attacker outputs 1, meaning that his guess isthat the oracle encrypted the correct bit string.
– CASE 2: otherwise, the adversary tosses a coin andoutputs the result.
We can think of the probability space of the CCA2 attack as{0, 1} × Ωη , where {0, 1} represents the internal bit of theoracles. Even if the internal bit is 0, the simulation of the
protocol execution can be done according to the above rules.
If b denotes the internal bit of the oracles and b0 denotes theoutput of the CCA2 adversary, the following holds.
Adv(ACCA2 ) = Prob{b = b0 } −We did not write it out, but of course each step holds for all
fixed values η of the security parameter:

1 
η
η
Adv η (ACCA2 ) = · Probη {Sµ1 } − Probη {Sµ0 } .
4

1
2

1
1
1
· Prob{b = b0 |b = 1} + · Prob{b = b0 |b = 0} −
2
2
2

1 
0
0
= · Prob{b = b |b = 1} + Prob{b = b |b = 0} − 1
2
1 
1
1
= · Prob{b = b0 |b = 1} − + Prob{b = b0 |b = 0} −
2
2
2

η

It is clear from the definitions that for all η, we have S 00 ⊆ηηηSµ1 , and Probη {S 00 } ≤ Probη {Sµ1 }. Let us observe thatO
the probability that A21 (φ̂, ~x, ci ) 6= AO
x, ci ) holds for
22 (φ̂, ~a fixed i is:=X

Probη {φ̂, x, AO
1 (φ̂, x) = w}·

w

Let Sµ1 ⊆ Ω be the set where· Probη {AOx, ci ) 6= AO
x, ci ) |φ̂, x, AO
21 (φ̂, ~22 (φ̂, ~1 (φ̂, x) = w}

Mc , Π, Sµ1 , σ ||=Where w runs through all possible outcomes values of theinterpretation of the triple φ̂, x, AO
1 (φ̂, x). If w is fixed, therest of the randomness for AO(
φ̂,~x, ci ) 6= AO
x, ci )
21
22 (φ̂, ~with differing i’s are independent. Hence for any finite index
set I,

O
AO
x,{AO
x)}R
x, {AOx)}R21(φ̂, ~1 (φ̂, ~eK ) = A22 (φ̂, ~1 (φ̂, ~eK )but where
Mc , Π, Sµ1 , σ ||= AO
x, ci ) 6= AO
x, ci )
21 (φ̂, ~22 (φ̂, ~for all i = 1, ..., µ, (that is, CASE 1 happens when the realplaintext is encrypted in the CCA2 attack). Note that Sµ1 depends on the function µ, but still, S 00 ⊆ Sµ1 , so Sµ1 is also
non-negligible. Suppose, the internal bit of the oracle is 1.
Then, on {1} × Sµ1 , according to our setup of the CCA2
attacker, he outputs 1, giving the correct guess. That is, denoting by ACCA2 the CCA2 attacker as described above, theoutput of ACCA2 is 1 on {1}×Sµ1 . On {1}×(Ω\Sµ1 ), ACCA2
tosses a coin, so the probabilities there balance out.
Let Sµ0 ⊆ Ω be the set where

Probη {

AO
x, ci ) 6= AO
x, ci ) |φ̂, x, AO
21 (φ̂, ~22 (φ̂, ~1 (φ̂, x) = w}

i∈I

=
Y

Probη {AOx, ci ) 6= AO
x, ci ) |φ̂, x, AO
21 (φ̂, ~22 (φ̂, ~1 (φ̂, x) = w}i∈I

Further note that since the only difference between the ci ’s
is that they have independent random inputs (and this holds
also for c0 when the internal bit is 0), these probabilities are
actually all the same:

Mc , Π, Sµ0 , σ ||=O^

Probη {AOx, ci ) 6= AO
x, ci ) |φ̂, x, AO
21 (φ̂, ~22 (φ̂, ~1 (φ̂, x) = w}
=

O

O
AO
x,{0|A1 (φ̂,~x)| }R
x, {0|A1 (φ̂,~x)| }R
21(φ̂, ~eK ) = A22 (φ̂, ~eK )Probη {AOx, cj ) 6= AO
x, cj ) |φ̂, x, AO
21 (φ̂, ~22 (φ̂, ~1 (φ̂, x) = w}

but where
Mc , Π, Sµ0 , σ ||= AO
x, ci ) 6= AO
x, ci )
21 (φ̂, ~22 (φ̂, ~15

aLet’s call this probability pηw 0 , while let1 η) and hence (1 − 2η1a )η go toNow, we know that (1 − 2ηe−1/2 from below as η goes to infinity, so we havepηw = Probη {φ̂, x, AO
1 (φ̂, x) = w}.

1(pηw 0 )µ(η) ≤ e− 2 η ,Note also that when the internal bit is 0,
andProbη {AOx, c0 ) = AO
x, c0 ) |φ̂, x, AO
21 (φ̂, ~22 (φ̂, ~1 (φ̂, x) = w}

which is a negligible function. This means that it is enoughfor the adversary to encrypt 0’s himself µ(η) = η a+1 manytimes, so the adversary is still polynomial.
The proof for KDM-CCA2 is exactly analogous. The only
difference is that instead of AOx), there is an x there,
1 (φ̂, ~and the oracles accept the functions to be submitted. When it
comes to computing the encryptions of x, the KDM encryption oracle is requested. It is not directly x that is submitted,
but a description of a function of the keys instead. Since the
KDM adversary is simulating the protocol, all items except
for the secret keys and the random inputs to the encryptionsin the symmetric case are available to him.
• Fresh items do not compromise: The idea is exactly the sameas in case of the derivability predicate. A fresh item can justas well be created by the adversary, it cannot help him.

With all the above notation, we have thatXηProbη {Sµ0 } =(1 − pηw 0 ) · (pηw 0 )µ(η) · pηww

where (pηw 0 )µ is the µ(η)’th power of pηw 0 .
00

Remember, we
assumed that Prob{S } was non-negligible. This meansthat there is an a ∈ N, and a strictly increasing sequenceof naturals η 7→ n(η), such for all η,Probη {Sµ1n(η)} ≥ Probη {S 00

n(η)

}>

1
.
n(η)a

(11)

In the rest of the proof, we show that there is an η 7→ µ(η)
polynomial function such thatη

Probη {Sµ0 } ≤1+ fnegl (η)
2 · ηaWe now turn to the case of INT-CTXT key compromise.
Proofs of the first six axioms and the last one are entirely identical to the proofs for CCA2 key compromise. The soundness of the“encryptions with uncompromised keys do not compromise" axiom
is also analogous: We again show the following:0
RanGen(K) ∧ RanGen(K ) ∧ fresh(R; φ̂, ~x, x, K, K 0 )where fnegl is some negligible function. This will mean thatηη
because of Equation (11), Probη {Sµ1 } − Probη {Sµ0 } is
not negligible for this µ, and we will be done. To this end,
consider the seto[nŜ η :=ω ∈ Ωη Mc, Π, {ω}, σ||= φ̂, x, AO
1(φ̂, x) = w

ic∧ ~x, x 4 φ̂ ∧ φ̂, ~x, {|x|}Rx, x 6 Isic2 K 0
K 0 I K ∧ φ̂, ~−→ φ̂, ~x Iic K
Again, we have to show that for all S non-negligible sets and σevaluations of variables, if Mc , Π, S, σ satisfies the premise, thenit satisfies the conclusion as well. So let us suppose it satisfies thecpremise. We want to show Mc , Π, S, σ |= φ̂, ~x Iic K. Following
the definition of key compromise, take any subset S 0 ⊆ S. By thecicdefinition of key compromise, Mc , Π, S, σ |= φ̂, ~x, {|x|}R
K0 I K
sic2
implies there is a S 00 ⊆ S, and a PT algorithm AO , such thatw :1 ≤ pη 0 ≤ 1− 1
w
2η a
2η a

Clearly,ηProbη {Sµ0 }ηη= Probη {Sµ0 ∩ Ŝ η } + Probη {Sµ0 ∩ (Ωη \ Ŝ η )}.
Butη

Probη {Sµ0 ∩ (Ωη \ Ŝ η )} =X

(1 − pηw 0 ) · (pηw 0 )µ(η) · pηw

Mc , Π, S 00 , σ ||= sdec(AOw :η
pw 0 < 1a2ηη
pw 0 > 1 − 1a2η∧ ∀zR0 (AO

1
· pηw
a
2η
w
1 X η
1
≤ a ·
pw = a .
2η
2η
w

≤

X

0

0

R
R
(φ̂, ~
x, {|x|}R
x, {|x|}R
K 0 ) = {|z|}K → {|z|}K 6v φ̂, ~K0 )Mc , Π, S 000 , σ ||= sdec(AO∀zR0 (AO

sic2

sic2

(φ̂, ~
x, {|0|x| |}R
K 0 ), K) 6= ⊥ ∧
0

0

R
R
(φ̂, ~
x, {|0|x| |}R
x, {|0|x| |}R
K 0 ) = {|z|}K → {|z|}K 6v φ̂, ~
K0 )
sic2

and on S 00 , AO (φ̂, ~x, , {|0|x| |}R
K 0 ) is not equal any of the outputsof the encryption oracles. Again, as the length of x can be guessed,
sic2
there is a non-negligible S 0000 ⊆ S 000 and a BO such thatw :1 ≤ pη 0 ≤ 1 − 1
w
2η a
2η a

(pηw 0 )µ(η) · pηw

Mc , Π, S 0000 , σ ||= sdec(BOw :1 ≤ pη 0 ≤ 1 − 1
w
2η a
2η a

∧ ∀zR0 (BOLet us chose µ(η) := η a+1 . Then, on the set in question,(pηw 0 )µ(η) ≤ (1 −(φ̂, ~
x, {|x|}R
K 0 ), K) 6= ⊥

sic2

η

X

sic2

sic2

and on S 00 , AO (φ̂, ~x, , {|x|}RK 0 ) is not equal any of the outputs
cof the encryption oracles. Now, we also have that Mc , Π, S 00 , σ |=sic2 0φ̂, ~x, x 6 I K from the satisfaction of the premise. This gives usthat there is some S 000 non-negligible subset of S 00 such that

1·

Hence, if we can prove that Probη {Sµ0 ∩ Ŝ η } is negligible,
then we are done. For this, we haveXηProbη {Sµ0 ∩ Ŝ η } =(1 − pηw 0 ) · (pηw 0 )µ(η) · pηw

≤

1

η

Probη {Sη02 ∩ Ŝ η } ≤ e− 2 η ,= 1 − pηw 0 .

sic2

sic2

sic2

(φ̂, ~x), K) 6= ⊥00R(φ̂, ~x) = {|z|}Rx)
K → {|z|}K 6v φ̂, ~and on S 0000 , BO (φ̂, ~x) is not equal any of the outputs of the enc
cryption oracles. And that exactly means Mc , Π, S, σ |= φ̂, ~x Iic
K. Again, the KDM case is entirely analogous.

a
1 ηa+11)= ((1 − a )η )η
2η a
2η

16

Proof of the uncompromised key’s encryption cannot be fakedaxiom is immediate from the semantics of Iic . If

It may seem to the reader that the axioms provided in [6] (thatis, without key compromise) could also be sufficient to prove that
φ3  N is inconsistent with the axioms there by removing items
from φ3 in a different order from what we just did in Example 11.1.
Namely, the idea would be to proceed the following way: given
φ3  N , first remove the first encryption (by the secrecy axiom as
2
KAB was never sent out), and receive h(A, B), {|h2 , N |}R
K i  N.
Then remove the second encryption (by secrecy as K is not in
the frame any more after removing the first encryption) receiving(A, B)  N contradicting the no-telepathy axiom. However, application of the secrecy axiom in [6] (and also in this paper) to2h(A, B), {|h2 , N |}R
K i  N requires h2 4 (A, B), which means(A, B)h2 , but that does not hold, because h2 was computed from1h(A, B), {|K|}R
KAB i. Secrecy axiom can only be used if the frame
contains all necessary information for the computation of handles
in the plaintext. It is in fact possible to show that φ3  N is consistent with the axioms of [6]. Although those axioms are inconsistent
with h2  K, they do allow h2 to carry partial information about K
sufficient to compromise the second encryption. Without the handle h2 in the second encryption, the axioms of [6] are sufficient toprove inconsistency, but except for initial ones, protocol messages
are normally responses to agent inputs and contain handles.

c

Mc , Π, S, σ |= RanGen(K) ∧ φ̂, ~x  y ∧ dec(y, dK) 6= ⊥R
∧ ∀xR(y = {x}Rx)eK → {x}eK 6v φ̂, ~Then for all S 0 ⊆ S, there is a S 00 ⊆ S 0 and an algorithm A suchthat Mc , Π, S 00 , σ ||= A(φ̂, ~x) = y. Furthermore, the last conjunctmeans that the output of the algorithm is not any of the encryptionsin φ̂, ~x, and the third conjunct means the decryption does not fail.
cThis is exactly means that Mc , Π, S, σ |= φ̂, ~x Iic K.
The only remaining axiom is the fresh keys are not compromised
axiom for the INT-CTXT case. But that is rather easy. Suppose, thecencryption is INT-CTXT secure. Mc , Π, S, σ |= φ̂ Iic K means
sic2
there is a S 00 ⊆ S, and a PT algorithm AO , such that
Mc , Π, S 00 , σ ||= sdec(AO0sic2(φ̂), K) 6= ⊥O sic2∧ ∀zR (A00R(φ̂) = {|z|}R
K → {|z|}K 6v φ̂)

sic2

and on S 00 , AO (φ̂) is not equal any of the outputs of the encryption oracles. But that exactly means that there is a non-negligiblesic2
set (namely S 00 ), on which AO can produce a ciphertext, contradicting the INT-CTXT property.

11.

E XAMPLE 11.2. Now suppose
R2
1
φ3 ≡ h(A, B), {|K|}R
KAB , {|KAB , h2 , N |}K i

SIMPLE EXAMPLES

Now let us see on a few simple examples how inconsistency canbe shown with the above axioms. In [6], the authors presented someof the most basic examples, therefore the ones we analyze here area little more complex, all are related to sending keys around. We
use symmetric encryption in these examples.

and let us try to show that φ3 ON contradicts the axioms. Note that
there is a key cycle in this example, K and KAB encrypt each other.
So assume φ3 ON . For IND-CCA2 security, from the ‘uncompromised key securely encrypts’ axiom we get φ2 , KAB , h2 , N Isic2
K if we follow the same steps as we did in Example 11.1. Thenthe same way as before, we can remove h2 and N , and since φ2 ≡
R1
sic2
1
φ1 , {|K|}R
K. But this does
KAB , receive φ1 , {|K|}KAB , KAB I
not lead to a contradiction! According to the equational theory,1
K = sdec({|K|}R
KAB , KAB ), and by the ‘functions are computable’sic2
1
axiom, we get φ1 , {|K|}R
K. So we always have
KAB , KAB R1
sic2
φ1 , {|K|}KAB , KAB I
K too by the ‘derivability implies compromise’ axiom, there is no contradiction. However, if we have
KDM security, then just as in the previous example, using the ‘uncompromised key securely encrypts’ axiom, φ3 skc2 N immediately leads to φ2 Iskc2 K, and the rest of the derivation is the sameas in the previous example. So in this case, while φ3 sic2 N is
consistent with the axioms, φ3 skc2 N is inconsistent.

E XAMPLE 11.1. Suppose the first messages in a frame are
R21
φ3 ≡ h(A, B), {|K|}R
KAB , {|h2 , N |}K i,

with names KKAB N R1 R2 , and where the symmetric encryption
is IND- (or KDM-) CCA2 secure. We want to show that φ3  N isinconsistent with the axioms, that is, N remains secret. Let now O
denote either sic2 or skc2. Suppose φ3  N holds. Then we have
φ3 O N by the more oracles help more axiom. That is the sameOO2
as φ2 , {|h2 , N |}R
K  N . By the no-telepathy axiom, φ2 6  N as
fresh(N ; φ2 ) holds (which follows directly from the definition of
the freshness constraint, not from axioms). By the ‘uncompromised key securely encrypts’ axiom for CCA2 symmetric case,with the roles ~x ≡ hi, x ≡ hh2 , N i, y ≡ N , since we assumedOO2
φ2 , {|h2 , N |}R
K  N , we also have that either φ2  N (alreadysic2
ruled out) or (depending on O) φ2 , h2 , N I
K or φ2 Iskc2 K .
In the IND-CCA2 case, by the ‘fresh items do not compromise’axiom, we then have φ2 , h2 Isic2 K as N does not appear in
φ2 . Since the handle is always derived from the frame, φ2  h2
holds, hence φ2 sic2 h2 and by the transitivity axiom applied for
φ2 , h2 Isic2 K and φ2 sic2 h2 , we have φ2 Isic2 K, just as we
had in the KDM case earlier. But that is the same as (now for bothO
1
IND and KDM cases) φ1 , {|K|}R
KAB I K. By the ‘encryptions
with uncompromised keys do not compromise’ axiom, with roles
K 0 ≡ KAB , ~x ≡ hi and x ≡ K, we have that either φ1 IO K,
or φ1 , K Isic2 KAB or φ1 Iskc2 KAB . However, φ1 6 IOK because of the ‘fresh keys are not compromised’ axiom, and the sameis true for φ1 6 IOKAB . So for the KDM case we have a contradiction and we are done. For the IND case, again by the ‘fresh
items do not compromise’ axiom, φ1 , K Isic2 KAB together withfresh(K; φ1 , KAB ) implies φ1 Isic2 KAB , hence again we arrived
at a contradiction.

E XAMPLE 11.3. Now consider
R2
R31
φ3 ≡ h(A, B), {|K|}R
KAB , {|{|KAB |}K 0 , h2 , N |}K i

with names KK 0 KAB N R1 R2 , R3 Strictly speaking, K and KAB
are still in cycles, but they do not disturb each other because ofK 0 . Again, assuming IND-CCA2 security, from φ3 sic2 N firstsic2
2
φ2 , {|KAB |}R
K is derived using the ‘uncomproK 0 , h2 , N I
mised key securely encrypts’ axiom as in Example 11.1. As in Exsic22
ample 11.1, h2 and N are removed: φ2 , {|KAB |}R
K. At
K0 I
this point, the ‘encryptions with uncompromised keys do not compromise’ axiom implies that either φ2 Isic2 K or φ2 , KAB Isic2
K 0 . In the former case, we are back at the situation of Example
11.1 and we arrive at a contradiction. In the latter case, by funcsic2
1
tion (encryption) application on φ1 , {|K|}R
K 0 , we
KAB , KAB I
receive that φ1 , K, KAB , R1 Isic2 K 0 , but by ‘the fresh items do
not compromise’ axiom all of K, KAB , R1 can be removed, andreceive that φ1 Isic2 K 0 contradicting the ‘fresh keys are uncompromised’ axiom.

17

12.

AN NEW ATTACK ON NSL

Notice that this attack is not a usual type-flaw attack, becauseeven if type-flaw attacks are allowed, honestly generated nonces
are normally considered atomic. For example, the reader may suggest that this attack is in fact very similar to the one shown in [27](as we both wrote it as N = hn, Qi ). However, there is a fundamental difference. The attack in [27] is based on the fact thatan honest agent sends a pair with a nonce and an agent name, andthe receiving honest agent understands this as a single nonce. In
other words, in [27] the honest receiver reads the pair of a nonce
and a name into an input variable meant for a nonce. There, n is
the honest nonce and N is the input variable. In our attack, it is anactual nonce that is understood by the receiver as a pair of a nonce
and a name. In our case, an actual nonce is read into the pair of two
input variables: one for a nonce and another for a name. Here N is
the honest nonce and n corresponds to the input variable. This is afundamental difference as in our case there are no atomic objects atall. Even an honest nonce is allowed to be split. To our knowledge,
this is the first such attack on the NSL protocol.

Using our technique, we found an attack on the NSL protocol,
that, to our knowledge had not been found by others. It was published in [6], but for the sake of a complete presentation, we include
in this long version as well.
With the notations of Example 4.1, if we assume that RanGen(N )∧ W (π2 (N )) is computationally satisfiable (where W (π2 (N ))means π2 (N ) is an agent name), then we have the following computational attack on the NSL protocol. RanGen(N ) ∧ W (π2 (N ))is the same as saying that with non-negligible probability, it is possible to choose a name (bit string) Q for an agent such that for the
output N of some honest nonce generation, there is a bit string nsuch that hn, Qi = N . To show that this is not at all unrealistic,
suppose that the pairing h·, ·i is concatenation, and the length ofagent names does not depend on the security parameter, say always
8 bits. Then for any name Q, n can be chosen with hn, Qi = N
as long as the last four digits of N equals Q, which, if N is evenly
generated, is of just 1/28 , i.e. non-negligible probability. So thissituation is realistic. Now, the attack is the following, it needs two
sessions:

13.

1. The adversary choses a name Q as above.
2. The adversary catches the last message {N2 }eKB in a session between A and B, two honest agents.
3. The adversary, acting as agent Q initiates a new session withB, sending {N2 }eKB to him.
4. Since B believes this is a new session with Q, it will parse{N2 }eKB according to its role, namely as {N10 , Q}eKB . This
will succeed as long as there is an n with hn, Qi = N2 , thatis, it will succeed with non-negligible probability 1/28 .
5. B then generates a new nonce, N20 , and sends {n, N20 , B}eKQ
to Q.
6. The adversary Q decrypts {n, N20 , B}eKQ , reads n, and computes N2 = hn, Qi. The secrecy of N2 is hence broken.
This attack is shown graphically in Figure 3.
3.

A{N2 }eK−→ B

B

attacker catches {N2 }eK , starts new session with B
Bthrough corrupted agent Q

1.

Q{N2 }eK

B={n,Q}eK

−→

B

B
↓

2.

Q

{n,N20 ,B}eK←−

Q

CORRECTNESS PROOF OF NSLIn this long version of our paper we also recite the verification
result of the NSL protocol published in [6]. The reason is thatnow with the derivation with oracles the syntax and the axioms
are somewhat different, but we want to emphasize that the proof isbasically the same with the new set of axioms as well.
The correctness of the NSL protocol was done for any (bounded)
number of sessions. It was shown that violation of secrecy or authentication is inconsistent with the axioms. In this proof, it was
assumed that agent A only executed the initiator role, and agent
B only executed the responder role (proof in the case when we allow them to run both roles is also doable, but it is much longer).
But both A and B were allowed to have other sessions runningwith possibly corrupted agents. First it was shown that nonces thatwere generated by honest initiator A and sent to honest responder B, or vice-versa, remained secret. This was done by picking
any step m of the execution tree, and listing all possible messages
sent by A and B, and then showing that φm 6 aic2 N together withthe axioms and agent checks imply φm+1 6 aic2 N for each possible sent message. Hence, φm 6 aic2 N , the axioms and the agent
checks, and φm+1 aic2 N are inconsistent. Since φ0 6 aic2 N initially holds by no-telepathy, by induction we have φm 6 aic2 N (andhence φm 6  N ) after any finite number of steps m. The reader cansee below that the induction hypothesis is a little more complex,
but essentially this is what was done.
Once secrecy is proven, authentication and agreement are shown.
We pick the point on the execution tree when the responder finished
his task, and using that nonces remain secret, together with nonmalleability, it is shown that the initiator also finished his task andthe corresponding values seen by the two parties match. In otherwords, B finished, A not finished or values don’t match, and theaxioms and the agent checks are inconsistent.

B
confirms Q = π2 (N2 )computes n = π1 (N2 )0generates N2

B

Q computes n and N2 = hn, Qi and gives it to the attacker

13.1

Figure 3: An Attack on the NSL Protocol

Secrecy

The aim of the secrecy proof is to show that nonces N sent between A and B remain secret. The fact that N is a nonce sent by
A to B in the NSL protocol can be expressed as

So, we can conclude that if hn, Qi = N is possible computationally with non-negligible probability, then the protocol fails. In
such case, trace-lifting soundness proofs fail as a bit string can beunderstood both as hn, Qi and as N .
Clearly, if the implementation of the protocol is such that B always checks the length of n, then this attack is not possible. It justhas to be made sure somehow that the implementation satisfies the
RanGen(N ) → ¬W (π2 (N )) property.

∃R {N, A}ReKB v φ̂ .
If B sent it to A, that means∃hR {π1 (dec(h, dKB )) , N, B}ReKA v φ̂ .
18

So, such nonces can be characterized by the condition

indeed inconsistent with the axioms. Therefore, together with theinduction step of Proposition 13.1, we have:

C[N ] ≡ RanGen(N ) ∧ ∃R.{N, A}ReKB v φ̂T HEOREM 13.2 (S ECRECY ). Consider a symbolic executionof the NSL protocol, with an arbitrary number of possible dishonest
participants and two honest participants A, B that follow the initiator and responder roles correspondingly, and that only execute
these roles in each of their bounded number of sessions. Further,
consider the convention hx, y, zi ≡ hx, hy, zii.
Our axioms together with the agent checks and RanGen(N ) →¬W (π2 (N )) imply that for any n ∈ N and for any nonce N thatwas either generated by A and sent to B, or vice versa, φn 6 aic2 N .

∨ ∃hR.{π1 (dec(h, dKB )) , N, B}ReKA v φ̂ .
Then the secrecy property we want to show is that
∀N C[N ] −→ φ̂ 6 aic2 N ,meaning that such nonces cannot be computed by the adversary.
 It
is equivalent to show that its negation, ∃N C[N ] ∧ φ̂ aic2 N , isinconsistent with the axioms and the agent checks on every possible
symbolic trace.
Suppose the total length of the symbolic trace in question is n.
At the end of the trace the frame φ contains n terms. Let us denote the frames at each node of this trace by φ0 , φ1 , φ2 , etc. Eachframe contains one more term than the previous one. Satisfactionof C[N ] by this trace means that one of the terms {N, A}ReKB
or {π1 (dec(h, dKB )) , N, B}ReKA appears in frame φn for someh, R. Let us fix such N . If ~x is a list of a finite number of nonces~x ≡ N1 , ..., Nl that were all generated by either A or B (possibly intended to each other, possibly intended for other possibly
malicious agents), and they are all different from N , then we say
condition C 0 [~x, N ] is satisfied:

The above Theorem states that secrecy of nonces satisfying C[N ]is never broken. That is, nonces that were generated by A or B andintended to be sent between each other, remain secret. In particular,requiring ~x to be the empty list, the formula ∃N C[N ]∧φ̂aic2 N ,together with the axioms and the agent checks, and RanGen(N )→ ¬W (π2 (N )) are inconsistent on any symbolic trace.

13.2

The agreement from the responder’s viewpoint is the following:0
Resp BN SL [B, i , N2 , h2 , h4 , R2 ]AND
π2 (dec(h2 , dKB )) = A

C 0 [N1 , ..., Nl , N ] ≡l^i=1∃QR.{Ni , A}Rv φ̂ ∨eKQ∃QhR.{π1 (dec(h, dKB )) , Ni , B}Rv
φ̂eKRanGen(Ni ) ∧ N 6= Ni ∧Agreement and Authentication⇓!

EXIST i, N1 , h1 , h3 , R1 , R3 SUCH THAT
Init AN SL [A, i, B, N1 , h1 , h3 , R1 , R3 ]ANDdec(h2 , dKB ) = hN1 , AiANDdec(h3 , dKA ) = hN1 , N2 , BiANDdec(h4 , dKB ) = N2

Q

Then an inductive proof is carried out on the length of φn . As itturns out, in order to avoid loops in the proof, instead of ∃N C[N ]∧φ̂ aic2 N , it is better to prove that∃N ∃~x C[N ] ∧ C 0 [~x, N ] ∧ φ̂, ~x aic2 N(12)
is inconsistent with the axioms and agent checks. On the symbolic
trace, this means that for all n,∃N ∃~x C[N ] ∧ C 0 [~x, N ] ∧ φn , ~x aic2 N
is inconsistent with the axioms and agent checks. We do this by
fixing an arbitrary N satisfying C[N ], and by
 showing that if forsome m < n, ∃~x C 0 [~x, N ] ∧ φm , ~x aic2 N is inconsistent with

the axioms and agent checks, then ∃~x C 0 [~
x, N ]∧φm+1 , ~x aic2 N
is also inconsistent with the axioms and agent checks. As at m = 0
the statement follows from no telepathy, we are done. This is what
the following theorem says. Again, note that within C and C 0 , φ̂ isalways φn and not φm .

where by the implication sign we mean that the agent checks andthe axioms imply this. We can also write this within our syntax:
cr (A, B, N1 , N2 ) v φ̂
∧ A = π2 (dec(h2 , dKB )) ∧ N1 = π1 (dec(h2 , dKB ))ci (A, B, N1 , N2 ) v φ̂ ∧−→ ∃h3 .
N2 = π1 (π2 (dec(h3 , dKA )))What we have to prove is that the negation of this is inconsistent
with the axioms and agent checks. But for that it is sufficient toshow that the agent checks and axioms, and the premise of the formula imply the conclusion of this formula, as the following theorem states with the proof available in [5] without oracles, but it isstraightforward to rewrite it with oracles.

P ROPOSITION 13.1. In the above execution of NSL protocol,
let N be such that C[N ] is satisfied, and let m < n. If for all~
x such that C 0 [~x, N ] holds, the axioms and agent checks imply(by FOL deduction rules) that φm , ~x 6 aic2 N , then for all ~x such0that C [~x, N ] holds, the axioms and agent checks imply (by FOL
deduction rules) that φm+1 , ~x 6 aic2 N holds.

T HEOREM 13.3 (AGREEMENT AND AUTHENTICATION ). We
consider a symbolic execution of the NSL protocol, with an arbitrary number of possible dishonest participants and two honest
participants A, B that follow the initiator and responder roles correspondingly, and that only execute these roles in each of theirbounded number of sessions. Furthermore, consider the convention hx, y, zi ≡ hx, hy, zii.
Our axioms together with the agent checks and RanGen(N ) →¬W (π2 (N )) are inconsistent with the negation of the formulacr (π2 (dec(h2 , dKB )) ,B, π1 (dec(h2 , dKB )) ,N2 ) v φ̂
 ∧ A = π2 (dec(h2 , dKB ))
ci (A, B, N1 , π1 (π2 (dec(h3 , dKA )))) v φ̂−→ ∃N1 h3 .  ∧ N2 = π1 (π2 (dec(h3 , dKA )))∧ N1 = π1 (dec(h2 , dKB ))Once this is shown, we still have to prove that the property initially holds, that is, ∃N ∃~x C[N ] ∧ C 0 [~x, N ] ∧ φ0 , ~x aic2 N is0
inconsistent with the axioms. Let C[N ] and C [~x, N ] hold for N
and ~x ≡ N1 , ..., Nl . At step 0, N , N1 , ..., Nl are still fresh (remember, we assumed for simplicity that everything was generated
upfront, and clearly, these nonces have not been sent), so by theno telepathy axiom, φ0 6 aic2 N , and then by the independence offresh items, φ0 , N1 6 aic2 N . Then again by the independence offresh items, φ0 , N1 , N2 6 aic2 N , etc. So φ0 , N1 , ..., Nl 6 aic2Nholds, meaning that ∃N ∃~x C[N ] ∧ C 0 [~x, N ] ∧ φ0 , ~x aic2 N is
19

14.

[3] M. Backes, B. Pfitzmann, and M. Waidner. A composable
cryptographic library with nested operations. In CCS’03,
pages 220–230. ACM, 2003.
[4] M. Backes, B. Pfitzmann, and M. Waidner. The reactive
simulatability (rsim) framework for asynchronous systems.
Information and Computation, 205(12):1685–1720, 2007.
[5] G. Bana, P. Adão, and H. Sakurada. Computationallycomplete symbolic attacker in action—Long version.
Available at IACR ePrint Archive, Report 2012/316.
[6] G. Bana, P. Adão, and H. Sakurada. Computationally
Comlete Symbolic Attacker in Action. In FSTTCS’12,
LIPIcs, pages 546–560. Schloss Dagstuhl, 2012.
[7] G. Bana and H. Comon-Lundh. Towards unconditionalsoundness: Computationally complete symbolic attacker.
Available at IACR ePrint Archive, Report 2012/019.
[8] G. Bana and H. Comon-Lundh. Towards unconditionalsoundness: Computationally complete symbolic attacker. In
POST’12, LNCS, pages 189–208. Springer, 2012.
[9] G. Bana, K. Hasebe, and M. Okada. Computationalsemantics for first-order logical analysis of cryptographic
protocols. In Formal to Practical Security, volume 5458 of
LNCS, pages 33–58. Springer, 2009.
[10] G. Barthe, B. Grégoire, and S. Zanella Béguelin. Formal
certification of code-based cryptographic proofs. In
POPL’09, pages 90–101. ACM, 2009.
[11] G. Barthe, B. Grégoire, and S. Zanella Béguelin. Formal
certification of code-based cryptographic proofs. In POPL,
pages 90–101. ACM, 2009.
[12] M. Bellare, A. Boldyreva, and S. Micali. Public-key
encryption in a multi-user setting. In EUROCRYPT’00,
pages 258–274. Springer, 2000.
[13] M. Bellare, A. Desai, D. Pointcheval, and Ph. Rogaway.
Relations among notions of security for public-key
encryption schemes. In CRYPTO’98, LNCS. Springer, 1998.
[14] M. Bellare and Ch. Namprempre. Authenticated encryption:
Relations among notions and analysis of the genericcomposition paradigm. J. Cryptology, 21(4):469–491, 2008.
[15] B. Blanchet. A computationally sound mechanized prover
for security protocols. IEEE Transactions on Dependable
and Secure Computing, 5(4):193–207, 2008.
[16] J. Camenisch, N. Chandran, and V. Shoup. A public key
encryption scheme secure against key dependent chosen
plaintext and adaptive chosen ciphertext attacks. In
EUROCRYPT’09, LNCS, pages 351–368. Springer, 2009.
[17] H. Comon, C. Marché, and R. Treinen, editors. Constraints
in Computational Logics: Theory and Applications,International Summer School, CCS’99, LNCS, 2001.
[18] H. Comon-Lundh and V. Cortier. Computational soundnessof observational equivalence. In CCS’08, pages 109–118.
ACM, 2008.
[19] H. Comon-Lundh and V. Cortier. How to prove security ofcommunication protocols? A discussion on the soundness offormal models w.r.t. computational ones. In STACS’11,
LIPIcs, pages 29–44. Schloss Dagstuhl, March 2011.
[20] H. Comon-Lundh, V. Cortier, and G. Scerri. Tractable
inference systems: an extension with a deducibility
predicate. In CADE’13, LNAI. Springer, 2013.
[21] Hubert Comon-Lundh, Masami Hagiya, Yusuke Kawamoto,and Hideki Sakurada. Computational soundness ofindistinguishability properties without computable parsing.
In ISPEC’12, pages 63–79. Springer, 2012.

THE SYMMETRIC
NEEDHAM-SCHROEDER PROTOCOL

With the axioms that we presented, we have proven the amended
symmetric Needham-Schroeder protocol:
1. A → B : A
2. B → A : {A, N1 }KBT
3. A → T : hA, B, N2 , {A, N1 }KBT i
4. T → A : {N2 , B, K, {K, N1 , A}KBT }KAT
5. A → B : {K, N1 , A}KBT
6. B → A : {N3 }K
7. A → B : {N3 − 1}KThis protocol first has a key distribution part, and then the distributed key is used to securely encrypt a nonce. We showed thatno symbolic (hence computational) attacker succeeds the following way (motivated by [28]). Using IND-CCA2 and INT-CTXT
axioms, we first showed by an inductive technique (similar to the
NSL proof) that the key K from the trusted party meant for honest A and B are never compromised (compromise is inconsistent
with the axioms and agent checks). Then, again with an inductive
technique we showed that N3 is never leaked. Finally, agreement
and authentication were shown. Besides the presented axioms, we
also needed that adding 1 and subtracting 1 are inverses of eachother, and x − 1 6= x. We needed an additional property, namely,that applying the first projection of a pairing on an honestly generated nonce cannot result the nonce itself with more than negligible
probability. Triples, quadruples were constructed out of pairs. The
detailed proof is available online at the first author’s homepage. We
assumed that A is running the initiator role in all his sessions, andB is running the responder’s role. There is only one trusted party.
They all are allowed to run any number of multiple parallel sessions
with honest and corrupted agents.
On a note about dynamic corruption, the proof works even if the
protocol allows the release of the key K at a later time. Secrecy
can still be proven until that point, authentication that was carriedout earlier can still be verified.

15.

CONCLUSIONSIn this paper we further expanded the framework proposed by
Bana and Comon-Lundh [8] for computationally complete symbolic adversary. We have shown how key exchange can be handled. Proofs with this technique are computationally sound without the need of any further assumptions such as no bad keys, etc.
that are assumed in other literature. We presented a modular set of
axioms that are computationally sound for implementations using
IND-CCA2, KDM-CCA2 and INT-CTXT secure encryptions respectively. We illustrated their power via simple examples and theverification entire protocols.
We are investigating extensions of the general soundness theorem in order to account for unbounded number of sessions and also
to be able to handle indistinguishability properties. More importantly, we are also researching automation.

16.

REFERENCES[1] P. Adão, G. Bana, J. Herzog, and A. Scedrov. Soundness andcompleteness of formal encryption: the cases of key-cycles
and partial information leakage. Journal of Computer
Security, 17(5):737–797, 2009.
[2] M. Backes, A. Malik, and D. Unruh. Computationalsoundness without protocol restrictions. In CCS’12, pages
699–711. ACM, 2012.
20

[22] V. Cortier and B. Warinschi. Computationally sound,automated proofs for security protocols. In ESOP’05, LNCS,
pages 157–171, 2005.
[23] A. Datta, A. Derek, J. C. Mitchell, V. Shmatikov, and
M. Turuani. Probabilistic polynomial-time semantics for a
protocol security logic. In ICALP’05, LNCS, pages 16–29.
Springer, 2005.
[24] A. Datta, A. Derek, J. C. Mitchell, and B. Warinschi.
Computationally sound compositional logic for key exchange
protocols. In CSFW ’06, pages 321–334. IEEE, 2006.
[25] Melvin Fitting. An embedding of classical logic in s4. The
Journal of Symbolic Logic, 35(4):529–534, 1970.
[26] R. Küsters and M. Tuengerthal. Computational soundness for
key exchange protocols with symmetric encryption. In
CCS’09, pages 91–100. ACM, 2009.
[27] Jonathan K. Millen and Vitaly Shmatikov. Constraint solving
for bounded-process cryptographic protocol analysis. In
Michael K. Reiter and Pierangela Samarati, editors, ACM
Conference on Computer and Communications Security,
pages 166–175. ACM, 2001.
[28] F. J. Thayer, J. C. Herzog, and J. D. Guttman. Strand spaces:
Proving security protocols correct. Journal of Computer
Security, 7(1):191–230, 1999.

21