How to Prevent Type-Flaw Attacks on Security Protocols Under Algebraic Properties
Type-flaw attacks upon security protocols wherein agents are led to misinterpret message types have been reported frequently in the literature. Preventing them is crucial for protocol security and verification. Heather et al. proved that tagging every message field with it's type prevents all type-flaw attacks under a free message algebra and perfect encryption system. In this paper, the authors prove that type-flaw attacks can be prevented with the same technique even under the ACUN algebraic properties of XOR which is commonly used in "Real-world" protocols such as SSL 3.0. Their proof method is general and can be easily extended to other monoidal operators that possess properties such as Inverse and Idempotence as well.