A simple proof of the coincidence of observational and labeled equivalence of processes in applied pi-calculus

TL;DR

This work addresses the fundamental question of whether observational equivalence and labeled equivalence coincide for extended processes in the applied pi-calculus. By employing slightly altered transition definitions and a streamlined structural framework, the author derives a simplified pathway to the standard coincidence result. Key contributions include Theorem 1 on reducing CEPs to a canonical ν̃n.( {^{̃e}/_{̃x}} | P ) form, and Theorems establishing the existence and properties of observational bisimulation (OBS) and labeled bisimulation (LBS), culminating in the proof that the relations $\approx$ and $\approx_l$ are identical. The result has practical impact for formal verification of cryptographic protocols and related systems, and points toward algorithmic approaches (e.g., graph-based representations) for checking observational equivalence in broader classes of pi-calculus processes.

Abstract

This paper presents a new, significantly simpler proof of one of the main results of applied pi-calculus: the theorem that the concepts of observational and labeled equivalence of extended processes in applied pi-calculus coincide.