Michaël Rusinowitch

Title: Protocol Analysis for WS Security

Date: Friday June 18, 09:00

Abstract:

We present some potential applications of security protocol analysis techniques to service oriented computing. In particular we consider the synthesis of a composed service and its validation. This ongoing work takes place in the context of Avantssar project.

Catherine Meadows

Title: Quantifying Pervasive Authentication: The Case of the Hancke-Kuhn Protocol

Date: Friday June 18, 15:00

Abstract:

There is a growing body of work on developing techniques for the formal analysis of cryptographic protocols. However, most of it depends on depends on the representation of cryptographic algorithms as algebraic systems. Although much progress has been made on the richness of the algebraic theories that can be represented, and on proving these theories sound in a computational model, less attention has been devoted to reasoning directly in a probabilistic model.

However, there are important emerging classes of protocols which require such a probabilistic analysis. As mobile devices pervade physical space, the familiar authentication patterns are becoming insufficient: besides entity authentication, many applications require, e.g., location authentication. Many interesting protocols have been proposed and implemented to provide such strengthened forms of authentication, but there are very few proofs that such protocols satisfy the required security properties. In some cases, the proofs can be provided in the symbolic models, albeit with more work and some clever trick. More often, various physical factors invalidate the perfect cryptography assumption, and the symbolic model does not apply. In such cases, the protocol cannot be secure in an absolute logical sense, but only with a high probability. But although probabilistic reasoning is thus necessary, the analysis in the full computational model may not be warranted, since the relative security does not depend on a general computational assumption, but rather upon an assumption of randomness.

We refine the Dolev-Yao algebraic method for protocol analysis by a probabilistic model of guessing, needed to analyze protocols that mix weak cryptography with physical properties of nonstandard communication channels. Applying this model, we provide a precise security proof for a proximity authentication protocol, due to Hancke and Kuhn, that uses probabilistic reasoning to achieve its goals. Finally, we discuss the feasibility of implementing such an approach via rewriting logic.

Bruno Blanchet

Title: The automatic security protocol verifier ProVerif

Date: Saturday June 19, 9:00

Abstract:

ProVerif is an automatic security protocol verifier based on an abstract representation of the protocol by a set of Horn clauses, and on a resolution algorithm on these clauses. This technique allows a flexible encoding of many cryptographic primitives by rewrite rules or equations. It can verify a wide range of security properties of the protocols, such as secrecy, authentication, and some process equivalences, in a fully automatic way. Furthermore, the obtained security proofs are valid for an unbounded message space and an unbounded number of sessions of the protocol, in parallel or not. We will present the basic technique used by ProVerif as well as more recent evolutions and applications.

Ralf Kuesters

Title: Enabling ProVerif to Analyze Protocols with XOR and Diffie-Hellman Exponentiation

Date: Sunday June 20, 9:00

Abstract:

ProVerif is one of the most successful tools for cryptographic protocol analysis. However, dealing with algebraic properties of operators such as the exclusive OR (XOR) and Diffie-Hellman exponentiation has been problematic.

In this talk, I will present an approach which enables ProVerif, and related tools, to analyze a large class of protocols that employ the XOR operator and Diffie-Hellman exponentiation.

The core of our approach is to reduce the derivation problem for Horn theories modulo algebraic properties of XOR/Diffie-Hellman exponentiation to a purely syntactical derivation problem for Horn theories. The latter problem can then be solved by tools such as ProVerif. Our reduction works for a large class of Horn theories, allowing to model a wide range of intruder capabilities and protocols. We implemented our reduction and, in combination with ProVerif, applied it to automatically analyze several state-of-the-art protocols that use XOR or Diffie-Hellman exponentiation.

This talk is based on joint work with Tomasz Truderung, published at CCS 2008 and CSF 2009.