# A Reduced Semantics for Deciding Trace Equivalence

## TL;DR

This paper introduces a reduced symbolic semantics and partial order reduction technique for trace equivalence checking in security protocols, significantly improving efficiency and integrated into the APTE tool.

## Contribution

It generalizes and adapts partial order reduction for equivalence checking, providing a practical optimization for symbolic execution tools.

## Key findings

- Dramatic improvements in benchmark performance
- Effective elimination of redundant interleavings
- Enhanced scalability of trace equivalence analysis

## Abstract

Many privacy-type properties of security protocols can be modelled using trace equivalence properties in suitable process algebras. It has been shown that such properties can be decided for interesting classes of finite processes (i.e., without replication) by means of symbolic execution and constraint solving. However, this does not suffice to obtain practical tools. Current prototypes suffer from a classical combinatorial explosion problem caused by the exploration of many interleavings in the behaviour of processes. M\"odersheim et al. have tackled this problem for reachability properties using partial order reduction techniques. We revisit their work, generalize it and adapt it for equivalence checking. We obtain an optimisation in the form of a reduced symbolic semantics that eliminates redundant interleavings on the fly. The obtained partial order reduction technique has been integrated in a tool called APTE. We conducted complete benchmarks showing dramatic improvements.