Implementing a Unification Algorithm for Protocol Analysis with XOR

Unification algorithms are central components in constraint solving procedures for security protocol analysis. For the analysis of security protocols with XOR a unification algorithm for an equational theory including ACUN is required. While such an algorithm can easily be obtained using general combination methods such methods do not yield practical unification algorithms. In this work, we present a unification algorithm for an equational theory including ACUN which performs well in practice and is well-suited as a subprocedure in constraint solving procedures for security protocols with XOR. Our algorithm contains several optimizations which make use of the specific properties of the equational theories at hand. The efficiency of our implementation is demonstrated by experimental results.

Logo BII

BII

Rechte

Nutzung und Vervielfältigung:

Keine Lizenz. Es gelten die Bestimmungen des deutschen Urheberrechts (UrhG).

Bitte beachten Sie, dass einzelne Bestandteile der Publikation anderweitigen Lizenz- bzw. urheberrechtlichen Bedingungen unterliegen können.

Zitieren

Zitierform:
Zitierform konnte nicht geladen werden.