POR for Security Protocol Equivalences : Beyond Action-Determinism


Security protocols have become an important area of formal verification. Over the past years, much research has focused on verifying trace equivalence on protocols, which is notably used to model many interesting privacy properties, e.g., anonymity or unlinkability. Many tools for checking trace equivalence rely on a naive and expensive exploration of all interleavings of concurrent actions, which calls for POR techniques. In this paper, we present the first POR technique for protocol equivalences that does not rely on an action-determinism assumption: we recast the trace equivalence problem as a reachability problem, to which persistent and sleep set techniques can be applied, and we show how to effectively and efficiently put these results to work through symbolic analysis. We report on a prototype implementation, integrated in the tools Apte and DeepSec.