Open Bisimilarity for the $\pi$-Calculus with Mismatch

The $\pi$-calculus is a mathematical model developed for studying and describing concurrent systems, particularly focusing on how these systems can communicate and change their structures dynamically. It was introduced by Milner, Parrow, and Walker in the late 1980s and early 1990s [18, 19]. Within this framework, equivalence relations, known as bisimilarities, were developed to compare the behaviors of processes. Milner, Parrow and Walker initially defined the late and early bisimilarity [19], which provide foundational approaches for reasoning about process equivalence. Later, Sangiorgi and Walker extended these notions by introducing open bisimilarity [22] and quasi-open bisimilarity [23], which allow for a more flexible treatment of free and bound names. These extensions address limitations in the original definitions, particularly with respect to handling name instantiation and substitution.

An important property for an equivalence relation in the $\pi$-calculus is that it is a congruence. A congruence relation ensures that if two processes are bisimilar, they remain bisimilar in any context. While late and early bisimilarities fail to satisfy congruence, as they are not preserved by the input prefix operator, both open and quasi-open bisimilarities are congruence relations. This property guarantees that if two processes are shown to be open or quasi-open bisimilar, they will exhibit identical behavior under any contextual composition.

However, Sangiorgi’s definition does not account for the mismatch operator $[x\ne y]P$, which is crucial for modeling protocols that require explicit distinctions between names. The mismatch operator, denoted as $[x\ne y]P$, enables a process $P$ to proceed only if the names $x$ and $y$ are distinct. If $x$ and $y$ are the same, the process cannot proceed and essentially behaves like the deadlock process $0$.

We are particularly interested in congruence relations (open and quasi-open bisimilarity). With congruence, one can prove equivalence for individual components of a system and infer equivalence for the entire system without re-evaluating interactions in every context. This greatly simplifies reasoning about correctness and facilitates the modular design of mobile systems, where processes often operate in dynamic and evolving environments. While quasi-open bisimilarity with mismatch has been explored and formalised in previous work [13], open bisimilarity with mismatch remains an open topic. In this paper, we fill this gap by extending Sangiorgi’s original definition of open bisimilarity to include mismatch.

Our interests in (quasi-)open bisimulation stem from its operational nature that brings it closer to implementation. In particular, it gets rid of one source of infinity – the quantification over all input when reasoning about processes that are parameteric on the input they receive. The lazy treatment of input values in open bisimulation is similar to that of symbolic bisimulation [12, 7], but with the additional advantage of being a congruence. The former allows for practical implementations of bisimulation checkers for the $\pi$-calculus and its extensions (see e.g., [5, 27, 26]), while the latter has been shown to be crucial in reasoning about privacy properties of security protocols formalised in the applied-pi calculus, a cryptographic extension of the $\pi$-calculus [15]. The addition of mismatch enables processes to make decisions based on name inequalities. This capability allows one to, for example, encode a typical if-then-else construct in programming languages and protocols, with the else branch corresponds to the mismatch prefix. This use of the mismatch operator is important in modeling real-world protocols, as such protocols typically incorporate various error conditions (that are typically captured in the else-branch of a decision point) that could potentially lead to privacy leakage, as shown in cryptographic extensions of the $\pi$-calculus, e.g., [4, 9]. By studying mismatch in a minimal setting in the $\pi$-calculus, we hope to gain insights into its uses in (cryptographic) extensions of the $\pi$-calculus.

In most presentations of the $\pi$-calculus including the original syntax, the mismatch operator is absent for several reasons. Firstly, introducing mismatch can violate the monotonicity property of substitutions in the $\pi$-calculus. Substitutions typically should not reduce the capability of a process for action [24, Chapter 1.1]. Formally, if $P\stackrel{𝛼}{\to }{P}^{\prime }$, then we want $P\sigma \stackrel{\alpha \sigma }{\to }{P}^{\prime }\sigma$ for all possible $\sigma$ [20]. However, mismatch can lead to situations where two originally distinct names become identical after substitution, resulting in a process being less capable of performing actions due to name equality. For example, $[x\ne y]\tau$ can perform a $\tau$-transition, but when we apply the substitution $\{y/x\}$, the process transforms into $[y\ne y]\tau$ which equals $0$. Secondly, a naive extension of open bisimilarity with mismatch would result in a non-compositional open bisimilarity, breaking the congruence property that ensures the open bisimilarity is preserved under all contexts. We will use counterexamples to illustrate this point in the next section.

