Fairness is a desirable and crucial property of many protocols that handle, for instance, exchanges of message.
It states that if at least one agent engaging in the protocol is honest, then either the protocol will unfold correctly and fulfill its intended goal for all participants, or it will fail for everyone.
In this work, we present a game-based framework for the study of fairness protocols, that does not define a priori an attacker model.
It is based on the notion of strong secure equilibria, and leverages the conceptual and algorithmic toolbox of game theory.
In the case of finite games, we provide decision procedures with tight complexity bounds for determining whether a protocol is immune to nefarious attacks from a coalition of participants, and whether such a protocol could exist based on the underlying graph structure and objectives.

§ PLAN

Just for draft purposes

* Modèles

* Modèles de systèmes:

* Text descriptions

* Process algebra like $\pi$-calculus

Traduction vers Jeux sur graphe

* Modèle d'attaquant: Dolev-Yao (zero-sum) vs rational agents (non-zero sum)

* Protocoles

* Needham-Shroeder

* Fair exchange protocols

* Algorithmes

§ INTRODUCTION

Fairness is a desirable and crucial property of many protocols that handle, for instance, exchanges of messages.
It states that if at least one agent engaging in the protocol is honest, then either the protocol will unfold correctly and fulfill its intended goal for all participants (and this is clearly the most desired outcome), or it will fail for everyone.
In other words, for exchange protocols, it means that either every agent involved in the exchange will send their message and receive the one intended for them, or that nobody will receive any message.
Traditionally, such a fairness property is formalized by expressing it as a trace property of the protocol : one must make sure that for every possible execution of the protocol, the property holds.
While verifying trace properties is well-understood, formalizing fairness that way imposes a very stringent requirement, as it constrains every single trace or execution, including those associated with irrational and non-credible behavior.
Reasoning on traces under the assumption that these non-credible behaviors will not occur means reasoning on sets of traces (i.e. using hyperproperties), which require a different approach to the verification of these protocols and more elaborated modeling and verification techniques.
Furthermore, imposing such a strong notion of fairness usually requires  the involvement of a trusted third party (TTP for short) [22].
On the other hand, while a number of general formalisms for hyperproperties exist, restrictions on what behaviors are credible or not are not generally focused on, at least in the context of fairness. Additionally, general algorithms for deciding hyperproperties typically have very high complexity making them somewhat impractical.
Here we therefore restrict ourselves to finding the right notion of acceptable behavior and focus on this notion in order to obtain a reasonable decision procedure.

In this work, we introduce a novel semantic framework based on multi-player games and an appropriate notion of equilibrium. This framework allows for reasoning about fair exchange protocols without enforcing the excessively strong fairness constraint based on traces, while still providing guarantees that are relevant and practical. Additionally, we explore the algorithmic tools required to develop verification procedures within this semantic framework.

Relaxation of the fairness property has previously been attempted.
In fact, some previous works already refer to a notion of rational fairness.
See the related works paragraph below <ref> for a more detailed account of those attempts.
Often, the works in this direction rely on modeling protocols via two-player games, and choosing a solution concept (usually a variant of Nash equilibria) to describe the desired outcomes of the game/protocol and its robustness against attacks.
In our approach, we assert that protocols should be represented as games with more than two players, allowing for the modeling of malignant coalitions that could potentially derail the protocol. We propose a solution concept that remains robust against such deviations, operating under reasonable (albeit pessimistic) rationality assumptions about the participants.

Before presenting our contributions in further details, let us give a few insights on solution concepts in game theory and their relation to rationality.

§.§ Rationality in games

In fair exchange protocols, participants are not purely adversarial, as each agent has an individual goal (e.g., receiving the messages they expect from others) that is not necessarily merely being a nuisance to other players.
Consequently, these protocols cannot be faithfully formalized as zero-sum games, and we need to use the more general framework of non zero-sum games to model them accurately.
In this setting, each agent has a goal that they pursue through making choices of actions, known as strategies, and every outcome of the collective strategies of all agents (a profile) results in a potentially different payoff for each player. The central notion for these games is equilibrium: a profile of strategies from which it is not worthwhile to deviate.
The notion of equilibrium was first introduced by Nash in the 1950s [21], for the case where a single agent deviating would not increase their payoff. Since then, several notions of equilibria have been defined to capture different models of rationality: Aumann [4] defined Strong Nash Equilibria, where several players deviating conjointly cannot increase their payoff. Other notions include Immune Equilibria [7], where players should not be able to decrease the payoff of others by deviating, and Secure Equilibria [11, 9], in which players first aim at maximizing their payoff and, as a secondary objective, try to minimize the payoff of the other players.

Although most of these initial definitions originated in economic theory, game models have also been studied by computer scientists for addressing underlying algorithmic questions: how difficult it is to construct an equilibrium, and how challenging it is to decide the existence of an equilibrium with desirable properties, but also for modeling purposes. In the application context we consider (e.g., fair exchange protocols), the most appropriate instantiation of these game models is games played on directed finite graphs [15]. Each vertex of a graph represents a state of affairs in the execution of the protocol, and each state belongs to a given player who can choose, based on the sequence of previously visited vertices, how to move to the next vertex. This transition models the execution of one more step in the protocol, thus producing a path that, in turn, models a complete execution of the protocol.
The payoff for each player can be determined by a Boolean condition on this path: does the execution meet the goal of the player?

This general framework allows us to reason about the rationality of players: if a player has a strategy that enables them to achieve their objective given the strategies of other players, they may have no reason to deviate from it. Therefore, when reasoning about the correctness of a protocol, it should be unnecessary to consider irrational behaviors. A protocol can be deemed adequate if it is correct for rational behaviors, even if irrational behaviors could lead to violations of the strong fairness condition. Our framework also accommodates a degree of pessimism: if a player can deviate to preserve their own goal while harming others, they might choose to do so. Additionally, it allows us to reason about coalitions that agents might form to gain an advantage or cause harm through deviation.

§.§ Approach and contributions

Taking into account the modeling needs induced by exchange protocols with fairness objectives, we introduce the concept of strong secure equilibria (SSE) and argue that it is the appropriate solution concept. Indeed, SSE ensures robustness against both coalition deviations (strong) and nuisance-only deviations (secure). We propose a modeling approach for protocols, termed the protocol challenge, which is expressive enough to encode classical exchange protocols, including those with TTPs and infrastructure as regular players. Additionally, our notion of protocol challenge allows for fine-tuning the levels of rationality and fairness among agents, potentially eliminating the need for a TTP. This is achieved using relatively simple objectives (i.e., Boolean), for which decision procedures can be devised (for any $\omega$-regular objectives).

In our approach, and contrary to most approaches in the literature, the study of fairness protocols does not rely on a predefined attacker model. In our framework, the attacker is implicit and can consist of any coalition of agents, with their power being a parameter of the instance at hand. The types of attacks captured include any deviation that is considered rational under the notion of Strong Secure Equilibria.

Our technical contribution focuses on the case of games played on finite directed graphs with $\omega$-regular objectives (which subsume Linear Temporal Logics objectives, for instance), which are well-suited to the study of fairness protocols. The finiteness assumption is adequate as the set of messages that can be exchanged in these protocols is usually finite — up to nonces or other secret data that can be abstracted by a finite number of messages.

We provide decision procedures for determining whether a protocol is immune to nefarious (but rational) attacks from a coalition of participants, and whether such a protocol could exist based on the underlying graph structure and objectives. Most of the computational complexity bounds for our algorithms are tight, and we include an analysis of the case with a fixed number of agents, which is often the dominant factor in the complexity of multiplayer games and which is usually small in practical applications.

§.§ Related Works

Several works rely on notions of equilibria to argue for the resilience of the provided protocol, such as the RatFish peer-to-peer protocol [5], although they rely on 2-player Nash equilibria.
In [1], the authors use resilient strong Nash equilibria to show that their protocol does not require a TTP as long as the agents are all rational, but they do not provide a general framework.
A more general formalism to handle rational fairness is laid out in [10], where the authors point out the limit of fairness as a strong trace property.
They also choose the game modeling approach and propose a variant of Nash equilibria as the appropriate solution concept to capture rationality in protocols.
However, their notion of rationality of the agents is optimistic: they are not assumed to be willing to deviate from the protocol only to affect negatively the others, it must at the very least impact them strictly positively.
Furthermore, since the model they choose is strictly two-player, there is no notion of robustness against malignant coalitions. Thus, they favor a sort of best Nash equilibria as a rational solution concept.
Finally, while they propose a relevant general framework to model protocols in terms of multiplayer games, they provide no implementations or decision procedure.

At the other end of the spectrum, a very general approach uses hyperproperties [12, 24].
These allow to express properties of sets of traces, and are therefore well suited to the verification of protocols.
The drawback of such a general approach is that decision problems are often undecidable or non-elementary for relevant fragments; in comparison, the complexity of the most difficult problems in our setting is only $\ExpTime$.

Although a wide array of notions of rationality in games have been defined, few works focus on the notion of secure equilibria.
Two notable exceptions are [11] which actually also motivates the use of secure equilibria with the need to model malicious agents, and [9], for quantitative objectives.
Both however only consider the case of two player games.
Two player games are also considered in [19] to evaluate the fairness of an exchange protocol, through the logic ATL.
The authors actually hint at using coalitions, as they solve several two player games to take into account the fact that the infrastructure may side with one agent or the other to facilitate their cheating.

§ THE CHALLENGES OF FAIR EXCHANGE

The aim of designing a protocol is to establish a set of behavior rules that yield a specific outcome if thoroughly followed, and that are self-enforceable: every participating agent must adhere to these rules, lest they do not get anything out of the interactions.

Before moving on the more formal definitions and results of the paper, let us run through the obstacles and possible solutions to the design a good fair exchange protocol.
Towards this, let us consider the simple setting of only two agents, Alice and Bob, that wish to exchange messages or currency online. (For instance, Alice could want to purchase digital art from Bob.)
How to ensure that the exchange is fair ?
A first naive approach to designing such a protocol could be “let both send their part to the other one”.
(See  <ref> in Appendix <ref> for a depiction of the possible sequences of actions following this basic guideline.)
If both of them do this, even asynchronously, then the exchange is performed.
Of course, there could be a malicious third party involved here, that could derail the conduction of the protocol for any reason.
This is what is traditionally called an external attacker, and protocols being robust to external attacks is the subject of many works in the security community.
Another source of trouble could be the failure of the communication channels.
In this work, we assume that the channels are resilient: they deliver every message perfectly, albeit maybe with an arbitrary but finite delay (every message is eventually delivered).

However, another critical aspect to take into account is what assumptions we make about the motivations of the agents.
Indeed, one can argue that there is no reason for an agent to trust the other one.
In fact, both may even prefer an outcome where they receive something from the other as intended, but do not send their share.
Depending on such assumptions, the solutions for designing a fair protocol may vary: clearly, the naive approach sketched above fails as soon as one agent is not fully trustworthy.

Let us briefly describe two approaches to ensure robustness against these possibly untrustworthy agents.

Consider the problem of the swap of two items between two agents through a postal service.
The agents performing this exchange may not trust each other, and neither wants to fulfill their end of the deal if they do not obtain the other in exchange.
On the other hand, getting the other agent's item while still keeping their own is not only acceptable but even preferred (albeit morally dubious).

The normal protocol to follow would be that they both send the item to the other and they should both end up with their end of the bargain fulfilled.
This however is open to cheating from either party who can not send their item and be rewarded.
This simple setting can be represented with the graph of  <ref>.
From each state each agent can choose to perform actions they have control over: Alice's actions are the solid red arrows while Bob's one are dashed and blue.
While the intended protocol is to have items exchanged fully, it is clear that the agent having received an item first can just deviate from it and never send the other item; the other agent has no control whatsoever in that situation.

§.§ With a trusted third party

A first possible solution to ensure fairness while making no assumption on the trustworthiness of the participants is to involve a trusted third party (TTP) in the protocol.
This particular agent is assumed to be trustworthy, and to have no other interest than the completion of the exchange.
Furthermore, it is supposed to have sufficient leverage on the agents to enforce the completion of the exchange, if one of them tries to deflect from the intended course of actions.
The TTP is thus considered to be an agent with absolute authority.
One could consider performing the exchange only via the TTP, sending both agents' parts to the TTP that would, upon full reception, redistribute them appropriately. This, however foolproof, is extremely costly, as the TTP is used in every instance of the protocol.
Usually, this is avoided by amending the naive protocol to add the rule “if an agent does not receive anything while he has sent his share, he contacts and alerts the TTP, who then makes sure the other agent comply”.
This is what is called an optimistic version of a protocol involving a TTP. It is assumed that the participating agents desire the intended outcome of the protocol, and thus that in most traces of it, the TTP will not need to intervene at all.
A depiction of a such a TTP moderated protocol exchange can be found in  <ref> in Appendix <ref>.
This is also the approach of the Zhou-Gollmann protocol that uses a TTP only in case of a (suspected or real) cheating attempt (and is encompassed by our framework, see Section <ref> later on).

A third party can be used as an intermediary to which both parties send their items.
They are then transferred to the intended recipient only when both items have been received (or returned to the original owner after a predefined amount of time).
This idea works only if it is assumed that the third party is always honest: a corrupted third party could well transmit both items to a single agent, violating the security of the exchange protocol.
In practice, such trusted third party is often costly, and one may wish her role to be less central, and used only as a fallback mechanism: its mere presence should ensure both Alice and Bob behave honestly. c'est ça optimistic classiquement
This is the case in the example of  <ref>: when an item has been sent but the other has not been received, the trusted third party $\ttp$ can force the dishonest party to finish the transaction (green dotted arrows).
Then there is nothing to be gained by deviating from the intended protocol and not sending the promised item.

§.§ Beyond trust

The TTP approach is well-known and widely accepted as a necessity (as well-justified by the impossibility result of [22]).
What can be done when this approach is not applicable ?
Indeed, there are many cases where the trustworthiness of a third party is not clear enough to reasonably rely upon it.
For thoses cases, can we design protocols which rules are self-enforceable and that eliminate the need of a TTP ?
In other terms, what if the incentives to complete the protocol properly were stronger than the ones to deviate from the intended behaviors ?
An alternative, and the approach we choose in this work, is to rely, not on the trustworthiness of agents, but instead on their rationality.
While not amenable to every possible context where fair exchange is needed, it can provide a viable solution in relevant situations.
For instance, in peer-to-peer settings, no one can be absolutely trusted in theory, but all agents have an incentive to be honest, since keeping a good reputation enable them to perform further exchanges.
As another example, a ride-share application can be used as a trusted third party between a driver and a traveler without being trusted per se, but because both the driver and the traveler know that if the application had dishonest behaviors in some situations, then no one would trust it anymore, and the company that holds it would stop their profits.

In both these examples, important common features are their multi-agent nature and the repeatability of the exchange, albeit with different agents.
To illustrate further and start going towards a more abstract model, consider the following setting, depicted by Figure <ref>.
Alice, Bob and Charlie are three agents who wish to exchange an infinity of items: each agent has infinitely many items to send to both other agents.
Again, there is no protocol that could satisty the usual definitions of fairness.
Indeed, there is an agent (say, for instance, Alice) that can scam another agent (say Bob), i.e. that can send only finitely many items to Bob and receive at least one more item from him.
That is the case if the agents exchange their items directly, but also if they use the third agent (Charlie) as an intermediary, because Charlie is not a TTP and can therefore choose to help Alice, forming a (malicious) coalition, to scam Bob (or the reverse).

In the real world, however, the existence of an agent that can always be absolutely trusted by all the agents is a very strong assumption; but trust can arise from the knowledge of the interests of that party.
A ride-share application, for example, can be used as a trusted third party between a driver and a traveler without being trusted per se, but because both the driver and the traveler know that if the application had dishonest behaviors in some situations, then no one would trust it anymore, and the company that holds it would stop their profits.
Similarly, in peer-to-peer settings, no one can be absolutely trusted in theory, but all agents have an incentive to be honest, since keeping a good reputation enable them to perform further exchanges.

Consider, more precisely, the following setting, depicted by Figure <ref>.
Alice, Bob and Charlie are three agents who wish to exchange an infinity of items: each agent has infinitely many items to send to both other agents.
For the same reason as before, in every protocol one could design in that setting, the usual definitions of fairness are not satisfied: there is an agent (say, for instance, Alice) that can scam another agent (say Bob), i.e. that can send only finitely many items to Bob and receive at least one more item from him.
That is the case if the agents exchange their items directly, but also if they use the third agent (Charlie) as an intermediary, because Charlie is not a TTP and can therefore choose to help Alice scam Bob (or the reverse).
However, since the process is repeating for further exchanges, if Charlie does so, Bob may react by stopping exchanges not only with Alice, but also with Charlie.
Alice would then be satisfied (she actually scammed Bob), but Charlie would be worse off (she did not scam anyone herself, and can no longer exchange with Bob).
So if Charlie behaves rationally, she has no incentive to help another agent scam the third.
In practice, therefore, such a protocol can be considered as reasonably safe: Alice, Bob, and Charlie all take, alternatively, the role of the TTP and enable an exchange of items between the two other agents; and if an agent deviates from the protocol, the other ones stop all exchanges with them.

