Title:
    Building Blocks for Secure Services:
    Authenticated Key Transport and Rational Exchange Protocols

    Ph.D. Thesis No. 2511 (2001)
    Swiss Federal Institute of Technology -- Lausanne (EPFL)

Author:
    Levente Buttyan

Academic supervisor:
    Prof. Jean-Pierre Hubaux (EPFL)

Thesis committee:
    Dr. N. Asokan (Nokia Research, Helsinki, Finland)
    Prof. Refik Molva (Eurecom, Sophia-Antipolis, France)
    Prof. Michael Reiter (Carnegie Mellon University, Pittsburgh, USA)

Abstract:
This thesis is concerned with two security mechanisms:
authenticated key transport and rational exchange protocols. These
mechanisms are potential building blocks in the security
architecture of a range of different services. Authenticated key
transport protocols are used to build secure channels between
entities, which protect their communications against eavesdropping
and alteration by an outside attacker. In contrast, rational
exchange protocols can be used to protect the entities involved in
an exchange transaction from each other. This is important,
because often the entities do not trust each other, and both fear
that the other will gain an advantage by misbehaving. Rational
exchange protocols alleviate this problem by ensuring that a
misbehaving party cannot gain any advantages. This means that
misbehavior becomes uninteresting and it should happen only
rarely.

The thesis is focused on the construction of formal models for
authenticated key transport and rational exchange protocols. In
the first part of the thesis, we propose a formal model for key
transport protocols, which is based on a logic of belief. Building
on this model, we also propose an original systematic protocol
construction approach. The main idea is that we reverse some
implications that can be derived from the axioms of the logic, and
turn them into synthesis rules. The synthesis rules can be used to
construct a protocol and to derive a set of assumptions starting
from a set of goals. The main advantage is that the resulting
protocol is guaranteed to be correct in the sense that all the
specified goals can be derived from the protocol and the
assumptions using the underlying logic. Another important
advantage is that all the assumptions upon which the correctness
of the protocol depends are made explicit. The protocol obtained
in the synthesis process is an abstract protocol, in which
idealized messages that contain logical formulae are sent on
channels with various access properties. The abstract protocol can
then be implemented in several ways by replacing the idealized
messages and the channels with appropriate bit strings and
cryptographic primitives, respectively.

We illustrate the usage of the logic and the synthesis rules
through an example: We analyze an authenticated key transport
protocol proposed in the literature, identify several weaknesses,
show how these can be exploited by various attacks, and finally,
we redesign the protocol using the proposed systematic approach.
We obtain a protocol that resists against the presented attacks,
and in addition, it is simpler than the original one.

In the second part of the thesis, we propose an original formal
model for exchange protocols, which is based on game theory. In
this model, an exchange protocol is represented as a set of
strategies in a game played by the protocol parties and the
network that they use to communicate with each other. We give
formal definitions for various properties of exchange protocols in
this model, including rationality and fairness. Most importantly,
rationality is defined in terms of a Nash equilibrium in the
protocol game. The model and the formal definitions allow us to
rigorously study the relationship between rational exchange and
fair exchange, and to prove that fairness implies rationality
(given that the protocol satisfies some further usual properties),
but the reverse is not true in general.

We illustrate how the formal model can be used for rigorous
verification of existing protocols by analyzing two exchange
protocols, and formally proving that they satisfy the definition
of rational exchange. We also present an original application of
rational exchange: We show how the concept of rationality can be
used to improve a family of micropayment schemes with respect to
fairness without substantial loss in efficiency.

Finally, in the third part of the thesis, we extend the concept of
rational exchange, and describe how similar ideas can be used to
stimulate the nodes of a self-organizing ad hoc network for
cooperation. More precisely, we propose an original approach to
stimulate the nodes for packet forwarding. Like in rational
exchange protocols, our design does not guarantee that a node
cannot deny packet forwarding, but it ensures that it cannot gain
any advantages by doing so. We analyze the proposed solution
analytically and by means of simulation.