To maintain the monotonicity property, one crucial measure is to impose some restrictions on the substitution of names. We stipulate that, without any further assumptions, $[x\ne y]P$ can only execute if it is guaranteed that $x$ and $y$ can never become equal under an arbitrary context that can potentially modify $x$ or $y$, e.g., if the process is nested inside an input prefix binding $x$ or $y$. To account for the interactions between input names and restricted names (induced by scope extrusion in the $\pi$-calculus), a notion of name distinctions [22] is introduced in both the operational semantics of the $\pi$-calculus and our new definition of open bisimulation. Under this definition, these two processes $[x\ne y]\tau$ and $\tau$ can be distinguished using open bisimilarity because the former can perform a $\tau$-transition only if the inequality between $x$ and $y$ is ensured, i.e., $x$ and $y$ cannot be equal under any possible substitutions, while the latter can perform the $\tau$-transition unconditionally.

Horne et al. [13] introduced an extended definition of quasi-open bisimilarity that incorporates mismatch. In the same work, they also explored open bisimilarity with mismatch, proposing an extended definition based on a history-indexed syntax that allows histories to be prepended. An alternative extension of open bisimilarity was proposed in [17], also utilizing history-indexed syntax, but leveraging on a certain rigidisation relation. However, as we will demonstrate in Section 3, these definitions are fundamentally unsound in a strong sense, i.e., they are not preserved by parallel composition. We propose here a new definition of open bisimilarity that extends only slightly Sangiorgi’s original definition, by essentially requiring open bisimilarity to be preserved by additions of name distinctions. We then prove that this new open bisimilarity is both an equivalence relation and a congruence.

We touch on some related work on process calculi featuring mismatch and work on open bisimilarity.

Parrow and Victor introduced the fusion calculus [21], which is a unified communication model where name equivalence and name fusion replace name-passing and scope extrusion, simplifying the core concepts of mobility. The Fu and Yang provided complete axiomatizations for fusion calculus both with and without the mismatch operator. The paper discusses how mismatch can complicate the semantics but is essential for certain types of behavioral equivalences and conditions. In [11], the authors investigated weak bisimulation congruences for finite $\pi$-calculus processes, focusing on challenges posed by the mismatch operator. The paper demonstrates that the standard definition of weak open congruence leads to problematic equivalence relations when mismatch is included, and proposes two alternatives: late open congruence and early open congruence.

Open bisimulation shares many similarities with symbolic bisimulation, in particular in its “lazy” treatment of name instantiations. Symbolic bisimulation has been extensively studied for different calculi: For value-passing CCS, Hennessy and Lin [12] generalised the standard notion of labelled transition graphs to symbolic transition graphs, allowing the operational semantics of value-passing processes to be represented in finite terms even when the underlying transition graph is infinite. This work introduces algorithms applicable to early and late bisimulation equivalences, extending the scope of standard bisimulation techniques. Symbolic bisimulation for the $\pi$-calculus was addressed in [7], where symbolic transition systems are tailored to handle mobility and dynamic process communication, culminating in a sound and complete proof system for symbolic bisimulation. Delaune et al. proposed a symbolic semantics for the finite applied $\pi$-calculus [10], adapting symbolic bisimulation for modeling cryptographic protocols. While this approach is sound, it is not complete, primarily automating observational equivalence under constraints from external inputs. A more comprehensive framework was proposed in [16], which achieved both soundness and completeness for symbolic bisimulation in the full applied $\pi$-calculus. This framework also supports replication and other complex constructs, making it suitable for equivalence checking in dynamic and security-critical systems.

The original semantics provided for the applied $\pi$-calculus is sound and complete with respect to observational equivalence [1]. However, as we know, observational equivalence is not closed under input prefix, as per its definition in the context of protocol verification. This distinguishes it fundamentally from open bisimulation. Early work on symbolic bisimulation for CCS and its subsequent extension to the $\pi$-calculus can be characterised as “classical”. In these approaches, labelled transition semantics are indexed by constraints – arising from name equality or inequality in the $\pi$-calculus, and more complex terms in the applied $\pi$-calculus. Different solutions to these constraints correspond to different continuations of a given symbolic process. The constraint languages employed are based on classical logic, inherently incorporating the principle of the excluded middle for names ($x=y\vee x\ne y$). As demonstrated in [3], open bisimulation, in contrast, is inherently intuitionistic. Consequently, symbolic bisimulations are distinct from open bisimulation at that fundamental level.

Horne and Mauw have explored open bisimilarity in the applied $\pi$-calculus that features mismatch. In [14], they introduced a generalisation of the distinction relation to sets of inequalities between terms, where inequalities act as constraints that exclude unifying messages under an equational theory. Their framework was developed to support a chain of techniques for verifying privacy properties in a real-world ePassport case study, highlighting the practical relevance of open bisimilarity in applied security protocols. While their work demonstrates the applicability of the concept in a more expressive calculus, it does not establish a congruence result for the proposed bisimilarity. In contrast, this paper addresses this theoretical gap in the simpler setting of the $\pi$-calculus with mismatch, where many of the core challenges of compositional reasoning arise.

