Ralf Treinen: Some Recent Talks

Mancoosi tools for the analysis and quality assurance of FOSS distributions

We will present a set of tools for the analysis and quality assurance of FOSS distributions. These tools analyse meta-data of packages (like dependencies, build-dependencies, conflicts, etc), and answer questions like: This talk is not pkgsrc-specific, but will give an overview over the work done by Mancoosi and discuss possible collaborations between Mancoosi and the pkgsrc community.

This is joint work with Pietro Abate, Yacine Boufkhad, Jaap Boender, Roberto Di Cosmo, Jérôme Vouillon, and Stefano Zacchiroli.

Talk given at the

[Slides (PDF)]

News from EDOS: finding outdated packages

The best-known tool from the EDOS project, today called dose-debcheck, analyses the installability of packages according to its metadata (conflicts, dependencies,etc.). This allows us to find packages that certainly are not installable, but it is not always very helpful to pinpoint the origin of a problem. In this talk we present a new notion: A package is outdated if it is not installable, and furthermore if the only way to make it installable is to update the package itself, as opposed to mereley upgrading some of its dependencies. It turns out that this property can be defined in terms of installability in possible future versions of a repository. We explain how our algorithm can actually check this property, and we report on our experience with running the tool in debian.

This is joint work with Pietro Abate, Roberto Di Cosmo, and Stefano Zacchiroli.

Talk given at the

[Slides (PDF)]

Symbolic Protocol Analysis for Monoidal Equational Theories
(or: How Algebra Helps to Solve Intruder Constraints)

We consider the design of automated procedures for analyzing the (in)security of cryptographic protocols in the Dolev-Yao model for a bounded number of sessions when we take into account some algebraic properties satisfied by the operators involved in the protocol. This leads to a more realistic model than what we get under the perfect cryptography assumption, but it implies that protocol analysis deals with terms modulo some equational theory instead of terms in a free algebra.

The main goal of this paper is to set up a general approach that works for a whole class of so-called monoidal theories which contains many of the specific cases that have been considered so far in an ad-hoc way, e.g. exclusive or, Abelian groups, exclusive or in combination with the homomorphism axiom.

We follow a classical schema for cryptographic protocol analysis which proves first a locality result and then reduces the insecurity problem to a symbolic constraint solving problem. This approach strongly relies on the correspondence between a monoidal theory E and a semiring SeE which we use to deal with the symbolic constraints. We show that the well-defined symbolic constraints that are generated by reasonable protocols can be solved provided that unification in the monoidal theory satisfies some additional properties. The resolution process boils down to solving particular quadratic Diophantine equations that are reduced to linear Diophantine equations, thanks to linear algebra results and the well-definedness of the problem. Examples of theories that do not satisfy our additional properties appear to be undecidable, which suggests that our characterization is reasonably tight.

This is joint work with Stéphanie Delaune, Pascal Lafourcade, and Denis Lugiez.

Talk given at

[Slides (postscript)]

Symbolic Protocol Analysis in Presence of a Homomorphism Operator and Exclusive-Or

Security of a cryptographic protocol for a bounded number of sessions is usually expressed as a symbolic trace reachability problem. We show that symbolic trace reachability for well-defined protocols is decidable in presence of the exclusive or theory in combination with the homomorphism axiom. These theories allow us to model basic properties of important cryptographic operators.

This trace reachability problem can be expressed as a system of symbolic deducibility constraints for a certain inference system describing the capabilities of the attacker. One main step of our proof consists in reducing deducibility constraints to constraints for deducibility in one step of the inference system. This constraint system, in turn, can be expressed as a system of quadratic equations of a particular form over Z/2Z[h], the ring of polynomials in one indeterminate over the finite field Z/2Z. We show that satisfiability of such systems is decidable.

This is joint work with Stéphanie Delaune, Pascal Lafourcade, and Denis Lugiez.

Talk given at

[Slides (postscript)]

Le Projet PROUVÉ : PRotocoles cryptographiques: OUtils de VÉrification automatique

PROUVÉ est un projet RNTL sur trois ans qui réuni CRIL Technology, France Télécom R&D, INRIA Lorraine, LSV et VERIMAG. Le projet porte sur la vérification de protocoles cryptographiques. Le point de départ du projet est une critique des méthodes existantes de vérification de protocoles cryptographiques : Les objectifs du projet sont : Le projet s'attaquera à deux études de cas significatives: un porte-monnaie électronique et un protocole d'enchères, qui lui permettront à la fois de guider les recherches, d'expérimenter les outils et de valider les résultats.

Talk given at

[Slides (postscript)]

Easy Intruder Deductions

We investigate extensions of the Dolev-Yao model of a passive intruder into a cryptographic protocol by some algebraic properties of cryptographic primitives. We provide sufficient conditions under which the intruder deduction problem is decidable in polynomial time. We apply this result to the equational theory of homomorphism, and show that in this case the intruder deduction problem is linear, provided that the messages are in normal form. This is joint work with Hubert Comon-Lundh.

Talk given at

[Slides (postscript)]

Tree Automata and Tree Constraints

We are interested in the question whether automata techniques can help to solve constraints over trees.

Tree constraints are first-order formulas built over a given set of predicate symbols with a fixed interpretation in a domain of trees. The semantics of such a tree constraint is a relation over trees. Tree automata, on the other hand, provide a mechanism to define sets of trees. Tree automata are well-investigated; they are known to enjoy basically the same nice properties than word automata.

Unfortunately, classical automata are not well equipped to recognize the kind of relation that we can get as the semantics of a constraint. What is missing is

In the case of word automata both extensions pose no problem since they are subsumed by the closure properties of word automata. The same holds for the extension of tree automata to tuples, and it also holds at least in some interesting special cases for the extension of tree automata by tests. Unfortunately, we encounter severe problems if we want to combine both extensions to tree automata.

We will discuss the (mostly negative) results that we have obtained for our new class of tree automata, and we will illustrate the automata approach at hand of the (still open) problem of entailment of non-structural subtype constraints.

This is in parts joint work with Alex Aiken, Joachim Niehren, Tim Priesnitz, and Zhendong Su.

Talk given at

[Slides (postscript)]

Ralf Treinen
July 13, 2012.