# Implementing a Unification Algorithm for Protocol Analysis with XOR

2 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174), INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : 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.
Type de document :
Communication dans un congrès
20th International Workshop on Unification - UNIF'06, Aug 2006, Seattle, WA/USA, pp.1-5, 2006

Littérature citée [13 références]

https://hal.inria.fr/inria-00103602
Contributeur : Mathieu Turuani <>
Soumis le : mercredi 4 octobre 2006 - 17:35:00
Dernière modification le : vendredi 6 juillet 2018 - 15:06:09
Document(s) archivé(s) le : mardi 6 avril 2010 - 18:15:09

### Identifiants

• HAL Id : inria-00103602, version 1
• ARXIV : cs/0610014

### Citation

Max Tuengerthal, Ralf Küsters, Mathieu Turuani. Implementing a Unification Algorithm for Protocol Analysis with XOR. 20th International Workshop on Unification - UNIF'06, Aug 2006, Seattle, WA/USA, pp.1-5, 2006. 〈inria-00103602〉

### Métriques

Consultations de la notice

## 159

Téléchargements de fichiers