In this section we review the syntax and operational semantics of the finite fragment (i.e., the fragment without replication or recursion) of the $\pi$-calculus and open bisimilarity.

As mentioned in the introduction, maintaining the monotonicity property requires imposing certain restrictions on name substitution. Several works have attempted to address this challenge. In this section, we review existing approaches to incorporating mismatch into open bisimilarity and discuss the shortcomings of each approach.

Horne at al. [13] presented an extended open bisimilarity using the notion of history $h$, which is a list of names annotated with either $i$ (denoting an input name) or $o$ (denoting an output name). A history $h$ captures the sequence of names that a process sends and receives during its transitions. It is essentially a (partial) trace of a process. The use history-indexed open bisimulation was first proposed in [25] for the spi-calculus [2], a cryptographic extension of the $\pi$-calculus, although the idea dates back to the encoding of the $\pi$-calculus in a logical framework [27], where the quantifier alternation used in statements surrounding bisimilarity captures the notion of histories we use here. A history or a quantifier alternation gives rise to an implicit encoding of distinction, and is very natural from both the logical and an implementation perspective. The latter, for example, could build on existing logical frameworks (such as [5]) to provide a simple implementation of open bisimulation. It is thus a natural question to ask whether one could reformulate open bisimulation using histories to encode distinctions. The answer for the case without mismatch is in the affirmative; in the presence of mismatch, this turns out to be not true. We shall come back to this in Section 6.

We simplify the notion of histories from [25] to include only names, rather than general terms. Names annotated with $o$ (written as $z^o$) represent the output names that a process emits in its bound output transitions. Conversely, names annotated with $i$ (written as $z^i$) signify the symbolic inputs (i.e., variables) received by the process. The difference between these two types of annotations is formalised in the following definition of respectful substitutions.

In this context, the $o$-annotated names act like constants, while $i$-annotated names act like scoped variables, with their scoping determined by their relative positions in the history. Viewing a history as a trace of names that a process inputs and outputs, this scoping ensures that a name received earlier in the trace cannot be identified with a fresh name outputted later. Tiu and Miller have discussed in [27, Corollary 22] that open bisimulation indexed by histories does not affect the resulting notion of bisimilarity compared to Sangiorgi’s original definition.

Given a history $h$, it is easy to generate a distinction that can functionally replace $h$. Let $P$ and $Q$ be two processes, $h$ be a history. Define a distinction $D_h$ from $h$ such that

The converse does not hold, as not all possible distinctions can be represented as histories. However, the open bisimilarity relation (i.e., the largest open bisimulation), defined via the history-indexed style, coincides with Sangiorgi’s original definition (Definition 2), as one can show that open-bisimilarity between two processes (under the empty distinction) can be witnessed by a bisimulation relation indexed only by distinctions that are representable as histories [27].

With the history-indexed semantics, the operational semantics of mismatch can be adapted as follows.

where $h\vDash x\ne y\text{iff}x\sigma \ne y\sigma$ for all $\sigma$ respecting $h$. Other operational semantics can be indexed by history similarly.

This semantics successfully preserves the monotonicity rule mentioned in the introduction. The history-indexed monotonicity rule can be stated as: Suppose $h:P\stackrel{𝜋}{\to }Q$. Then $h\sigma :P\sigma \stackrel{\pi \sigma }{\to }Q\sigma$ for all $\sigma$ that respect $h$ and satisfy for all $x\in \mathrm{bn}(\pi )$, $y\sigma =x$ iff $x=y$. The proof that monotonicity holds with the history-indexed mismatch rule is provided in [17].

While the monotonicity issue has been resolved, the congruence problem remains challenging. Let us look at a history-indexed open bisimilarity defined in [17].

This definition aligns with Sangiorgi’s open bisimilarity (Def. 2). In the third clause with bound output transitions, the history (environment) is updated with a fresh private name, which serves the same function as adding the fresh name to the distinction set.

This definition is not congruent in the presence of the mismatch operator. The process $[x\ne y]\tau$ under the history $h=x^i\cdot y^i$ is open bisimilar to $0$, as there exists a respectful substitution $\{x/y\}$ that invalidates $x\ne y$, thereby preventing the $\tau$-transition from $[x\ne y]\tau$. However, this open bisimilarity does not extend to $\overline{a}(x).[x\ne y]\tau$ and $\overline{a}(x).0$ under the history $h^{\prime }=y^i\cdot x^o$, since $[x\ne y]$ always holds under the history $h^{\prime }$.

To address this limitation, a few studies have been conducted. Horne et. al. [13] provided an extended version of the history-indexed open bisimilarity that allows to extend histories in the past, which gives rise to a strictly coarser semantics. Their definition can be stated as follows.

