# On the Realizability of Contracts in Dishonest Systems

Massimo Bartoletti, Emilio Tuosto, Roberto Zunino

► To cite this version:

Massimo Bartoletti, Emilio Tuosto, Roberto Zunino. On the Realizability of Contracts in Dishonest Systems. 14th International Conference on Coordination Models and Languages (COORDINATION), Jun 2012, Stockholm, Sweden. pp.245-260, 10.1007/978-3-642-30829-1_17. hal-01529594

HAL Id: hal-01529594

https://inria.hal.science/hal-01529594

Submitted on 31 May 2017

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# On the realizability of contracts in dishonest systems

Massimo Bartoletti¹, Emilio Tuosto², and Roberto Zunino³

¹ Dipartimento di Matematica e Informatica, Università degli Studi di Cagliari, Italy

² Department of Computer Science, University of Leicester, UK

³ DISI, Università di Trento and COSBI, Italy

**Abstract.** We develop a theory of contracting systems, where behavioural contracts may be violated by dishonest participants after they have been agreed upon — unlike in traditional approaches based on behavioural types. We consider the contracts of [10], and we embed them in a calculus that allows distributed participants to advertise contracts, reach agreements, query the fulfilment of contracts, and realise them (or choose not to). Our contract theory makes explicit who is culpable at each step of a computation. A participant is honest in a given context S when she is not culpable in each possible interaction with S. Our main result is a sufficient criterion for classifying a participant as honest in all possible contexts.

## 1 Introduction

Contracts are abstract descriptions of the behaviour of services. They are used to compose services which are *compliant* according to some semantic property, e.g. the absence of deadlocks [6, 9, 10], the satisfaction of a set of constraints [8], or of some logical formula [1, 4, 15]. Most of the existing approaches tacitly assume that, once a set of compliant contracts has been found, then the services that advertised such contracts will behave accordingly. In other words, services are assumed to be *honest*, in that they always respect the promises made.

In open and dynamic systems, the assumption that all services are honest is not quite realistic. In fact, services have different individual goals, are made available by different providers, and possibly do not trust each other. What happens is that services agree upon some contracts, but may then violate them, either intentionally or not. Since this situation may repeatedly occur in practice, it should not be dealt with as the failure of the whole system. Instead, contract violations should be automatically detected and sanctioned by the service infrastructure.

The fact that violations may be sanctioned gives rise to a new kind of attacks, that exploit possible discrepancies between the promised and the runtime behaviour of services. If a service does not accurately behave as promised, an attacker can induce it to a situation where the service is sanctioned, while the attacker is reckoned honest. A crucial problem is then how to avoid that a service results *culpable* of a contract violation, despite of the honest intentions of its developer. More formally, the problem is that of deciding if a process *realizes* a contract: when this holds, the process is guaranteed to never be culpable w.r.t. the contract in all the possible execution contexts.

In this paper we develop a formal theory of contract-oriented systems that enjoys a sound criterion for establishing if a process always realizes its contracts. Our theory
combines two basic ingredients: a calculus of contracts, and a calculus of processes that use contracts to interact. Contracts are used by distributed participants to reach agreements; once stipulated, participants can inspect them and decide what to do next.

Ideally, a honest participant is supposed to harmoniously evolve with her contracts; more realistically, our theory also encompasses computations of *dishonest* participants, which may violate at run-time some contracts they have stipulated. A remarkable result (Theorem 2) is that it is always possible to detect who is culpable of a contract violation at each state of a computation. Also, a participant can always exculpate herself by performing the needed actions (Theorems 1 and 3).

Notably, instead of defining an ad-hoc model, we have embedded the contract calculus in [10] within the process calculus CO₂ [2]. To do that, the contracts of [10] have been slightly adapted to define culpability, and CO₂ has been specialized to use these contracts. We have formalised when a participant realizes a contract in a given context, i.e. when she is never (irreparably) culpable in computations with that context, and when she is *honest*, i.e. when she realizes *all* her contracts, in *all* possible contexts. We have proved that the problem of deciding whether a participant is honest or not is undecidable (Theorem 4). Our main contribution (Theorem 6) is a sound criterion for detecting when a participant is honest. Technically this is achieved through a semantics of participants that abstracts away the behaviour of the context. Such semantics allows us to define when a participant always fulfills her contracts, even in the presence of dishonest participants.

Because of space constraints, we include the proofs of all our statements in a separated Technical Report [3].

## 2 A calculus of contracts

We assume a finite set of *participant names* (ranged over by A, B, ...) and a denumerable set of *atoms* (ranged over by a, b, ...). We postulate an involution $co(a)$, also written as $\bar{a}$, extended to sets of atoms in the natural way.

Def. 1 introduces the syntax of contracts, taking inspiration from [10]. We distinguish between (unilateral) contracts c, which model the promised behaviour of a single participant, and bilateral contracts $\gamma$, which combine the contracts of two participants.

**Definition 1.** Unilateral contracts are defined by the following grammar:

$$c,d ::= \bigoplus_{i \in I} a_i; c_i \mid \sum_{i \in I} a_i \cdot c_i \mid \text{ready } a.c \mid \text{rec } X.c \mid X$$

where (i) the index set 1 is finite; (ii) the atoms in $\{a_i\}_{i \in I}$ are pairwise distinct; (iii) the ready prefix may appear at the top-level, only; (iv) recursion is guarded.

Let $e$ be a distinguished atom such that $e = \bar{e}$, and with continuation $E = \text{rec } X.e; X$. We say that $c$ succeeds iff either $c = e; E \oplus d$, or $c = e; E + d$, or $c = \text{ready } e; E$. We will omit trailing occurrences of $E$ in contracts.

Bilateral contracts are terms of the form $A \text{ says } c \mid B \text{ says } d$, where $A \neq B$ and at most one occurrence of ready is present.
A says (a; c ⊕ c') | B says (ā.d + d') $\mathop{\longrightarrow}_{A \text{ says a}}$ A says c | B says ready ā.d [INTEXT]

