Disabling equational theories in unification for cryptographic protocol analysis through tagging
Cryptography and Security
2010-04-13 v2 Discrete Mathematics
Logic in Computer Science
Symbolic Computation
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.
Cite
@article{arxiv.1003.5406,
title = {Disabling equational theories in unification for cryptographic protocol analysis through tagging},
author = {Sreekanth Malladi},
journal= {arXiv preprint arXiv:1003.5406},
year = {2010}
}
Comments
8 pages, submitted for publication