2010/03/28 by Sreekanth Malladi, Malladi, Sreekanth
Biochemistry, Genetics and Molecular Biology · Computer Science · #Advanced Authentication Protocols Security #Cryptography and Security (cs.CR) #DNA and Biological Computing #Discrete Mathematics (cs.DM) #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Symbolic Computation (cs.SC) #User Authentication and Security Systems #cs.CR #cs.DM #cs.LO #cs.SC
paper · pdf · doi:10.48550/arxiv.1003.5406
8 pages, submitted for publication
openalex publication_date 2010/03/28 · arxiv created 2010/04/10 · arxiv updated 2010/04/13 · openalex created_date 2022/09/05 · openalex updated_date 2026/07/28
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.