Source author record

Mathieu Turuani

Mathieu Turuani appears in the imported research catalog. Authorship, coauthor and topic links are available while profile ownership is still unclaimed.

ResearcherUnclaimed source record

Cryptography and Security

Catalog footprint

What is connected

3works

1topics

4close collaborators

Actions

Connect this record

Open graph Browse works

Inspect adjacent papers, topics, institutions and collaborators without losing the researcher page.

Building this map preview

BZPEER is loading the nearby papers, people, topics and institutions for this page.

preprint2012arXiv

Intruder deducibility constraints with negation. Decidability and application to secured service compositions

The problem of finding a mediator to compose secured services has been reduced in our former work to the problem of solving deducibility constraints similar to those employed for cryptographic protocol analysis. We extend in this paper the mediator synthesis procedure by a construction for expressing that some data is not accessible to the mediator. Then we give a decision procedure for verifying that a mediator satisfying this non-disclosure policy can be effectively synthesized. This procedure has been implemented in CL-AtSe, our protocol analysis tool. The procedure extends constraint solving for cryptographic protocol analysis in a significative way as it is able to handle negative deducibility constraints without restriction. In particular it applies to all subterm convergent theories and therefore covers several interesting theories in formal security analysis including encryption, hashing, signature and pairing.

preprint2011arXiv

Satisfiability of General Intruder Constraints with and without a Set Constructor

Many decision problems on security protocols can be reduced to solving so-called intruder constraints in Dolev Yao model. Most constraint solving procedures for protocol security rely on two properties of constraint systems called monotonicity and variable origination. In this work we relax these restrictions by giving a decision procedure for solving general intruder constraints (that do not have these properties) that stays in NP. Our result extends a first work by L. Mazaré in several directions: we allow non-atomic keys, and an associative, commutative and idempotent symbol (for modeling sets). We also discuss several new applications of the results.

preprint2006arXiv

Implementing a Unification Algorithm for Protocol Analysis with XOR

In this paper, we propose a unification algorithm for the theory $E$ which combines unification algorithms for $E\_{\std}$ and $E\_{\ACUN}$ (ACUN properties, like XOR) but compared to the more general combination methods uses specific properties of the equational theories for further optimizations. Our optimizations drastically reduce the number of non-deterministic choices, in particular those for variable identification and linear orderings. This is important for reducing both the runtime of the unification algorithm and the number of unifiers in the complete set of unifiers. We emphasize that obtaining a ``small'' set of unifiers is essential for the efficiency of the constraint solving procedure within which the unification algorithm is used. The method is implemented in the CL-Atse tool for security protocol analysis.