ARA SSIA Formacrypt: Detailed description
Return to FormaCrypt main page
The verification of cryptographic protocols has been a very active
research area in the last years.
Most works on this topic use one of
the following two historically independent approaches:
 The computational approach considers that protocols
manipulate bitstrings, and proves probabilistic results on what
the adversary can obtain. The adversary is a probabilistic polynomialtime
Turing machine. This model is close to the real execution
of protocols, but the proofs are manual and informal.
 The formal approach models messages of protocols by terms
built from the cryptographic primitives. This is the socalled
DolevYao approach: The primitives are assumed to be perfect (one can
decrypt only if one has the key), and the adversary computes using
cryptographic primitives as black boxes. This model is more
abstract than the computational one. This makes it possible
to build automatic or partly automatic tools, using various techniques
(modelchecking, typing, theorem proving, among others). This model might be
closer to what protocol users understand. However, the obtained
security proofs are in general not sound with respect to the computational
model.
The FormaCrypt project focuses on bridging the gap between the two approaches.
This path promises tremendous benefits:
protocols can be analyzed and proved secure using the simpler,
automated methods specific to the formal approach, yet the security
guarantees are with respect to the more comprehensive computational
model.
This raises significant challenges, since these approaches
have been developed by two largely independent communities. They have
developed their own models and notions of security, and reconciling
these models presents considerable difficulties.
In order to bridge the gap between the two points of view on
cryptography, we plan to use several approaches, with inspiration
coming to varying degrees from the computational and the formal
worlds: the direct approach will formalize and automate
computational proofs as they are usually done by cryptographers (Theme 1); on
the other extreme, the modular approach will prove the
computational soundness of unmodified formal proofs (Theme 3); in between,
we will modify a formal approach in order to adapt it to computationally
sound proofs. More precisely, we will design a computationally sound
logic for proving protocols (Theme 2).
All these approaches will rely on a formalization of cryptographic
protocols in process calculi, which will be essentially equivalent
to each other, even if they may differ in the details for practical
reasons. (The most appropriate language may depend on the considered
classes of protocols and properties.)
Theme 1: The direct approach. A computationally sound prover
In the direct approach, we will formalize the computational
proofs, and relying on this formalization, build a specialized
automatic prover for cryptographic protocols, sound in the computational
model.
Computational security proofs
The basic idea of the computational approach of the security for
cryptographic schemes is to show that breaking a specific security
notion is at least as hard as breaking a wellknown computational
problem, such as integer factoring, the RSA problem [34], or
the DiffieHellman problem [20]. These proofs are led in the
complexity theory framework, providing reductions between these two
problems: the wellknown computational problem can be reduced to an
attack of the scheme. Therefore, for a long time, security proofs in
cryptography were the description of a reduction, and then the
presentation of arguments to explain why the reduction works.
This kind of proof technique is very efficient when one wants to prove
the security of an asymmetric encryption scheme [23] or a
signature scheme [24,25], but it becomes much more
intricate when interactive protocols are in consideration (such as key
exchange schemes) or when several computational assumptions are
necessary (the scheme is secure if the RSA problem is hard, and the
family (f_k) is a family of pseudorandom functions, etc).
A recent proof technique
Very recently, the proofs in computational cryptography apply a new
concept introduced by Shoup [37,36,38]: using a sequence of
games. Each game defines the interaction between the
participants of a protocol and an adversary. The first game consists
of the real attack: the adversary interacts with all the participants
with access to several oracles to formalize the various kinds of
information he may have access to, according to the security model.
The rest of the proof then aims at showing that, in this game,
the probability that the adversary finds a certain information (for
example distinguishes the key exchanged between honest participants of
the protocol from a random key) is negligible. More precisely, we
consider a specific event that happens when the adversary has
broken the scheme. And we want to bound the probability of this event,
in the probability space defined by all the random coins of the
adversary, the participants, and the oracles.
The following games are obtained by transformation of the first game,
such that the difference of probabilities between different games can
be easily bounded: the probability of our crucial event is thus
``almost'' the same in all the games. The transformations are chosen,
such that the probability of this event in the last game is obvious
from the form of the game. The probability corresponding to the
initial game can then be easily computed.
Formalizing security proofs
The various games are usually described informally in English,
together with arguments establishing upper bounds on
the probabilities involved. Our
goal is to build a formal framework in which these proofs can be
described and verified. The games correspond to processes in the
formal model, so they will be formalized in a process calculus. The
spi calculus [3], the applied pi calculus [2]
(which are
often used to describe protocols in the formal approach), and the
probabilistic polynomialtime calculus of [29,30]
will be obvious
sources of inspiration for this process calculus. However, some
adaptations will be necessary. For example, we plan to bound the
number of sessions of the protocol by a variable N, and to obtain
probabilities function of N. In contrast, [29,30]
bound the number
of sessions by a polynomial, and obtain asymptotic security results.
The drawback of such results is that they prove security for keys long
enough, but cannot be used to evaluate which is the minimal length of
the key that guarantees a certain level of security. In the formal
world, the number of sessions is either bounded by a small constant
(typically 1, 2, or 3), in which case the protocol is proved secure
only when the number of sessions is smaller than the bound, or
unbounded, which is impossible in the computational approach: if runs
can be unbounded, the adversary always ends up finding the secrets by
exhaustive exploration. We also plan to include additional constructs
in our calculus, for example to simulate lists, which are often used
in computational proofs to represent the global state of the system
of N sessions.
We will obviously define a semantics for this calculus,
corresponding to the computational model: this semantics will
consider messages as bitstrings, nonces as random numbers,
while the primitives will have the real (probabilistic) semantics.
The direct approach
In the direct approach, our goal is to directly formalize the
computational proofs by sequences of games.
So we will formalize the allowed transformations of games, and the
conditions under which they can be applied. These transformations come
from security properties of the cryptographic primitives, from general
properties of probabilities, or from allowed syntactic transformations
of the process calculus. We will prove these transformations correct
with respect to the computational semantics of the calculus.
This formalization will give the necessary theoretical
background for implementing a specialized prover, designed
for the proof of cryptographic protocols in a computational model.
This tool will take as input a description of the protocol in our
process calculus, and an indication of the security property to prove.
The prover will then automatically search a proof of the desired property.
To do this, it will try to apply the game transformations associated with
the definition of each cryptographic primitive used in the protocol.
(These are the main transformation steps.) When these transformations
are not directly applicable, it will determine and perform the necessary
syntactic transformations in order to make one of them applicable.
It will then compute the new
game after transformation, and the relation between probabilities in the games.
The process can then be repeated on the obtained game, until
the game is simple enough for the system to be able to compute the
desired probability directly, and therefore the desired security property
proved.
Theme 2: A computationally sound logic
The formal approach, which uses a highly idealized representation of
cryptographic primitives, has been a successful basis for formal
logics and automated tools. Our second theme aims at adapting such
logics to the computational approach, which yields more insight into
the strength and vulnerabilities of protocols, but it is more
difficult to apply, since it involves explicit reasoning about
probability and computational complexity. The purpose of this theme
is to show that formal reasoning, based on an abstract treatment of
cryptographic primitives, can be used to reason about probabilistic
polynomialtime protocols in the face of probabilistic polynomialtime
attacks.
The method
This approach aims at describing a cryptographically sound formal
logic for proving protocol security properties without explicitly
reasoning about probability, asymptotic complexity, or the actions of
a malicious attacker. A fragment of this expected logic has already
been defined in [19], proving that the method works and is
reasonable for usual properties. However, many difficult extensions of
this first fragment are expected and still need to be done. The
approach rests on a new probabilistic, polynomialtime semantics for
an existing protocol security logic, replacing an earlier semantics
that uses nondeterministic formal evaluation. Naturally, the
advantage of reusing an existing protocol security logic is that any
existing security proof in this logic with respect to the formal
semantics will become a computational proof with respect to the (new)
computationally sound semantics, with only minor corrections. While
the basic form of the protocol logic remains unchanged from previous
work, there are interesting technical problems involving the
difference between efficiently recognizing and efficiently producing a
value, and involving a reinterpretation of standard logical
connectives that seems necessary to support certain forms of
reasoning. Such distinctions were not available in the coarser
formal model, and raises some apparently fundamental issues about
the inherent logic of asymptotic probabilistic properties.
The protocol composition logic (PCL)
The most natural way to represent a protocol specification for use with
this method is to use the simple ``protocol programming language'' first
defined in [22,17,18]. It represents a protocol by a set of
roles, such as ``Initiator'', ``Responder''
or ``Server'', each specifying a sequence of actions to be executed
by a honest participant.
The set of actions must be complete enough to allow us to code any
usual protocol. In particular, we need actions to create a nonce, encrypt
or decrypt a term, match a term against a given pattern, or send and receive
a message. More actions might also be needed to model some specific protocols
(signaturebased actions, hashing, among others.)
The Protocol Composition Logic [6,17,18,22]
is a logic designed to express security properties over cryptographic
protocols. It consists of both logical formulas and modal formulas. Modal
formulas use a modal operator similar to FloydHoare logic.
Intuitively, the formula psi [P]_X phi means that if
psi is true at some point in the execution of a protocol (in the
presence of a malicious attacker), then phi will be true after
agent X performs the sequence P of actions. The pre and
postconditions are formulas, and may describe actions taken by
various principals and characterize the information that is available
to or hidden from them. For example, a pre or postcondition
psi = for all x.Fresh(X,x) => (for all Y.X!=Y => not Possess(Y,x))
specify that for any fresh nonce x generated by participant X, no
participant (Y) different from X knows x. A nonce is fresh when
it has been generated but not sent yet. In a (computational)
probabilistic semantics of this formula, not Possess becomes
knowing x with only a negligible probability.
Moreover, it seems that we should not limit ourselves to the
predicates already defined in the PCL for its formal semantics:
there are predicates which had no meaning in the formal world, but
are very useful in the computational one. For example, it would be
very helpful to have a specific predicate Indist(Y,x)
saying that Y cannot distinguish the message x from a random
bitstring with a probability significantly higher that one half. Such
operators introduce a fine granularity in our model that we did not
have in the formal world.
A probabilistic polynomialtime semantics
The semantics we want to explore recasts the methods of Micciancio and Warinschi [32]
in a logical setting, and reflects accepted modeling approaches used in the
field of cryptography, particularly [10,35].
The central organizing idea is to interpret
formulas as operators on probability distributions on traces.
Informally, representing a probability distribution by a set of
equiprobable traces (each tagged by the random sequence used to
produce it), the meaning of a formula phi on a set T of traces
is the subset T' of T in which phi holds. This
interpretation yields a probability: the probability that phi
holds is the ratio T'/T. Conjunction and disjunction are
simply intersection and union. There are several possible
interpretations for implication, and it is not clear at this point
which will prove most fruitful in the long run.
For example, we can interpret phi => psi as the union of
not(phi) and the composition of psi with phi;
the latter is also the conditional probability of psi given phi.
This interpretation supports a soundness proof for a sizable fragment of
the protocol logic, and resembles
the probabilistic interpretation of implication in [33].
Since the logic does not mention probability explicitly,
the idea is to consider a formula ``true'' if
it holds with asymptotically overwhelming probability.
While this approach seems promising and has already produced some
good results, there are still
various issues to fix and extensions to include. For example,
it is to be decided what is the best way to model a predicate
like Indist(Y,x), i.e. to make it fully coherent with other
predicates. The problem is to design a generic way to combine
predicates defined with different probability thresholds (1/2+epsilon
for Indist and 1epsilon for Possess). If we can define a generic framework
solving this issue, we will be able to combine any kind of computational
predicates in this logic. In the same direction, it is also to be decided
what new computational predicates we can, or should, include in
the logic. Moreover, any new predicate usually comes with a set
of associated new axioms or rules that also need to be well interpreted
in the probabilistic polynomialtime semantics.
Another problem is to analyze precisely
why we are able to define many different implication operators in
the probabilistic semantics of the PCL logic, and in which case each
of them should, or should not, be used. In the end, we will get
a very useful, flexible, and direct method to prove the security of
protocols using a computationally sound logic as easily as proving
their security with respect to the previous, formal, semantics.
Theme 3: The modular approach
In the modular approach, our goal is to justify formal notions of
security from a computational point of view. This
has two main interests. First, this makes possible
to reuse directly existing formal tools or standard formal techniques in
order to obtain computationallyvalid proofs of security.
In addition, it helps to understand what are the implicit cryptographic hypotheses
made in the formal models. In particular, what is the computational meaning of
``perfect cryptography''?
We call this approach modular as it relies on a computational
soundness theorem, proved once and for all, and specific formal
analyses for each protocol. Then the computational security proof of a protocol
can be achieve modularly: one has only to prove that the idealized protocol verifies the desired
property in the formal model and that the cryptographic primitives verify the computational security
properties.
Theme 3.1: Justifying formal models
Existing works on modular approaches in the active case such
as [7,32,8,27,16] have
concentrated so far on trace properties (e.g. authentication)
and more recently (in a limited way) secrecy [8,16].
In this part of the project, we plan to consider yet unstudied
security properties and cryptographic primitives.
Regarding security properties, we plan to consider branching
properties such as fairness, which are relevant for the analysis of
branching protocols (intuitively protocols in which honest
participants can make choices, such as contract signing protocols).
Our goal is to achieve similar
soundness results for these properties as for trace properties, that
is: if the property holds in the formal world, then its computational
counterpart holds on the concrete protocol with overwhelming
probability.
We also plan to study further secrecy
properties. Indeed, [8,16] relate formal and
computational secrecy only for nonces. We wish to extend these results
to other primitives, in particular, keys. This cannot be a trivial
extension of previous work since, as already noticed in by
D. Pointcheval, defining the secrecy of a key requires to change the
adversary's game. In addition, the fact that secrecy on traces
implies indistinguishability seems to rely strongly on the particular
cryptographic primitives (nondeterministic encryption, signatures). For
more general cryptographic primitives, we will rely on other
formal definitions of secrecy like observational equivalence for
example, related to Theme 3.3.
Regarding cryptographic primitives, we plan to consider more general
cryptographic primitives like symmetric encryption, hashes and
macs. Moreover even for asymmetric encryption and signatures (for
which soundness results have already been established), one might need
to consider specialized primitives that do not satisfy the strong
cryptographic hypotheses required in such soundness theorems. For
example, for encryption, one might need to consider encryption
primitives that are only INDCPA. For electronic
voting [28], the signature has some special properties. We
plan to study soundness of such particular primitives (one can unblind
a blind signature). This might require to add equational theories in
the formal model, which will be also studied in Theme 3.2.
Theme 3.2: Equational theories
Previous results of computational soundness
rely on formal models that use free (term) algebras.
Unfortunately this is not sufficient to model cryptographic primitives
which cannot be grouped into sets of constructors and destructors,
resp. for building messages (e.g. encryption, pairing)
and decomposing them (e.g. decryption, projection). This is why
most recent formal
models such as [2,13,1,12,14]
rely on equational theories and their corresponding initial algebras.
Our goal will be to exhibit sufficient conditions on protocols and
their implementations so as to ensure the computational soundness of
some formal models based on equational theories. Relevant primitives
that we plan to study include XOR, the modular
(DiffieHellman) exponentiation and the CBC encryption.
For each of these primitives (together with pairing and projections),
a number of issues will be successively considered.
 In the passive case, we will study to what extent the notion of