This motivates our model: a protocol is considered safe if no alliance of agents can wrong another agent without wronging a member of the alliance itself.
The security of the protocol stems from the assumption that all agents, even though they might be evil, would nonetheless behave rationally.

toexchange=[->,>=latex',draw,bend left=15]
exlab=[sloped,fill=white,inner sep=2pt]
[font=] (a) at (150:3cm) $\alice$;
[font=] (b) at (30:3cm) $\bob$;
[font=] (c) at (-90:3cm) $\charlie$;

(a) edge[toexchange] node[exlab] $(\iab_n)_{n\in\NN}$ (b);
(b) edge[toexchange] node[exlab] $(\iba_n)_{n\in\NN}$ (a);
(a) edge[toexchange] node[exlab] $(\iac_n)_{n\in\NN}$ (c);
(c) edge[toexchange] node[exlab] $(\ica_n)_{n\in\NN}$ (a);
(b) edge[toexchange] node[exlab] $(\ibc_n)_{n\in\NN}$ (c);
(c) edge[toexchange] node[exlab] $(\icb_n)_{n\in\NN}$ (b);

Expected exchanged items between Alice, Bob, and Charlie.

§ GENERAL FORMALISMS

In this section, we present our model and argue that, in the game-theoretic setting, safe protocols are characterized by strong secure equilibria.
We then provide definitions of games on finite graphs, in order to handle them algorithmically.
In particular, we present techniques to model the infrastructure (e.g., communication channels) as a player among others in these finite games.

§.§ Framework

We consider the following general scenario: several agents (for instance: programs, or human users) interact through behaviors (for instance: sending some message after having received some other), and aim to reach a correctness condition (for instance, exchanging a cryptographic key, or signing a contract).
But, some of those agents may be tempted to deviate from that objective, in order to wrong some other agent; as long as they are not themselves wronged.
We thus make the hypothesis that an attack on the protocol comes from the same agent(s) that engage in it.
In other terms, the participating agents are assumed rational but malicious. If we want to model an external attacker in the classical sense, we can by introducing him as an explicit new agent in our framework.
In such a scenario, we wish to design, or to verify, protocols that all those agents should follow, so that the correctness condition is achieved, and that no alliance of agents can cheat other agent and wrong them.

In that setting, the Infrastructure is seen as an agent among the others, with several possible behaviors but no wrongness condition, so that it can help anyone to wrong anyone.

[Protocol challenge]
A protocol challenge is a tuple:

\[\pc = \left(\agents, (\behaviors_a)_{a \in \agents}, (\Wrong_a)_{a \in \agents}, \Corr\right),\]

* $\agents$ is the set of agents;

* each agent $a \in \agents$ has a set $\behaviors_a\neq \emptyset$ of available behaviors (and for $A \subseteq \agents$, we write $\behaviors_A = \prod_{a \in A} \behaviors_a$);

* for each agent $a$, the set $\Wrong_a \subseteq \behaviors_\agents$ is the wronging condition of agent $a$;

* the set $\Corr \in \behaviors_\agents$ is called the correctness condition, and is such that for each agent $a$, we have $\Corr \cap \Wrong_u = \emptyset$;

[Protocol, implementation]
A protocol is a nonempty set $P \subseteq \behaviors_\agents$.
An implementation of $P$ is an element $\bbeta$ of $P$.

The reason why a protocol is not a single behavior, but a set, is that protocols are often not defined in a deterministic way: they may be ambiguous about minor aspects, and leave some room for interpretation.
In such a case, all of the possible implementations must be verified.

Consider an item exchange protocol with a TTP (such as the one in Section <ref>), in which we explicitly take into account the fact that when Alice or Bob sends an item, it is not immediately received by the recipient, but spends some time within the communication infrastructure ($\II$).
It is reasonable to assume that this infrastructure, while offering no guarantee on delays, always delivers the item (this is the standard model of resilient channels).
The interested reader will find an illustration in Appendix <ref>,  <ref>.

Within the above formalism, there are four agents: Alice, Bob, the TTP, and the Infrastructure $\II$.
The available behaviors for each agent are given by the choice, at any given moment, to perform (or not) any of their own action whenever enabled.
The behaviors of the Infrastructure are further restricted by prohibiting behaviors that infinitely choose not to perform any action while infinitely enabled, to model the resilience of the channels.

Alice (or Bob) is wronged if she (he) remains indefinitely in a state where she (he) has neither items.
The TTP is wronged if either Alice or Bob is, which guarantees that both can trust it.
Regarding the correctness condition, it could consist simply in exchanging the items.
However, we choose here to add the condition that the exchange goes on without any intervention of the TTP, as such an intervention is in practice costly and should be used parsimoniously.

An example of a protocol is the set of behaviors defined as the product of the sets of following behaviors:

For Alice: Wait between 1 and 7 time units before sending $\textit{item}_1$. Then wait between 22 and 28 time units.
If $\textit{item}_2$ has not been received by then, alert the TTP.

For Bob: Wait between 3 and 12 time units before sending $\textit{item}_2$. Then wait between 20 and 30 time units.
If $\textit{item}_1$ has not been received by then, alert the TTP.

For the TTP: When alerted, immediately force the other party to send the item.

For the Infrastructure: Each received item is transmitted within 6 time units.

One can check that this allows the exchange to be performed, without any TTP intervention, in under 18 time units, so the correctness condition is achieved for any implementation of this protocol.
Note that that is true only if the Infrastructure behaves as planned by the protocol: in practice, no one controls it, and an item delivery may last (much) more than 6 time units.
In such cases, the correctness condition is no longer guaranteed: the TTP may be called.
But that is acceptable in light of another requirement to protocols, immunity against attacks, which must be guaranteed even if the Infrastructure helps the attacking agents.

While the usual attacking models are fully pessimistic, i.e. assume that malicious agents may do anything to wrong other agents, our model enable us to mitigate that pessimism by assuming no agent will wrong themself in order to perform an attack.

[Attack, safe protocol]
An attack of the alliance $A \subseteq \agents$ to the protocol $P$ is a tuple of behaviors $\balpha$, such that:

* there exists an implementation $\bbeta \in P$ such that, for each $a \in \agents \setminus A$, we have $\beta_a = \alpha_a$ (the agents that do not belong to $A$ follow the protocol $P$);

* for every $a \in A$, we have $\balpha \not\in \Wrong_a$ (none of the attacking agents is wronged);

* and there exists $a \not\in A$ such that $\balpha \in \Wrong_a$ (at least one agent is wronged).

A protocol $P$ is safe if there is no attack to $P$.

If the protocol $P$ is safe, then in particular, the empty alliance has no attack.
Therefore, no agent is wronged in any implementation $\bbeta \in P$.

Thus, modeling a concrete situation by a protocol challenge can be done by defining appropriate wronging conditions, depending on the type of attacks one wants to avoid: it defines simultaneously what a successful attack is, and what the agents cannot accept when they are involved in an attack.

In addition to being immune to attacks, a desirable property of a protocol is to conform to the correctness condition.
Therefore, a positive answer to the challenge is defined as follows:

A positive answer to a protocol challenge is a safe protocol $P$ such that $P \subseteq \Corr$.

If we consider the protocol described in Example <ref>, it appears that every implementation satisfies the correctness condition.
Moreover, there is no attack to the protocol: the only ways for Alice to satisfy her individual objective are to be helped by the TTP or by Bob; but then, that agent is wronged — and symmetrically for Bob.

On the other hand, consider again the protocol challenge in the context without the TTP.
Then, there is no safe protocol satisfying the correctness condition in that case: if the correctness condition is satisfied, then either the alliance $\{\alice\}$ or the alliance $\{\bob\}$ has an attack, by refusing to send the item.

§.§ Safe protocols as strong secure equilibria

We will now see how such protocol challenges can be modeled as games.
Let us first define games.

A game is a tuple $\Game = \left(\Pi, (\Sigma_i)_{i \in \Pi}, (\mu_i)_{i \in \Pi}\right)$, where:

* $\Pi$ is a set of players;

* for each player $i \in \Pi$, the set $\Sigma_i \neq \emptyset$ gathers the strategies available for player $i$ (when $P \subseteq \Pi$, we also write $\Sigma_P = \prod_{i \in P} \Sigma_i$);

* for each player $i$, the function $\mu_i: \Sigma_\Pi \to \RR$ is the payoff function of player $i$.

Given a strategy profile $\bsigma$ and a subset of players $C\subseteq \Pi$, $\bsigma_C \in \Sigma_C$ denotes the profile of strategies from $\bsigma$ for players of $C$.
The set $-C$ denotes $\Pi\setminus C$, the set of all players not in $C$.
For two disjoint sets of players $C_1,C_2$ with $C_1 \cap C_2=\emptyset$, two strategy profiles $\bsigma_{C_1} \in \Sigma_{C_1}$ and $\bsigma_{C_2}' \in \Sigma_{C_2}$ can be combined into a profile for all players in $C_1\cup C_2$, written $( \bsigma_{C_1}, \bsigma'_{C_2} ) \in \Sigma_{C_1\cup C_2}$.
In particular, given two profiles $\bsigma,\bsigma'\in\Sigma_\Pi$ and a set of players $C$, $( \bsigma_{-C}, \bsigma'_C )\in \Sigma_\Pi$ is the profile made from strategies of $\bsigma$ for players not in $C$ and in $\bsigma'$ for players in $C$.

In such games, we are interested in a new notion of equilibrium, that does not allow deviations of any coalition (strong equilibrium) that would harm another player without harming a member of the coalition (secure equilibrium).

[Strong secure equilibrium]
Let $\Game$ be a game.
Let $\bsigma \in \Sigma_\Pi$ be a strategy profile in $\Game$: a harmful deviation of the coalition $C \subseteq \Pi$ is a strategy profile $\bsigma'_C \in \Sigma_C$ such that for every player $i \in C$, we have $\mu_i( \bsigma_{-C}, \bsigma'_C ) \geq \mu_i( \bsigma )$, and for some player $i \not\in C$, we have $\mu_i( \bsigma_{-C}, \bsigma'_C ) < \mu_i( \bsigma )$.
A strong secure equilibrium in $\Game$, or SSE for short, is a strategy profile that admits no harmful deviation.

That notion captures our notion of safe protocol: in an SSE, players cannot collude to harm another player, as long as we assume that they will not sacrifice themselves to do so.

Let $\pc$ be a protocol challenge, and let us consider the game $\Game$ defined as follows: the players are the agents of $\pc$, the strategies available for each player $i$ are the behaviors available for agent $a$ in $\pc$, and the payoff functions are defined as follows:

$$\mu_a: \bsigma \mapsto \begin{cases}
0 & \text{if } \bsigma \in \Wrong_a \\
1 & \text{if } \bsigma \not\in \Wrong_a
\end{cases}.$$

Then, the protocol $P$ is safe if and only if each $\bsigma \in P$ is an SSE satisfying $\mu_i(\bsigma) = 1$ for every player $i$.

That result will be an immediate consequence of Theorem <ref>.

§.§ Finite models of protocols

Modeling and verifying protocols through games is only possible when available behaviors are generated from a finite object; the most frequent underlying game model being games on graph, where players navigate a finite graph, the player owning the vertex choosing the next edge.
In what follows, given a set $S$, we write $S^*$ (resp. $S^\omega$) the set of finite (resp. infinite) sequences $s_1\dots s_n$ (resp. $s_1 s_2 \dots$) of elements of $S$.

[Game on graph]
A game on graph is a tuple $\Game=\left(\Pi,V,E,\left(\mu_i\right)_{i\in\Pi}\right)$ where:

* $\Pi$ is a set of players;

* $V = \biguplus_{i\in\Pi} V_i$ is the set of vertices, partitioned according to which player owns each vertex;

* $E\subseteq V\times V$ is the set of edges, which is assumed to create no sink vertex: $\forall v\in V, \exists v'\in V, (v,v')\in E$;

* for each player $i$, the function $\mu_i:V^\omega\rightarrow\RR$ is the payoff function of player $i$.

A game is initialized by specifying an initial vertex $v_0\in V$.
Game $\Game$ initialized in $v_0$ is denoted $\Game_{\|v_0}$.

We write $\mu: V^\omega\rightarrow\RR^\Pi$ the payoff vector function defined by $\mu(\rho)=\left(\mu_i(\rho)\right)_{i\in\Pi}$ for $\rho\in V^\omega$.
A path in the graph $(V, E)$ is called history when it is finite, and play when it is infinite.

An initialized game on graph is a particular case of a game, as defined in Definition <ref>.
Indeed, strategies for a given player $i$ can be defined as mappings $\sigma_i: V^*V_i \to V$ such that $(v,\sigma_i(wv))\in E$ for any $w\in V^*$.
Then, from an initial vertex $v_0$, a strategy profile $\bsigma=\left(\sigma_i\right)_{i\in\Pi}$ (one strategy per player) generates a single infinite path $\< \bsigma\> = \pi_0\pi_1\cdots$ with $\pi_0 = v_0$, such that for every $j\in \NN$, if $\pi_j\in V_i$, then $\pi_{j+1} = \sigma_i(\pi_0\cdots \pi_j)$.
One can then define the payoff $\mu_i(\bsigma)$ as $\mu_i(\< \bsigma \>)$.

Recall the item exchange of Section <ref>.
A blunt representation of the possible states of the system is in means remembering, for each of the three agents, the set of items it currently possesses.
That means an infinite (and even non-enumerable!) set of vertices.
Instead, if we add the assumption that no player $i$ will send the item $\iij_{n+1}$ before they have received both items $\iki_n$, one can model the infinite exchange as a single round of the exchange, repeating infinitely.
Such an assumption is reasonable: indeed, a player $i$ that sends an item before the previous round is finished could be easily scammed.

Some strategies, called finite memory strategies, can themselves be encoded by finite objects, called Mealy machines.
In such a machine, the states represent the memory of the player.
At each turn, the current vertex in the game is read, firing a transition to a new state; and if the current vertex is controlled by the player using the machine, then the transition outputs a new vertex, to which the player goes.
We do not impose determinism on Mealy machines, since we represent a protocol as a set of strategy profiles and not necessarily as a singleton.

[Mealy machine]
A Mealy machine for player $i$ on a game $\Game$ is a tuple $\Mach = (Q, q_0, \Delta)$, where $Q$ is a finite set of states, where $q_0 \in Q$ is the initial state, and where $\Delta \subseteq (Q \times V_{-i} \times Q) \cup (Q \times V_i \times Q \times V)$ is a finite set of transitions, such that for every $(p, u, q, v) \in \Delta$, we have $uv \in E$, and such that for every $p \in Q$ and $u \in V$, there exists a transition $(p, u, q)$ or $(p, u, q, v) \in \Delta$.
When for each $p$ and $u$, there exists exactly one such transition, we say that the machine $\Mach$ is deterministic.

A strategy $\sigma_i$ in $\Game_{\|v_0}$ is compatible with $\Mach$ if there exists a mapping $h \mapsto q_h$ that maps every history $h$ in $\Game_{\|v_0}$ to a state $q_h \in Q$, such that for every $hv \in \Hist_{-i} \Game_{\|v_0}$, we have $(q_h, v, q_{hv}) \in \Delta$, and for every $hv \in \Hist_i \Game_{\|v_0}$, we have $(q_h, v, q_{hv}, \sigma_i(hv)) \in \Delta$.
The set of strategies in $\Game_{\|v_0}$ compatible with $\Mach$ is written $\Comp_{\|v_0}(\Mach)$; these strategies are called finite-memory.
If $\Mach$ is deterministic, then there is exactly one strategy compatible with $\Mach$.

We define analogously Mealy machines capturing strategy profiles for several players, and in particular for the whole set $\Pi$.
In such a case, we simply call it machine on the game $\Game$, with no mention of a player.

§.§ About compliant infrastructures

The proposed model relies on the assumption that agents are rational and therefore would always prefer to satisfy their individual objective and to avoid being wronged.
However, it is often necessary to consider a special agent whose case is slightly different: the Infrastructure, written $\II$, which may do anything and help any player, as long as it satisfies some compliance hypothesis.
For example, it is a common assumption that (neutral) communication channels can delay messages for an arbitrary duration, but cannot drop a message altogether.
In the case of protocol challenges and games specified abstractly, this can be done explicitly: the set $\behaviors_\II$ does not contain the behaviors we choose to exclude.
But when we want to see a protocol challenge as a game played on a finite graph, some behaviors that are assumed to be impossible cannot be excluded by the game structure itself: they must be included in it, but the payoff function must be designed in a way that guarantees that they will never be used.

