Open session:15:00 Syed Naqvi (CETIC, Belgium)
Security Requirement Analysis: Formals Models, Policy Derivation, and Security Rationales
15:30 Alejandro Russo (Chalmers University of Technology, Sweden)
Closing Internal Timing Channels by Transformation
16:00 Kostas Chatzikokolakis (Ecole Polytechnique Paris, France)
Anonimity Protocols as Noisy Channels
16:30 Marnix Dekker (Security group, TNO ICT, DIES group University of Twente, The Netherlands)
Administrative Privilege Inheritance
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.
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:
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.