How to prevent type-flaw attacks on security protocols under algebraic properties

In this paper, we prove that type-tagging prevents type-flaw attacks on security protocols that use the Exclusive-OR operator as our main contribution. Our proof method is general and can be easily extended to other monoidal operators that possess properties such as Inverse and Idempotence. We also discuss how tagging could be used to prevent type-flaw attacks under other properties such as associativity of pairing, commutative encryption, prefix property and homomorphic encryption. Key words: Cryptographic protocols, Type-flaw attacks, Tagging, Algebraic properties, Equational theories, Constraint solving, Decidability.

• Type: Journal
• Year: 2010
• Where: CORR
• Authors: Sreekanth Malladi, Pascal Lafourcade
• Keywords: CORR 2010, Education, Monoidal Operators, Prevents Type-flaw Attacks, Type-flaw Attacks