static equivalence from the applied pi calculus [2]
corresponds to cryptographic indistinguishability between concrete
messages.
 Then we plan to study the case of trace properties in the
presence of an active adversary. The proof will consist in showing
that under sufficient assumptions on the protocol, any concrete
execution trace corresponding to an attack can be mapped into a
formal (attack) trace or else the primitives can be broken.
 A further issue in the active case will be to identify a formal
notion of secrecy that is strong enough to imply secrecy in the
usual computational sense. Existing works on secrecy properties
currently rely on the formal notion of reachability (or simple)
secrecy. We believe that this notion is unlikely (in general) to
imply computational secrecy, i.e. the fact that any two
instances of the protocol differing only by the value of the secret
are indistinguishable. Instead we plan to computationally justify a
notion of process equivalence inspired by the observational
equivalence of the applied pi calculus [2]. As this
observational equivalence might not be implementable, we do not
foresee to justify it computationally at this point. Instead we plan
to use a stronger notion of equivalence that is currently used by
Blanchet's tool Proverif [11,12].
To answer these questions, we will rely in particular on the recent
work of Baudet et al. [9] concerning passive
adversaries. This work provides a general criterion for the
computational soundness of static equivalence and applies it on two
example theories modeling the XOR and ciphers. A very nice
way to achieve our goals would be to generalize Baudet et al.'s
criterion to active adversaries and then show how to instantiate it.
For that purpose, we will also study the possibility of using composition
theorems to deduce such a criterion on a given set of primitives from its
validity on smaller sets of primitives.
Theme 3.3: Application to guessing attacks
Guessing attacks occur in cryptography when an attacker is able to
recover the value of a secret by trying every possible value for it.
Secrets that are vulnerable to guessing attackssometimes called
weak secretsare those whose entropy is low enough for an
exhaustive search to be practical. This is typically the case for
passwords chosen by regular (human) users.
The security of protocols against guessing attacks has received a lot
of attention since the first attacks were discovered (see e.g.
Gong [26]). Various formalizations of
guessing attacks have been proposed since the seminal work of
Lowe [31]. Yet, except the very recent definition of Abadi
and Warinschi [5], none has received a computational
justification yet.
Abadi and Warinschi [5] define a notion of guessing attacks
based on patterns in the spirit of [4], for passive
adversaries. Our first goal in this theme will be to compare the
definition of Abadi and Warinschi [5] with that of Corin
et al. [15] based on static equivalence. Specifically
we will look for a specialized equational theory such that the
corresponding notion of static equivalence (together
with [15]) leads to the same notion of guessing attacks as
Abadi and Warinschi.
In other words, the point of view that we will adopt is the following:
rather than proposing new (somewhat arbitrary) models of security to
take into account weak secrets, we wish to introduce a dedicated
equational theory able to model practical implementations of protocols
that involve weak secrets. Then, and notably for the active case, we
will obtain the security against guessing attacks as a particular case
of equivalence between processes. Thus this theme will be highly
related to Theme 3.2. We foresee to reuse a number of the techniques
mentioned above.
Theme 4: Case studies and comparison of the various approaches
We plan to apply the techniques presented above to various protocols,
from protocols of the literature (such as the OtwayRees, Yahalom, and
NeedhamSchroeder protocols) to more complex, realistic protocols,
such as SSH (secure shell) and IKEv2 (the new key establishment
protocol for IPsec).
We will obviously compare the results obtained by the different
approaches, to determine the advantages and difficulties for each of
them. All these approaches will provide proofs in the computational
model, either directly, or via a proof in the formal model. (If the
modular approach is successful, we may modify a DolevYaostyle
protocol verification tool, so that it checks the additional hypotheses
needed to guarantee the soundness of the proof in the computational
model, and thus provides a proof in the latter model.)
References
 1