The above definition extends the original open bisimilarity by the second clause allowing for the prepending of history, enabling the incorporation of additional environmental information.

As it turns out, however, this semantics is not compositional.

In another attempt to address the issue [17], the authors resolved the monotonicity problem leveraging history-indexed operational semantics. Then to address the congruence property, they introduced the concept of rigidisation to refine open bisimilarity. The rigidisation of names allows us transforming an i-annotated name into an o-annotated name.

Then open bisimilarity is extended by adding the second clause using the rigidisarion relation.

This definition is also not compositional, as the following counterexample shows.

We now present our approach to incorporating mismatch in open bisimulation in a way that ensures the resulting bisimilarity is a congruence.

We reflect here on semantically different definitions of open bisimilarity with mismatch. A question is whether open bisimilarity, as in Def. 13, has an equivalent definition in terms of histories, by extending Def. 5 to allow more histories to be induced. In particular, an extended definition could permit more permutations such that inputs behave like universal quantifiers and outputs of fresh names like nominal quantifiers. This is a natural question, since several deep embeddings of the $\pi$-calculus work in this way.

It turns out that using (linear) histories would result in a distinct semantics. Consider the following example process.

Clearly, according to Def. 13 these processes are not open bisimilar, since we can extend the set of distinction with the inequalities $x\ne y$ and $w\ne z$ without having to decide whether any of the other inequalities hold.

If however a ground output in a history were used to induce $x\ne y$ and $w\ne z$ then we require a history with $x^i$ before $y^o$ or $x^o$ before $y^i$. In the same history we also require $w^i$ before $z^o$ or $z^o$ before $w^i$. Without loss of generality suppose that $x^i$ is before $y^o$ and $w^i$ is before $z^o$ in a history. Now, since a history is an ordered sequence of inputs and outputs we have that $w^i$ is before $y^o$ or $y^o$ is before $w^i$, as considered here.

• $\mathrm{■}$

  If $w^i$ is before $y^o$, then we have that $w\ne y$ holds and hence a $\tau$ transition is enabled for both processes.

• $\mathrm{■}$

  If $y^o$ is before $w^i$, then since we assumed also that $x^i$ is before $y^o$ and $w^i$ is before $z^o$ we have that $x^i$ is before $z^o$. Hence $x\ne z$ holds and hence a $\tau$ transition is enabled for both processes.

Thus, regardless of how the definition is constructed, if a definition of open bisimilarity relies on a linear history to force distinctions, the processes $P$ and $Q$ above will be open bisimilar.

This paper presents a novel definition of open bisimilarity for the $\pi$-calculus that integrates the mismatch operator. Mismatch, while crucial for modeling protocols requiring explicit name distinctions, introduces challenges such as violating the congruence property and breaking monotonicity. Building on Sangiorgi’s original framework, we address these issues by introducing a distinction-indexed operational semantics that allows for arbitrary extensions of distinctions. Our approach ensures that open bisimilarity remains a congruence relation even in the presence of mismatch. While prior approaches that relied on history-indexed relations or rigidisation strategies did not achieve compositionality, our method successfully addresses this limitation while also providing greater simplicity and conceptual clarity. Through formal proofs, we demonstrated that the extended open bisimilarity is both equivalent and congruent. This makes it a robust and expressive framework for reasoning about mobile processes and communication protocols, enabling better modeling of real-world systems.

As immediate future work, we plan to formalise the results of this paper in the theorem prover Isabelle/Nominal [28], building on an existing formalisation of the $\pi$-calculus [6].

Another avenue for possible future work is to generalise our transition semantics to be parameterised by logical constraints. Logically speaking, both distinctions and substitutions can be seen as expressing a conjunction of (in)equalities between names. This can be generalised in at least two possible directions: one in which we allow expressions of (in)equalities between (algebraic) terms (like those arising from the transition semantics for the applied $\pi$-calculus [1, 14]) and another where we allow other logical connectives (e.g., disjunction, implication, quantifiers). In such an extension, it is then natural to ask how such a logical constraint should be interpreted semantically, e.g., whether it should be viewed as a formula in classical (first-order) logic, or intuitionistic logic. We conjecture that the first interpretation (in classical logic) would give rise to the notion of symbolic bisimulation [12], and the second interpretation would give rise to open bisimulation. Work on symbolic bisimilarity for the $\psi$-calculus [8] takes a step in this direction. The $\psi$-calculus is parametrised on a constraint system that can be very general. Notably in Sec. 7 of the aforementioned paper a constraint logic is defined that must be classical for the completeness results in that paper to hold. By simply working without the law of excluded middle, we hypothesise that a notion of open bisimulation for $\psi$-calculi is obtained where the constraint logic can otherwise be general.