Towards a Hierarchy of Cryptographic Protocol Models. (Invited Talk)
Catherine MEADOWS, Naval Research Lab, Washington DC, USA.
(Monday June 21: 10.00 to 11.00)

Recently there has been an increasing amount of research in the introduction of cryptographic ideas into discrete methods for cryptographic protocol analysis. This is often done by developing a discrete model and a cryptographic model such that the discrete model can be shown sound with respect to the cryptographic model. In this talk we discuss some of the other issues in cryptographic protocol analysis that could be addressed with this approach. We argue that it is not always necessary or desirable to restrict ourselves to two models. Instead, we propose a hierarchy of models, so that models at one level of the hierarchy can be shown sound with respect to models at the lower level of the hierarchy if certain conditions are satisfied. We illustrate our approach with examples from current research in the area.

A confinement criterion for securely executing mobile code.
Hervé GRALL, CERMICS (ENPC-INRIA), Marne-la-Vallée, France.
(Monday June 21: 11.30 to 12.10)

Mobile programs, like applets, are not only ubiquitous, but also potentially malicious. We study the case where mobile programs are executed by a host system in a secured environment, in order to control all accesses from mobile programs to local resources. The article deals with the following question: how to ensure that the local environment is secure?
We answer by giving a confinement criterion: if the type of the local environment satisfies it, then no mobile program can directly access to a local resource. The criterion, which is type-based and hence decidable, is valid for a functional language with references. By proving its validity, we solve a conjecture stated by Leroy and Rouaix at POPL'98; moreover, we show that the criterion is optimal. The article mainly presents the proof method, based on a language annotation which keeps track of code origin and which enables studying the interaction frontier between the local code and the mobile code; the generalization of the method is finally discussed.

Verification of Cryptographic Protocols and Automated Deduction. (Invited Talk)
Jean GOUBAULT-LARRECQ, LSV, Ecole Normale Supérieure, Cachan, France.
(Monday June 21: 14.00 to 15.00)

Following Blanchet or Seidl, cryptographic protocols can be modeled using Horn clause formats. I'll explain how sets of general Horn clauses can be abstracted to specific decidable formats (I'll take Nielson, Nielson and Seidl's H1 class as my preferred format), and how such clause formats can be decided using automated deduction techniques, namely ordered resolution with selection and splittingless splitting---yielding optimal decision procedures; e.g., this variant of resolution runs in DEXPTIME for H1, which is known to be DEXPTIME-complete. Resolution actually provides streamlined ways of showing that several decidable classes indeed are so. I'll demonstrate the h1 tool, which decides H1 using resolution. I'll also describe various results (joint work with K.N. Verma and M. Roger) on extensions modulo equational theories, which have recently allowed us to verify the IKA.1 initial key agreement protocol of the CLIQUES protocol suite, automatically. A novelty here is that abstraction is not just effected prior to applying a resolution prover, but also during the very deduction process. If time permits, I'll also address the question of certifying cryptographic protocols, and producing actual evidence, in the form of an independently checkable Coq proof, of the security of protocols. While talking, I'll actually run h1, h1mc and some other tools of the h1 tool suite to support my claims.

SPIKY: A Nominal Calculus for modelling Protocols that use PKIs.
David GRAY, Benjamin AZIZ, Geoff HAMILTON, University College, Cork, Dublin City University, Dublin, Ireland
(Monday June 21: 15.00 to 15.40)

In this paper, we present an extension of the spi calculus that incorporates primitives for the retrieval of (un)certified public and private keys belonging to users of PKI­based systems. The extended notation also formalises the notion of process ownership by a PKI user. We also define the operational semantics of the new notation and give examples of PKI­based security protocols and review some of their authenticity properties.

Some Results on Timed Process Algebra.
Jing CHEN, LIFO/Le STUDIUM, Orléans, France.
(Monday June 21: 16.00 to 16.40)