This is why, although the Infrastructure is not an agent endowed with reason and acting according to its interest, hence we always have $\Wrong_\II = \emptyset$, we define a compliance hypothesis that the Infrastructure will always guarantee.

The definition of what constitutes a protocol challenge and an attack can then be updated as follows:

[Protocol challenge (with compliance hypothesis)]
A protocol challenge is a tuple:

\[\pc = \left(\agents, (\behaviors_a)_{a \in \agents}, (\Wrong_a)_{a \in \agents}, \Com, \Corr\right),\]

* $\left(\agents, (\behaviors_a)_{a \in \agents}, (\Wrong_a)_{a \in \agents}, \Corr\right)$ is a protocol challenge;

* the agent Infrastructure, written $\II \in \agents$, has an empty wronging condition $\Wrong_\II = \emptyset$;

* the compliance hypothesis $\Com \subseteq \behaviors_\agents$ is such that the Infrastructure has a least one compliant behavior, i.e. a behavior $\beta_\II$ such that for every behavior $\bbeta_{-\II}$, we have $(\beta_\II, \bbeta_{-\II}) \in \Com$.

[Attack, safe protocol (under compliance hypothesis)]
An attack of the alliance $A \subseteq \agents$ to the protocol $P$ in the protocol challenge $\pc$ is a tuple of behaviors $\balpha$, such that:

* $\balpha$ is an attack on $P$, in the sense of Definition <ref>, in the protocol challenge $\left(\agents, (\behaviors_a)_{a \in \agents},\right.$ $\left.(\Wrong_a)_{a \in \agents}, \Corr\right)$;

* and $\balpha$ satisfies the compliance hypothesis $\Com$.

The protocol $P$ is safe if there is no attack to $P$, and if in every implementation of $P$, the Infrastructure's behavior is compliant.

A positive answer to a protocol challenge with compliance hypothesis is a protocol $P \subseteq \Corr$ that is safe under compliance hypothesis.

In the item exchange with explicit Infrastructure described in Example <ref>, consider the following deviation to our protocol: the Infrastructure delivers $\textit{item}_2$ to Alice, but keeps $\textit{item}_1$ forever.
Then, Alice gets her individual goal satisfied (without even effectively deviating), and Bob is wronged: even when he calls the TTP, she cannot arrange the situation, since Alice has already sent $\textit{item}_1$.
However, in such a scenario, the compliance hypothesis is no longer satisfied, hence it is not an attack under compliance hypothesis.

Why is the compliance hypothesis not encoded in the Infrastructure's wronging condition?
Intuitively, it may seem a natural abstraction to define the Infrastructure's wronging condition as the negation of its compliance hypothesis: it can then help any agent who tries to attack others, as long as the compliance hypothesis is maintained.
However, the compliance hypothesis cannot fit such a formalism: the wronging condition is what an agent cannot accept to help other agents, while non-compliance is what the Infrastructure cannot do.
A protocol can perfectly be safe if, in a scenario in which some agent, say Bob, deviates, some other agent, say Alice, accepts to be wronged in order to wrong Bob and, thus, punish him.
There can also be scenarii in which Alice cannot avoid to be wronged.
In contrast, the Infrastructure must always guarantee its compliance hypothesis whatever the other agents do.

The addition of the compliance hypothesis does not hinder the conversion of the problem into a game.
The payoffs are defined as follows:

* for $a \neq \II$:

$$\mu_i: \bsigma \mapsto \begin{cases}
0 & \text{if } \bsigma \in \Wrong_a \cap \Com \\
1 & \text{if } \bsigma \in \overline{\Wrong_a} \cup \overline{\Com}
\end{cases};$$

* for the Infrastructure:

$$\mu_\II: \begin{cases}
0 & \text{if } \bsigma \in \overline{\Com} \\
1 & \text{if } \bsigma \in \Com
\end{cases}.$$

As we will see in the formal proof, the fact that non-compliance cancels the wronging conditions of the non-Infrastructure players will ensure that it is in the best interest of the Infrastructure to play according to a compliant strategy.

Let $P$ be a protocol in the protocol challenge with compliance hypothesis $\pc$.
The protocol $P$ is safe if and only if each $\bsigma \in P$ is an SSE satisfying $\mu_i(\bsigma) = 1$ for every player $i$.

* If $P$ is safe under compliance hypothesis.

Let $\bsigma \in P$.
From the compliance hypothesis, $\bsigma\in\Com$, so $\mu_\II(\bsigma)=1$.
Since $P$ has no attack from the empty alliance, we have $\bsigma \not\in \Wrong_a$, i.e. $\mu_a(\bsigma) = 1$, for every agent $a\neq \II$.

Let us now prove that $\bsigma$ is an SSE.
Assume that there exists a coalition $C \subseteq \agents$, that has a harmful deviation $\bsigma'_C$.
Let $\balpha=(\bsigma_{-C},\bsigma_C')$.
We have:

* $\mu_i(\balpha) = 1$ for all $i \in C$;

* and there exists $j \not\in C$ such that $\mu_i(\balpha) = 0$.

Then, if we have $\II \in C$, then $\mu_i(\balpha) = 1$, i.e. $\balpha$ satisfies the compliance hypothesis; and if $\II \not\in C$, then $\alpha_\II = \beta_\II$ is a compliant behavior, hence we also have $\balpha \in \Com$ and $\mu_\II(\balpha) = 1$.
Therefore, we have $j \neq \II$, which means that agent $j$ is wronged in $\balpha$, while no agent belonging to $C$ is: as a consequence, the behavior $\balpha$ is an attack of the alliance $C$ on $P$, which contradicts its safety.

* If every $\bsigma \in P$ is an SSE that yields payoff $1$ to every player.

First, let us assume that there exists $\bsigma \in P$ such that $\sigma_\II$ is not a compliant behavior.
Then, there exists $\bsigma'_{-\II}$ such that $(\bsigma'_{-\II}, \sigma_\II) \not\in \Com$, and therefore such that $\mu_\II(\bsigma'_{-\II}, \sigma_\II) = 0$, and $\mu_i(\bsigma'_{-\II}, \sigma_\II) = 1$ for each $i \neq \II$.
In other words, the coalition $\agents \setminus \{\II\}$ has a harmful deviation from the strategy profile $\bsigma$, which is therefore not an SSE: contradiction.

Let us now assume that there is an attack $\balpha$ of the alliance $A \subseteq \agents$ on the protocol $P$.
Let $\bsigma$ be an implementation of $P$ such that $\balpha_{\agents \setminus A} = \bsigma_{\agents \setminus A}$.
By assumption, the strategy profile $\bsigma$ is an SSE that gives every player a payoff equal to $1$.

Consider the coalition $A$: for each agent $i \in A \setminus \{\II\}$, we have $\balpha \notin \Wrong_i$, hence $\mu_i(\balpha) = 1$; and since the compliance hypothesis is satisfied in $\balpha$, we also have $\mu_\II(\balpha) = 1$.
Moreover, there exists $j \not\in A$ such that $\balpha \in \Wrong_j$, i.e. $\mu_i(\balpha) = 0$.
As a consequence, the strategy profile $\balpha_A$ is a harmful deviation of $\bsigma_A$, which is impossible since $\bsigma$ is an SSE: there is therefore no attack to $P$, which is then safe under compliance hypothesis.

§ MODELING MESSAGE EXCHANGES IN GAMES

In this section, we argue that finite games are, despite their relative simplicity, expressive enough to capture a wide range of fair exchange protocols. We first provide a general technique to encode these problems, and apply it to the Zhou-Gollmann optimistic protocol.
We show in Appendix <ref> that it can also be used to model (several variations of) the Baum-Waidner multi-party contract signing protocol.
We also provide a more formal description of the tripartite exchange of Section <ref>, where safety relies on agents' rationality.

§.§ Protocol challenges for message exchange

Not every protocol analysis can be effectively translated into a finite game on graphs.
One main limitation is protocols that are defined using an a priori unbounded variety of messages.
On the other hand, fair exchange protocols such as contract signing (whether two-party or multi-party), rely on a finite variety of messages: messages that do not conform in structure to what is expected can be discarded (or even trigger the termination of the protocol).
As a result, by treating cryptographic primitives (which are assumed to be perfect) in a symbolic way, one can limit the state-space to encode the set of messages that each participant has already received.

The only actions that an agent can perform is to send a message to another agent.
The set of possible actions (the sending of a messages) is denoted $\actions$.
From the set of messages currently known, agents have the possibility to send all messages they are allowed to based on rules describing the protocol.
When the agent is the Infrastructure, the action is the relaying of a message to its intended recipient; this correspond to the action of said recipient receiving the message.
Recall that in order to assume that the communication channels are reliable, i.e. that they cannot delay a message infinitely, it is sufficient to include that in the Infrastructure's compliance hypothesis.

As games on graphs are turn-based rather than concurrent, the model includes a round-robin: agents take turn in sending messages (or just skip their turn); as a result the state space also includes the identity of the active agent.

