A Symbolic Intruder Model for Hash-Collision Attacks

TL;DR

This paper introduces a symbolic model for hash-collision attacks, enabling analysis of intruders actively exploiting collision algorithms within protocol security proofs.

Contribution

It presents a novel decision procedure that models collision attacks symbolically, bridging the gap between collision algorithms and protocol analysis.

Findings

The method effectively models hash collisions at the symbolic level.

It allows for automated analysis of collision-based attacks.

The approach improves understanding of protocol vulnerabilities.

Abstract

In the recent years, several practical methods have been published to compute collisions on some commonly used hash functions. In this paper we present a method to take into account, at the symbolic level, that an intruder actively attacking a protocol execution may use these collision algorithms in reasonable time during the attack. Our decision procedure relies on the reduction of constraint solving for an intruder exploiting the collision properties of hush functions to constraint solving for an intruder operating on words.