How to prevent type-flaw and multi-protocol attacks on cryptographic protocols under Exclusive-OR

TL;DR

This paper demonstrates that tagging encrypted components can prevent type-flaw and multi-protocol attacks in cryptographic protocols that use the XOR operator, despite its algebraic properties, under certain assumptions.

Contribution

It extends the security analysis of tagged protocols to those employing XOR with algebraic properties, showing the effectiveness of tagging in this context.

Findings

Tagging encrypted components prevents attacks with XOR.

Security holds under certain algebraic assumptions.

Applicable to real-world protocols like SSL 3.0.

Abstract

Type-flaw attacks and multi-protocol attacks on security protocols have been frequently reported in the literature. Heather et al. and Guttman et al. have proven that these could be prevented by tagging encrypted components with distinct constants in a standard protocol model with free message algebra and perfect encryption. However, most "real-world" protocols such as SSL 3.0 are designed with the Exclusive-OR (XOR) operator that possesses algebraic properties, breaking the free algebra assumption. These algebraic properties induce equational theories that need to be considered when analyzing protocols that use the operator. This is the problem we consider in this paper: We prove that, under certain assumptions, tagging encrypted components still prevents type-flaw and multi-protocol attacks even in the presence of the XOR operator and its algebraic properties.