M. Abadi and V. Cortier.
Deciding knowledge in security protocols under (many more) equational
theories.
In Proc. 18th IEEE Computer Security Foundations Workshop
(CSFW'05), pages 6276, AixenProvence, France, June 2005. IEEE Comp. Soc.
Press.
 2

M. Abadi and C. Fournet.
Mobile values, new names, and secure communication.
In 28th Annual ACM SIGPLANSIGACT Symposium on Principles of
Programming Languages (POPL'01), pages 104115, London, United Kingdom,
Jan. 2001. ACM Press.
 3

M. Abadi and A. D. Gordon.
A calculus for cryptographic protocols: The spi calculus.
Information and Computation, 148(1):170, Jan. 1999.
An extended version appeared as Digital Equipment Corporation Systems
Research Center report No. 149, January 1998.
 4

M. Abadi and P. Rogaway.
Reconciling two views of cryptography (the computational soundness of
formal encryption).
Journal of Cryptology, 15(2):103127, 2002.
 5

M. Abadi and B. Warinschi.
Passwordbased encryption analyzed.
In L. Caires and L. Monteiro, editors, Proceedings of the 32nd
International Colloquium on Automata, Languages and Programming
(ICALP'05), volume 3580 of Lecture Notes on Computer Science,
Lisboa, Portugal, July 2005. Springer.
To appear.
 6

M. Backes, A. Datta, A. Derek, J. Mitchell, and M. Turuani.
Compositional analysis of contract signing protocols.
In 18th IEEE Computer Security Foundations Workshop, 2005.
To appear.
 7

M. Backes and B. Pfitzmann.
Symmetric encryption in a simulatable DolevYao style
cryptographic library.
In 17th IEEE Computer Security Foundations Workshop, Pacific
Grove, CA, June 2004. IEEE.
 8

M. Backes and B. Pfitzmann.
Relating symbolic and cryptographic secrecy.
In 26th IEEE Symposium on Security and Privacy, pages 171182,
Oakland, CA, May 2005. IEEE.
 9

M. Baudet, V. Cortier, and S. Kremer.
Computationally sound implementations of equational theories against
passive adversaries.
In L. Caires and L. Monteiro, editors, Proceedings of the 32nd
International Colloquium on Automata, Languages and Programming
(ICALP'05), volume 3580 of Lecture Notes on Computer Science, pages
652663, Lisboa, Portugal, July 2005. Springer.
To appear.
 10

M. Bellare and P. Rogaway.
Entity authentication and key distribution.
In 13th Annual International Cryptology Conference on Advances
in Cryptology (CRYPTO '93), pages 232249. SpringerVerlag, 1994.
 11

B. Blanchet.
Proverif 1.10 (automatic protocol verifier).
Available at http://proverif.inria.fr,
Feb. 2004.
 12

B. Blanchet, M. Abadi, and C. Fournet.
Automated verification of selected equivalences for security
protocols.
In 20th IEEE Symposium on Logic in Computer Science (LICS
2005), pages 331340, Chicago, IL, June 2005. IEEE Computer Society.
 13

Y. Chevalier, R. Küsters, M. Rusinowitch, and M. Turuani.
Deciding the security of protocols with DiffieHellman
exponentiation and products in exponents.
In P. K. Pandya and J. Radhakrishnan, editors, FST TCS 2003:
Foundations of Software Technology and Theoretical Computer Science, 23rd
Conference, volume 2914 of Lecture Notes on Computer Science, pages
124135, Mumbai, India, Dec. 2003. Springer.
 14

Y. Chevalier, R. Küsters, M. Rusinowitch, and M. Turuani.
An NP decision procedure for protocol insecurity with XOR.
Theoretical Computer Science, 338(13):247274, June 2005.
 15

R. Corin, J. M. Doumen, and S. Etalle.
Analysing password protocol security against offline dictionary
attacks.
In 2nd Int. Workshop on Security Issues with Petri Nets and
other Computational Models (WISP), Electronic Notes in Theoretical
Computer Science, June 2004.
 16

V. Cortier and B. Warinschi.
Computationally sound, automated proofs for security protocols.
In M. Sagiv, editor, Proc. 14th European Symposium on
Programming (ESOP'05), volume 3444 of Lecture Notes on Computer
Science, pages 157171, Edimbourg, U.K., Apr. 2005. Springer.
 17

A. Datta, A. Derek, J. Mitchell, , and D. Pavlovic.
A derivation system for security protocols and its logical
formalization.
In 16th IEEE Computer Security Foundations Workshop, pages
109125. IEEE Comp. Soc. Press, 2003.
 18

A. Datta, A. Derek, J. Mitchell, , and D. Pavlovic.
A derivation system and compositional logic for security protocols.
Journal of Computer Security, 2005.
To appear.
 19

A. Datta, A. Derek, J. C. Mitchell, V. Shmatikov, and M. Turuani.
Probabilistic polynomialtime semantics for a protocol security
logic.
In L. Caires and L. Monteiro, editors, ICALP 2005: the 32nd
International Colloquium on Automata, Languages and Programming, volume 3580
of Lecture Notes on Computer Science, Lisboa, Portugal, July 2005.
Springer.
To appear.
 20

W. Diffie and M. E. Hellman.
New Directions in Cryptography.
IEEE Transactions on Information Theory, IT22(6):644654,
November 1976.
 21

D. Dolev and A. C. Yao.
On the security of public key protocols.
IEEE Transactions on Information Theory, IT29(12):198208,
Mar. 1983.
 22

N. Durgin, J. Mitchell, , and D. Pavlovic.
A compositional logic for proving security properties of protocols.
Journal of Computer Security, 11:677721, 2003.
 23

S. Goldwasser and S. Micali.
Probabilistic Encryption.
Journal of Computer and System Sciences, 28:270299, 1984.
 24

S. Goldwasser, S. Micali, and R. Rivest.
A ``Paradoxical'' Solution to the Signature Problem.
In Proceedings of the 25th Symposium on the Foundations of
Computer Science (FOCS '84), pages 441448, Singer Island, U.S.A., 1984.
IEEE, New York.
 25

S. Goldwasser, S. Micali, and R. Rivest.
A Digital Signature Scheme Secure Against Adaptative ChosenMessage
Attacks.
SIAM Journal of Computing, 17(2):281308, April 1988.
 26

L. Gong, T. M. A. Lomas, R. M. Needham, and J. H. Saltzer.
Protecting poorly chosen secrets from guessing attacks.
IEEE Journal on Selected Areas in Communications,
11(5):648656, June 1993.
 27

R. Janvier, Y. Lakhnech, and L. Mazaré.
Completing the picture: Soundness of formal encryption in the
presence of active adversaries.
In M. Sagiv, editor, Proc. 14th European Symposium on
Programming (ESOP'05), volume 3444 of Lecture Notes on Computer
Science, pages 172185, Edimbourg, U.K., Apr. 2005. Springer.
 28

S. Kremer and M. D. Ryan.
Analysis of an electronic voting protocol in the applied pi calculus.
In M. Sagiv, editor, Programming Languages and Systems: 14th
European Symposium on Programming, ESOP 2005, volume 3444 of Lecture
Notes on Computer Science, pages 186200, Edimbourg, UK, Apr. 2005.
Springer.
 29

P. D. Lincoln, J. C. Mitchell, M. Mitchell, and A. Scedrov.
A probabilistic polytime framework for protocol analysis.
In ACM Computer and Communication Security (CCS5), pages
112121, San Francisco, California, Nov. 1998.
 30

P. D. Lincoln, J. C. Mitchell, M. Mitchell, and A. Scedrov.
Probabilistic polynomialtime equivalence and security protocols.
In J. Wing, J. Woodcock, and J. Davies, editors, FM'99 World
Congress On Formal Methods in the Development of Computing Systems, volume
1708 of Lecture Notes on Computer Science, pages 776793, Toulouse,
France, Sept. 1999. Springer.
 31

G. Lowe.
Analyzing protocols subject to guessing attacks.
In Workshop on Issues in the Theory of Security (WITS'02),
Portland, Oregon, Jan. 2002.
 32

D. Micciancio and B. Warinschi.
Soundness of formal encryption in the presence of active adversaries.
In M. Naor, editor, Theory of Cryptography Conference (TCC'04),
volume 2951 of Lecture Notes on Computer Science, pages 133151,
Cambridge, MA, USA, Feb. 2004. Springer.
 33

N. J. Nilsson.
Probabilistic logic.
Artificial Intelligence, 28(1):7187, 1986.
 34

R. Rivest, A. Shamir, and L. Adleman.
A Method for Obtaining Digital Signatures and Public Key
Cryptosystems.
Communications of the ACM, 21(2):120126, February 1978.
 35

V. Shoup.
On formal models for secure key exchange (version 4).
Technical Report RZ 3120, IBM, 1999.
 36

V. Shoup.
A Proposal for an ISO Standard for PublicKey Encryption, december
2001.
ISO/IEC JTC 1/SC27.
 37

V. Shoup.
OAEP Reconsidered.
In J. Kilian, editor, Advances in Cryptology  proceedings of
CRYPTO '01, volume 2139 of Lecture Notes in Computer Science, pages
239259, SantaBarbara, California, 2001. SpringerVerlag, Berlin.
 38

V. Shoup.
OAEP Reconsidered.
Journal of Cryptology, 15(4):223249, September 2002.
Page maintained by Bruno Blanchet