Security Protocols: Principles and Calculi
by Martin Abadi
Security protocols, as used in distributed systems for authentication
and related purposes, are notoriously prone to failures. Therefore,
over time, various methods have been developed for the design and
analysis of these protocols. These lectures introduce the principles
of protocol design. Taking a more formal approach, they describe
calculi and techniques for reasoning about protocols, in particular an
extension of the pi calculus with function symbols that can represent
cryptographic operations.
Identity-based Cryptography
by Liqun Chen
The idea of an identity-based system is that a public key can be
derived from an arbitrary data string, and the corresponding private
key is created by binding this string with a system master secret
owned by a trusted authority. This means that a user's identity
(e.g., the user's email address) can be used as the user's public
key and the trusted authority acts as a private key generation
centre. This solution is a good alternative to the more traditional
asymmetric system, Public Key Infrastructure (PKI), where the
trusted authority acts as a public key certificate issuer.
The concept of identity-based cryptography was proposed by
Shamir in 1984. However, it took about 20 years for this to
become a hot research topic, and many elegant and practical
mechanisms have been published in the past few years.
This lecture gives an overview of the state-of-art identity-based
cryptographic mechanisms in the following areas:
The lecture also briefly covers security analysis of these mechanisms and the position of international standardisation in the area of identity-based cryptography.
A Static Approach to Secure Service Composition
by Pierpaolo Degano
(Joint work with Massimo Bartoletti, Gian-Luigi Ferrari and Roberto Zunino)
We will present a static approach for studying secure composition of software.
We use lambda-box, an extension of the lambda-calculus, and we study
resource usage analysis and verification.
Lambda-box features dynamic creation of resources, and encloses
security-critical code in usage policy framings with a possibly
nested, local scope.
Additionally, it has primitives for selecting and invoking services
that respect given security requirements.
The actual run-time behaviour of services is over-approximated
by a type and effect system.
Types are standard and effects include the actions with possible
security concerns, as well as information about which services may be
invoked at run-time.
These approximations are model-checked to verify policy framings within
their scopes.
This allows for removing any run-time execution monitor, and for
instrumenting the code with local checks whenever these may help.
Also, our static analysis can be used to determine the plans driving
the selection of those services that match the security requirements
on demand.
Trust and Reputation Systems
by Audun Josang
Trust and reputation systems represent a significant trend in
decision support for accessing online services and resources.
For example, online market participants can rate each other
after the completion of a transaction, so that the aggregated
ratings about a given participant can be used to derive a
reputation score that can assist other participants in deciding
whether or not to transact with that participant in the future.
A natural side effect is that it also provides an incentive for
good behaviour, and therefore tends to have a positive effect on
the quality of online markets and communities. Trust and reputation
systems represent soft security mechanisms that complement
traditional hard security mechanisms. Trust and reputation systems
are already being used in successful commercial online applications.
There is also a rapidly growing scientific literature on this topic.
The purpose of this tutorial is to give an overview of existing and
proposed systems that can be used to derive measures of trust and
reputation for online services and resources, and to analyse the current
trends and developments in this area.
The tutorial will cover the following areas:
Systematic Security Analysis Method
by Daniel Le Metayer
Security analysis will be presented from an industrial point of
view with a short introduction to certification and best practices
in terms of risk analysis. We will argue that there is a need to fill
the gap between, on one hand, pragmatic, empirical methods which
may be difficult to justify and, on the other hand, formal methods
which are based on firm mathematical grounds but may be hard
to apply in some concrete situations.
As a contribution to reduce this gap, a systematic security analysis
method will be presented and illustrated.
Critical Infrastructures Protection
by Javier Lopez
A new mega-infrastructure is emerging from the convergence of
infrastructures of different industry sectors on the one side, and
the Internet communications and the electronic markets and electronic
commerce services on the other. The concept of Critical
Infrastructure is arising. According to the European Commission,
Critical Infrastructures consist of "those physical and information
technology facilities, networks, services and assets which, if
disrupted or destroyed, would have a serious impact on the health,
safety, security or economic well-being of citizens or the effective
functioning of governments in the Member States. Critical
Infrastructures extend across many sectors of the economy, including
banking and finance, transport and distribution, energy, utilities,
health, food supply and communications, as well as key government
services". Key sectors of modern society that are vital to the
national security and the essential functioning of industrialized
economies are dependent on a spectrum of highly interconnected
national (and international) software-based control systems for their
smooth, reliable, and continuous operation. This information
infrastructure underpins many elements of the aforementioned Critical
Infrastructures, and is hence called Critical Information
Infrastructures (CII), characterized by unique requirements for
communications performance, including timing, redundancy, centers
control and protection, and equipment control and diagnostics.
The challenges on protecting those CII are numerous and complex,
since problems in individual and homogeneous systems evolve into
problems in heterogeneous environments, where the security and
resilience of the overall system and its parts must be assured
before, during and after any operation. CII require multiple
high-data-rate communication links, a powerful central computing
facility, and an elaborate operations control center. All of them are
especially vulnerable when they are needed most - during serious
system stresses or disruptions. However, for deeper protection,
intelligent distributed control is strongly required to keep parts of
the network operational. It is commonly agreed by network experts
that Wireless Sensor Networks (WSN) is the technology that better
fulfills features like the ones required by CII. In fact, WSN can be
applied to a large number of areas, and its applications are
continuously growing.
In this lecture we will introduce basic and advanced concepts related
to CII and will put into perspective the diverse security problems
that applications in this type of scenarios bring into place. We also
will elaborate on the wireless sensor networks technology and the
security issues raised by its use in CII scenarios.
Closing Internal Timing Channels by Transformation
by Alejandro Russo
A major difficulty for tracking information flow in multithreaded
programs is due to the internal timing covert channel.
Information is leaked via this channel when secrets affect the
timing behavior of a thread, which, via the scheduler, affects the
interleaving of assignments to public variables. This channel is
particularly dangerous because, in contrast to external timing, the
attacker does not need to observe the actual execution time.
This paper presents a compositional transformation that closes the
internal timing channel for multithreaded programs (or rejects the program
if there are symptoms of other flows). The transformation is based on
spawning dedicated threads, whenever computation involves secrets,
and carefully synchronizing them. The target language features semaphores,
which have not been previously considered in the context of
termination-insensitive security.
Anonymity Protocols as Noisy Channels
by Kostas Chatzikokolakis
In this talk I present a framework in which anonymity protocols are
interpreted as particular kinds of channels, and the degree of anonymity
provided by the protocol as the converse of the channel.s capacity. This
view is justified in terms of the Bayesian probability of error that
limits the adversary.s capability of testing the protocol to infer the
user.s identity. I then illustrate how various notions of anonymity can
be expressed in this framework, and show the relation with some
definitions of probabilistic anonymity in literature.