This can be modeled by a game on graph $2^\actions\times\agents$.
From a state $(v,a)$, the sending of a set of messages $M\subseteq\actions$ from by $a$ means choosing as successor state $(v\cup M,a')$, where $a'$ is the next agent in the round-robin.
Abusively, we say that an agent “sends messages $x,y,z$” when $v'\setminus v=\{x,y,z\}$.
It is sometimes useful to refer to the absence of action ($v=v'$) as a special action $\noAct$.
The behavior of each agent is the choice of the message to be emitted when in a given state.

§.§.§ Applied Pi-Calculus

Protocols can be described using the concurrent process description known as Applied $\pi$-Calculus <cit.>.
Each role of the protocol is modeled by a process, and processes evolve concurrently, exchanging messages: the $\textit{out}$ operator sends a message while the $\textit{in}$ operator acts upon reception of a message; upon input, the content of the message can be bound to variables.
Fresh values (for example nonces) are created by the $\nu$ operator, and asymmetric encryption (resp. decryption) is done through the $\textit{enc}(x, \textit{pu})$ (resp. $\textit{dec}(z, \textit{pr})$) operators.
The values of variables can be compared in conditional operators.

Free variables allow for the process to choose any value for a given part of a message.
While this allows for an arbitrary number of different potential messages, it is possible to restrict to those which structure is syntactically accepted by some other process.

For example, if a process is $\textit{in}(x,z).\textit{if}\ \textit{dec}(z, \textit{pr}_A)) = N_A\ \textit{then}\ Q$ for some canal $x$ and some term $Q$, then the only possible messages is $\textit{enc}(z,\textit{pu}_A)$ and all the rest is discarded.
C'est pas très formel tout ça…(voire très pas formel :-D)

In the full process algebra, replication of processes (using the $!$ operator) allow for copy of roles in the protocol.
That, however, would yield an infinite game that cannot be encompassed with a finite arena.
As a result we shall only consider applied $\pi$-calculus terms that do not contain replication.

The protocol of  <ref> can be represented in Applied $\pi$-Calculus with the following process $P$:

\[\begin{array}{rcl}
P &=& \nu x_{\alice,\II},x_{\bob,\II},x_{\alice,\ttp},x_{\bob,\ttp}.(A \procPar B \procPar T \procPar I) \\
\text{where}&&\\
%% Alice
A &=& S_{A} \procPar \left(\textit{in}(x_{\alice,\II},\textit{item}_2) + \textit{out}(x_{\alice,\ttp},w_\alice)\right) \\
S_A &=& S_A + \textit{out}(x_{\alice,\II},\textit{item}_1) + \textit{in}(x_{\alice,\ttp},f_\alice).\textit{out}(x_{\alice,\II},\textit{item}_1) \\
%% Bob
B &=& S_{B} \procPar \left(\textit{in}(x_{\bob,\II},\textit{item}_1) + \textit{out}(x_{\bob,\ttp},w_\bob)\right) \\
S_B &=& S_B + \textit{out}(x_{\bob,\II},\textit{item}_2) + \textit{in}(x_{\bob,\ttp},f_\bob).\textit{out}(x_{\bob,\II},\textit{item}_2) \\
%% TTP
T &=& \textit{in}(x_{\alice,\ttp},w_\alice).\textit{out}(x_{\bob,\ttp},f_\bob) \procPar \textit{in}(x_{\bob,\ttp},w_\bob).\textit{out}(x_{\alice,\ttp},f_\alice)  \\
%% Infrastructure
I &=& \textit{in}(x_{\alice,\II},\textit{item}_1).\textit{out}(x_{\bob,\II},\textit{item}_1) \procPar \textit{in}(x_{\bob,\II},\textit{item}_2).\textit{out}(x_{\alice,\II},\textit{item}_2)
\end{array}\]

This process is made of several sub-processes running in parallel.
Sub-process $A$ represents $\alice$, $B$ is $\bob$, $T$ is $\ttp$, and $I$ is Infrastructure.
We first declare communication channels between these sub-processes.
Then $A$ is both waiting for $\textit{item}_2$ and can send $\textit{item}_1$ at any time.
Receiving $f_\alice$ from the TTP removes the choice of sending or not $\textit{item}_1$.
Sub-process $B$ works similarly.

§.§ The Zhou-Gollmann optimistic protocol

The Zhou-Gollmann optimistic protocol [26] allows for the sending of a message $M$ from Alice ($\alice$) to Bob ($\bob$) along with the exchange of non-repudiation proofs between them.
The protocol only relies on a trusted third party (TTP, $\ttp$) as a recovery process, hence the optimistic nature of the protocol.
The TTP is connected to both $\alice$ and $\bob$ by resilient communication channels that ensure immediate transmission of messages.
Alice and Bob are, however, connected through channels that can delay messages for an arbitrarily long time; it is often assumed that messages are always indeed delivered and not delayed forever.
Messages are never altered by the channels.

The protocol is performed as follows.
Alice first sends the message $M$ ciphered with a fresh key $k$, along with the evidence of origin of the message: the ciphered message and some metadata, signed with $\alice$'s private key.
This whole message will be denoted as $\EOO$.
Bob replies with an evidence of receipt message $\EOR$: the ciphered  $M$ and some metadata, signed with $\bob$'s private key.
Alice then sends the key $k$, again with evidence of origin in the form of a privately signed string containing $k$ and the metadata; altogether this message is denoted $\EOO_k$.
Bob replies with an evidence of receipt of $k$, denoted $\EOR_k$, made of a privately signed $k$ and some metadata.
Remark that having both the ciphered message and the key, Bob is now able to obtain $M$.
The non-repudiation proof of origin ($\NRO$) is made of the evidence of origin of both $M$ and $k$.
Conversely, the non-repudiation proof of receipt ($\NRR$) is made of the evidence of receipt of both $M$ and $k$.

In the case where $\alice$ never receives the $\EOR$, she stops the protocol and the transmission of $M$ is aborted.
If Alice has, however, received the $\EOR$ but not the $\EOR_k$, a situation in which she is at risk of being cheated since Bob now has $M$ and the $\NRO$, Alice can initiate a recovery protocol with the TTP.
In this case she sends key $k$ along with a signed evidence of origin $\Sub_k$ to $\ttp$.
The TTP can then publish $k$ along with a signed confirmation $\Con_k$ that acts as the evidence of receipt for Alice.
This confirmation can also be used by Bob as a confirmation of origin; in the case Alice had initiated the recovery process without first actually sending $\EOO_k$, Bob can still recover it from the TTP.

As the Infrastructure may delay messages, it makes sense for this protocol to have a commonly agreed time after which it is considered that messages that were not received were actually never sent and the protocol should be stopped.
So $\alice$ indicates a deadline $t$ in her metadata: after $t$, the recovery protocol cannot be initialized.
As a result, after $t$, Bob can ask the TTP for the key and $\Con_k$ if he has not received $\EOO_k$ yet.
If the TTP does not have it, then the protocol is aborted.
This means that Alice must initiate the recovery protocol before $t$; the TTP would just refuse to provide $\Con_k$ after $t$.

The rest of the metadata in this protocol allows each participant to identify protocol runs and prevents man-in-the-middle type attacks, but is not relevant to the setting of this work, and will be ignored henceforth.

In our framework, both $\alice$, $\bob$, and $\ttp$ are agents, and $\II$ is the Infrastructure.
The actions available to the agents as the messages they can send, and a special $\noAct$ action that amounts to not doing anything.
When $X\in\{\alice,\bob\}$ sends a message $m$ to the other, $Y$, they actually sends it to $\II$ which relays it (maybe later, if ever) to its recipient.
This is modeled by two actions $m^\s$, a message from $X$ to $\II$, and $m^\r$, from $$ to $Y$.
As communication with the TTP is perfect, the Infrastructure is not involved in that case.
Except for $_k$, each message has a given recipient which will not be specified in the corresponding action:
\begin{itemize}
\item $\alice$ can execute $\EOO^\s$, $\EOO_k^\s$, $\Sub_k$, and $\noAct_\alice$.
\item $\bob$ can execute $\EOR^\s$, $\EOR_k^\s$, and $\noAct_\bob$.
\item $\ttp$ can execute $\Con_k^\alice$ (to Alice), $\Con_k^\bob$ (to Bob), and $\noAct_\ttp$.
\item $\II$ can execute $m^\r$ for $m\in\{\EOO,\EOR,\EOO_k,\EOR_k\}$, and $\noAct_\II$.
\end{itemize}
The rules prevent the sending of a message containing elements unknown to an agent yet.
So the Infrastructure cannot send $m^\r$ before $m^\s$ has occurred.
And as evidence of receipt contains the message received (in some form), Bob cannot execute $\EOR^\s$ (resp. $\EOR_k^\s$) before $\EOO^\r$ (resp. $\EOO_k^\r$) occurred.
Similarly, $\ttp$ cannot execute $\Con_k^\alice$ or $\Con_k^\bob$ before $\Sub_k$.

% The wrongness conditions of the agents are defined as follows.
As a notation, we identify the fact that an action (except $\noAct$s) has been executed with a propositional variable, and collectively denote them as the set $\actions$.
The variable becomes true once the action has been executed, and remains so.
That amounts to define the arena as the turn-based game on vertices $2^\actions\times\{\alice,\bob,\ttp,\II\}$.
\ifPagesLimited
The set of transitions $E$ that ensures the above rules are respected and uses a round-robin to rotate through players is formally given in Appendix~\ref{app:ZhouGollmannTransitions}.
\else
\input{appZhouGollmannTransitions}
\fi

All conditions can then be expressed as Linear Temporal Logic (LTL) formulas~[23].
This logic allows reasoning over traces by using time modalities.
The \emph{eventually} modality, written $\eventually \varphi$, means that the formula $\varphi$ must be true at some time in the future.
Dually, the \emph{globally} modality, written $\globally \varphi$, means that $\varphi$ must be true at all time from now on.

We first define (boolean) formulas for the non-repudiation proofs:
\begin{mathpar}
\NRO = \EOO^\r \wedge (\EOO_k^\r \vee \Con_k^\bob)
\and
\NRR = \EOR^\r \wedge (\EOR_k^\r \vee \Con_k^\alice)
\end{mathpar}
Then we can define the wrongness condition of Alice and Bob as wanting their non-repudiation proof to be obtained by the other without obtaining a non-repudiation proof themselves.
Otherwise said, Alice is wronged if $\NRO$ is eventually true and $\NRR$ is never (\emph{i.e.} always not) true.
In LTL syntax, this is written as:
\begin{mathpar}
\Wrong_\alice = \eventually \NRO \wedge \globally \neg\NRR
\and
\Wrong_\bob = \eventually \NRR \wedge \globally \neg\NRO
\end{mathpar}
The wrongness condition of the TTP is defined to correspond to situation where at least one of the other agents is wronged, since its goal is to ensure a fair exchange of said proofs:
\[\Wrong_\ttp = \Wrong_\alice \cup \Wrong_\bob\]
The compliance hypothesis models the assumption that the Infrastructure cannot delay messages forever.
\[\Com = \bigwedge_{m\in\{\EOO,\EOR,\EOO_k,\EOR_k\}} \globally (m^\s \Rightarrow \eventually m^\r)\]
Note that there is a way for the Infrastructure to ensure compliance regardless of the behaviors of others, for example by immediately transmitting any message it receives.
Finally, the correctness of the protocol is the full exchange of both non-repudiation proofs:
\[\Corr = \eventually \NRR \wedge \eventually \NRO\]
% Note that for every trace $\tau\in\Com$, the strategy of $\II$ to transmit messages as it does in $\tau$ for every prefix $\tau'$ of $\tau$ and immediately transmit the message in any other case is a compliant behavior. \Ms{Not sure we need this anymore}

Remark that all these conditions can be encoded with relatively simple parity conditions (see Definition~\ref{def:parityCondition} below) over the arena.
For example for $\Wrong_\alice$, give priority $1$ to vertices where $\NRR$ holds, $2$ to other vertices where $\NRO$ holds, and $3$ elsewhere.
In the corresponding game, the winning condition combines the negation of the wrongness condition with the negation of the compliance condition.
As the arena is a directed acyclic graph, this can still be done by a simple parity condition.
Namely, vertices where  $\NRR$ holds or there is a sent message that has not been transmitted get priority $0$, other vertices where $\NRO$ holds have priority $1$, and all remaining vertices get priority $2$.

The protocol as described above where the Infrastructure chooses to transmit messages without delay and Alice chooses a deadline that is $\theta$ time units after the start of the protocol can be modeled by the Mealy machine $\M_\theta$ of \figurename~\ref{fig:mealyZGprotocol}\ifPagesLimited{ in Appendix~\ref{app:ZhouGollmannMealy}}\else.

\input{appZhouGollmannMealy}\fi

\begin{rk}[On previous verification efforts] The Zhou-Gollmann optimistic protocol was verified in~[19]. The authors considered a list of verification conditions expressed in alternating time temporal logic (ATL)~[3], an extension of branching time logics that allows reasoning about the strategic abilities of agents in alternating transition systems. Those alternating transition systems are equivalent to the game graphs used in our framework. The properties verified in that paper are logically equivalent to ensuring that the Zhou-Gollmann optimistic protocol enforces anSSE. Thus, their verification requirements align with the correctness condition implied by our framework.

However, our method operates at a higher level. We only need to express the correctness condition of the protocol and the wronging conditions for each participating agent. The semantics of the protocol challenge then automatically define the conditions that need to be verified on the game graph, relieving the specifier from reasoning about possible coalitions and their objectives. While our framework provides guarantees equivalent to those obtained through the verification tasks in~[19], it significantly reduces the specifier's burden by eliminating the need for ad hoc reasoning about agent rationality and potential coalitions that could threaten the protocol.
\end{rk}

\subsection{Beyond trust (continued)}\label{sec:motivatingExampleInfiniteFiniteModel}

Recall the tripartite item exchange of Section~\ref{sec:motivatingExampleInfinite}.
As explained in Example~\ref{ex:finiteModelTripartiteExchange}, this can be modeled as a finite arena as long as it is assumed that the process takes place in rounds.

In this setting, the goal of each player is still to exchange items infinitely often, and they can punish a player deviating from the predefined protocol by stopping exchanges with them.
Therefore the arena of the game consists of vertices remembering the current ownership of the six different items, regardless of their index.
A player's wronging condition is expressed by not having received an item after sending theirs (being \emph{scammed}) or not being able to continue the exchange when they have not scammed another player.
Formally, for each player $i$, the wronging condition of $i$ is given by the following LTL formula:
\begin{mathpar}
\Wrong_i = \left(\exists j, \Scam_{j,i}\right) \vee (\exists j, \exists k, \neg \eventually \left( i \text{ has } \obj{j}{i}_k \right) \wedge \forall j' \neg \Scam_{i,j'})
\\\text{where}\and\Scam_{i,j} = \exists k, \forall \ell\leq k, \eventually \left(i \text{ does not have } \obj{j}{i}_\ell \right) \wedge \neg \eventually j \text{ has } \obj{i}{j}_k.
\end{mathpar}

In the game formalism, determining which players are wronged can be expressed through an automaton reading the infinite sequence of states of the arena.
A player, say Alice, wins by visiting infinitely often a vertex where the exchange of the current round is finished (i.e. when she owns $\iba$ and $\ica$) or when she successfully ``stole'' an item, for example owning $\iab$, $\iba$, $\iac$.
One can go one step further and externalize the winning conditions for each player into a separate automaton, in this case a B\"uchi\footnote{A \B\"uchi automaton accepts an infinite run if it visits at least one accepting state infinitely.} automaton.
The arena can then be reduced to a simple round-robin allowing players to alternatively send an item to any other participant, or skip their turn (see \figurename~\ref{fig:infiniteExchangeArena}).
Each B\"uchi automaton's state remembers what the player currently possesses: a player who sends an item that they do not currently have leads the parity automaton to a sink (not accepting) state $\bot$.
When a player has reached a state where the exchanges for this round have been performed, the automaton loops back to the initial state, meaning the next round is now being played.
The accepting states are the states where a player has finished the round or when they have stolen an item.
This is partially depicted in \figurename~\ref{fig:infiniteExchangeParityAuto}.
This separation does simplify the model as it separates the knowledge of each player, although it does not reduce the actual complexity of the analysis (see Section~\ref{sec:algorithms}).%
\begin{figure*}
\centering
\ifArxiv
\begin{tikzpicture}[node distance=3cm]
\tikzstyle{neutral}=[state,shape=rounded rectangle, inner xsep=2pt,inner ysep=3pt,draw]

\node[state,player1] (va) at (0,0) {$v_\alice$};
\node[state,player2] (vb) at (7,0) {$v_\bob$};
\node[state,player3] (vc) at (3.5,-5) {$v_\charlie$};

\path[->] (va) edge[bend left=90,distance=4cm] (vb);
\path[->] (vb) edge[bend left] (vc);
\path[->] (vc) edge[bend left] (va);

\node[neutral,above right of=va,anchor=south west] (sABB) {$\alice$ sends $\iab$ to $\bob$};
\node[neutral,below right of=va,anchor=north west] (sBCC) {$\alice$ sends $\ibc$ to $\charlie$};
\node[neutral] (sABC) at (barycentric cs:sABB=4,sBCC=1) {$\alice$ sends $\iab$ to $\charlie$};
\node[neutral] (sACB) at (barycentric cs:sABB=3,sBCC=2) {$\alice$ sends $\iac$ to $\bob$};
\node[neutral] (sACC) at (barycentric cs:sABB=2,sBCC=3) {$\alice$ sends $\iac$ to $\charlie$};
\node (sDots) at (barycentric cs:sACC=1,sBCC=1) {$\vdots$};
\path[->] (va) edge[bend left=30] (sABB);
\path[->] (sABB) edge[bend left=30] (vb);
\path[->] (va) edge[bend left=20] (sABC);
\path[->] (sABC) edge[bend left=20] (vb);
\path[->] (va) edge[bend left=9] (sACB);
\path[->] (sACB) edge[bend left=9] (vb);
\path[->] (va) edge[bend right=9] (sACC);
\path[->] (sACC) edge[bend right=9] (vb);
\path[->] (va) edge[bend right=30] (sBCC);
\path[->] (sBCC) edge[bend right=30] (vb);

\node[neutral,dashed,shape=rectangle, rounded corners=9pt,anchor=west,text width=3.25cm,text centered,inner sep=5pt] (bobSends) at (7.5,-3) {$\bob$ sends $\obj{i}{j}$ to $k$\\$i \in\{\alice,\bob,\charlie\}$, $j,k \in \{\alice,\charlie\}$\\$i\neq j$};
\path[->] (vb) edge[bend left] (bobSends);
\path[->] (bobSends) edge[bend left] (vc);

\node[neutral,dashed,shape=rectangle, rounded corners=9pt,anchor=east,text width=3.25cm,text centered,inner sep=5pt] (charlieSends) at (-0.5,-3) {$\charlie$ sends $\obj{i}{j}$ to $k$\\$i\in\{\alice,\bob,\charlie\}$, $j,k \in \{\alice,\bob\}$\\$i\neq j$};
\path[->] (vc) edge[bend left] (charlieSends);
\path[->] (charlieSends) edge[bend left] (va);
\end{tikzpicture}
\else
\begin{tikzpicture}[node distance=2cm,yscale=0.55]
\tikzstyle{neutral}=[state,shape=rounded rectangle, inner xsep=2pt,inner ysep=3pt,draw]

\node[state,player1] (va) at (0,0) {$v_\alice$};
\node[state,player2] (vb) at (5.5,0) {$v_\bob$};
\node[state,player3] (vc) at (2.75,-5) {$v_\charlie$};

\path[->] (va) edge[bend left=90,distance=5cm] (vb);
\path[->] (vb) edge[bend left] (vc);
\path[->] (vc) edge[bend left] (va);

\node[neutral,above right of=va,anchor=south west] (sABB) {$\alice$ sends $\iab$ to $\bob$};
\node[neutral,below right of=va,anchor=north west] (sBCC) {$\alice$ sends $\ibc$ to $\charlie$};
\node[neutral] (sABC) at (barycentric cs:sABB=4,sBCC=1) {$\alice$ sends $\iab$ to $\charlie$};
\node[neutral] (sACB) at (barycentric cs:sABB=3,sBCC=2) {$\alice$ sends $\iac$ to $\bob$};
\node[neutral] (sACC) at (barycentric cs:sABB=2,sBCC=3) {$\alice$ sends $\iac$ to $\charlie$};
\node (sDots) at (barycentric cs:sACC=1,sBCC=1) {$\vdots$};
\path[->] (va) edge[bend left=30] (sABB);
\path[->] (sABB) edge[bend left=30] (vb);
\path[->] (va) edge[bend left=20] (sABC);
\path[->] (sABC) edge[bend left=20] (vb);
\path[->] (va) edge[bend left=9] (sACB);
\path[->] (sACB) edge[bend left=9] (vb);
\path[->] (va) edge[bend right=9] (sACC);
\path[->] (sACC) edge[bend right=9] (vb);
\path[->] (va) edge[bend right=30] (sBCC);
\path[->] (sBCC) edge[bend right=30] (vb);

\node[neutral,dashed,shape=rectangle, rounded corners=9pt,anchor=west,text width=3.25cm,text centered,inner sep=5pt] (bobSends) at (7,-3) {$\bob$ sends $\obj{i}{j}$ to $k$\\$i \in\{\alice,\bob,\charlie\}$, $j,k \in \{\alice,\charlie\}$\\$i\neq j$};
\path[->] (vb) edge[bend left] (bobSends);
\path[->] (bobSends) edge[bend left] (vc);

\node[neutral,dashed,shape=rectangle, rounded corners=9pt,anchor=east,text width=3.25cm,text centered,inner sep=5pt] (charlieSends) at (-1.5,-3) {$\charlie$ sends $\obj{i}{j}$ to $k$\\$i\in\{\alice,\bob,\charlie\}$, $j,k \in \{\alice,\bob\}$\\$i\neq j$};
\path[->] (vc) edge[bend left] (charlieSends);
\path[->] (charlieSends) edge[bend left] (va);
\end{tikzpicture}
\fi
\caption{Arena for the exchange of items between three players (partial depiction).}
\label{fig:infiniteExchangeArena}
\end{figure*}

\begin{figure*}
\centering
\ifArxiv
\begin{tikzpicture}[auto]
\tikzstyle{parState}=[automatonState,text width=1cm,minimum width=1cm,inner sep=1pt,text centered]
\tikzstyle{accepting}+=[double distance=2pt]
\node[parState,font=\Large] (fail) at (-5,0) {$\bot$};
\node[parState,initial,initial above] (ab-ac) at (0,0) {$\iab$\\$\iac$};
\node[parState] (ac) at (2.5,3) {$\iac$};
\node[parState] (ab) at (2.5,-3) {$\iab$};
% \node[parState] (empty) at (5,0) {$\emptyset$};
\node[parState,accepting] (ba-ca) at (5,0) {$\iba$\\$\ica$};
\node[parState,accepting] (ba-ca-ac) at (6,3) {$\iba$\\[-5pt]$\ica$\\[-5pt]$\iac$};
\node[parState,accepting] (ba-ca-ab) at (6,-3) {$\iba$\\[-5pt]$\ica$\\[-5pt]$\iab$};
\node[parState,accepting] (ba-ca-ab-ac) at (8,0) {$\iba$\\[-6.5pt]$\ica$\\[-6.5pt]$\iab$\\[-6.5pt]$\iac$};