Two different timed calculi are presented and their properties are discussed. Timed Pi calculus, a calculus of timed mobile processes, is presented first. This is a timed extension of Pi-calculus, which can model not only evolving systems but also systems with real-time behaviors. A theory of timed bisimulations is studied, and it is shown that the important properties of Pi-calculus are preserved in the timed setup. In real-time research, properties such as \emph{Maximal Progress} are fundamental especially when behaviors such as Timeout or Timestop need to be modeled. But when mobility is not part of the concern, e.g. as in cryptographic protocol analysis, these notions can also be modeled in a simpler and more natural way, in terms of a Timed Synchronous (Value-passing) Algebra, where synchronization is the central notion; we also present such an algebra and illustrate its expressive power with a few examples.

A Formal Tool for User Based Network Security Policy. Specification
R. LABORDE, B. NASSER, F. GRASSET, F. BARRERE, A. BENZEKRI, IRIT/SIERA, Toulouse, France.
(Monday June 21: 16.40 to 17.20)

Security policy models allow reasoning about security goals achievements. When security mechanisms are implemented, it is difficult to formally validate the security properties against the security goals especially in a network environment. To assess the implemented security properties, one should consider details regarding the network topology, the forwarding as well as filtering and transform engines. In this paper, we present a Colored Petri Net based tool which allows to describe graphically a given network topology, the network security mechanisms and the security goals required. The tool computes the different functionalities to set up the security properties and formally validates the solution using the dead state of the generated reachability graph analysis. Different security properties such as confidentiality and availability can be studied.

Priority Systems. (Invited Talk)
Joseph SIFAKIS, VERIMAG, Grenoble, France.
(Tuesday June 22: 9.30 to 10.30)

We present a framework for the incremental construction of deadlock-free systems meeting given safety properties. The framework lends concepts and basic results from the controller synthesis paradigm by considering a step in the construction process as a controller synthesis problem. That is, given a system S and a safery property, a deadlock-free system S' can be obtained as the composition of S with a controller preserving this property. We formalize and study the relationhip between S and S' by using the notion of deadlock-free control restriction. A key result is that (dynamic) priorities can define such restrictions provided that they satisfy some consistency conditions. Checking these conditions boils down to computing a kind of transitive closure of priority relations. We define priority systems which are transition systems restricted with priorities: from a given state, only enabled actions with maximal priority can be executed. We study composability of priorities on priority systems. As a rule, priorities are not composable e.g., the result of the successive application of two priority relations on a system, depends on the order of application. We show that this difficulty can be overcome by using symmetric composition operators for priorities which preserve safety and deadlock-freedom. We show that priorities are expressive enough to represent restrictions induced by deadlock-free controllers preserving safety properties. We define a correspondence between such restrictions and priorities and provide compositionality results about the preservation of this correspondence by operations on safety properties and priorities. Finally, we provide examples illustrating applications of the results.

A Formalization of Credit and Responsibility.
Roberto GORRIERI, Universita di Bologna, Italy,
Fabio MARTINELLI, Marinella PETROCCHI, Istituto di Informatica e Telematica - CNR, Pisa, Italy.
(Tuesday June 22: 10.50 to 11.30)

In this talk we will formally define a notion of credit and responsibility within the Generalized Non Deducibility on Compositions schema for the definition of security properties. We then investigate the validity of our definitions through some of the examples discussed by Abadi in one of his papers, titled "Two Facets of Authentication". Finally, we provide a sketch of a formal comparison between the two properties.

Using Admissible Interference to Detect Denial of Service. Vulnerabilities
Stéphane Lafrance, CRAC, Ecole Polytechnique, Montréal, Canada.
(Tuesday June 22: 11.30 to 12.10)

C. Meadows recently proposed a formal cost-based framework for analysis of denial of service. It was showed how some principles that have already been used to make cryptographic protocols more resistant to denial of service by trading off the cost to defender against the cost to the attacker can be formalised. The first contribution of this paper is to introduce a new security property called impassivity which intends to capture the ability of a protocol to achieve these goals in the framework of a generic value-passing process algebra called Security Process Algebra (SPPA) extended with local function calls, cryptographic primitives and special semantics features in order to cope with cryptographic protocols. More specifically, impassivity is defined as an information property founded on bisimulation-based non-deterministic admissible interference. A sound and complete proof method for impassivity is also provided. The method extends previous results presented in a previous paper on bisimulation-based non-deterministic admissible interference and its application to the analysis of cryptographic protocols. The method is illustrated throughout the paper on the TCP/IP connection protocol.