A says (a; c ⊕ c') | B says ā; d $\mathop{\longrightarrow}_{A \text{ says a}}$ A says c | B says ready ā.d [INTINT]

A says (a.c + c') | B says (ā.d + d') $\mathop{\longrightarrow}_{A \text{ says a}}$ A says c | B says ready ā.d [EXTEXT]

A says ready a. c | B says d $\mathop{\longrightarrow}_{A \text{ says a}}$ A says c | B says d [RDY]

$\frac{a \notin co(\{b_i\}_{i \in I})}{A \text{ says } a; c \oplus c' | B \text{ says } \sum_{i \in I} b_i \cdot d_i \mathop{\longrightarrow}_{A \text{ says } a} A \text{ says } E | B \text{ says } 0}$ [INTEXTFAIL]

$\frac{\{a\} \neq co(\{b_i\}_{i \in I})}{A \text{ says } a; c \oplus c' | B \text{ says } \bigoplus_{i \in I} b_i \cdot d_i \mathop{\longrightarrow}_{A \text{ says } a} A \text{ says } E | B \text{ says } 0}$ [INTINTFAIL]

$\frac{(\{a\} \cup \{a_i\}_{i \in I}) \cap co(\{b_i\}_{i \in J}) = \emptyset}{A \text{ says } (a.c + \sum_{i \in I} a_i \cdot c_i) | B \text{ says } \sum_{i \in J} b_i \cdot d_i \mathop{\longrightarrow}_{A \text{ says } a} A \text{ says } E | B \text{ says } 0}$ [EXTEXTFAIL]

<caption>Fig. 1. Semantics of contracts (symmetric rules for B actions omitted)</caption>

Intuitively, the internal sum $\bigoplus_{i \in I} a_i$; $c_i$ allows to choose one of the branches $a_i$; $c_i$, to perform the action $a_i$, and then behave according to $c_i$. Dually, the external sum $\sum_{i \in I} a_i \cdot c_i$ constrains to wait for the other participant to choose one of the branches $a_i \cdot c_i$, then to perform the corresponding $a_i$ and finally behave according to $c_i$. Separators ; and . allow us to distinguish singleton internal sums (e.g., a; c) from singleton external sums (e.g., a.c). The atom e (for “end”) enables a participant to successfully terminate, similarly to [10]. This will be reflected in Def. 4. Hereafter, we shall always consider contracts with no free occurrences of recursion variables X. We shall use the binary operators to isolate a branch in a sum: e.g. $(a; c) \oplus c'$ where $c'$ is an internal sum. We let ; and . have higher precedence than $\oplus$ and $+$, e.g., $a; c \oplus b$; $c' = (a; c) \oplus (b; c')$.

The evolution of bilateral contracts is modelled by a labelled transition relation $\stackrel{\mu}{\Rightarrow}$ (Def. 2), where labels $\mu = A \text{ says } a$ model a participant A performing the action a.

**Definition 2.** The relation $\stackrel{\mu}{\Rightarrow}$ on bilateral contracts is the smallest relation closed under the rules in Fig. 1 and under the structural congruence relation $\equiv$, defined as the least congruence which includes $\alpha$-conversion of recursion variables, and satisfies $\text{rec } X. c \equiv c\{\text{rec } X. c/x\}$ and $\bigoplus_{i \in \emptyset} a_i$; $c_i \equiv \sum_{i \in \emptyset} a_i \cdot c_i$. Accordingly, empty sums (either internal or external) will be denoted with 0. We will not omit trailing occurrences of 0. Hereafter we shall consider contracts up to $\equiv$.

In the first three rules in Fig. 1, A and B expose complementary actions a, ā. In rule [INTEXT], participant A selects the branch a in an internal sum. Participant B is then forced to commit to the corresponding branch ā in his external sum: this is done by marking that branch with ready ā while discarding all the other branches. Participant B will then perform his action in the subsequent step, by rule [RDY]. In rule [INTINT], both participants make an internal choice; a reaction is possible only if one of the two is
a singleton — B in the rule — namely he can only commit to his unique branch. Were B exposing multiple branches, the transition would not be allowed, to account for the fact that B could pick a conflicting internal choice w.r.t. that of A. In rule [EXTExt], both participants expose external sums with complementary actions, and each of the two can choose a branch (unlike in the case [INTExt], where the internal choice has to move first). In the [*FAIL] rules, the action chosen by A is not supported by B. Then, A will reach the success state E, while B will fall into the failure state 0.

*Example 1.* Let $\gamma = A \text{ says } (\mathbf{a}; c_1 \oplus \mathbf{b}; c_2) \mid B \text{ says } (\bar{\mathbf{a}}.d_1 + \bar{\mathbf{c}}.d_2)$. If the participant A internally chooses to perform a, then $\gamma$ will take a transition to $A \text{ says } c_1 \mid B \text{ says ready } \bar{\mathbf{a}}.d_1$. Suppose instead that A chooses for perform b, which is not offered by B in his external choice. In this case, $\gamma$ will take a transition to $A \text{ says } E \mid B \text{ says } 0$, where 0 indicates that B cannot proceed with the interaction. Coherently with [10], below we will characterise this behaviour by saying that the contracts of A and B are *not* compliant.

The following lemma states that bilateral contracts are never stuck unless both participants have contract 0. Actually, if none of the first four rules in Fig. 1 can be applied, the contract can make a transition with one of the [*FAIL] rules.

**Lemma 1.** A bilateral contract $A \text{ says } c \mid B \text{ says } d$ is stuck iff $c = d = 0$.

Below we establish that contracts are deterministic. This is guaranteed by the requirement (ii) of Def. 1. Determinism is a very desirable property indeed, because it ensures that the duties of a participant at any given time are uniquely determined by the past actions. Note that the contracts in [10] satisfy distributivity laws like $(\mathbf{a}; c) \oplus (\mathbf{a}; d) = \mathbf{a}$; $(c \oplus d)$, which allow for rewriting them so that (ii) in Def. 1 holds. Therefore, (ii) is not a real restriction w.r.t. [10].

**Lemma 2 (Determinism).** For all $\gamma$, if $\gamma \stackrel{\mu}{\Rightarrow} \gamma'$ and $\gamma \stackrel{\mu}{\Rightarrow} \gamma'$, then $\gamma = \gamma'$.

*Compliance.* Below we define when two contracts are *compliant*, in a similar fashion to [10]. Intuitively, two contracts are compliant if whatever sets of choices they offer, there is at least one common option that can make the contracts progress. Differently from [10], our notion of compliance is symmetric, in that we do not discriminate between the participant roles as client and server. Consequently, we do not consider compliant two contracts where only one of the parties is willing to terminate. For example, the buyer contract ship; E is not compliant with the seller contract ship. pay; E, because the buyer should not be allowed to terminate if the seller still requires to be paid.

Similarly to [10], given two contracts we observe their *ready sets* (Def. 3) to detect when the enabled actions allow them to synchronise correctly.

**Definition 3 (Compliance).** For all contracts $c$, we define the set of sets $RS(c)$ as:

$$RS(0) = \{\emptyset\} \qquad RS(\text{ready a.c}) = \{\text{ready}\} \qquad RS(\text{rec X. c}) = RS(c) \\ RS(\bigoplus_{i \in I} a_i; c_i) = \{\{a_i\} \mid i \in I\} \text{ if } I \neq \emptyset \qquad RS(\sum_{i \in I} a_i \cdot c_i) = \{\{a_i\} \mid i \in I\} \text{ if } I \neq \emptyset$$

The relation $\bowtie$ between contracts is the largest relation such that, whenever $c \bowtie d$:

$$ (1) \quad \forall x \in RS(c), y \in RS(d). \text{ co}(x) \cap y \neq \emptyset \text{ or } ready \in (x \cup y) \setminus (x \cap y) $$
$$ (2) \quad A \text{ says } c \mid B \text{ says } d \xrightarrow{\mu} A \text{ says } c' \mid B \text{ says } d' \implies c' \unlhd d' $$

When $c \unlhd d$, we say that the contracts $c$ and $d$ are compliant.

**Example 2.** Recall from Ex. 1 the contracts $c = a; c_1 \oplus b; c_2$ and $d = \bar{a} \cdot d_1 + \bar{c} \cdot d_2$. We have that $RS(c) = \{\{a\}, \{b\}\}$, and $RS(d) = \{\{\bar{a}, \bar{c}\}\}$, which do not respect item (1) of Def. 3 (take $x = \{b\}$ and $\gamma = \{\bar{a}, \bar{c}\}$). Therefore, $c$ and $d$ are not compliant.

The following lemma provides an alternative characterization of compliance. Two contracts are compliant iff, when combined into a bilateral contract $\gamma$, no computation of $\gamma$ reaches a state where one of the contracts is 0. Together with Lemma 1, we have that such $\gamma$ will never get stuck. (Below, the Kleene * denotes reflexive transitive closure.)

**Lemma 3.** For all bilateral contracts $\gamma = A \text{ says } c \mid B \text{ says } d$:

$$ c \unlhd d \iff (\forall c', d'. \gamma \to^* A \text{ says } c' \mid B \text{ says } d' \implies c' \neq 0 \text{ and } d' \neq 0) $$

The following lemma guarantees, for all $c$ not containing 0, the existence of a contract $d$ compliant with $c$. Intuitively, we can construct $d$ from $c$ by turning internal choices into external ones (and viceversa), and by turning actions into co-actions.

**Lemma 4.** For all 0-free contracts $c$, there exists $d$ such that $c \unlhd d$.

**Culpability.** We now tackle the problem of determining who is expected to make the next step for the fulfilment of a bilateral contract. We call a participant A *culpable* in $\gamma$ if she is expected to perform some action so to make $\gamma$ progress. Also, we consider A *culpable* when she is advertising the “failure” contract 0. This agrees with our [*FAIL*] rules, which set A’s contract to 0 when the other participant legitimately chooses an action not supported by A. Note that we do not consider A *culpable* when her contract has enabled e actions.

**Definition 4.** A participant A is *culpable* in $\gamma = A \text{ says } c \mid B \text{ says } d$, written $A \unlhd \gamma$, iff:

$$ c = 0 \lor \left( \gamma \underset{A \text{ says e}}{\overset{A \text{ says e}}{\rightleftharpoons}} \land \exists a. \gamma \underset{A \text{ says a}}{\overset{A \text{ says a}}{\rightleftharpoons}} \right) $$

When A is not *culpable* in $\gamma$ we write $A \unlhd \gamma$.

The following result states that a participant A is always able to recover from culpability by performing some of her duties. Furthermore, this requires at most two steps in an “A-solo” trace where no other participant intervenes.

**Definition 5.** Let $\rightarrow$ be an LTS with labels of the form $A_i \text{ says } (\cdots)$, for $A_i$ ranging over participants names. For all A, we say that $a \rightarrow$-trace $\eta$ is A-solo iff $\eta$ only contains labels of the form A says (\cdots). If $\eta = (\mu_i)_{i \in 0..n}$, we will write $\eta \xrightarrow{\mu_0} \text{ for } \mu_0 \xrightarrow{\cdots} \mu_n$.

**Theorem 1 (Contractual exculpation).** For all $\gamma = A \text{ says } c \mid B \text{ says } d$ with 0-free $c$, there exists $\gamma'$ and A-solo $\eta$ with $|\eta| \le 2$ such that $\gamma \xrightarrow{\eta} \gamma'$ and $A \unlhd \gamma'$.
commutative monoidal laws for on processes and systems

$$
\begin{array}{l@{\qquad}l@{\qquad}l}
u[(v)P] \equiv (v)u[P] & \text{if } u \neq v & Z \mid (u)Z' \equiv (u)(Z \mid Z') \text{ if } u \notin \text{fv}(Z) \cup \text{fn}(Z) & (u)(v)Z \equiv (v)(u)Z \\
(u)Z \equiv Z & \text{if } u \notin \text{fv}(Z) \cup \text{fn}(Z) & A[K] \mid A[P] \equiv A[K \mid P] & \downarrow_s c \equiv \mathbf{0} \equiv \text{fuse}_s \cdot P
\end{array}
$$

<caption>**Fig. 2.** Structural equivalence for CO₂ (Z, Z' range over systems or processes)</caption>

A crucial property of culpability is to ensure that either two participants are both succeeding, or it is possible to single out who has to make the next step. An external judge is therefore always able to detect who is violating the contracts agreed upon.

**Theorem 2.** For all $c, d$ if $c \triangleright d$ and $A$ says $c \mid B$ says $d \rightarrow^* \gamma = A$ says $c' \mid B$ says $d'$, then either $c'$ and $d'$ succeed, or $A \triangleleft \gamma$, or $B \triangleleft \gamma$.

*Example 3.* A participant might be culpable even though her contract succeeds. For instance, let $\gamma = A \text{ says } c \mid B \text{ says } d$, where $c = e + \bar{a}$ and $d = a + b$. By Def. 1 we have that $c$ succeeds, but $A$ is culpable in $\gamma$ because she cannot fire $e$, while she can fire $\bar{a}$ by rule [EXTEXT]. This makes quite sense, because $A$ is saying that she is either willing to terminate or to perform $\bar{a}$, but the other participant is not allowing $A$ to terminate. Note that also $B$ is culpable, because he can fire $a$.

**3 A Calculus of Contracting Processes**

We now embed the contracts introduced in § 2 in a specialization of the parametric
process calculus CO₂ [2]. Let $\mathcal{V}$ and $\mathcal{N}$ be two disjoint countably infinite sets of ses-
sion variables (ranged over by x, y, ... ) and session names (ranged over by s, t, ... ). Let
u, v, ... range over $\mathcal{V} \cup \mathcal{N}$.

**Definition 6.** The abstract syntax of CO₂ is given by the following productions:

$$
\begin{array}{l@{\qquad}l@{\qquad}l@{\qquad}l@{\qquad}l@{\qquad}l}
\text{Systems} & S ::= & \mathbf{0} & | & A[P] & | & s[\gamma] & | & S \mid S & | & (u)S \\
\text{Processes} & P ::= & \downarrow_u A \text{ says } c & | & \sum_i \pi_i.P_i & | & P \mid P & | & (u)P & | & X(\vec{u}) \\
\text{Prefixes} & \pi ::= & \tau & | & \text{tell}_A \downarrow_u c & | & \text{fuse}_u & | & \text{do}_u a & | & \text{ask}_u \phi
\end{array}
$$

The only binder for session variables and names is the delimitation (u̅), both in sys-
tems and processes. Free variables/names are defined accordingly, and they are denoted
by fv(·) and fn(·). A system or a process is closed when it has no free variables.

Systems are the parallel composition of *participants* $A[P]$ and *sessions* $s[\gamma]$.

A *latent contract* $\downarrow_x A$ says $c$ represents a contract $c$ (advertised by $A$) which has not been stipulated yet; upon stipulation, $x$ will be instantiated to a fresh session name. We impose that in a system $A[P] \mid A[Q] \mid S$, either $P$ or $Q$ is a parallel composition of latent contracts. Hereafter, $K, K', \dots$ are meta-variables for compositions of latent contracts. We allow prefix-guarded finite sums of processes, and write $\pi_1.P_1 + \pi_2.P_2$ for $\sum_{i=1,2} \pi_i.P_i$, and $\mathbf{0}$ for $\sum_{\emptyset} P$. Recursion is allowed only for processes; for this we
<figure><img src="image_2.png" /><figcaption>**Fig. 3.** Reduction semantics of CO₂</figcaption></figure>

stipulate that each process identifier $X$ has a unique defining equation $X(u_1, \dots, u_j) \stackrel{\text{def}}{=} P$ such that $fv(P) \subseteq \{u_1, \dots, u_j\} \subseteq \mathcal{V}$ and each occurrence of process identifiers in $P$ is prefix-guarded. We shall take the liberty of omitting the arguments of $X(\vec{u})$ when they are clear from the context.

Prefixes include silent action $\tau$, contract advertisement $\text{tell}_A \downarrow_u c$, contract stipulation $\text{fuse}_{u}$, action execution $\text{do}_u a$, and contract query $\text{ask}_u \phi$. In each prefix $\pi \neq \tau$, $u$ refers to the target session involved in the execution of $\pi$. We omit trailing occurrences of **0**.

Note that participants can only contain latent contracts, while sessions can only contain bilateral contracts, constructed from latent contracts upon reaching agreements.

The semantics of CO₂ is formalised by a reduction relation $\rightarrow$ on systems that relies on the structural congruence defined in Fig. 2, where the last law allows for collecting garbage terms possibly arising from variable substitutions.

**Definition 7.** The relation $\rightarrow$ is the smallest relation closed under the rules of Fig. 3, defined over systems up to structural equivalence, as defined in Fig. 2. The relation $K \triangleright_X \sigma \gamma$ holds iff (i) $K$ has the form $\downarrow_y A$ says $c | \downarrow_z B$ says $d$, (ii) $c \triangleright d$, (iii) $\gamma = A$ says $c | B$ says $d$, and (iv) $\sigma = \{s/x,y,z\}$ maps all $x,y,z \in \mathcal{V}$ to $s \in \mathcal{N}$.

Rule [TAU] simply fires a $\tau$ prefix as expected. Rule [TELL] advertises a latent contract $\downarrow_x A$ says $c$, by putting it in parallel with the existing participants and sessions (the structural congruence laws in Fig. 2 allow for latent contracts to float in a system and, by the second last law, to move across the boxes of participants as appropriate). Rule [FUSE] finds agreements among the latent contracts $K$ of $A$; an agreement is reached when $K$ contains a bilateral contract $\gamma$ whose unilaterals are compliant (cf. Def. 7). Note that, once the agreement is reached, the compliant contracts start a fresh session containing $\gamma$. Rule [Do] allows a participant $A$ to fulfill her contract $\gamma$, by performing the needed actions in the session containing $\gamma$ (which, accordingly, evolves to $\gamma'$). Rule [Ask] checks if a condition $\phi$ holds in a session. The actual nature of $\phi$ is almost immaterial in this paper: the reader may assume that $\phi$ is a formula in an LTL logic [13]. For
closed $\gamma$ and $\phi$, $\gamma \vdash \phi$ holds iff $\gamma \models_{LTL} \phi$ according to the standard LTL semantics where, for a $\rightarrow$-trace $\eta = (\gamma_i \stackrel{\mu_i}{\Rightarrow} \gamma_{i+1})_i$ from $\gamma_0 = \gamma$, we define $\eta \models a \iff \exists A. \mu_0 = A \text{ says } a$. The last three rules are standard.

Hereafter it will be sometimes useful to record the prefix $\pi$ fired by A by implicitly decorating the corresponding reduction step, as in $\stackrel{A:\pi}{\longrightarrow}$.

The rest of this section is devoted to a few examples that highlight how bilateral contracts can be used in CO₂.

**Example 4.** Consider an online store A with the following contract $c_A$: buyers can add items to the shopping cart, and then either leave the store or pay with a credit card. Assume the store modelled as the CO₂ process $P_A = (x) (\text{tell}_A \downarrow_x c_A \cdot X \mid \text{fuse}_x)$, where:

$$c_A = \text{rec } Z. \text{ addToCart.} Z + \text{creditCard.} (\overline{\text{ok}} \oplus \overline{\text{no}}) + e \\ X \stackrel{\text{def}}{=} \text{do}_x \text{addToCart.} X + \text{do}_x \text{creditCard.} (\tau.\text{do}_x \overline{\text{ok}} + \tau.\text{do}_x \overline{\text{no}})$$

Let B be a buyer with contract $c_B = \overline{\text{addToCart}}; \overline{\text{creditCard}}; (\text{ok} + \text{no})$, and let:

$$P_B = (y) \text{tell}_A \downarrow_y c_B \cdot Y \qquad Y \stackrel{\text{def}}{=} \text{do}_y \overline{\text{addToCart.}} \text{do}_y \overline{\text{creditCard.}} \text{do}_y \text{ok}$$

A possible, successful, computation of the system $S = A[P_A] \mid B[P_B]$ is the following:

$$\begin{align*}
S & \rightarrow^* (x, y) (A[\downarrow_x A \text{ says } c_A \mid \downarrow_y B \text{ says } c_B \mid \text{fuse}_x \mid X] \mid B[Y]) \\
& \rightarrow (s) (A[X\{s/x\}] \mid B[Y\{s/y\}] \mid s[A \text{ says } c_A \mid B \text{ says } c_B]) \\
& \rightarrow^* (s) (A[X\{s/x\}] \mid B[\text{do}_s \overline{\text{creditCard.}} \text{do}_y \text{ok}] \mid s[A \text{ says } c_A \mid B \text{ says } \overline{\text{creditCard}}; (\text{ok} + \text{no})]) \\
& \rightarrow^* (s) (A[\tau.\text{do}_x \overline{\text{ok}} + \tau.\text{do}_x \overline{\text{no}}] \mid B[\text{do}_y \text{ok}] \mid s[A \text{ says } \overline{\text{ok}} \oplus \overline{\text{no}} \mid B \text{ says } \text{ok} + \text{no}]) \\
& \rightarrow (s) (A[\text{do}_x \overline{\text{ok}}] \mid B[\text{do}_y \text{ok}] \mid s[A \text{ says } \overline{\text{ok}} \oplus \overline{\text{no}} \mid B \text{ says } \text{ok} + \text{no}]) \\
& \rightarrow^* (s) (A[\mathbf{0}] \mid B[\mathbf{0}] \mid s[A \text{ says } E \mid B \text{ says } E])
\end{align*}$$

**Example 5.** An on-line store A offers buyers two options: clickPay or clickVoucher. If a buyer B chooses clickPay, A accepts the payment (pay) otherwise A checks the validity of the voucher with V, an electronic voucher distribution and management system. If V validates the voucher, B can use it (voucher), otherwise he will pay.

The contracts $c_A = \text{clickPay}.\text{pay} + \text{clickVoucher}.(\text{reject}; \text{pay} \oplus \text{accept}; \text{voucher})$ and $c'_A = \text{ok} + \text{no}$ model the scenario above. A CO₂ process for A can be the following

$$\begin{align*}
P_A &= (x)(\text{tell}_A \downarrow_x c_A \cdot (\text{do}_x \text{clickPay.} \text{do}_x \text{pay} + \text{do}_x \text{clickVoucher.}((y)\text{tell}_V \downarrow_y c'_A \cdot X))) \\
X &= \text{do}_y \text{ok.} \text{do}_x \overline{\text{accept.}} \text{do}_x \text{voucher} + \text{do}_y \text{no.} \text{do}_x \overline{\text{reject.}} \text{do}_x \text{pay} + \tau. \text{do}_x \overline{\text{reject.}} \text{do}_x \text{pay}
\end{align*}$$

Contract $c_A$ (resp. $c'_A$) is stipulated when (i) B (resp. V) advertises to A (resp. V) a contract $d$ with $c_A \triangleright d$ (resp. $c'_A \triangleright d$) and (ii) a fuse$_z$ is executed in A (resp. V).

Variables $x$ and $y$ in $P_A$ correspond to two separate sessions, where A respectively interacts with B and V. The semantics of CO₂ ensures that $x$ and $y$ will be instantiated to different session names (if at all).

The advertisement of $c'_A$ causally depends on the stipulation of the contracts of A and B, otherwise A cannot fire $\text{do}_x \text{clickVoucher}$. Instead, A and B can interact regardless the presence of V since $\text{tell}_V \downarrow_y c'_A$ is non blocking and the $\tau$-branch of A in $X$ is enabled (letting A to autonomously reject the voucher, e.g. because B is not entitled to use it).
*Example 6.* Consider a travel agency A which queries in parallel an airline ticket broker F and a hotel reservation service H in order to complete the organization of a trip. The travel agency service A[P] can be defined as follows:

$$ 
\begin{align*}
P &= (x,y)(\text{tell}_F \downarrow_x \text{ticket}; (\text{commitF} \oplus \text{abortF}).X \mid \text{tell}_H \downarrow_y \text{hotel}; (\text{commitH} \oplus \text{abortH}).Y) \\
X &\stackrel{\text{def}}{=} \text{do}_x \text{ticket}.((\text{ask}_y \text{true}. \text{do}_x \text{commitF}) + \tau.\text{do}_x \text{abortF}) \\
Y &\stackrel{\text{def}}{=} \text{do}_y \text{hotel}.((\text{ask}_x \text{true}. \text{do}_y \text{commitH}) + \tau.\text{do}_y \text{abortH})
\end{align*}
$$

where the τ actions model timeouts used to ensure progress. The travel agency in process X starts buying a ticket, and commits to it only when the hotel reservation session y is started. Similarly for process Y.

The next example shows a peculiar use of ask whereby a participant inspects a stipulated contract to decide its future behaviour.

*Example 7.* An online store A can choose whether to abort a transaction (abort) or to commit to the payment (commit). In the latter case, the buyer has two options, either he pays by credit card (creditCard) or by bank transfer (bankTransfer). The contract of A is modelled as $c = \text{abort} \oplus \text{commit}$; (creditCard + bankTransfer). Consider the process

$$ P_A = (x)(\text{tell}_A \downarrow_x c. (\text{ask}_x \phi. \text{do}_x \text{commit}. \text{do}_x \text{creditCard} + \text{do}_x \text{abort})) $$

where $\phi = \square(\text{commit} \rightarrow \neg\diamond\text{bankTransfer})$. The process $P_A$ first advertises c. Once a session $s[\gamma]$ is initiated with $\gamma = A \text{ says } c \mid B \text{ says } d$, A tests $\gamma$ through $\text{ask}_x \phi$ before committing to the payment. If $\text{ask}_x \phi$ detects that B has promised not to use the bank transfer option, then A commits to the payment, and then never offers B to perform a bank transfer. Otherwise, if $d$ does not rule out the bank transfer, even if B might actually pay by credit card, A aborts the session. Note that in both cases A realizes her own contract, even if she is never performing the bank transfer. This notion of “realization of a contract” will be formalized in Def. 11.

# 4 On honesty

In this section we set out when a participant A is honest (Def. 11). Intuitively, we consider all the possible runs of all possible systems, and require that in every session A is not definitely culpable. To this aim, we first provide CO₂ with the counterpart of the (non)culpability relation introduced in Def. 4. Intuitively, we write $A \rightsquigarrow_S S$ when, in the system S, if the participant A is involved in the session s, then she is not culpable w.r.t. the contract stipulated therein.

**Definition 8.** We write $A \rightsquigarrow_S S$ whenever $\forall \vec{u}, \gamma, S'$. ($S \equiv (\vec{u})(s[\gamma] | S') \Rightarrow A \rightsquigarrow \gamma$). We write $A \rightsquigarrow S$ whenever $A \rightsquigarrow_S S$ for all session names s.

A technical issue is that a participant may not get a chance to act in all the traces. For instance, let $S = A[\text{do}_s \text{pay}] \mid B[X] \mid S'$, where $S'$ enables A's action and $X \stackrel{\text{def}}{=} \tau.X$; note that S generates the infinite trace $S \rightarrow S \rightarrow S \rightarrow \dots$ in which A never pays, despite her honest intention. To account for this fact, we will check the honesty of a participant in fair traces, only, i.e. those where persistent transitions are eventually followed.
**Definition 9.** Given an LTS $\xrightarrow{\mu}$, we say that a (finite or infinite) trace $\eta = (P_i \xrightarrow{\mu_i} P_{i+1})_i$ having length $|\eta| \in \mathbb{N} \cup \{\infty\}$ is fair w.r.t. a set of labels $\mathcal{L}$ if and only if

$$ \forall i \in \mathbb{N}, \mu \in \mathcal{L}. \left( i \le |\eta| \land \left( \forall j \in \mathbb{N}, i \le j \le |\eta| \implies P_j \xrightarrow{\mu} \right) \implies \exists j \ge i. \mu_j = \mu \right) $$

A fair trace is a trace which is fair w.r.t. all the labels in the LTS.

Note that, by Def. 9, a fair trace is also a maximal one (w.r.t. $\mathcal{L}$). Indeed, if a fair trace is finite, the condition above guarantees that its final state has no $\mathcal{L}$ transitions enabled.

Finally, when checking the fairness of a trace, we shall implicitly assume that the labels $\mu$ in our LTSs of contracts and processes always distinguish between different occurrences of the same prefix. E.g., a $\to$-fair trace of $A[X|X]$ where $X \stackrel{\text{def}}{=} \tau.X$ is not allowed to only perform the $\tau$'s of the first $X$. Technically, labels $\mu$ always implicitly carry the syntactic address of the prefix which is being fired, in the spirit of the Enhanced Structured Operational Semantics [12].

It is often useful to reason about how a specific session $s$ evolves in a given trace. Technically, $\alpha$-conversion allows the name $s$ to be renamed at every step, making it hard to trace the identity of names. More concretely, $\alpha$-conversion is only needed to make delimitations fresh when unfolding recursive processes. Accordingly, w.l.o.g. hereafter we shall often restrict $\alpha$-conversion by considering stable traces, only, defined below. In this way, we ensure that $s$ represents the same session throughout the whole trace.

**Definition 10.** A stable $\to$-trace is a trace $(\vec{u}_0)S_0 \to (\vec{u}_1)S_1 \to (\vec{u}_2)S_2 \to \dots$ in which (1) all delimitations carry distinct names and variables, (2) delimitations have been brought to the top-level as much as possible (using $\equiv$), and (3) no $\alpha$-conversion is performed in the trace except when unfolding recursive processes.

Below, we define several notions of contract faithfulness for participants. We start by clarifying when a participant A *realizes* a contract (inside a session $s$) within a specific context. This happens when from any reachable system state $S_0$, participant A will eventually perform actions to exculpate herself (in $s$). In this phase, A is protected from interference with other participants. Then, we say A *honest in a system* if she realizes every contract in that system. When $A[P]$ is honest independently of the system, we simply say that $A[P]$ is *honest*. In this last case, we rule out those systems carrying stipulated or latent contracts of A outside of $A[P]$; otherwise the system can trivially make A culpable: e.g., we disallow $A[P] | B[\downarrow_x A \text{ says } \overline{pay} | \dots]$.

**Definition 11 (Honesty).** We say that:

- A realizes $c$ at $s$ in $S$ iff whenever $S = (\vec{u})(s[A \text{ says } c | B \text{ says } d] | S')$, $S \to^* S_0$, and $(S_i)_i$ is a $\{A : \pi\}$-fair A-solo stable $\to$-trace then $A \rightsquigarrow_s S_j$ for some $j \ge 0$;

- A is honest in $S$ iff for all $c$ and $s$, A realizes $c$ at $s$ in $S$;

- $A[P]$ is honest iff for all $S$ with no $A$ says $\dots$ nor $A[\dots]$, A is honest in $A[P]$ | $S$.

**Example 8.** A computation of the store-buyer system $S = A[P_A] | B[P_B]$ from Ex. 4 is:

$$ \begin{align*} S \to^* (s) & (A[\tau.do_x \overline{ok} + \tau.do_x \overline{no}] | B[do_y ok] | s[A \text{ says } \overline{ok} \oplus \overline{no} | B \text{ says ok + no}]) \\ \to^* (s) & (A[do_x \overline{no}] | B[do_y ok] | s[A \text{ says } \overline{ok} \oplus \overline{no} | B \text{ says ok + no}]) \\ \to^* (s) & (A[\mathbf{0}] | B[do_y ok] | s[\gamma]) \end{align*} $$
where $\gamma = A$ says $E$ | $B$ says ready no. The system is then stuck, because $\gamma$ is not allowing the [Do] step. By Def. 4 we have $A \rightsquigarrow \gamma$, $B \rightsquigarrow \gamma$, so A is honest in S while B is not. Actually, B has violated the contract agreed upon, because he is waiting for a positive answer from the store, while in $c_B$ he also promised to accept a $\overline{no}$. By Def. 11, B is not honest, while we will show in § 5 that A is honest (see Ex. 10).

**Example 9.** Consider the system $A[(x, y) (P_A | fuse_x | fuse_y)] | B[P_B] | C[P_C]$, where:

$$P_A \stackrel{\text{def}}{=} \text{tell}_A(\downarrow_x a.E) \cdot \text{tell}_A(\downarrow_y b; E) \cdot \text{do}_x a.\text{do}_y b$$

$$P_B \stackrel{\text{def}}{=} (z) (\text{tell}_A(\downarrow_z \bar{b}.E) \cdot \text{do}_z b)$$

$$P_C \stackrel{\text{def}}{=} (w) (\text{tell}_A(\downarrow_w \bar{a}; E) \cdot \mathbf{0})$$

Even though A might apparently look honest, she is not. Indeed, A cannot fulfill her contract with B, because the $do_x a$ is blocked due to the fact that C (dishonestly) does not perform his internal choice. Note that, if we considered honest a participant whose culpability only depends on the culpability of someone else, then a participant could cunningly have one of her contracts violated, so to avoid fulfilling another contract (e.g., to avoid paying one million euros to B, A stipulates a dummy contract “I ship one candy if you pay 1 cent”, which is then violated by a colluding participant C).

We now define when a process enables a contract transition, independently from the context. To do that, first we define the set $RD_s(P)$ (after “ready do”), which collects all the atoms with an unguarded action $do_s$ in P.

**Definition 12.** For all P and all s, we define the set of atoms $RD_s(P)$ as:

$$RD_s(P) = \{a \mid \exists \vec{u}, P', Q, R. P \equiv (\vec{u}) (do_s a.P' + Q \mid R) \text{ and } s \notin \vec{u}\}$$

Next, we check when a contract “unblocks” a set of atoms $x$: e.g., if $x$ accounts for at least one branch of an internal choice, or for all the branches of an external choice.

**Definition 13.** For all sets of atoms $x$ and for all $c \neq 0$, we say that $c$ unblocks $x$ iff:

$$\exists Y \in RS(c). Y \subseteq x \cup \{e\} \quad \text{or} \quad c = \text{ready } a.c' \wedge a \in x \cup \{e\}$$

**Lemma 5.** For all P and for all $\gamma = A$ says $c$ | $B$ says $d$, if $c$ unblocks $RD_s(P)$ and $S = (\vec{u})(A[P] | s[\gamma] | S')$, then either $A \rightsquigarrow \gamma$ or $S \xrightarrow{A: do_s a}$.

The following theorem is the CO₂ counterpart of Theorem 1. It states that, when a session $s$ is established between two participants A and B, A can always exculpate herself by performing (at most) two actions A: $do$. Note that when the contracts used to establish $s$ are compliant, then we deduce the stronger thesis $A \rightsquigarrow s S_j$.

**Theorem 3 (Factual exculpation).** Let $(S_i)_i$ be the following A-solo stable $\rightarrow$-trace, with $S_i = (\vec{u}_i)(A[Q_i] | s[A \text{ says } c_i \mid B \text{ says } d_i] | S'_i)$, and:

$$S_0 \xrightarrow{\mu_0} \dots \xrightarrow{\mu_{i-2}} S_{i-1} \xrightarrow{A: do_s a} S_i \xrightarrow{\mu_i} \dots \xrightarrow{\mu_{j-2}} S_{j-1} \xrightarrow{A: do_s b} S_j \xrightarrow{\mu_j} \dots$$

where $\mu_h \neq A: do_s$ for all $h \in [i, j-2]$. Then, either $c_j = 0$ or $A \rightsquigarrow s S_j$.
<figure><img src="image_3.png" /><figcaption>**Fig. 4.** Abstract LTSs for contracts and processes ($\sigma: V \to \mathcal{N}$, name A in $\to^{\mathcal{A}}$ is omitted).</figcaption></figure>

The following theorem states the undecidability of honesty. Our proof reduces the halting problem to checking dishonesty.

**Theorem 4.** *The problem of deciding whether a participant $A[P]$ is dishonest is recursively enumerable, but not recursive.*

# 5 A criterion for honesty

In this section we devise a sufficient criterion for honesty. Actually, checking honesty is a challenging task: indeed, by Th. 4, it is not even decidable. We will then provide a semantics of contracts and processes, that focusses on the actions performed by a single participant A, while abstracting from those made by the context. Note that our abstract semantics assumes processes without top-level delimitations, in accordance with Def. 10 which lifts such delimitations outside participants. Further, we sometimes perform this lifting explicitly through the open(-) operator.

**Definition 14.** For all participant names A, the abstract LTSs $\xrightarrow{\mathcal{A}}$ and $\xrightarrow{\mathcal{A}}^{\mathcal{A}}$ on contracts and on processes, respectively, are defined by the rules in Fig. 4, where $\sigma: V \to \mathcal{N}$.

The intuition behind the abstract rules is provided by Lemma 6 and Lemma 7 below, which establish the soundness of the abstractions.

**Lemma 6.** For all bilateral contracts $\gamma = A$ says $c$ | B says $d$:

$$1. \quad \gamma \xrightarrow{A \text{ says } a} A \text{ says } c' | B \text{ says } d' \quad \implies \quad c \xrightarrow{a} \mathcal{A} c' \wedge (d \xrightarrow{\text{ctx}} \mathcal{A} d' \vee d \xrightarrow{0} \mathcal{A} d')$$

$$2. \quad \gamma \xrightarrow{A \text{ says } a} A \text{ says } c' | B \text{ says } d' \wedge c \triangleright d \quad \implies \quad c \xrightarrow{a} \mathcal{A} c' \wedge d \xrightarrow{\text{ctx}} \mathcal{A} d'$$

Intuitively, a move of $\gamma$ is caused by an action performed by one of its components $c$ and $d$. If $c$ moves, the $\xrightarrow{a} \mathcal{A}$ rules account for its continuation. This might make $d$ commit to one of the branches of a sum, as shown in the $\xrightarrow{\text{ctx}} \mathcal{A}$ rules. Further, $c$ can perform an action not supported by $d$, by using a [*FAIL] rule: accordingly, $\xrightarrow{0} \mathcal{A}$ transforms $d$ into 0. The compliance between $c$ and $d$ ensures the absence of such failure moves.
**Lemma 7.** For each (finite or infinite) stable $\rightarrow$-trace $(S_i)_i$, with $S_i = (\vec{u}_i)(A[Q_i] | S'_i)$, there exists a $\rightarrow_{\#}$-trace $Q_0 \xrightarrow{\mu_0} \rightarrow_{\#} Q_1 \xrightarrow{\mu_1} \rightarrow_{\#} Q_2 \xrightarrow{\mu_2} \cdots$ where $\mu_i = \pi$ if $S_i \xrightarrow{A:\pi} S_{i+1}$, and $\mu_i = \text{ctx otherwise. Moreover, if } (S_i)_i \text{ is fair, then } (Q_i)_i \text{ is } \{\tau, \text{tell}\}\text{-fair.}$

In the above lemma, each step of the whole system might be due to either the process $Q_i$ or its context. If $Q_i$ fires a prefix $\pi$, then it changes according to the $\xrightarrow{\pi} \#_i$ rule in Fig. 4. In particular, that accounts for tell$_A$ - adding further latent contracts to $Q_i$, as well as fuse possibly instantiating variables. Newly exposed delimitations are removed using open(-): indeed, they already appear in $\vec{u}_i$, since the trace is stable.

We now define when a process $P$ “$\#_i$-realizes” a contract $c$ in a session $s$ (written $P \models_s c$), without making any assumptions about its context. Intuitively, $P \models_s c$ holds when (1) $P$ eventually enables the $do_s$ actions mandated by $c$, and (2) in the abstract LTS $\rightarrow_{\#_i}$, the continuation of $P$ after firing some $do_s$ must realize the continuation of $c$ (under $\rightarrow_{\#_i}$). Note that $P$ is not required to actually perform the relevant $do_s$, because the context might prevent $P$ from doing so. For instance, in the system $A[P] | s[A \text{ says } c | B \text{ says ready a.d}]$ the process $P$ can not fire any $do_s$.

**Definition 15.** Given a session $s$ and a participant $A$, we define the relation $\models_s^A$ (“$\#_i$-realizes”) between processes and contracts as the largest relation such that, whenever $P_0 \models_s^A c$, then for each $\{\tau, \text{tell}\}\text{-fair } \rightarrow_{\#_i}^A$-trace $(P_i)_i$ without labels $do_s$, we have:

1. $\exists k. \forall i \ge k. c \ \text{unblocks } RD_s(P_i)$

2. $\forall i, a, P', c'. (P_i \xrightarrow{do_s} \#_i P' \wedge c \xrightarrow{a} \#_i c' \implies P' \models_s^A c')$

**Example 10.** Recall the online store $A$ from Ex. 4. We show that $X\{s/x\} \models_s^A c_A$. First note that transitions in $\{\tau, \text{tell}\}$-fair $\rightarrow_{\#_i}$-traces without $do_s$ from $X\{s/x\}$ can only be labelled with $ctx$. Thus, each $P_i$ on such traces has the form $X\{s/x\} | K_i$, for some $K_i$. We have $RD_s(P_i) = RD_s(X\{s/x\}) = \{\text{TO CART, creditCard}\}$. Also, $c_A \ \text{unblocks } RD_s(X\{s/x\})$ hence condition (1) of Def. 15 holds. For condition (2), if $c_A \xrightarrow{\text{creditCard}} \#_i c' = \text{accept} \oplus \text{reject}$ and $P_i \xrightarrow{\text{do}_s \text{ creditCard}} \#_i P' = \tau \cdot \text{do}_s \text{ accept} + \tau \cdot \text{do}_s \text{ reject} | K_i$ then $P' \models_s^A c'$. Actually, all processes on a $\{\tau, \text{tell}\}$-fair $\rightarrow_{\#_i}$-traces without $do_s$ from $P'$ have either the form $do_s \text{ accept} | K$ or the form $do_s \text{ reject} | K$. For the recursive case, $c_A \xrightarrow{\text{addToCart}} \#_i c_A$ and $P_i \xrightarrow{\text{do}_s \text{ addToCart}} \#_i X\{s/x\}$, hence $X\{s/x\} \models_s^A c_A$ by coinduction. Note that the case $c_A \xrightarrow{e} \#_i$ did not apply, because $P_i$ cannot take $\rightarrow_{\#_i}$-transitions labelled $do_s e$.

**Theorem 5** below establishes an invariant of system transitions. If a participant $A[Q_0]$ $\#_i$-realizes a stipulated contract $c_0$, then in each evolution of the system the descendant of $A[Q_0]$ still $\#_i$-realizes the related descendant of $c_0$. The theorem only assumes that $c_0$ is in a session with a compliant contract, as it is the case after firing a fuse.

**Theorem 5.** Let $(S_i)_i$ be a stable $\rightarrow$-trace with $S_i = (\vec{u}_i)(A[Q_i] | s[A \text{ says } c_i | B \text{ says } d_i] | S'_i)$ for all $i$. If $c_0 \succcurlyeq d_0$ and $Q_0 \models_s^A c_0$, then $Q_i \models_s^A c_i$ for all $i$.

We now define when a participant is $\#_i$-honest. Intuitively, we classify as such a participant $A[P]$ when, for all prefixes tell$_x$ $c$ contained in $P$, the continuation $Q$ of the prefix $\#_i$-realizes $c$. We also require that the session variable $x$ cannot be used by any process in parallel with $Q$, because such processes could potentially compromise the ability of $Q$ to realise $c$ (see Ex. 11).
**Definition 16 (‡-honest participant).** A participant A[P] is ‡-honest iff P does not contain $↓_y$ A says c, and for all linear contexts C (•), x, c, Q, R, and s fresh in P

$$P = C(\text{tell} ↓_x c.Q + R) \implies \text{open}(Q\{s/x\}) \models_s^A c \wedge C \text{ is x-safe}$$

where C (•) is x-safe iff $\exists C'. C(\bullet) = C'((x)\bullet)$ or C is free from $do_x$.

*Example 11.* Substitute $Q = fuse_x.do_x \text{ creditCard}$ for $fuse_x$ in the process $P_A$ from Ex. 4. Then A[$P_A$] is not honest, because A cannot complete her contract if the $do_x$ within Q is performed. However, the modified A[$P_A$] violates x-safety, hence it is not ‡-honest.

The following lemma relates ‡-honesty with the abstract semantics of processes. If a ‡-honest process P abstractly fires a tell $↓_x c$, then the continuation of P realises c (item 1). Also, ‡-honesty is preserved under abstract transitions (item 2).

**Lemma 8.** For all ‡-honest participants A[P], such that $P = \text{open}(P)$:

1. if $P \xrightarrow{\text{tell}_B \downarrow_x c} \mu_P'$, then $P'\{s/x\} \models_s^A c$, for all s fresh in P.

2. if $P \xrightarrow{\mu} \mu_P'$, then A[$P'$] is ‡-honest.

Our main result states that ‡-honesty suffices to ensure honesty. Note that while honesty, by Def. 11, considers all the (infinite) possible contexts, ‡-honesty does not. Hence, while verifying honesty can be unfeasible in the general case, it can also be ensured by establishing ‡-honesty, which is more amenable to verification. For instance, for finite control processes [11] it is possible to decide ‡-honesty e.g. through model-checking. In fact, in these processes parallel composition cannot appear under recursion, hence their behaviour can be represented with finitely many states.

**Theorem 6.** All ‡-honest participants are honest.

Noteworthy, by Theorem 6 we can establish that all the participants named A in Examples 4, 5, and 6 are honest. This is obtained by reasoning as in Example 10. Instead, participant A in Example 7 is honest but not ‡-honest.

# 6 Related Work and Conclusions

We have developed a formal model for reasoning about contract-oriented systems. Our approach departs from the common principle that contracts are always respected after they are agreed upon. We represent instead the more realistic situation where promises are not always kept. The process calculus CO₂ [2] allows participants to advertise contracts, to establish sessions with other participants with compliant contracts, and to fulfill them (or choose not to). Remarkably, instead of defining an ad-hoc contract model, we have embedded the contract theory of [10] within CO₂. To do that, we have slightly adapted the contracts of [10] in order to define culpability, and we have specialized CO₂ accordingly at the system-level. The main technical contribution of this paper is a criterion for deciding when a participant is honest, i.e., always respects the advertised contracts in all possible contexts. This is not a trivial task, especially when multiple
sessions are needed for realizing a contract (see e.g. Ex. 5 and 6) or when participants want to inspect the state of a contract to decide how to proceed next (see e.g. Ex. 7).

At the best of our knowledge, this is the first paper that addresses the problem of establishing when a participant is honest in a contract-based system populated by dishonest participants. Several papers investigated the use of contracts in concurrent systems; however, they typically focus on coupling processes which statically guarantee conformance to their contracts. This is achieved e.g. by typing [5, 9, 10], by contract-based process synthesis [7], or by approaches based on behavioural preorders [6]. As future work, it may also be interesting to study weaker notions of honesty, e.g., by requiring participants to respect contracts in *honest* contexts, only.

The process calculus CO₂ has been introduced in [2] as a generic framework for relating different contract models; the variant in this paper has been obtained by instantiating it with the contracts of [10]. Some primitives, e.g. multiparty fuse, have been consequently simplified. In [2], a participant A is honest when A becomes not culpable from a certain execution step; here, we only require that, whenever A is culpable, then she can exculpate herself by performing some actions. This change reflects the fact that bilateral contracts à la [10] can describe endless interactions.

The notion of compliance in [10] is asymmetric. Namely, if *c* is the client contract and *d* is the server contract, then *c* and *d* are compliant if *c* always reaches a success state or engages *d* in an endless interaction. In our model instead compliance is symmetric: the server contract, too, has to agree on when a state is successful. The LTS semantics of unilateral contracts in [10] yields identical synchronization trees for internal and external choice; to differentiate them, one has to consider their ready sets. We instead give semantics to *bilateral* contracts, and distinguish between choices at the LTS level. Note that we do not allow for unguarded sums, unlike [10]. Were these be allowed, we would have to deal e.g. with a participant A with a contract of the form *a*; $c_0 \oplus (b.c_1 + c.c_2)$. According to our intuition A should be culpable, because of the internal choice. If A legitimately chooses not to perform *a*, to exculpate herself she would have to wait for the other participant to choose (internally) between *b* and *c*. Therefore, A can exculpate herself only if the other participant permits her to. By contrast, by restricting to guarded sums our theory enjoys the nice feature that a culpable participant can always exculpate herself by performing some actions, which pass the buck to the other participant (Theorems 1 and 3).

Design-by-contract is transferred in [5] to distributed interactions modelled as (multiparty) asserted global types [14]. The projection of asserted global types on local ones allows for the automatic generation of monitors whereby incoming messages are checked against the local contract. Such monitors have a “local” view of the computation, i.e. they can detect a violation but cannot, in general, single out the culpable component. In fact, a monitor cannot know if an expected message is not delivered because the partner is violating his contract, or because he is blocked on interactions with other participants. Conversely, in our approach we compose participants in a “bottom-up” fashion: a participant declares its contract independently of the others and then advertises it; the fuse primitive tries then to harmonise contracts by searching for a suitable agreement. Our notion of *honesty* singles out culpable components during the computation. An interesting problem would be to investigate how our notion of culpability could
be attained within the approach in [5]. In fact, this seems to be a non trivial problem,
even if forbidding communication channels shared among more than two participants.

Contracts are rendered in [8, 7] as soft constraints (values in a c-semiring) that al-
low for different levels of agreement between contracts. When matching a client with
a service, the constraints are composed. This restricts the possible interactions to those
acceptable (if any) to both parties. A technique is proposed in [7] for compiling clients
and services so that, after matching, both actually behave according to the mutually
acceptable interactions, and reach success without getting stuck. Our framework is fo-
cused instead on blaming participants, and on checking when a participant is honest,
i.e. always able to avoid blame in all possible contexts. The use of soft constraints in a
context where participants can be dishonest seems viable, e.g. by instantiating the ab-
stract contract model of CO2 with the contracts in [7]. A challenging task would be that
of defining culpability in such setting.

***Acknowledgments.*** This work has been partially supported by the Aut. Region of Sar-
dinia under grants L.R.7/2007 CRP2-120 (Project TESLA) and CRP-17285 (Project
TRICS), and by the Leverhulme Trust Programme Award “Tracing Networks”.

References

1. A. Artikis, M. J. Sergot, and J. V. Pitt. Specifying norm-governed computational societies. *ACM Trans. Comput. Log.*, 10(1), 2009.

2. M. Bartoletti, E. Tuosto, and R. Zunino. Contracts in distributed systems. In *ICE*, 2011.

3. M. Bartoletti, E. Tuosto, and R. Zunino. On the realizability of contracts in dishonest sys- tems. *CoRR*, abs/1201.6188, 2012.

4. M. Bartoletti and R. Zunino. A calculus of contracting processes. In *LICS*, 2010.

5. L. Bocchi, K. Honda, E. Tuosto, and N. Yoshida. A theory of design-by-contract for dis- tributed multiparty interactions. In *CONCUR*, 2010.

6. M. Bravetti and G. Zavattaro. Towards a unifying theory for choreography conformance and contract compliance. In *Software Composition*, 2007.

7. M. Buscemi, M. Coppo, M. Dezani-Ciancaglini, and U. Montanari. Constraints for service contracts. In *TGC*, 2011. To appear.

8. M. G. Buscemi and U. Montanari. CC-Pi: A constraint-based language for specifying service level agreements. In *ESOP*, 2007.

9. S. Carpineti and C. Laneve. A basic contract language for web services. In *ESOP*, 2006.

10. G. Castagna, N. Gesbert, and L. Padovani. A theory of contracts for web services. *ACM Transactions on Programming Languages and Systems*, 31(5), 2009.

11. M. Dam. On the Decidability of Process Equivalences for the π-calculus. *Theoretical Computer Science*, 183(2):215–228, 1997.

12. P. Degano and C. Priami. Enhanced operational semantics. *ACM Comput. Surv.*, 33(2):135–176, 2001.

13. E. A. Emerson. Temporal and modal logic. In *Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics (B)*. North-Holland Pub. Co./MIT Press, 1990.

14. K. Honda, N. Yoshida, and M. Carbone. Multiparty asynchronous session types. In *POPL*, 2008.

15. C. Prisacariu and G. Schneider. A formal language for electronic contracts. In *FMOODS*, 2007.