\path[->] (ab-ac) edge node[swap,text width=4.375cm,text centered] {$\alice$ sends $\obj{i}{j}$ to $k$,\\$(i,j)\notin\{(\alice,\bob),(\alice,\charlie)\}$,\\$k\in\{\bob,\charlie\}$} (fail);
\path[->] (fail) edge[loop below,distance=0.5cm] node {$*$} (fail);
\path[->] (ab-ac) edge node[pos=0.75,text width=3.375cm,text centered] {$\alice$ sends $\iab$ to $k$,\\$k\in\{\bob,\charlie\}$} (ac);
\path[->] (ab-ac) edge node[swap,pos=0.75,text width=3.375cm,text centered] {$\alice$ sends $\iac$ to $k$,\\$k\in\{\bob,\charlie\}$} (ab);
\path[->] (ab-ac) edge[loop below,distance=0.5cm] node {else} (ab-ac);
% \path[->] (ab) edge node[swap,pos=0.25,text width=3.375cm,text centered] {$\alice$ sends $\iab$ to $k$,\\$k\in\{\bob,\charlie\}$} (empty);
% \path[->] (ac) edge node[pos=0.25,text width=3.375cm,text centered] {$\alice$ sends $\iac$ to $k$,\\$k\in\{\bob,\charlie\}$} (empty);
\path[->] (ba-ca) edge node[swap] {$*$} (ab-ac);

\outVanishingArrows{ac}{-90,-60,...,30}
\inVanishingArrows{ac}{60,90,...,150}
\outVanishingArrows{ab}{90,60,...,-60}
\inVanishingArrows{ab}{-90,-120,...,-180}
\inVanishingArrows{fail}{-60,-30,90,120,150,180,210}
\outVanishingArrows{ba-ca-ac}{-90,-60,...,60}
\inVanishingArrows[shorten <=1pt]{ba-ca-ac}{90,120,...,240}
\outVanishingArrows{ba-ca-ab}{-90,-60,...,60}
\inVanishingArrows[shorten <=1pt]{ba-ca-ab}{90,120,...,240}
\outVanishingArrows{ba-ca-ab-ac}{-90,-60,...,60}
\inVanishingArrows[shorten <=1pt]{ba-ca-ab-ac}{90,120,...,240}
\inVanishingArrows{ab-ac}{200,230,30,-30,60}
\inVanishingArrows[shorten <=1pt]{ba-ca}{90,-90}
\end{tikzpicture}
\else
\begin{tikzpicture}[auto,yscale=0.666]
\tikzstyle{parState}=[automatonState,text width=1cm,minimum width=1cm,inner sep=0pt,text centered]
\tikzstyle{accepting}+=[double distance=2pt]
\node[parState,font=\Large] (fail) at (-5,0) {$\bot$};
\node[parState,initial,initial above] (ab-ac) at (0,0) {$\iab$\\$\iac$};
\node[parState] (ac) at (3,2.5) {$\iac$};
\node[parState] (ab) at (3,-2.5) {$\iab$};
% \node[parState] (empty) at (5,0) {$\emptyset$};
\node[parState,accepting] (ba-ca) at (5,0) {$\iba$\\$\ica$};
\node[parState,accepting] (ba-ca-ac) at (6.5,2.5) {$\iba$\\[-5pt]$\ica$\\[-5pt]$\iac$};
\node[parState,accepting] (ba-ca-ab) at (6.5,-2.5) {$\iba$\\[-5pt]$\ica$\\[-5pt]$\iab$};
\node[parState,accepting] (ba-ca-ab-ac) at (8,0) {$\iba$\\[-6.5pt]$\ica$\\[-6.5pt]$\iab$\\[-6.5pt]$\iac$};

\path[->] (ab-ac) edge node[swap,text width=4.375cm,text centered] {$\alice$ sends $\obj{i}{j}$ to $k$,\\$(i,j)\notin\{(\alice,\bob),(\alice,\charlie)\}$,\\$k\in\{\bob,\charlie\}$} (fail);
\path[->] (fail) edge[loop below,distance=0.5cm] node {$*$} (fail);
\path[->] (ab-ac) edge node[pos=0.85,text width=3.375cm,text centered] {$\alice$ sends $\iab$ to $k$,\\$k\in\{\bob,\charlie\}$} (ac);
\path[->] (ab-ac) edge node[swap,pos=0.85,text width=3.375cm,text centered] {$\alice$ sends $\iac$ to $k$,\\$k\in\{\bob,\charlie\}$} (ab);
\path[->] (ab-ac) edge[loop below,distance=0.5cm] node {else} (ab-ac);
% \path[->] (ab) edge node[swap,pos=0.25,text width=3.375cm,text centered] {$\alice$ sends $\iab$ to $k$,\\$k\in\{\bob,\charlie\}$} (empty);
% \path[->] (ac) edge node[pos=0.25,text width=3.375cm,text centered] {$\alice$ sends $\iac$ to $k$,\\$k\in\{\bob,\charlie\}$} (empty);
\path[->] (ba-ca) edge node[swap] {$*$} (ab-ac);

\outVanishingArrows{ac}{-90,-60,...,30}
\inVanishingArrows{ac}{60,90,...,150}
\outVanishingArrows{ab}{90,60,...,-60}
\inVanishingArrows{ab}{-90,-120,...,-180}
\inVanishingArrows{fail}{-60,-30,90,120,150,180,210}
\outVanishingArrows{ba-ca-ac}{-90,-60,...,60}
\inVanishingArrows[shorten <=1pt]{ba-ca-ac}{90,120,...,240}
\outVanishingArrows{ba-ca-ab}{-90,-60,...,60}
\inVanishingArrows[shorten <=1pt]{ba-ca-ab}{90,120,...,240}
\outVanishingArrows{ba-ca-ab-ac}{-90,-60,...,60}
\inVanishingArrows[shorten <=1pt]{ba-ca-ab-ac}{90,120,...,240}
\inVanishingArrows{ab-ac}{200,230,-50,60}
\inVanishingArrows[shorten <=1pt]{ba-ca}{90,-90}
\end{tikzpicture}
\fi
\caption[B\"uchi automaton $\auto_\alice$ in the tripartite exchange of items protocol challenge.]{B\"uchi automaton $\auto_\alice$ in the tripartite exchange of items protocol challenge (partial depiction). Doubly rounded states are accepting.}
\label{fig:infiniteExchangeParityAuto}
\end{figure*}

\section{Algorithms}\label{sec:algorithms}

In this section, we study decision problems about SSEs for games on graphs.
Therefore, from now on, by \emph{game}, we always mean game on graph.
We focus on the decision problems that arise from the links we have drawn with security protocols.
First, we study the SSE-checking problem, which appears when a given protocol has to be formally verified.
Second, we study the fixed-payoff SSE existence problem, which appears when one wants to know whether a positive answer exist for a given protocol challenge.

Since in all the examples we have seen before, the wrongness conditions of the agents and the compliance hypotheses, and therefore the objectives of the players in the corresponding games, were $\omega$-regular objectives that could be described by LTL formulae, we study those problems in two classes of games with $\omega$-regular objectives: \emph{$\omega$-regular games} in which the objectives are defined by a parity automaton (a canonical and succinct way to represent $\omega$-regular objectives), and \emph{parity games}, in which the objectives are simple enough to be described by labeling directly the vertices of the game instead of the states of an automaton.
We do not consider objectives that are directly described by an LTL formula, because such a representation is so succinct that classical algorithms to handle it (model-checking, synthesis) have a very high complexity, that would hide the complexity of the interesting part of our problems.

We also consider only perfect information games, even though actual protocols are of course often hiding information to agents.
We justify that choice with the following arguments.

\begin{itemize}
\item The most important hidden or revealed information (typically, a cryptographic key) can be abstracted, and therefore captured by the arena itself, rather than by imperfect information.

\item Protocol safety cannot rely on obscurity.
Thus, relying on randomized strategies and imperfect information only makes an attack unlikely, instead of impossible.
Therefore, from the attackers' perspective, information does not matter: one must consider the case where they would chose the right actions to succeed in their attack, be it by chance.
In other words, they must be assumed to have perfect information.

\item Thus, not relying on hidden information is only a constraint that the protocols must satisfy: it does not intervene in checking that a protocol is safe.
The only decision problem where considering imperfect information might be a useful is therefore the SSE existence problem, if one wants to avoid the synthesis of protocols where the agents' actions rely on information they cannot be sure of.
That is a track for possible future works ---~however, one can already assume that complexities will be much worse.
\end{itemize}

\subsection{Definition of the problems}

For a given play $\alpha$, we write $\Occ(\alpha)$ (resp. $\Inf(\alpha)$) for the set of vertices that appear (resp. appear infinitely often) in $\alpha$.

\begin{defi}[Parity condition]\label{def:parityCondition}
Let $(V, E)$, and let $\kappa: V \to \NN$ be a mapping, called \emph{color mapping}.
The set $\Parity(\kappa)$ is the set of infinite paths $\alpha$ in $(V, E)$, such that $\min_{v \in \Inf(\alpha)} \kappa(v)$ is an even integer.
\end{defi}

\begin{defi}[Parity automaton]
A {\em parity automaton} over alphabet $X$ is a tuple $\auto=(X,S,s_0,T,\kappa)$ where $S$ is a set of states, $T:S\times X \to S$ is a deterministic transition function, and $\kappa: S \to \NN$ is a color mapping.
Given a word $w=w_0w_1\cdots\in X^\omega$, the run of $\auto$ on $w$ is $\rho_\auto(w)=s_0 s_1 \cdots$ where for $i\in \NN$, $s_{i+1}=T(s_i,w_i)$.
The set of infinite words accepted by $\auto$ is $\Lang(\auto)= \left\{w\in X^\omega \mmid \rho_\auto(w)\in\Parity(\kappa)\right\}$.
\end{defi}

It is well-known that the set of languages recognized by parity automata is exactly the set of $\omega$-regular languages.
Now, we consider two classes of games, that fit with the games that are in practice obtained from protocol challenges: games in which the payoff awarded to a player is defined by a parity condition, or by a parity automaton.

\begin{defi}[Parity game]
A \emph{parity game} is a multi-player game $\Game_{\|v_0}$ such that there exists an integer $k$ and for each player $i$, a color mapping $\kappa_{i}: V \to \{0, \dots, k-1\}$, such that for each play $\pi$, we have $\mu_i(\pi) = 1$ iff $\pi\in \Parity(\kappa_{i})\}$.
\end{defi}

\begin{defi}[$\omega$-regular game]
An \emph{$\omega$-regular game} is a multi-player game $\Game_{\|v_0}$ such that there exists an integer $k$, and for each player $i$, a parity automaton $\auto_{i}$ over alphabet $V$ using at most $k$ colors, such that  for each play $\pi$, we have $\mu_i(\pi) = 1$ iff $\pi \in \Lang(\auto_{i})$.
\end{defi}

Remark that a parity game is a particular case of an $\omega$-regular game, where all automata $\auto_{i}$ have the same structure: one state $s_v$ per vertex $v$ of the game to remember the last visited vertex.
The transition function is $T(s_v,v')=s_{v'}$.
For each automaton $\auto_{ij}$, the color of $s_v$ is $\kappa_{ij}(v)$.
\begin{table*}[ht] %% Table moved so that it appears
\centering
\begin{tabular}{|c|c|c|c|c|c|}\cline{3-6}
\multicolumn{2}{c|}{} & \multicolumn{2}{c|}{Parity} & \multicolumn{2}{c|}{$\omega$-regular} \\ \cline{3-6}
\multicolumn{2}{c|}{}                        & Gen. case    & Fixed params & Gen. case    & Fixed params \\ \hline
\multirow{2}{*}{Checking}       & Monolithic & $\coNP$-c.   & $n$: $\FPT$              & \multirow{2}{*}{$\PSpace$-c.} & \multirow{2}{*}{$n$: In $\Poly$, $\W[1]$-h.}\\ \cline{2-4}
& Composite  & $\PSpace$-c. & $n$: In $\Poly$, $\W[1]$-h. &                               & \\ \hline
\multicolumn{2}{|c|}{Fixed-payoff}           & \multirow{2}{*}{$\PSpace$-c.} & $n,k$: $\FPT$       & \multirow{2}{*}{$\ExpTime$-c.} & $n,k$: in $\Poly$, $\XP$-c. \\
\multicolumn{2}{|c|}{(constrained) existence}              &              & $n=2$: Parity$^\dagger$-h.     &               & $k=2$: $\PSpace$-h. \\ \hline
\end{tabular}
\medskip

\begin{tabular}{rl}
$n$:&Number of players \\
$k$:&Number of colors \\
$^\dagger$Parity:& 2-players Parity Games (in $\NP\cap \coNP$)
\end{tabular}}
% \hfill
% \emph{Unless otherwise specified, the fixed parameter is $n$.}
\caption{Complexity results for SSE problems.}
\label{tab:complexityResults}
\end{table*}
\begin{exa}
The model for the tripartite exchange of items as described in Section~\ref{sec:motivatingExampleInfiniteFiniteModel} uses B\"uchi automata, which are parity automata using only two colors: $0$ for accepting states and $1$ for other states.

