Disabling equational theories in unification for cryptographic protocol analysis through tagging

TL;DR

This paper introduces a tagging scheme that disables equational theories in unification, simplifying cryptographic protocol analysis by preventing certain algebraic manipulations.

Contribution

The authors propose a novel tagging method that effectively disables equational theories during unification, enhancing the security analysis of cryptographic protocols.

Findings

Disabling equational theories simplifies protocol analysis.

The tagging scheme effectively prevents algebraic manipulations.

Potentially improves security verification accuracy.

Abstract

In this paper, we show a new tagging scheme for cryptographic protocol messages. Under this tagging, equational theories of operators such as exclusive-or, binary addition etc. are effectively disabled, when terms are unified. We believe that this result has a significant impact on protocol analysis and security, since unification is at the heart of symbolic protocol analysis. Hence, disabling equational theories in unification implies disabling them altogether in protocol analysis for most operators and theories.