Towards Control of Resources for Synchronous Systems. (Invited Talk)
Roberto AMADIO, LIF, Université de Provence, Marseille, France.
(Tuesday June 22: 14.00 to 15.00)

We describe ongoing work towards the control of resources for synchronous systems carried on in the CRISS project http://www.cmi.univ-mrs.fr/~amadio/Criss/criss.html . We aim at developing static analysis techniques for bounding the resources necessary for the execution of a program. The basic appoach goes back to early work in complexity theory and consists in proving termination of the program and in synthesizing a bound on the size of the computed data as a function of the input data. We will focus on three distinct and recent contributions: - The use of the notion of quasi-interpretation to bound the size of the values computed by a first-order functional program. - The possibility to carry on size and termination verifications at the level of the bytecode of a simple virtual machine. - The extension of the approach from functional programs to systems of synchronous cooperative threads.

On Rewriting Protocol Specifications.
Monica NESI, G. RUCCI, M. VERDESCA, Universitą degli Studi di L'Aquila, Italy
(Tuesday June 22: 15.00 to 15.40)

This paper reports on work in progress on using rewriting techniques for the analysis and the verification of communication protocols. In a way similar to the approximation technique defined by Genet and Klay, a rewrite system R specifies the protocol and a tree automaton A describes the initial set of communication requests. In a previous work we have defined a rewriting strategy that, given a term t that represents a property of the protocol to be proved, suitably expands and reduces t using the rules in R and the transitions in A to derive whether or not t is recognized by an intruder. This is done by simulating a completion process in a bottom-up manner starting from t and trying to derive a transition t --> q_f from critical pairs, where q_f is a final state of the tree automaton. The rewriting strategy has been applied to the Needham-Schroeder public-key protocol for reasoning about the authentication and secrecy properties. We are now investigating the extension of the strategy to the class of symmetric-key protocols and related properties, by experimenting with the Needham-Schroeder symmetric-key protocol and the freshness property.

Tree Tuple Languages as Logic Programs and Applications.
Sébastien LIMET, LIFO, Université d'Orléans, France.
(Tuesday June 22: 16.00 to 16.40)

We present a general translation of term rewrite systems (TRS) to logic programs such that basic rewriting derivations become logic deductions. Certain TRS result in so-called cs-programs, which were originally studied in the context of constraint systems and tree tuple languages. By applying decidability and computability results of cs-programs we obtain new classes of TRS that have nice properties like decidability of unification or regular sets of descendants. Our findings generalize former results in the field of term rewriting and and can be useful for reachability problems issued from infinite state system verification for example.

Random polynomial­time attacks and Dolev­-Yao models.
Mathieu BAUDET, LSV, Ecole Normale Supérieure, Cachan, France.
(Tuesday June 22: 16.40 to 17.20)

For several decades two different communities have been working on the formal security of cryptographic protocols. Many efforts have been made recently to take benefit of both approaches, in brief: the comprehensiveness of computational models and the automatizability of formal methods. The purpose of this paper is to investigate an original approach to relate the two views, that is: to extend existing Dolev­-Yao models to account for random polynomial­-time (Las Vegas) computability. This is done first by noticing that Dolev-­Yao models can be seen as transition systems, possibly infinite. We then extend these transition systems with computation times and probabilities. The extended models can account for normal Dolev­-Yao transitions as well as non--standard operations such as inverting a one-­way function. Our main contribution consists in showing that under sufficient realistic assumptions the extended models are equivalent to standard Dolev-­Yao models as far as security is concerned. Thus our work enlarges the scope of existing decision procedures.

Back to the Workshop Page