Protocol insecurity with finitely many sessions and XOR

TL;DR

This paper provides a new proof demonstrating the insecurity of protocols using XOR with finitely many sessions, employing typed terms to extend the applicability of previous insecurity results.

Contribution

It introduces a novel proof technique based on typed terms, removing previous restrictions on protocol classes for analyzing XOR-based protocol insecurity.

Findings

XOR protocols are insecure with finitely many sessions.

Typed proof methods can generalize insecurity results.

The approach simplifies analysis of protocol vulnerabilities.

Abstract

We present a different proof of the insecurity problem for XOR, solved in by Chevalier, Kuesters, Rusinowitch and Turuani (2005). Our proof uses the notion of typed terms and well-typed proofs, and removes a restriction on the class of protocols to which the [CKRT05] proof applies, by introducing a slightly different (but very natural) notion of protocols, where honest agent sends are derivable from previous receives in the same session.