pith. sign in

arxiv: 2510.07258 · v2 · submitted 2025-10-08 · 💻 cs.LO

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

Andrew M. Mironov This is my paper

Pith reviewed 2026-05-18 09:29 UTC · model grok-4.3

classification 💻 cs.LO
keywords applied pi-calculusobservational equivalencelabeled equivalenceprocess equivalencebisimulationextended processes
0
0 comments X

The pith

Observational equivalence and labeled equivalence coincide for extended processes in the applied pi-calculus.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper establishes that observational equivalence, defined through barbs and arbitrary contexts, is identical to labeled equivalence, defined through matching labeled transitions, for extended processes in the applied pi-calculus. This coincidence means that behavioral properties of processes modeling cryptographic protocols and concurrent systems can be checked using whichever definition is more convenient for a given proof. The contribution is a significantly shorter proof of this long-known result, making the equivalence easier to apply and to extend. A reader cares because process equivalences underpin security and correctness arguments in the calculus, and a direct proof reduces the effort needed to trust or use the result.

Core claim

The paper proves that observational equivalence and labeled equivalence of extended processes coincide in the applied pi-calculus. Under the standard reduction semantics and equational theory for messages, a process satisfies the observational definition if and only if it satisfies the labeled definition.

What carries the argument

The coincidence theorem that equates the two relations by showing each implies the other through direct use of the labeled transition rules and context closure.

If this is right

  • Equivalence proofs can use labeled transitions without separately quantifying over all possible contexts.
  • Bisimulation techniques become interchangeable with observational checks for security properties.
  • The result supports modular reasoning in protocol analysis without switching between equivalence notions.
  • Extensions of the calculus can inherit the coincidence once their semantics are shown to preserve the same barbs and transitions.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Automated tools could implement a single equivalence checker based on the labeled side and still cover observational properties.
  • The simpler proof structure may transfer to related calculi that share barb observation and labeled reduction rules.
  • One could test whether adding new primitives such as probabilistic choice preserves the coincidence without a full re-proof.

Load-bearing premise

The standard definitions of observational equivalence via barbs and contexts and of labeled equivalence via labeled transitions are taken exactly as given in prior literature.

What would settle it

An explicit pair of extended processes that are related by one equivalence relation but not the other.

read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 2 minor

Summary. The paper presents a significantly simpler proof that observational equivalence (defined via barbs and closing under contexts) coincides with labeled equivalence (defined via the standard labeled transition system) for extended processes in the applied pi-calculus. The argument establishes the two directions of inclusion using the usual reduction semantics and equational theory for messages, without additional restrictions on the signature.

Significance. The coincidence of these equivalences is a foundational result in applied pi-calculus, justifying the use of labeled transitions to reason about observational properties in security protocol analysis. A self-contained and simpler proof, if correct, enhances accessibility and supports extensions of the calculus; the manuscript's use of standard definitions and mutual-inclusion structure is a clear strength.

minor comments (2)
  1. The claim of a 'significantly simpler' proof would benefit from a short explicit comparison (in the introduction or conclusion) to the length and structure of the original argument in Abadi and Fournet (2001) or subsequent presentations.
  2. Notation for extended processes, barbs, and the LTS rules should be collected in a single preliminary section before the proof begins, to improve readability for readers unfamiliar with the precise formulation.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive assessment of the manuscript, recognition of its significance as a foundational result, and recommendation for minor revision. We appreciate the acknowledgment that the proof is self-contained, uses standard definitions, and avoids additional restrictions on the signature.

Circularity Check

0 steps flagged

No significant circularity

full rationale

The manuscript supplies a self-contained proof that observational equivalence coincides with labeled equivalence for extended processes in applied pi-calculus. The argument proceeds by mutual inclusion using the standard definitions of barbs, contexts, reduction semantics, and the labeled transition system taken directly from prior literature; no step reduces a claimed prediction or uniqueness result to a fitted parameter, self-definition, or load-bearing self-citation whose justification is internal to the present paper. All steps remain within the usual equational theory for messages and impose no additional restrictions, rendering the derivation independent of its own inputs.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

Based on the abstract, the paper relies on standard background from the applied pi-calculus literature rather than introducing new parameters or entities.

axioms (1)
  • domain assumption Standard operational semantics and equational theory of applied pi-calculus
    The proof assumes the usual reduction rules, labeled transitions, and message algebra as defined in prior work.

pith-pipeline@v0.9.0 · 5544 in / 1082 out tokens · 32110 ms · 2026-05-18T09:29:02.314432+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.