It is possible to add an explicit Infrastructure agent, with the compliance hypothesis stating that every message sent is eventually received (following the model of resilient channels); or, equivalently, every message is infinitely not in waiting (since a message cannot be received if it has not been sent before).
The winning condition for the Infrastructure can therefore be encoded into a parity automaton $\auto_\II$ (of size $2^m\cdot m$ states, where $m$ is the number of different messages) with two priorities $0$ and $1$ (a B\"uchi automaton).
The parity automata for other players have to be modified in order to take into account that a player can win if the compliance hypothesis is not satisfied.
That means, \emph{e.g.} for Alice, combining the co-B\"uchi automaton obtained by negating the winning condition of $\auto_\II$ with the B\"uchi automaton of \figurename~\ref{fig:infiniteExchangeParityAuto}, into a product automaton with parities $0$, $1$, and $2$.
% That can be done by a cross product of $\auto_\alice$ and $\auto_\II$: a state which is accepting in $\auto_\alice$ will have priority $0$ (regardless of the state in $\auto_\II$; a state which is accepting in $\auto_\II$ (thus should be only visited finitely often for $\alice$ to win) gets priority $1$ (as long as it is not accepted with respect to $\auto_\alice$); other states get priority $2$.
\end{exa}

We can now define the decision problems we will study.
First, given a protocol, we want to be able to verify that it is safe --- from a game perspective, that amounts to decide, given the description of a strategy profile, whether all strategy profiles compatible with that description are SSEs.
Two approaches are possible regarding how the strategy profile is described: with one unique machine (monolithic), or one per agent (composite).

\begin{pb}[SSE-checking problem]
Given a parity game (resp. $\omega$-regular game) $\Game_{\|v_0}$ and a Mealy machine $\Mach$ on $\Game$, is every strategy profile compatible with $\Mach$ an SSE?
\end{pb}

\begin{pb}[Compositional SSE-checking problem]
Given a parity game (resp. $\omega$-regular game) $\Game_{\|v_0}$ and a family of Mealy machines $(\Mach_i)_{i \in \Pi}$ on $\Game$, is every strategy profile $\bsigma$, with $\sigma_i \in \Comp(\Mach_i)$ for each $i$, an SSE?
\end{pb}

In terms of protocols, solving the checking problem means verifying whether a protocol is safe.
Checking that a protocol is a positive answer to a protocol challenge also requires checking (independently) whether all implementations comply with the correctness condition, which is done through classical automata techniques (and with lower complexities than the problems at hand).
The compositional version can be used when protocols are given by a set of local descriptions of the procedure for each agent.

Later, we will also study a more complex problem: deciding the existence of a safe protocol in a given protocol challenge.
That amounts to search for an SSE with a given outcome in a given game.

\begin{pb}[Fixed-payoff SSE existence problem]
Given a parity game (resp. $\omega$-regular game) $\Game_{\|v_0}$ and a payoff vector $\bx$, does there exist an SSE $\bsigma$ in $\Game_{\|v_0}$ such that $\mu\< \bsigma \> = \bx$?
\end{pb}

Since we need to ensure that the produced protocol, i.e. the SSE, satisfies the correctness property, one can specify additional constraints on $\bsigma$.
We assume that those constraints are given in the same formalism as the payoffs, i.e. through a parity condition or an automaton.

\begin{itemize}
\item For a parity game, the correctness condition is given by a coloring mapping $\kappa_\Corr$.
A path $\alpha$ satisfies $\Corr$, written $\alpha \vDash \Corr$, if $\alpha \in\Parity(\kappa_\Corr)$.
\item For an $\omega$-regular game, the correctness condition is given by a parity automaton $\auto_\Corr$.
A path $\alpha$ satisfies $\Corr$, written $\alpha \vDash \Corr$, if $\alpha \in \Lang(\auto_\Corr)$.
\end{itemize}
\begin{pb}[Fixed-payoff SSE constrained existence problem]
Given a parity game (resp. $\omega$-regular game) $\Game_{\|v_0}$ and a payoff vector $\bx$, does there exist an SSE $\bsigma$ in $\Game_{\|v_0}$ such that $\mu\< \bsigma \> = \bx$ and $\< \bsigma \> \vDash \Corr$?
\end{pb}

The constrained existence problem is a more general case of the existence problem (with trivial parity coloring that goes to $0$ and single-state automaton with color $0$), and does not actually bring any additional complexity to the algorithms: from a complexity point of view, this is akin to adding an extra player; note that this player would need to be treated slightly differently as it does not count as being harmed by a deviation, and therefore we choose to treat it separately in the proofs (\ifPagesLimited{Appendix}\else{Section}\fi~\ref{sec:existenceSSE}).

Solving the constrained existence problem allows to check whether there is a potential positive answer to a protocol challenge.

\subsection{Results}

We give tight complexity bounds to all those problems, and also characterize their complexities when fixing the number of players or the number of colors (i.e. the degree of complexity of the wrongness conditions), which is in practice often small compared to the size of the game or of the automaton.
We recall that a problem is \emph{fixed-parameter tractable} ($\FPT$) when the parameter $p$ is fixed if it can be solved in time at most $O\left(f(p) P(n)\right)$, where $f: \NN \to \NN$ is some mapping, $P$ is a polynomial, and $n$ is the size of the instance.
Thus, a $\FPT$ problem is in practice polynomial, if we assume that $p$ remains small.

It is \emph{slice-wise polynomial} ($\XP$) when the parameter $p$ is fixed if it can be solved in time at most $O\left(f(p) n^{g(p)}\right)$, where $f,g: \NN \to \NN$ are some mapping, and $n$ is the size of the instance.
The class of $\XP$ problems strictly contains the $\FPT$ problems.
In between these classes lie the \emph{weft} hierarchy; while $\W[0]=\FPT$, $\W[1]$-hard problems are not thought\footnote{It is unknown whether $W[1]=\FPT$, but $W[1]\neq\FPT \Rightarrow \Poly\neq \NP$.} to be solvable with an $\FPT$ algorithm for said parameter.

These results are gathered in \tablename~\ref{tab:complexityResults}.
\ifPagesLimited
The details are omitted due to space constraints and can be found in Appendix~\ref{app:algorithms}.
\fi

Let us note in particular that all those problems are decidable in complexity at most $\ExpTime$.
Therefore, we have defined a model that is expressive enough to capture usual protocols and protocol challenges, while opening new possibilities using rationality hypotheses; and that is, simultaneously, simple enough so that the natural decision problems that arise are all decidable in a reasonable complexity, in particular when the number of agents is fixed, as in these cases most of our algorithms execute in polynomial time.

\ifPagesLimited\relax\else\input{appendixAlgorithmsBooleanSSE}\fi

\section{Conclusion}\label{sec:conclusion}

% \begin{itemize}
%     \item Multivalued games? (can we find an application for that?) \Le{Don't think so, je focusserais plutôt sur l'info imparfaite comme future work. D'ailleurs il faut qu'on explique quelque part pourquoi on se permet de regarder l'info parfaite pour l'instant.}
% \end{itemize}

In this paper, we present a game-theoretic approach to formalize fair exchange protocols under assumption of rational but possibly malicious agents. This framework is more expressive than previous frameworks for rational fairness.

We establish a strong link between our framework and concepts in game theory. More precisely, we show that the correctness conditions induced by our framework are strongly related to the concept of Strong Secure Equilibrium. This link with game theory allows us to develop efficient algorithms for the verification problems and we show that our algorithms have tractable complexity when the number of players is fixed, which is relevant in practice as the number of agents often remains small.

In future work, we plan to investigate the influence on imperfect information on the complexity of our problems and on the modeling.

\ifDraft
\label{LastPage}
\noindent\textcolor{black!60}{\dotfill Pagecount: \pageref{LastPage}\dotfill}
\fi
\newpage
% Generated by IEEEtranS.bst, version: 1.14 (2015/08/26)
\begin{thebibliography}{10}
\providecommand{\url}[1]{#1}
\csname url@samestyle\endcsname
\providecommand{\newblock}{\relax}
\providecommand{\bibinfo}[2]{#2}
\providecommand{\BIBentrySTDinterwordspacing}{\spaceskip=0pt\relax}
\providecommand{\BIBentryALTinterwordstretchfactor}{4}
\providecommand{\BIBentryALTinterwordspacing}{\spaceskip=\fontdimen2\font plus
\BIBentryALTinterwordstretchfactor\fontdimen3\font minus
\fontdimen4\font\relax}
\providecommand{\BIBforeignlanguage}[2]{{%
\expandafter\ifx\csname l@#1\endcsname\relax
\typeout{** WARNING: IEEEtranS.bst: No hyphenation pattern has been}%
\typeout{** loaded for the language `#1'. Using the pattern for}%
\typeout{** the default language instead.}%
\else
\language=\csname l@#1\endcsname
\fi
\providecommand{\BIBdecl}{\relax}
\BIBdecl

[1]
I.~Abraham, D.~Dolev, R.~Gonen, and J.~Halpern, ``Distributed computing meets
game theory: robust mechanisms for rational secret sharing and multiparty
computation,'' in \emph{Proceedings of the 25th Annual ACM Symposium on
Principles of Distributed Computing (PODC'06)}.\hskip 1em plus 0.5em minus
0.4em\relax New York, NY, USA: Association for Computing Machinery, 2006, p.

[2]
\BIBentryALTinterwordspacing
E.~{Allen Emerson} and C.-L. Lei, ``Modalities for model checking: branching
time logic strikes back,'' \emph{Science of Computer Programming}, vol.~8,
no.~3, pp. 275--306, 1987. [Online]. Available:
\url{https://www.sciencedirect.com/science/article/pii/0167642387900360}
\BIBentrySTDinterwordspacing

[3]
R.~Alur, T.~A. Henzinger, and O.~Kupferman, ``Alternating-time temporal
logic,'' \emph{J. {ACM}}, vol.~49, no.~5, pp. 672--713, 2002.

[4]
R.~J. Aumann, ``{Acceptable points in games of perfect information.}''
\emph{Pacific Journal of Mathematics}, vol.~10, no.~2, pp. 381 -- 417, 1960.

[5]
M.~Backes, O.~Ciobotaru, and A.~Krohmer, ``Ratfish: A file sharing protocol
provably secure against rational users,'' in \emph{Proceedings of the 5th
European Symposium on Research in Computer Security (ESORICS'10)},
D.~Gritzalis, B.~Preneel, and M.~Theoharidou, Eds.\hskip 1em plus 0.5em minus
0.4em\relax Berlin, Heidelberg: Springer, 9 2010, pp. 607--625.

[6]
B.~Baum-Waidner and M.~Waidner, ``Round-optimal and abuse free optimistic
multi-party contract signing,'' in \emph{Proceedings of the 27th
International Colloquium on Automata, Languages and Programming
({ICALP}'00)}.\hskip 1em plus 0.5em minus 0.4em\relax Berlin, Heidelberg:
Springer-Verlag, 2000, p. 524–535.

[7]
\BIBentryALTinterwordspacing
R.~Brenguier, ``Robust equilibria in mean-payoff games,'' in \emph{Proceedings
of the 19th International Conference on Foundations of Software Science and
Computation Structures ({FOSSACS}'16)}, ser. Lecture Notes in Computer
Science, B.~Jacobs and C.~L{\"{o}}ding, Eds., vol. 9634.\hskip 1em plus 0.5em
minus 0.4em\relax Springer, Apr. 2016, pp. 217--233. [Online]. Available:
\url{https://doi.org/10.1007/978-3-662-49630-5\_13}
\BIBentrySTDinterwordspacing

[8]
\BIBentryALTinterwordspacing
V.~Bruy{\`{e}}re, Q.~Hautem, and J.~Raskin, ``Parameterized complexity of games
with monotonically ordered omega-regular objectives,'' in \emph{29th
International Conference on Concurrency Theory, {CONCUR} 2018, September 4-7,
2018, Beijing, China}, ser. LIPIcs, S.~Schewe and L.~Zhang, Eds., vol.
118.\hskip 1em plus 0.5em minus 0.4em\relax Schloss Dagstuhl -
Leibniz-Zentrum f{\"{u}}r Informatik, 2018, pp. 29:1--29:16. [Online].
Available: \url{https://doi.org/10.4230/LIPIcs.CONCUR.2018.29}
\BIBentrySTDinterwordspacing

[9]
V.~Bruy{\`{e}}re, N.~Meunier, and J.~Raskin, ``Secure equilibria in weighted
games,'' in \emph{{CSL-LICS}}.\hskip 1em plus 0.5em minus 0.4em\relax {ACM},
2014, pp. 26:1--26:26.

[10]
L.~Butty{\'{a}}n, J.~Hubaux, and S.~Capkun, ``A formal model of rational
exchange and its application to the analysis of syverson's protocol,''
\emph{Journal of Computer Security}, vol.~12, no. 3-4, pp. 551--587, 2004.

[11]
K.~Chatterjee, T.~A. Henzinger, and M.~Jurdzi{\'{n}}ski, ``Games with secure
equilibria,'' in \emph{Formal Methods for Components and Objects}, F.~S.
de~Boer, M.~M. Bonsangue, S.~Graf, and W.-P. de~Roever, Eds.\hskip 1em plus
0.5em minus 0.4em\relax Berlin, Heidelberg: Springer Berlin Heidelberg, 2005,
pp. 141--161.

[12]
M.~R. Clarkson and F.~B. Schneider, ``Hyperproperties,'' \emph{Journal of
Computer Security}, vol.~18, no.~6, pp. 1157--1210, Sep. 2010.

[13]
\BIBentryALTinterwordspacing
H.~Comon{-}Lundh, M.~Dauchet, R.~Gilleron, C.~L{\"o}ding, F.~Jacquemard,
D.~Lugiez, S.~Tison, and M.~Tommasi, \emph{Tree Automata Techniques and
Applications}.\hskip 1em plus 0.5em minus 0.4em\relax Université de Lille,
ENS Cachan, RWTH Aachen, Université Aix-Marseille, INRIA, CNRS, Nov. 2007.
[Online]. Available:
\url{https://inria.hal.science/hal-03367725v1/file/tata.pdf}
\BIBentrySTDinterwordspacing

[14]
H.~Fernau, S.~Hoffmann, and M.~Wehar, ``Finite automata intersection
non-emptiness: Parameterized complexity revisited,'' 2021.

[15]
D.~Gale and F.~M. Stewart, ``Infinite games with perfect information,'' in
\emph{Contributions to the Theory of Games (AM-28), Volume II}, H.~W. Kuhn
and A.~W. Tucker, Eds.\hskip 1em plus 0.5em minus 0.4em\relax Princeton:
Princeton University Press, 1953, pp. 245--266.

[16]
D.~Hausmann, M.~Lehaut, and N.~Pitermann, ``Symbolic reactive synthesis for the
safety and {EL}-fragment of {LTL},'' 2023.

[17]
P.~Hunter and A.~Dawar, ``Complexity bounds for regular games,'' in
\emph{Mathematical Foundations of Computer Science 2005}, J.~J{\c
e}drzejowicz and A.~Szepietowski, Eds.\hskip 1em plus 0.5em minus 0.4em\relax
Berlin, Heidelberg: Springer Berlin Heidelberg, 2005, pp. 495--506.

[18]
D.~Kozen, ``Lower bounds for natural proof systems,'' in \emph{18th Annual
Symposium on Foundations of Computer Science ({SFCS}'77)}, 1977, pp.

[19]
\BIBentryALTinterwordspacing
S.~Kremer and J.-F. Raskin, ``A game-based verification of non-repudiation and
fair exchange protocols,'' \emph{Journal of Computer Security}, vol.~11,
no.~3, pp. 399--429, 2003. [Online]. Available:
\url{http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Kremer-gameNRextended.ps}
\BIBentrySTDinterwordspacing

[20]
T.~Latvala and K.~Heljanko, ``Coping with strong fairness,'' \emph{Fundamenta
Informaticae}, vol.~43, no. 1-4, pp. 175--193, 2000.

[21]
J.~F. Nash, ``Equilibrium points in $n$-person games,'' in \emph{PNAS},
vol.~36.\hskip 1em plus 0.5em minus 0.4em\relax National Academy of Sciences,
1950, pp. 48--49.

[22]
H.~Pagnia, F.~C. G{\"a}rtner \emph{et~al.}, ``On the impossibility of fair
exchange without a trusted third party,'' Citeseer, Tech. Rep., 1999.

[23]
A.~Pnueli, ``The temporal logic of programs,'' in \emph{Proceedings of the 18th
Annual Symposium on Foundations of Computer Science (FoCS'77)}.\hskip 1em
plus 0.5em minus 0.4em\relax IEEE Computer Society, Oct. 1977, pp. 46--57.

[24]
I.~Rakotonirina, G.~Barthe, and C.~Schneidewind, ``Decision and complexity of
{D}olev-{Y}ao hyperproperties,'' \emph{Proceedings of ACM on Programming
Languages}, vol.~8, no. POPL, Jan. 2024.

[25]
M.~Wehar, ``On the complexity of intersection non-emptiness problems,'' Ph.D.
dissertation, State Universit of New York at Buffalo, 2016.

[26]
J.~Zhou and D.~Gollmann, ``An efficient non-repudiation protocol,'' in
\emph{Proceedings of The 10th Computer Security Foundations Workshop}.\hskip
1em plus 0.5em minus 0.4em\relax IEEE Computer Society, Jun. 1997, pp.

\end{thebibliography}

\ifArxiv\appendix\else\appendices\fi
\section{Different approaches for fair exchange}\label{app:first_examples}

The naive exchange model is depicted in \figurename~\ref{fig:ongoingExampleTwoPlayers}.

\begin{figure*}[h!]
\centering
\begin{tikzpicture}[auto,node distance=4cm]
\node[abstractstate] (init) at (0,0) {$\begin{array}{rl}%
\alice:&\textit{item}_1 \\
\bob:&\textit{item}_2
\end{array}$};%$\alice:\textit{item}_1$\\$\bob:\textit{item}_2$};
\node[abstractstate] at (6,2) (aliceOwnsAll) {$\begin{array}{rl}%
\alice:&\textit{item}_1,\textit{item}_2 \\
\bob:&\emptyset
\end{array}$};
\node[abstractstate] at (6,-2) (bobOwnsAll) {$\begin{array}{rl}%
\alice:& \emptyset\\
\bob:&\textit{item}_1,\textit{item}_2
\end{array}$};
\node[abstractstate] at (12,0) (end) {$\begin{array}{rl}%
\alice:&\textit{item}_2 \\
\bob:&\textit{item}_1
\end{array}$};

\path[->,aliceMove] (init) edge node[swap,sloped] {$\alice$ sends $\textit{item}_1$} (bobOwnsAll);
\path[->,bobMove] (init) edge node[sloped] {$\bob$ sends $\textit{item}_2$} (aliceOwnsAll);
\path[->,aliceMove] (aliceOwnsAll) edge node[sloped] {$\alice$ sends $\textit{item}_1$} (end);
\path[->,bobMove] (bobOwnsAll) edge node[swap,sloped] {$\bob$ sends $\textit{item}_2$} (end);
\end{tikzpicture}
\caption{Exchange between Alice and Bob only.}
\label{fig:ongoingExampleTwoPlayers}
\end{figure*}

The exchange model with optimistic use of the TTP is given in \figurename~\ref{fig:ongoingExampleWithTTP}.

\begin{figure*}[h!]
\centering
\begin{tikzpicture}[auto,node distance=4cm]
\node[abstractstate] (init) at (1,0) {$\begin{array}{rl}%
\alice:&\textit{item}_1 \\
\bob:&\textit{item}_2
\end{array}$};%$\alice:\textit{item}_1$\\$\bob:\textit{item}_2$};
\node[abstractstate] at (5,3) (aliceOwnsAll) {$\begin{array}{rl}%
\alice:&\textit{item}_1,\textit{item}_2 \\
\bob:&\emptyset
\end{array}$};
\node[abstractstate] at (5,-3) (bobOwnsAll) {$\begin{array}{rl}%
\alice:& \emptyset\\
\bob:&\textit{item}_1,\textit{item}_2
\end{array}$};
\node[abstractstate] at (14,0) (end) {$\begin{array}{rl}%
\alice:&\textit{item}_2 \\
\bob:&\textit{item}_1
\end{array}$};
\node[abstractstate] at (12,3) (aliceOwnsAllTtpAlerted) {$\begin{array}{rl}%
\alice:&\textit{item}_1,\textit{item}_2 \\
\bob:&\emptyset \\
& \ttp \text{ alerted}
\end{array}$};
\node[abstractstate] at (12,-3) (bobOwnsAllTtpAlerted) {$\begin{array}{rl}%
\alice:& \emptyset\\
\bob:&\textit{item}_1,\textit{item}_2\\
& \ttp \text{ alerted}
\end{array}$};

\path[->,aliceMove] (init) edge node[sloped,pos=0.55] {$\alice$ sends $\textit{item}_1$} (bobOwnsAll);
\path[->,bobMove] (init) edge node[swap,sloped,pos=0.55] {$\bob$ sends $\textit{item}_2$} (aliceOwnsAll);
\path[->,aliceMove] (aliceOwnsAll) edge node[swap,sloped] {$\alice$ sends $\textit{item}_1$} (end);
\path[->,bobMove] (bobOwnsAll) edge node[sloped] {$\bob$ sends $\textit{item}_2$} (end);
\path[->,aliceMove] (bobOwnsAll) edge node[swap,sloped] {$\alice$ alerts $\ttp$} (bobOwnsAllTtpAlerted);
\path[->,bobMove] (aliceOwnsAll) edge node[sloped] {$\bob$ alerts $\ttp$} (aliceOwnsAllTtpAlerted);
\path[->,ttpMove] (aliceOwnsAllTtpAlerted) edge node[text width=2.5cm,pos=0.8] {$\ttp$ forces $\alice$ to send $\textit{item}_1$} (end);
\path[->,ttpMove] (bobOwnsAllTtpAlerted) edge node[swap,text width=2.5cm,pos=0.8] {$\ttp$ forces $\bob$ to send $\textit{item}_2$} (end);
\end{tikzpicture}
\caption{Exchange between Alice and Bob with a trusted third party.}
\label{fig:ongoingExampleWithTTP}
\end{figure*}

% \section{Exchange with an explicit infrastructure and TTP}
\label{app:ongoingExampleWithTTPandInfra}

The model of item exchange with explicit modeling of the infrastructure is depicted in \figurename~\ref{fig:ongoingExampleWithTTPandInfra}.

\begin{figure*}[hp!]
\begin{tikzpicture}[auto,node distance=4cm]
% \tikzstyle{abstractstate}+=[inner ysep=2.5pt] % Nécessaire si on ajoute une phrase dans la section
\node[abstractstate] (init) at (0,0) {$\begin{array}{rl}%
\alice:&\textit{item}_1 \\
\bob:&\textit{item}_2 \\
\II:&\emptyset
\end{array}$};
\node[abstractstate] at (0,8) (bobSent) {$\begin{array}{rl}%
\alice:&\textit{item}_1 \\
\bob:&\emptyset \\
\II:&\textit{item}_2
\end{array}$};
\node[abstractstate] at (3,5) (bobSentTtpAlerted) {$\begin{array}{rl}%
\alice:&\textit{item}_1 \\
\bob:&\emptyset \\
\II:&\textit{item}_2 \\
& \ttp \text{ alerted}
\end{array}$};
\node[abstractstate] at (7,4) (received2aliceSent) {$\begin{array}{rl}%
\alice:&\textit{item}_2 \\
\bob:&\emptyset \\
\II:&\textit{item}_1
\end{array}$};
\node[abstractstate] at (10,8) (received2aliceSentTtpAlerted) {$\begin{array}{rl}%
\alice:&\textit{item}_2 \\
\bob:&\emptyset \\
\II:&\textit{item}_1 \\
& \ttp \text{ alerted}
\end{array}$};
\node[abstractstate] at (5,10) (aliceOwnsAll) {$\begin{array}{rl}%
\alice:&\textit{item}_1,\textit{item}_2 \\
\bob:&\emptyset \\
\II:&\emptyset
\end{array}$};
\node[abstractstate] at (0,-8) (aliceSent) {$\begin{array}{rl}%
\alice:& \emptyset\\
\bob:&\textit{item}_2 \\
\II:&\textit{item}_1
\end{array}$};
\node[abstractstate] at (3,-5) (aliceSentTtpAlerted) {$\begin{array}{rl}%
\alice:& \emptyset\\
\bob:&\textit{item}_2 \\
\II:&\textit{item}_1 \\
& \ttp \text{ alerted}
\end{array}$};
\node[abstractstate] at (7,-4) (received1bobSent) {$\begin{array}{rl}%
\alice:& \emptyset\\
\bob:&\textit{item}_1 \\
\II:&\textit{item}_2
\end{array}$};
\node[abstractstate] at (10,-8) (received1bobSentTtpAlerted) {$\begin{array}{rl}%
\alice:& \emptyset\\
\bob:&\textit{item}_1 \\
\II:&\textit{item}_2 \\
& \ttp \text{ alerted}
\end{array}$};
\node[abstractstate] at (5,-10) (bobOwnsAll) {$\begin{array}{rl}%
\alice:& \emptyset\\
\bob:&\textit{item}_1,\textit{item}_2 \\
\II:&\emptyset
\end{array}$};
\node[abstractstate] at (5,0) (allSent) {$\begin{array}{rl}%
\alice:& \emptyset\\
\bob:& \emptyset\\
\II:&\textit{item}_1,\textit{item}_2
\end{array}$};
\node[abstractstate] at (14,0) (end) {$\begin{array}{rl}%
\alice:&\textit{item}_2 \\
\bob:&\textit{item}_1 \\
\II:&\emptyset
\end{array}$};
\node[abstractstate] at (13.5,4) (aliceOwnsAllTtpAlerted) {$\begin{array}{rl}%
\alice:&\textit{item}_1,\textit{item}_2 \\
\bob:&\emptyset  \\
\II:&\emptyset\\
& \ttp \text{ alerted}
\end{array}$};
\node[abstractstate] at (13.5,-4) (bobOwnsAllTtpAlerted) {$\begin{array}{rl}%
\alice:& \emptyset\\
\bob:&\textit{item}_1,\textit{item}_2 \\
\II:&\emptyset\\
& \ttp \text{ alerted}
\end{array}$};

\path[->,aliceMove] (init) edge node[swap,sloped,pos=0.4] {$\alice \xrightarrow{\textit{item}_1}$} (aliceSent);
\path[->,infraMove] (aliceSent) edge node[swap,sloped,pos=0.4] {$\xrightarrow{\textit{item}_1}\bob$} (bobOwnsAll);

\path[->,bobMove] (init) edge node[sloped,pos=0.4] {$\bob\xrightarrow{\textit{item}_2}$} (bobSent);
\path[->,infraMove] (bobSent) edge node[sloped,pos=0.4] {$\xrightarrow{\textit{item}_2}\alice$} (aliceOwnsAll);

\path[->,infraMove] (aliceSent) edge[out=70, in=-160,out distance=3cm] node[sloped,pos=0.6] {$\bob \xrightarrow{\textit{item}_2}$} (allSent);
\path[->,infraMove] (bobSent) edge[out=-70, in=160,out distance=3cm] node[swap,sloped,pos=0.6] {$\alice \xrightarrow{\textit{item}_1}$} (allSent);
\path[->,infraMove] (allSent) edge node[sloped] {$\xrightarrow{\textit{item}_1}\bob$} (received1bobSent);
\path[->,infraMove] (allSent) edge node[swap,sloped] {$\xrightarrow{\textit{item}_2}\alice$} (received2aliceSent);

\path[->,aliceMove] (aliceOwnsAll) edge node[swap,sloped] {$\alice \xrightarrow{\textit{item}_1}$} (received2aliceSent);
\path[->,infraMove] (received2aliceSent) edge node[swap,sloped,pos=0.4] {$\xrightarrow{\textit{item}_1}\bob$} (end);
\path[->,bobMove] (bobOwnsAll) edge node[sloped] {$\bob\xrightarrow{\textit{item}_2}$} (received1bobSent);
\path[->,infraMove] (received1bobSent) edge node[sloped] {$\xrightarrow{\textit{item}_2}\alice$} (end);

\path[->,aliceMove] (bobOwnsAll) edge[out=0,in=-90,out distance=6cm,in distance=4cm] node[swap,sloped] {$\alice\xrightarrow{\text{\warning}}\ttp$} (bobOwnsAllTtpAlerted);
\path[->,aliceMove] (received1bobSent) edge node[swap,sloped] {$\alice\xrightarrow{\text{\warning}}\ttp$} (received1bobSentTtpAlerted);
\path[->,aliceMove] (aliceSent) edge[out=20,in=-100] node[swap,sloped] {$\alice\xrightarrow{\text{\warning}}\ttp$} (aliceSentTtpAlerted);
\path[->,bobMove] (aliceOwnsAll) edge[out=0,in=90,out distance=6cm,in distance=4cm] node[sloped] {$\bob\xrightarrow{\text{\warning}}\ttp$} (aliceOwnsAllTtpAlerted);
\path[->,bobMove] (received2aliceSent) edge node[sloped] {$\bob\xrightarrow{\text{\warning}}\ttp$} (received2aliceSentTtpAlerted);
\path[->,bobMove] (bobSent) edge[out=-20,in=100] node[sloped] {$\bob\xrightarrow{\text{\warning}}\ttp$} (bobSentTtpAlerted);

\path[->,ttpMove] (bobOwnsAllTtpAlerted) edge node[sloped] {$\ttp$ \force$[\bob\xrightarrow{\textit{item}_2}]$} (received1bobSent);
\path[->,ttpMove] (received1bobSentTtpAlerted) edge[bend right] node[sloped] {$\ttp$ \force$[\bob\xrightarrow{\textit{item}_2}]$} (received1bobSent);
\path[->,ttpMove] (aliceSentTtpAlerted) edge node[swap,sloped] {$\ttp$ \force$[\bob\xrightarrow{\textit{item}_2}]$} (allSent);
\path[->,ttpMove] (aliceOwnsAllTtpAlerted) edge node[sloped,swap] {$\ttp$ \force$[\alice\xrightarrow{\textit{item}_1}]$} (received2aliceSent);
\path[->,ttpMove] (received2aliceSentTtpAlerted) edge[bend left] node[sloped,swap] {$\ttp$ \force$[\alice\xrightarrow{\textit{item}_1}]$} (received2aliceSent);
\path[->,ttpMove] (bobSentTtpAlerted) edge node[sloped] {$\ttp$ \force$[\alice\xrightarrow{\textit{item}_1}]$} (allSent);
\end{tikzpicture}
\caption{Exchange between $\alice$ and $\bob$ with explicit infrastructure modeling and TTP.}
\label{fig:ongoingExampleWithTTPandInfra}
\end{figure*}
\ifPagesLimited
\section{The Zhou-Gollmann optimistic protocol (details)}\label{app:ZhouGollmann}

\subsection{Transitions in the Zhou-Gollmann game}\label{app:ZhouGollmannTransitions}

\input{appZhouGollmannTransitions}

\subsection{Mealy machine for the Zhou-Gollmann protocol}\label{app:ZhouGollmannMealy}

\input{appZhouGollmannMealy}\fi

\section{Case study: Baum-Waidner Optimistic Multi-Party Contract Signing}\label{app:BaumWaidner}

In [6], the authors present a protocol for $n$ agents $\{\player_1,\dots,\player_n\}$ to sign a contract, only relying on a trusted third-party (TTP, $\ttp$) to recover from timeout (or potential cheating attempt).
The protocol is carried out over $n+1$ rounds.
In the first round, all agents send a level-1 promise of signature to all other agents to start the protocol.
All agents wait to have received all such promises to move to round $2$.
In subsequent rounds ($2$ to $n+1$), agents send level-$r$ promises as well as acknowledgment of success for level $r-1$.
Once an agent has received all level-$r$ promises and acknowledgment of success for level $r-1$, they move to round $r+1$.
A level-$r$ promise from $\player_i$ is a message signed by $i$ that contains all the acknowledgments from all agents for round $r-2$, that were received at the end of the previous round.
Note that at level $2$, the promises of level $1$ serve as acknowledgments that ``round $0$'' was successfully carried out.
The level-$n+1$ promise is considered an actual signature of the contract.

If at any point an agent suspects the protocol is not going as expected (for example if they fail to receive a message from another agent), they can contact the TTP to request a resolution at round $r$.
The resolution request must contain the promises of level $r-1$ and acknowledgments of level $r-2$ received from all the other agents: these should have been received from everyone before even moving to round $r$.
The TTP can simply abort if the level of promises in the resolution request is not high enough; this abortion can later be recovered if another agent provides a resolution request with level of promises that proof that level $r$ was actually successfully performed.
Otherwise, they produce a resolution token that will be transmitted to any subsequent agent requesting a resolution, as it acts as a proof of signature.
Any given agent is only given one chance to contact the TTP (all further requests are ignored); therefore an agent that asks for a resolution at an early stage, receiving an abort token, but still participates in the protocol would never be able to obtain a resolution token from the TTP if the protocol does not reach its normal end.

Remark that in this case the channels are assumed perfect and therefore are not part of the model: any message sent is immediately received by the intended recipient.

\subsection{Modeling of the protocol}

\subsubsection{Messages}

The possible messages of the protocol are as follows.
They all are assumed to include the necessary metadata identifying the contract being signed and the instance of the protocol.
For each agent $i,j \in \{1,\dots,n\}$ and $r\in \{1,\dots,n+1\}$, $\Promise(i,j,r)$ is the sending of signature promise of level $r$ from $\player_i$ to $\player_j$.
For each agent $i,j,r \in \{1,\dots,n\}$, $\Ack(i,j,r)$ is the sending of acknowledgment of the completion of level $r$, from $\player_i$ to $\player_j$.
The TTP can send $\Aborted(r,i)$ which is an abort token sent to $\player_i$ and $\Signed(r,i)$, a proof of the contract signature.

As the level-$r$ promise includes the acknowledgments received from other agents and is signed by the sender, $\Promise(i,j,r)$ must first be sent:
\begin{itemize}
\item by agent $\player_i$,
\item if $r>1$, for all $j\neq i$, $\Ack(j,i,r-1)$ has been sent.
\end{itemize}
The acknowledgments are signed so $\Ack(i,j,r)$ must first be sent by $\player_i$, but nothing prevents them from sending it at any time (even though it may be a bad idea).
Nothing prevents promises, acknowledgments, or a proof of signature from the TTP to be forwarded to other players:
\begin{itemize}
\item Once $\Promise(i,j,r)$ has been sent, $\player_j$ can send $\Promise(i,k,r)$ for any $k\in\{1,\dots,n\}$.
\item Once $\Ack(i,j,r)$ has been sent, $\player_j$ can send $\Ack(i,k,r)$ for any $k\in\{1,\dots,n\}$.
\item Once $\Signed(r,i)$ has been sent, $\player_i$ can send $\Signed(r,j)$ for any $j\in\{1,\dots,n\}$.
\end{itemize}

For each agent $i \in \{1,\dots,n\}$ and $r\in \{1,\dots,n+1\}$, $\Resolve(i,r)$ is the sending of resolution request to the TTP at round $r$.
It can only be sent:
\begin{itemize}
\item by agent $\player_i$,
\item if $r>2$, for all $j\neq i$, $\Ack(j,i,r-2)$ has been sent.
\item if $r>1$, for all $j\neq i$, $\Promise(j,i,r-1)$ has been sent.
\end{itemize}

Message $\Signed(r,i)$ contains information from a $\Resolve$ request at level $r$ so one must have been sent to $\ttp$ before: for $r\in\{1,\dots,n+1\}$, $\Signed(r,i)$ can be sent only by the TTP and if for some $j$, $\Resolve(j,r)$ was sent before.

The $\Signed(r,i)$ message can act for $\player_i$ as a proof of the signature of the contract by all parties.
We can therefore define, for each player $i$, the state of having a signed contract as:
\[O_{\Signed,i} \eqdef \bigwedge_{j\neq i} \Promise(j,i,n+1) \vee \Signed(r,i)\]
A correct execution of the protocol, and therefore the collaborative goal of the agents is \[\Corr=\bigwedge_i O_{\Signed,i}.\]

\subsubsection{Arena}
The game arena is composed of states $2^\actions\times\{\ttp,\player_0,\dots,\player_n\}$ where
\ifArxiv\[\begin{array}{rcl}
\actions &=&
\left\{\Promise(i,j,r) \ \middle|\  r\in \{1,\dots,n+1\}, i,j \in \{1,\dots,n\}\right\}\\&\cup&
\left\{\Ack(i,j,r) \ \middle|\  r\in \{1,\dots,n+1\}, i,j \in \{1,\dots,n\}\right\}\\&\cup&
\left\{\Resolve(i,r) \ \middle|\  r\in \{1,\dots,n+1\}, i \in \{1,\dots,n\}\right\}\\&\cup&
\left\{\Signed(r,i) \ \middle|\  r\in \{1,\dots,n+1\}, i \in \{1,\dots,n\}\right\}\\&\cup&
\left\{\Aborted(r,i) \ \middle|\  r\in \{1,\dots,n+1\}, i \in \{1,\dots,n\}\right\}
\end{array}\]
\else
$\actions$ is given in \tablename~\ref{tab:actionsBW}.
\begin{table*}
\[\begin{array}{rclcl}
\actions &=&
\left\{\Promise(i,j,r) \ \middle|\  r\in \{1,\dots,n+1\}, i,j \in \{1,\dots,n\}\right\} &\cup&
\left\{\Ack(i,j,r) \ \middle|\  r\in \{1,\dots,n+1\}, i,j \in \{1,\dots,n\}\right\}\\&\cup&
\left\{\Resolve(i,r) \ \middle|\  r\in \{1,\dots,n+1\}, i \in \{1,\dots,n\}\right\} &\cup&
\left\{\Signed(r,i) \ \middle|\  r\in \{1,\dots,n+1\}, i \in \{1,\dots,n\}\right\}\\&\cup&
\left\{\Aborted(r,i) \ \middle|\  r\in \{1,\dots,n+1\}, i \in \{1,\dots,n\}\right\}
\end{array}\]
\caption{Actions in the Baum-Weidner protocol.}
\label{tab:actionsBW}
\end{table*}
\fi
\subsubsection{Mealy machines for strategy following the protocol}

A Mealy machine $\M_i^\tau$ for the strategy of $\player_i$ that allows up to $\tau$ turns per round before starting the resolution process with the TTP can be defined as follows.
In this description, we may abusively use $\player_0$ to denote $\ttp$, in order to facilitate the round-robin nature of the game.
Machine $\M_i^\tau$ has $(n+1)\times (\tau+1)+2$ states: $(r,t)\in\{1,\dots,n+1\}\times\{0,\dots,\tau\}$, a recovery state $R$ and a stop state $s$.

From $(1,t)$, if the game is in a state $(v,\player_i)$ that satisfies $\bigwedge_{j\neq i} \Promise(j,i,1)$, then there is a transition to $(2,0)$ with output:
$$(v\cup \{\Promise(i,j,2),\Ack(i,j,1) ~|~ j\neq i\},\player_{i+1\mod n}).$$
Otherwise, if $t<\tau$ then reading $(v,\player_i)$ outputs $(v,\player_{i+1 \mod n})$ and moves to $(1,t+1)$.
From $(1,\tau)$, reading $(v,\player_i)$ that does not satisfy $\bigwedge_{j\neq i} \Promise(j,i,1)$ leads to state $R$ with output: $$(v\cup \{\Resolve(i,1)\},\player_{i+1 \mod n}).$$

From $(r,t)$ with $1<r\leq n$, if the game is in a state $(v,\player_i)$ that satisfies $\bigwedge_{j\neq i} \Promise(j,i,n) \wedge \Ack(j,i,n-1)$, then there is a transition to $(r+1,0)$ with output: $$(v\cup\{\Promise(i,j,n+1),\Ack(i,j,n) ~|~ j\neq i\}.$$
Otherwise, if $t<\tau$ then reading $(v,\player_i)$ outputs $(v,\player_{i+1 \mod n})$ and moves to $(r,t+1)$.
From $(r,\tau)$, reading $(v,\player_i)$ that does not satisfy $\bigwedge_{j\neq i} \Promise(j,i,n) \wedge \Ack(j,i,n-1)$ leads to state $R$ with output: $$(v\cup \{\Resolve(i,r)\},\player_{i+1 \mod n}).$$

From $R$, reading $(v,\player_i)$ where $v$ satisfies $\Aborted(r,i) \vee \Signed(r,i)$  from some $r$ leads to $S$.
All other values lead to $R$ with output $(v,\player_{i+1\mod n})$.
From $S$, reading $(v,\player_i)$ outputs $(v,\player_{i+1\mod n})$ and remains in $S$.

In all states, if $(v,\player_j)$ is read with $j\neq i$, the machine does not move and outputs $(v,\player_{j+1\mod n})$.

\bigskip
A Mealy machine for the TTP $\M_\ttp$ has states of the form $(c,a,s)$ where $c\subseteq \{1,\dots,n\}$ is the set of players who have contacted the TTP, $a\subseteq \{1,\dots,n\}\times\{1,\dots,n+1\}$ is the set of abort tokens having been sent, $s\in\{0,\dots,n+1\}$ indicates that a signing token has been sent at level $s$, with $0$ indicating no signing token has been sent.
From state $(c,a,0)$, if the game is in state $(v,\ttp)$ where $v$ satisfies $\Resolve(i,1)$ and $i\notin c$, the machine goes to state $(c\cup\{i\},a\cup\{(i,1)\},0)$ and outputs $(v\cup\{\Aborted(r,i)\},\player_1)$.
From state $(c,a,0)$, if the game is in state $(v,\ttp)$ where $v$ satisfies $\Resolve(i,r)$ for $r>1$, $i\notin c$
\begin{itemize}
\item if for any $(p,\ell)\in a$, $\ell<r$, the machine goes to state $(c\cup\{i\},a,r)$ and outputs $(v\cup\{\Signed(r,i)\},\player_1)$.
\item otherwise the machine goes to state $(c\cup\{i\},(a\cup\{(i,r)\},0)$ and outputs transition $(v\cup\{\Aborted(r,i)\},\player_1)$.
\end{itemize}
From state $(c,a,\rho)$, if the game is in state $(v,\ttp)$ where $v$ satisfies $\Resolve(i,r)$ for $r>1$, and $i\notin c$, then the machine goes to state $(c\cup\{i\},a,\rho)$ and outputs $(v\cup\{\Signed(\rho,i)\},\player_1)$.
All other cases of input $(v,\player_i)$ have the machine remain in the same state and output $(v,\player_{i+1\mod n})$.

\begin{comment}
\bigskip

The Mealy machines implementing this protocol are given in \figurename{}s~\ref{fig:mealyBaumWeidnerPi} for parties to the contract ($\player_1$ to $\player_n$) and~\ref{fig:mealyBaumWeidnerTTP} for the TTP.
In the machine for $\player_i$ it is assumed that all states have a $n$ self loops $\top,\player_j|\empty,\player_{j+1\mod n}$ for all $j\in \{0,\dots,i-1,i+1,\dots,n\}$ to account for other players' turn (with the slight abuse of notation that $\player_{0}$ is $\ttp$).

\begin{sidewaysfigure}
\centering
\begin{tikzpicture}[auto,node distance=10cm]
\node[state,initial] (r1) {$1$};
\node[state,right of=r1] (r2) {$2$};
\node[state,right of=r2] (r3) {$3$};
\node[below of=r3] (dots) {$\dots$};
\node[state,left of=dots,node distance=13cm] (rn) {$n$};
\node[state,left of=rn,node distance=11cm,yshift=3cm,inner sep=0pt] (rnp1) {$n+1$};

\path[mealyTrans] (r1) edge[loop above] node {\(\begin{array}{rcl}%
\top &|& \{\Promise(i,j,1) | j\neq i\}\\
\bigvee_{j\neq i} \neg\Promise(j,i,1) &|& \emptyset
\end{array}\)} (r1);
\path[mealyTrans] (r1) edge node {\(\begin{array}{rcl}%
\bigwedge_{j\neq i} \Promise(j,i,1) &|& \{\Promise(i,j,2),\Ack(i,j,1) | j\neq i\}
\end{array}\)} (r2);
\path[mealyTrans] (r2) edge[loop below] node {\(\begin{array}{rcl}%
\bigvee_{j\neq i} \neg\Promise(j,i,1)\vee\neg \Ack(j,i,1) &|& \emptyset
\end{array}\)} (r2);
\path[mealyTrans] (r2) edge node {\(\begin{array}{rcl}%
\bigwedge_{j\neq i} \Promise(j,i,2) \wedge \Ack(j,i,1) &|& \{\Promise(i,j,3),\Ack(i,j,2) | j\neq i\}
\end{array}\)} (r3);
\path[mealyTrans] (r3) edge[loop above] node[anchor=south east,xshift=1cm] {\(\begin{array}{rcl}%
\bigvee_{j\neq i} \neg\Promise(j,i,3)\vee\neg \Ack(j,i,2) &|& \emptyset
\end{array}\)} (r3);
\path[mealyTrans] (r3) edge node[anchor=south,rotate=-90] {\(\begin{array}{rcl}%
\bigwedge_{j\neq i} \Promise(j,i,3) \wedge \Ack(j,i,2) &|& \{\Promise(i,j,4),\Ack(i,j,3) | j\neq i\}
\end{array}\)} (dots);
\path[mealyTrans] (dots) edge node[swap] {\(\begin{array}{rcl}%
\bigwedge_{j\neq i} \Promise(j,i,n-1) \wedge \Ack(j,i,n-2) &|& \{\Promise(i,j,n),\Ack(i,j,n-1) | j\neq i\}
\end{array}\)} (rn);
\path[mealyTrans] (rn) edge[loop below] node {\(\begin{array}{rcl}%
\bigvee_{j\neq i} \neg\Promise(j,i,n)\vee\neg \Ack(j,i,n-1) &|& \emptyset
\end{array}\)} (r2);
\path[mealyTrans] (rn) edge node[anchor=south,sloped] {\(\begin{array}{rcl}%
\bigwedge_{j\neq i} \Promise(j,i,n) \wedge \Ack(j,i,n-1) &|& \{\Promise(i,j,n+1),\Ack(i,j,n) | j\neq i\}
\end{array}\)} (rnp1);
\path[mealyTrans] (rnp1) edge[loop above] node {\(\begin{array}{rcl}%
\top &|& \emptyset
\end{array}\)} (rnp1);
\end{tikzpicture}
\caption{Mealy machine for agent $\player_i$. States correspond to the round of the protocol the agent is currently in.}
\label{fig:mealyBaumWeidnerPi}
\end{sidewaysfigure}

\begin{figure}
\centering
\begin{tikzpicture}
% Is it worth it?
\end{tikzpicture}
\caption{Mealy machine for agent $\ttp$.}
\label{fig:mealyBaumWeidnerTTP}
\end{figure}
\bigskip
\end{comment}

\subsection{Objectives and attacks models}

In general, agents consider that they are in a bad situation if they have given their signature to another party while not having the full set of signatures.
The actual individual objectives of agents may however vary with the attack model being considered.

\subsubsection{Selfish agents}
In this model, agents are selfish and only care about the objectives informally described above.
We define:
\begin{mathpar}
%     \Ind_i \eqdef O_{\Signed,i} \wedge \bigvee_{j\neq i}\neg O_{\Signed,j}
% \and
\Wrong_i \eqdef \neg O_{\Signed,i} \wedge \bigvee_{j\neq i} \Promise(i,j,n+1)
\end{mathpar}

\subsubsection{Sacrifices for the greater ``good''}

In the original model, it is assumed that up to $n-1$ agents can be dishonest and not follow the protocol in order to cheat the last (and honest) agent.
But one can also assume that these dishonest may even be willing to sacrifice themselves by being wronged as long as one member of the group does achieve its individual objective.
In order to differentiate ``losing by sacrifice'' from ``losing by being cheated'', we introduce a $\Boast$ family of actions that allows cheaters achieving their individual objective to exclude other agents from the coalition: if he is wronged that would count as a loss, not a sacrifice.
Message $\Boast(i,j)$ is the announcement by $\player_i$ that if $\player_j$ is wronged it should not count as a sacrifice performed to help $i$.
It can be sent only by $\player_i$ at any time.

We can now define the objectives for all players:
\begin{mathpar}
%     \Ind_i \eqdef O_{\Signed,i} \wedge \bigvee_{j\neq i} \left(\Boast(i,j) \wedge\neg O_{\Signed,j} \right)
% \and
\Wrong_i \eqdef   \bigvee_{j\neq i} \left(\Boast(j,i) \wedge O_{\Signed,j}\right)  \wedge \neg O_{\Signed,i} \wedge\bigvee_{j\neq i} \Promise(i,j,n+1)
\end{mathpar}
These objective mean that to achieve an attack, an agent must have a signed contract and be able to point another agent who does not.
By being pointed (only by such an agent), and being in a bad situation of having sent its signature while not having received a signed contract, a user is wronged.
Accomplices that sacrifice themselves to allow for another agent to achieve its individual goal are not considered wronged if they were not pointed.
It allows these agents to actually participate in a dishonest coalition without officially being wronged.

\subsubsection{A ghost in the protocol}
The above approach can be generalized to include finer specifications on the way coalitions are allowed to form.
That can be achieved by using a \emph{Ghost} agent $\ghost$ whose only actions are to $\Curse$ players who, then, cannot sacrifice themselves in order to form a harmful coalition.
Agent $\ghost$ has no action besides $\Curse(i)$ for $i\in\{1,\dots,n\}$, that indicates that $\player_i$ is a potential target of an attack: if he is wronged that would count as a loss, not a sacrifice.

For example, the above case can be formalized using the following objectives for players:
\begin{mathpar}
%     \Ind_i \eqdef \bot
% \and
\Wrong_i \eqdef \Curse(i) \wedge \neg O_{\Signed,i} \wedge \bigvee_{j\neq i} \Promise(i,j,n+1)
\end{mathpar}
And for the ghost $\Wrong_\ghost \eqdef \bot$.

As it has no action (besides cursing), this can only be achieved with the help of other agents.

Also note that the above definition allows up to $n-1$ agents to team up in the attack, but finer models could also be used by modifying the ghost's wronging condition.
For example, to allow only $k$ attackers to sacrifice themselves to cheat, one could define
% \[\Ind_\ghost'=\Ind_\ghost \wedge \bigvee_{\substack{A \subseteq \{1,\dots,n\}\\|A|\geq\left\lfloor\frac{n}{2}\right\rfloor}} \bigwedge_{i \in A} \Curse(i)\]
\[\Wrong_\ghost'=\bigvee_{i \in \Pi} \Curse(i) \wedge \bigvee_{\substack{A \subseteq \{1,\dots,n\}\\|A|\geq k}} \bigwedge_{j \in A} \neg\Curse(j).\]

\iffalse
\subsection{Needham-Shroeder protocol}
The Needham-Shroeder protocol~\cite{NeedhamSchroeder78} is designed for two agents Alice ($\alice$) and Bob ($\bob$) to mutually identify themselves.
This identification is performed by each agent creating a nonce and sending it to the other, and showing to the other that they have indeed received their nonce.
As a result the current state of the protocol contains not only what information is known to the other but also what information any agent knows the other agent has.
The third agent, Charlie ($\channel$) can control the communication channel and therefore eavesdrop and intercept messages.
He cannot decode messages unless he knows the secret key.

Originally, $\alice$ knows her private key  $\textit{pr}_\alice$, her nonce $N_\alice$, and the names and public keys of all agents ($\alice$, $\bob$, $\channel$, $\textit{pu}_\alice$, $\textit{pu}_\bob$, $\textit{pu}_\channel$).
That is similar for $\bob$ and $\channel$.
In addition, $\alice$ knows that other agents know just that, even if she does not know what is the actual values of these.
For example $\alice$ has the epistemic knowledge $K_\alice$ which is a function of the other agents: $K_\alice(\bob)=\{\textit{pr}_\bob, N_\bob, \textit{pu}_\alice, \textit{pu}_\bob, \textit{pu}_\channel\}$.

All agents can send in a message anything they know, possibly encrypted with a public key.
A message encrypted with a public key can only be deciphered with the corresponding private key.
In order to limit the potential messages to a finite number, we assume that only pairs of the base messages and encryptions of these pairs.

The game is modeled as a round-robin between all three players.
At their turn, an agent can send a message to another, from anything they currently know.
A message sent by $\alice$ or $\bob$ adds its content to the knowledge of $\channel$.
Only $\channel$ actually sends messages to $\alice$ or $\bob$.
Note that is $\channel$ so chooses he can just relay messages and the rest would happen as if it was a fully reliable channel.

The protocol itself as given by~\cite{NeedhamSchroeder78} works as follows, assuming the channel is indeed perfect:
\begin{enumerate}
\item $\alice$ sends the pair $(\alice, N_\alice)$ encrypted with $\textit{pu}_\bob$ to $\bob$.
\item $\bob$ replies by sending the second component of the decrypted pair (presumably $N_\alice$) among with $N_\bob$, encrypted with $\textit{pu}_\alice$ to Alice.
\item After checking that the original nonce $N_\alice$ was indeed sent back by $\bob$, Alice encrypts the second component of what she received (presumably $N_\bob$) with $\textit{pu}_\bob$ and sends it to Bob.
\item Bob checks that $N_\bob$ was indeed received.
\end{enumerate}

The correctness hypothesis, which is the mutual identification of Alice and Bob, is a state where:
\begin{itemize}
\item Alice knows $N_\bob$.
\item Bob knows $N_\alice$.
\item Alice knows that Bob knows $N_\alice$.
\item Bob knows that Alice knows $N_\bob$.
\item No on else knows either $N_\alice$ or $N_\bob$.
\end{itemize}