In this paper, we study the problem of Atl* model checking for Bitcoin smart contracts when formalized in the BitML high-level formal language. Starting from a BitML contract specification, we show how to construct a concurrent game structure (CGS) that captures its semantics. For a significant subset of BitML, we show that, while we adopt imperfect information and perfect recall semantics, we can retain decidability by reducing our problem to model checking on a CGS with only public actions, which is known to be decidable even in this general setting. We validate our framework through practical applications, including the verification of contract liquidity properties and the strategic analysis of key smart contracts.
Distributed Ledger Technologies (DLT) such as Bitcoin [
Smart contracts, like traditional programs or protocols, are not immune to security issues. Attackers may exploit vulnerabilities in implementing contracts or publish contracts with hidden vulnerabilities to control their behavior in ways not expected by users. For example, several vulnerabilities in Ethereum smart contracts have caused the theft or the freezing of Ether or other digital assets worth millions of USD at the time: the famous attacks on The DAO [21], the Parity Multisig Wallet [22, 23, 24], the King of the Ether Throne smart contract [25] are only few notorious examples. Another important source of problems comes from coding errors or design issues that afect the behaviour of the contract at the interaction level: the participants might not be incentivized to behave honestly because they can exploit an unfair advantage with dishonest behaviour [26, 27, 28, 29]. For example, a naive design of a rock-paper-scissors game [30] allows playing sequentially rather than concurrently and gives an advantage to the second player who can see the opponent’s move. The DAO attack is an example where a coding bug incentivized dishonest behavior. See [31, 32, 33, 34, 35, 36, 37] for surveys on the matter.
To overcome the mentioned security issues, the industry and the research community have put a lot of efort into developing techniques for formally specifying and verifying smart contract correctness. A plethora of diferent model formalisms, specification languages, and verification techniques studied for traditional programs have been applied or adapted in the context of smart contracts [38, 32, 39, 40, 41]. Regarding formal verification, one of the main used technique is model checking, a well-established formal method that automatically checks for system correctness [42, 43, 44, 45]. In this framework, we represent the system into a formal model, typically a state-transition graph such as Kripke structures [46] or labelled transition systems (LTS) [47], specify the property using temporal logics such as Ltl [48], Ctl [42], or Ctl* [49], and check formally that the model satisfies the temporal logic specification.
However, in model checking, the system is assumed to be closed, i.e., a system whose behavior is completely determined by its state. In contrast, an open system interacts with multiple participants, and its behaviour depends on this interaction [50, 51]. In fact, most techniques for formally verifying smart contracts treat them as closed systems, disregarding the interaction aspect [52], but a smart contract that does not accept inputs from its participants is not realistic nor interesting. A common workaround is to fix the users’ behavior in advance to make the system closed, enabling the use of model checking. While this approach is enough for the verification of interesting properties, e.g. the (strategyless) liquidity property [53, 54], it has the major downside of potentially missing adversary strategies that could exploit security vulnerabilities. Adopting module checking [51, 55] as a verification framework for open systems would help, but at the cost of only considering two-player games between the participants’ coalition and the environment, hence limiting the expressiveness of the model and what can be reasoned about. For example, we cannot reason about strategic abilities of smart contract users, e.g. which outcome can be enforced or prevented by a single participant or a coalition of participants.
In this paper, we put forward the idea of modeling the interaction between a smart contract and its participants as a game between agents in a multi-agent system [56, 57]. In particular, starting from a Bitcoin smart contract, formalized in the high-level modelling language BitML [58], we define a BitML game as a concurrent game structure with imperfect information (iCGS) [59] that follows the BitML semantics, in the sense that there is a tight correspondence between the runs in the two formalisms. Then, for a relevant subset of BitML contracts, we study the problem of model checking alternating-time temporal logic (Atl* ) [59] specifications over BitML games. Atl* is a logic formalism that allows reasoning about agents’ strategies within a multi-agent system, by introducing path quantifiers to range over those paths that a team of agents can force the system into. Here, we adopt the setting of imperfect information, which is needed to model secret commitments, and perfect recall. While in general this setting leads to undecidability of the Atl* model checking problem [60], we show how our game structure from BitML contracts can be cast into a iCGS with only public action [61], for which our problem remains decidable. Finally, we show that several strategic properties of interest can be captured by Atl* specifications on BitML games, e.g. liquidity [54].
The rest of the paper is structured as follows: Section 2 reviews previous works related to ours; Section 3 introduces the BitML formalism; Section 4 describes our translation from BitML specification to a CGS; Section 5 defines our model checking problem and proves decidability; Section 6 discusses use cases, such as general patterns of liquidity analysis and Atl* model checking with concrete BitML smart contracts; and Section 7 concludes the paper and discusses future works.
One of the first works that used some form of strategic reasoning in the context of smart contracts was presented in [26], where the authors combined probabilistic model checking and game theory to analyze a specific protocol that also involve players (human users) with diferent/competing gaming strategies. They used game theory to analyze the protocol’s players’ behaviour, and then the resulting strategies were modelled in a probabilistic system for automated validation. TypeCoin [62] is a highlevel language for Bitcoin smart contracts that allows the modeling of the updates of a state machine as afine logic propositions. Users can “run” this machine by putting transactions on the blockchain, with the guarantee that only the legit updates can be performed. A downside is that liveness is guaranteed only by assuming cooperative participants, i.e. a dishonest participant can make the others unable to complete an execution, hence they study only a specific type of user strategies. Chatterjee et al. [ 27] defined a simplified language for loop-free smart contracts, with a compiler to Solidity. Then, they provided an automatic translation into concurrent game structures and analyzed these games employing interval abstraction demonstrated to be sound. The technique is very powerful and of practical relevance, considering that models of concurrent games are very large. The main diference is that they focus on two-player games with quantitative objectives, while Atl* can model more general temporal properties, including some quantitative property (e.g. constraints on deposits), nested games, and reason about strategic abilities of coalitions. Moreover, their framework is suited for Ethereum-like platforms, but not easily adaptable for Bitcoin smart contracts. Tsankov et al. [53] study a property called liquidity, which holds when the contract always admits a trace where its balance is decreased (so, the funds stored within the contract do not remain frozen). A major limitation is that their approach considers only cooperating adversaries, and do not handle more complex strategic reasoning. Bartoletti and Zunino [54] study the liquidity property for BitML smart contracts in an adversarial setting, including the verification of general Ltl properties. To do so, their tool [63] relies on the Maude model checker [64, 65]. Their approach allows one checking whether the smart contract satisfies the liquidity property regardless of the participants’ behaviors or if certain user strategies are fixed beforehand. While being a very useful tool, it is not able to handle branching time properties, coalitions of agents, or complex strategic interactions as one could do in Atl* . The behavior of contract users can also be partially defined in a Turing-complete process calculus scl proposed by Laneve et al. [28]. scl models behaviors of a smart contract and a user as a parallel composition, where a user acts nondeterministically, while the behavior of a smart contract is determined by its execution logic. The scl models are, in fact, transition systems that are summarized by a first-order logic formula describing the values of the objective function for all possible runs and user strategies. Then, the game-theoretical analysis is performed to identify strategies that help users maximize their profits or minimize losses. There are a few diferences with our work: (i) we use a sequential model rather than process algebra but still model the interleaving between the users; (ii) their work considers only rational strategies, while we also aim to find the outcomes of strategies in the general cases of non-cooperative or dishonest (possibly non-rational) behavior; and (iii) they only consider quantitative objectives, while we also study the case with temporal qualitative objectives. van der Meyden [29] investigated the specification and verification of an atomic swap smart contract and argued that logics with the ability to express properties of players’ strategies in a multi-agent setting, such as Atl, are conceptually useful for this purpose. The MCK model checker was used to establish the correctness and fairness of a contract under the specified user behaviors. However, this approach sufers from the issue of having to fix the user strategy to verify certain properties without letting the system automatically figure out the possible strategies. Madl et al. [ 66] capture the interaction between the users of a marketplace contract by describing their behaviors as interface automata. The authors verify the composition of the automata in a model checker to ensure that participants can successfully cooperate, but once again, the strategies of the participants are fixed in advance. Nam and Kil [ 67] propose a technique to translate an Ethereum smart contract written in a subset of the Solidity language into an input file for the MCMAS tool [ 68] and then use the tool to verify certain Atl specifications. However, their framework does not handle imperfect information, and only focus on two-player games.
In this section we briefly overview BitML [58, 69]. We assume a set of participants , ranged over by A, B, . . . , and a set of names of two kinds: , , . . . denote deposits of B, while , , . . . denote secrets . We also use , ′, to range over non-negative rational values. We write ⃗ (resp. ⃗) for a finite sequence of deposit (resp. secrets) names. We denote with A ⊆ the set of secret names usable by A, requiring that A ∩ B = ∅ if A ̸= B. To facilitate strategic reasoning, we restrict the original semantics by removing contract advertisement rules, deposit rules, and authorizations of deposit operations. Syntax. BitML is a domain-specific language and a calculus for Bitcoin smart contracts, which allows participants to exchange cryptocurrency according to pre-agreed contract rules. A BitML contract specification, denoted with {G}C , is made of two components: a contract C , that specifies the rules to transfer bitcoins (B), and contract preconditions G , that is a set of preconditions to its execution. In the following, we will use the formalization proposed in [54].
Contract preconditions have the following syntax (the deposits in a contract precondition G must be distinct): G ::= A:! @ | A:? @ | A:secret . A contract precondition G may require participants to deposit some B in the contract (either upfront or at runtime) or to commit to some secret. More in detail, A:! @ requires A to own B in a persistent deposit (or !-deposits) , and to spend it for stipulating a contract C . Instead, A:? @ only requires A to pre-authorize the spending of the volatile deposit (or ?-deposits) , which can be gathered by the contract at run-time. The precondition A:secret requires A to commit to a secret before C starts. After stipulation, A can choose whether to disclose the secret , assuming the published commitment was not fake.
Contracts are terms with the syntax C ::= ∑︁ Di contract in Figure 1, where: (i) the sum ∑︀∈ Di ∈ is over a finite set of indices ; (ii) the names ⃗ in put ⃗ & reveal ⃗ if are distinct, and they include those in . We denote the empty sum with 0.
The order of decorations is immaterial, e.g., after : A : B : D is equivalent to B : A : after : D . Intuitively, a contract C is a choice among zero or Figure 1: Syntax of BitML contracts and preconditions. more branches. Each branch is a guarded contract, which enables an action and possibly proceeds with a continuation C ′. The guarded contract withdraw A transfers the whole balance to A, while split ‖ ( → Ci ) decomposes the contract into parallel components Ci , each with balance . The guarded contract put ⃗ & reveal ⃗ if atomically performs the following: (i) spend all the ?-deposits ⃗, adding their values to the contract balance; (ii) check that all the secrets ⃗ have been revealed and satisfy the predicate . When enabled, anyone can fire the above-mentioned actions at any time. To restrict who can execute actions and when, one can use the decoration A : D , which requires the authorization of A, and the decoration after : D , which requires waiting until time . We use the syntactic sugar reveal for put [] & reveal if true.
A BitML contract specification (or contract advertisement) is a term {G }C , such that: (i) each secret name in C occurs in G ; (ii) G requires a deposit from each A in {G }C . Intuitively, {G }C is the advertisement of a contract C with preconditions G. Condition (ii) is used to guarantee that the contract is stipulated only if all the involved participants give their consent: namely, A’s consent is rendered as A’s authorization to spend one of her deposits. When all the preconditions G have been satisfied, the contract C becomes stipulated. The contract starts its execution with a balance, initially set to the sum of the !-deposits required by its preconditions. Running C will afect this balance when participants deposit/withdraw funds to/from the contract. ::= predicate true truth D ::= guarded contract | ∧ conjunction || wsiptlhidtr‖a w(A → Ci) tsrpalnitstfhere bbaallaannccee to A || ¬∘ (n∘ e∈ga{tio=n, <}) | A : D wait for A’s authorization ::= expression | after : D wait until time constant | put ⃗ & reveal ⃗ if .C collect deposits/secrets | secret | ∘ (∘ ∈ { +, −} ) Semantics. We now define the semantics of BitML. A configuration Γ is a term with the syntax: Γ ::= 0 | {G }C | ⟨C , ⟩ | ⟨A, ⟩ | A[ ] | {A : # } | A : # | (Γ | Γ ′) | (Γ | ) ::= # ◁ {G }C | ◁ {G}C | ◁ D where: (i) in a committed secret, ∈ N ∪ {⊥} (where ⊥ denotes an ill-formed commitment); (ii) in a revealed secret, ∈ N; (iii) in a configuration, there are no duplicate authorizations; (iv) in a configuration containing ⟨· · · ⟩ and ⟨· · · ⟩ , it must be ̸= ; (v) there exists at most one term . We assume that (|, 0) is a commutative monoid, and we denote indexed parallel compositions with ‖. We say that Γ is a timed configuration when it contains a term . With cn(Γ) , we denote the set of contract and ◁ D is an authorization to take branch D . names such that Γ contains ⟨C , ⟩, for some C and , and with dn(Γ) the deposit names. The intuition behind the various terms in configurations is the following: ⟨C , ⟩ is a stipulated contract storing B, uniquely identified by the name ; ⟨A, ⟩ is a deposit of B owned by A, and uniquely identified by the name ; A[ ] is A’s authorizations to perform some action ; {A : # } represents A’s commitment to a secret (with ∈ N ∪ {⊥}), identified by ; A : # represents a secret (with ∈ N), identified by , and revealed by A. Regarding authorizations: # ◁ {G }C authorizes to commit secrets to stipulate {G }C ; ◁ {G }C authorizes to spend the !-deposit to stipulate {G }C ; The semantics of a BitML contract specification is a labelled transition system (LTS) between timed ℳ configurations. A LTS is a triple
= (, Λ , ) where is a set of states, Λ is a set of labels, and : × Λ
→ is the (deterministic) labelled transition function. We say there is a transition from state to state with label ℓ if (, ℓ) = . A run ℛ is a (possibly infinite) sequence Γ 0 | 0 →− where ℓ are the transition labels, Γ 0 is an initial configuration, and 0 = 0. If ℛ is finite, we write Γ ℛ for its last untimed configuration, and ℛ for its last time. We write ℛ→− ℛ ′ when ℛ′ extends ℛ ℓ ℓ0 Γ 1 | 1 →− · · · ℓ1 ℛ→− ℓ Γ ℛ′ | ℛ′ . We write ℛ → * ℛ′ to say that there exists a sequence of with the transition Γ ℛ | transitions such that ℛ
Below, we introduce the BitML semantics, formally defined in Figure 2. Labels represent the actions performed by participants. A dec′ can extend ℛ
.
in the label means oration A : · · · that the action can be performed only by A, while its absence means that it can be performed by anyone.
Note that labels are not instrumental to defining the
BitML semantics.
Yet, they are essential in the gametheoretic formalization of a BitML contract since we need to associate actions with the participants who can perform them.
Secret commitment.
late an advertised contract, all the participants mentioned in it must fulfill the preconditions by making available the required deposits and committing to the required secrets.
These steps are formalized by rule [C-AuthCommit], where the term {A : # } represents A’s commitment to the secret , while A[# ◁ {G }C ] represents finalising the commitment phase for A. The rule preconditions ensures that the final configuration fulfills the conditions required by G . Note that condition (iii) in the ∆ = ‖=1{A : #} 1 · · · secrets of A in G ∀ ∈ 1.. : ∄ : {A : #} ∈ Γ ∀ ∈ 1.. : ∄ : A : # in Γ ∀ ∈ 1.. : ∈ N ∪ {⊥} Γ →−− A:Δ Γ | ∆ | A[# ◁ {G}C ] [C-AuthCommit] ∆ = G = (︀ ‖∈ A:! @ )︀ | ︀( ‖∈ B:? ′ @ )︀ ︀( ‖∈ ⟨A, ⟩ | ︀) ︀( ‖∈ A[ ◁ {G}C ])︀ | | ︀( ‖∈ C[# ◁ {G}C ])︀ ︀( ‖∈ C : secret )︀ fresh ∆ | Γ →−− in⟨it C , ∑︀∈ ⟩ | Γ
fresh ⟨withdraw A, →⟩−−− − |⟨−− Γ− − − −
withdraw(A,,) A, ⟩ | Γ = ∑︀=1 = ( · )/
1 · · · fresh ⟨split‖=1 ( → Ci) , ⟩ | →−− Γ − − split() (︀ ‖=1 ⟨Ci, ⟩︀) | Γ [C-Withdraw]
[C-Split] ̸=⊥ {A : #} | Γ →−−
A: A : # | Γ [C-AuthRev]
[C-Init] [C-PutRev] definition of configurations ensures that rule
[C-AuthCommit] cannot be used more than once to generate the same authorization. The same is true for all the other rules that generate authorizations. Initialization. Once all the needed authorizations have been granted, the advertisement can be turned into an active contract. Rule [C-Init] consumes the deposits and the authorizations, and it initializes the new contract, with a fresh name , and with a balance corresponding to the sum of all the consumed ⃗ = 1 · · ·
Γ = ‖=1 ⟨A, ⟩ ⃗ = 1 · · · ∆ = ‖=1 B : #
fresh
JKΔ = true ⟨put ⃗ & reveal ⃗ if .C , ⟩ | Γ | ∆ | →−Γ− − −′−⟨− put(⃗,⃗,)
C , + ∑︀=1 ⟩ | Γ ′ | ∆ JtrueKΔ = true
J1 ∧ 2KΔ = J1KΔ and J2KΔ
J¬KΔ = not JKΔ JKΔ = if Γ contains A : #
J1 ∙ 2KΔ = J1KΔ ∙ J2KΔ
(∙ ∈ { +, −} ) JKΔ = J1 ∘ 2KΔ = J1KΔ ∘ J2KΔ
(∘ ∈ { =, <})
D ≡ A : D′ ⟨A : D + C , ⟩ →−|−− Γ− ⟨−− −
A:(,A : D) A : D + C , ⟩ | A[ ◁ A : D] | Γ [C-AuthBranch] ⟨D′, ⟩ | Γ→− ℓ Γ ′ D = A1 : · · · : A : after 1 : · · · : after : D′
D′ ̸≡ A : · · · ∈/ cn(Γ ′) ≥ 1, . . . ,
D′ ̸≡ after ′ : · · · ⟨D + C , ⟩ | (︀ ‖=1 A[ ◁ D])︀ | Γ | →− ℓ Γ ′ |
[C-Branch] > 0 Γ | →− Γ | +
[C-Delay] deposits. Note that the part ∆ of the configuration contains all the terms that are consumed by the step. The next rules define the behaviour of a contract after stipulation.
Withdraw. Executing withdraw A terminates the contract and transfer its balance to A. After the contract is terminated, a fresh deposit of B owned by A is created. This is defined by rule [C-Withdraw]. The case where the action withdraw A has an alternative branch is handled by rule [C-Branch] below. Split. The split primitive divides the contract balance in parts, each one controlled by its own contract. The general rule is [C-Split]. Note that the weights in the split do not represent actual B values, but the proportion w.r.t. the contract balance.
Revealing secrets. Any participant can reveal one of her secrets, using the rule [C-AuthRev]. The premise ̸= ⊥ is needed to avoid the case where a participant does not know the secret she has committed to. Indeed, at the level of Bitcoin, commitments are represented as cryptographic hashes of bitstrings, and revealing a secret amounts to broadcasting a preimage, i.e. a value whose hash is equal to the committed value. If a participant commits to a random value, then with overwhelming probability she will not be able to provide a preimage. The label A : represents the fact that only A, the participant who performed the commitment, can fire the transition.
Put-Reveal. The prefix put ⃗ & reveal ⃗ if can be fired with rule [C-PutRev] if all the deposits ⃗ are available, all the committed secrets ⃗ have been revealed, and satisfy the guard , where JKΔ is the evaluation of predicate in configuration ∆ .
Authorizing branches. With rule [C-AuthBranch], a branch A : D can be taken only provided that A has granted her authorization.
Reducing branches. Once all the authorizations for a branch occur in the configuration, anyone can trigger the transition with rule [C-Branch], provided that the time constraints (if any) are respected. Delaying. In any configuration, we allow time to advance with rule [C-Delay].
In this paper, we consider the LTS ℳ{G}C , associated with a contract specification {G }C , with only the participants occurring in G and as initial timed configuration Γ 0 | 0 (with 0 = 0) the set of persistent deposits and volatile deposits occurring in G held by their respective participants, as well as the authorizations A[ ◁ {G }C ] to spend the persistent deposits. While the original semantics of BitML included the possibility of fresh contract advertisement and manipulation of deposits, here we strip out it by leaving only the needed elements to reason on a single BitML contract. These simplifications rule out some interesting participants’ behaviors that were possible in the original semantics, e.g., advertising a new contract or destroying the deposits to prevent specific contract branch executions. Due to space limitations, we preferred to focus on the core features of a BitML contract and the main strategic reasoning tasks we can perform.
In this section, we are interested in defining a game structure that models the interaction between participants of a BitML smart contract. Given a set of elements, let ∈ ∪ + denote an infinite or non-empty finite sequence on . Then, we write for its ( + 1)-th element, i.e., = 01 . . . , and || for its length, with || = ∞ for ∈ . The first element of is denoted by first(), and its last by last (). We write ≥ for its sufix +1 . . . starting in , and ≤ for its prefix 0 . . . . The empty sequence is denoted by . For a vector ∈ Π , we denote its -th element by (). Games and strategies. A concurrent game structure with imperfect information (iCGS) [59] is a tuple = ⟨St, AP, Ag, {Act}∈Ag, , , , {∼ }∈Ag⟩ where: (i) St is a finite non-empty set of states; (ii) AP is a finite non-empty set of atomic propositions; (iii) Ag is a finite non-empty set of agents ( = |Ag|); Act is a set of actions of agent ∈ Ag, and with every state and agent we associate a subset Act() ⊆ Act of actions that can perform at ; (iv) ∈ St is the set of initial states; (iv) : St → 2AP is a labelling function; (v) For each state ∈ St and each joint action ∈ Jact() = ∏︀∈Ag Act(), we define the state (, ) ∈ St that results from state if every player chooses move , with called transition function; (vi) for each agent ∈ Ag, ∼ ⊆ St × St is an equivalence relation called indistinguishability relation.
Intuitively, the game starts in an initial state ∈ , and in any state each agent chooses an action ∈ Act(), and the game proceeds to state ′ = (, ), where ∈ Jact() stands for the joint action allowed in state , and () = is the action of agent in . For each state ∈ St, () is the finite set of atomic propositions that hold in , and for ∈ Ag, ∼ is an equivalence relation that represents the observation of agent : for two states , ′ ∈ St, ∼ ′ means that agent cannot tell the diference between and ′. We say that ′ is a successor of , with , ′ ∈ St, if there exists a joint action such that (, ) = ′. A run ∈ St is an infinite sequence = 012 · · · ∈ St such that 0 ∈ and for every integer ≥ 0, +1 is a successor of . The set of runs is denoted by Runs. A history ℎ ∈ St+ is a finite sequence ℎ = 012 . . . such that 0 ∈ and for 0 ≤ < , +1 is a successor of 0. The set of histories is denoted by Hist. Each indistinguishability relation is thus extended to runs and as follows: ≈ ′ if ∼ ′ for every ≥ 0. Similarly, for ℎ, ℎ′ ∈ Hist, ℎ ≈ ℎ′ if |ℎ| = |ℎ′| and ∼ ′ for every 0 ≤ < |ℎ|. A fairness constraint is a criterion to distinguish between fair and unfair runs. Here, we use unconditional fairness constraints, defined as a subset of states fc ∈ 2St, as in [70]. A run is fair according to a set of fairness conditions FC = {fc1, . . . , fc} if for each fairness condition fc , there exist infinitely many positions such that () ∈ fc .
A (perfect recall or memoryful) strategy for agent in a iCGS is a function : Hist → Act such that for all histories ℎ, (last (ℎ)) ∈ Act(last (ℎ)), and for all histories ℎ, ℎ′, (ℎ) = (ℎ′) whenever ℎ ≈ ℎ′. The latter constraint captures the essence of imperfect information: agents can base their strategic choices only on the information available to them. For ⊆ Ag and ∈ {, }, let : → Σ () denote a joint strategy associating a memoryful strategy with each agent ∈ . For ℎ ∈ Hist and a joint strategy , we write Out(ℎ, ), called the outcomes of from ℎ, for the set of runs ∈ Runs such that is consistent with ℎ and . That is, ∈ Out(ℎ, ) if (i) ℎ is a prefix of ; (ii) for every ≥ | ℎ| − 1, there exists a joint action ∈ Jact such that +1 = ( , ) and for every ∈ , () = ()( ≤ ). Moreover, we define Out(ℎ, ) = ⋃︀ℎ≈ ℎ′ Out(ℎ′, ), where ∼ = ⋃︀∈ ∼ and ≈ = ⋃︀∈ ≈ , which represents the set of outcomes under subjective semantics [71] and the “everybody knows” type of collective knowledge [72].
From BitML Contracts to Game Structures. To enable strategic reasoning on BitML smart contracts, in this section, we show how to compute a iCGS {G}C , starting from a BitML contract specification {G }C . The game structure {G}C will be designed so that the plays generated in {G}C have a corresponding run in the LTS ℳ{G}C , and vice-versa. This will enable the application of multi-agent strategic reasoning techniques based on the formal model of game structures, which resembles the BitML semantics. Note that because agents can commit to arbitrary secret strings and can advance the current time (a natural number) for an arbitrary time delay [54], ℳ{G}C has an infinite state space and infinite label space, and so the game structure {G}C , hence hindering the feasibility of reasoning techniques. In the next section, we show how to abstract the secret commitments and the time representation to make the state and action spaces finite.
Before presenting the formal definition, we explain our design choices for {G}C . (a) Firstly, we have to depart from a concurrent formalization and instead focus on a turn-based game since the inference rules of the BitML semantics (except the [C-Delay] rule) are associated with actions to be performed by a single agent. This is also reflected in the instantaneous nature of these actions, similar to many timed process calculi [73]. Hence, we can rule out agent actions that happen simultaneously with others. (b) Secondly, the interaction between the agents must be asynchronous, meaning that, from the perspective of a single agent, there is some nondeterminism that determines whose turn it is. We can rely on a turn-based asynchronous game structure by introducing a fair scheduler agent that decides which agent plays at each step (e.g. see [59, 74]), and all the other agents are forced to play the null action . Multi-agent systems with asynchronous execution, often formalized as interleaved interpreted systems (IIS) [72], are a well-known setting in the verification of multi-agent systems [ 44, 59, 75, 76, 77]. (c) Thirdly, some mechanisms in the game structure must guarantee that the adversary cannot prevent the execution of the contract unless the contract itself permits this. More precisely, we want to rule out the cases in which, during the initialization phase, some agents never commit to secrets via [C-AuthCommit], nor anyone initializes the contract via [C-Init]. This is required to focus on the analysis of the contract rather than the participants’ decision to participate in it. (d) Finally, we require that the progress of time is agreed upon by all participants, and that there is a fairness constraint that guarantees that eventually the time moves forward. This is crucial to comply with the assumption that participants can always meet deadlines if they want to.
Thus, we define the game structure {G}C as follows: ∙ St is the set of tuples ⟨Γ , , Aux ⟩, i.e. the set of all timed configurations reachable from Γ 0 | 0 in ℳ{G}C , plus a set of auxiliary predicates Aux for defining the fairness constraints. We define Conf() = Γ , Time() = , and Aux() = Aux . The (unique) initial state is = ⟨Γ 0, 0, ∅⟩. ∙ Ag = ∪{Sch}, where is the set of participants and Sch is the scheduler agent; ∙ Act: if ∈ , then for each rule of the BitML semantics, except [C-Delay], we have a corresponding action, e.g.: action “A : {A : 1#1}, . . . , {A : #}” from [C-AuthCommit], init from [C-Init]; withdraw (A, , ) from [C-Withdraw], and so on. To allow agents to progress the time synchronously, we include a new action, doneA, meaning that agent A agrees to progress the time by one unit. The efect of this action is to set the auxiliary proposition DoneA to true in the next state. If DoneA ∈ Aux(), we say that participant A ready to progress the time (or delay the time) in state , and we denote with the term Ready() the set of agents that have ready to delay the time in . Each agent also has the action , with no efect on the current state. If instead = Sch, we have an action for each agent in plus the action delay that increases the current time by one unit. In a state , if Ready() = , then the only enabled action is delay ; otherwise, the set of available actions is ∖ Ready(), i.e., the scheduler can assign the turn to an agent that is not ready yet to progress the time. ∙ The set of proposition AP captures relevant features of the game states. The actual choice for AP and will depend on the specification to be verified. Some examples will be discussed in the next sections. ∙ Being {G}C a turn-based asynchronous game, the transition function is defined according to the construction in [59]. In particular, for all states ∈ St and all joint actions 1, 2 ∈ Jact(), if 1(Sch) = 2(Sch) = and 1() = 2(), then (, 1) = (, 2). The efects of the auxiliary actions have been specified above, and the ones from the BitML semantics are specified by the inference rules. ∙ The indistinguishability relations ∼ , one for each participant ∈ , captures partial observability on the value of the secrets of the other participants ∖ {}. In other words, ∼ is such that states where other agents have committed to diferent secrets are all indistinguishable from ’s point of view. ∙ We add further auxiliary propositions in order to define our desired fairness constraints: (i) during the stipulation phase, each participant must eventually execute the action corresponding to [C-AuthCommit]; (ii) after that, some participants must eventually execute the init action to initialize the contract; (iii) the scheduler is fair, i.e., it does not neglect an agent forever; (iv) each participant is eventually ready to progress the time. We could define a fairness constraint for each action involved by adding auxiliary propositions in the Aux component of states, e.g., AuthCommitA to keep track of whether A has committed to secrets in the past, Initialized to keep track of whether the contract has been initialized, ActedA that holds in the current state if A was the last agent scheduled by Sch, and DoneA (already defined above) to keep track whether A has taken action doneA since the most recent time delay, and Delayed if the last action of Sch was delay . Given these auxiliary propositions, defining a fairness constraint for each requirement above is straightforward.
We observe that such construction complies with the abovementioned design choices (a), (b), (c) and (d). Also, the time progression machinery is not needed if there are no timeouts in the contracts. Moreover, note that we make an implicit assumption, often made in model checking cryptographic protocols, that is called "perfect cryptography". This assumption implies that the probability of adversaries discovering the secret value through brute force is zero [29].
Correspondence between the semantics. We show that each trajectory, i.e., sequence of state and actions = 0, 0, 1, 1, . . . compatible with in the game structure {G}C , has a corresponding run ℛ of the LTS ℳ{G}C , in the sense that and ℛ visit the same configurations by doing analogous transitions (modulo auxiliary propositions and synchronization actions). The correspondence also {G}C . Then, ℛ = () is a run of ℳ{G}C . holds in the other direction: given a run ℛ
, we can construct a trajectory in {G}C where the configurations and the actions in
ℛ occur in the same order. We give further definitions to formalize ℓ such correspondence before formally proving the result. We inductively define a transformation from trajectories = 0, 1, 1, . . . of {G}C to runs ℛ of ℳ{G}C , denoted with : for 0 = 0, where 0 = = ⟨Γ 0, 0, Aux 0⟩, we have (0) = Γ 0 | 0. Let = 0, 1, . . . , , be a generic sequence in {G}C of length , and ℛ = () be its associated run on ℳ{G}C . Consider a valid extension of , i.e. +1 = , +1, +1 such that (, +1) = +1. In case (Sch) = delay , then (+1) = ℛ→− 1 Γ +1 | +1, be the extension of ℛ after applying rule [C-Delay] with delay 1, with Γ +1 = Γ and +1 = + 1. Otherwise, in case (Sch) = A for some A ∈ that has not yet ready to progress the time in : (i) if (A) is one of or doneA, then (+1) = (); (ii) otherwise, is the configuration obtained after taking action +1(A) in state , and +1 = . (+1) = ℛ→−
Γ +1 | +1, where ℓ is the label corresponding to +1(A) in the LTS ℳ{G}C , Γ +1 Theorem 1. Let {G }C be a BitML contract specification. Let = 0, 1, 1, . . . be a trajectory on Proof sketch. The claim can be proved by the definition of , by the construction of {G}C , and by induction on the length of the trajectory. The idea is that auxiliary actions in , e.g., and doneA are trimmed out by , while the other actions are all translated in ℛ into legal moves of ℳ{G}C . Moreover, each run ℛ of the LTS ℳ{G}C has a corresponding trajectory in {G}C : Theorem 2. Let {G }C be a BitML contract specification. Let ℛ = Γ 0 | 0 →− be a run of ℳ{G}C . There exist a trajectory = 0, 1, 1, . . . , of {G}C such that () = ℛ. Proof sketch. The claim can be proved by the definition of , by the construction of {G}C , and by induction on the length of the run ℛ. Intuitively, has the same actions as ℛ, but whenever there is a time delay of , all the agents synchronize for rounds to increment the current time of units. ℓ1 Γ 1 | 1 →− · · · ℓ2 →− ℓ Γ |
In this section, we propose a unifying framework based on Atl* model checking, in which BitML game structures {G}C can be verified against
Alternating-time Temporal Logic. First, we introduce Alternating-time Temporal Logic (Atl* ) [59, 78], a well-known and popular logic formalism for modeling and verifying multi-agent systems. The temporal logic Atl* is defined with respect to a finite set of propositions
Ag = {1, . . . , } of players. The syntax of Atl* is given by the grammar ::= | ¬ | ∧ | ⎷ A⌄ ::= | ¬ | ∧ | ○ | where ∈ AP and ⊆
Ag. The temporal operators are ○ (“next”) and (“until”). The strategy quantifier is ⎷ ⌄ , meaning “the agents in A can enforce ”. The logic Atl* is similar to the branching-time temporal logic Ctl* [42], only that path quantifiers are parameterized by sets of players. Sometimes we defined from
¬ and ∧ in the usual manner. Moreover, we define “sometime in the future” as ♢ ≡ ⊤ write ⎷ a1, . . . , ⌄ instead of ⎷ {1, . . . , }⌄ , and ⎷⌄ instead of ⎷ ∅⌄ . Additional Boolean connectives are and “always in the future” as □ ≡ ¬ ♢ ¬ . formulas and are called state and path formulas of Atl* , respectively. State formulas constitute the language of Atl* . By imposing that temporal operators are immediately preceded by a strategic operator, we obtain the logic fragment Atl.
Since Alur et al.’s seminal paper, several diferent semantics of Atl* have been proposed. For instance, agents may be able to observe the full state of the system or only parts of it (perfect vs. imperfect information), and they may base their decisions on the current state only, or on the entire history of the game (perfect vs. imperfect recall) [79, 80, 81]. Moreover, agents can have objective or subjective ability to achieve their goals [71], their behavior can be subject to fairness constraints [59, 70], or they can be endowed with a mechanism for broadcasting information within a team [82, 83]. Another concern is how collective knowledge of a coalition is interpreted [72]. The most used variants are: agents with mutual knowledge (also known as “everybody knows” [79], where agents aggregate uncertainty), agents with distributed knowledge (where agents aggregate certainty), and agents with common knowledge (where agents aggregate uncertainty, plus uncertainty about uncertainty etc.).
In this paper, we assume (i) perfect recall, (ii) imperfect information with subjective semantics, and (iii) mutual knowledge as collective knowledge relation. We use the so-called truly perfect recall semantics [81, 61]. We simultaneously define, by induction on the formulas, (, ℎ) |= where ℎ ∈ Hist and is a history formula, and (, , ) |= where ∈ Runs, ≥ 0, and is a path formula: ∙ (, ℎ) |= if ∈ (last (ℎ)), for ∈ AP; ∙ (, ℎ) |= ⎷ A⌄ if ∃ ∈ Σ () such that, ∀ ∈ Out(ℎ, ), we have (, , |ℎ| − 1) |= ∙ (, , ) |= if (, ≤ ) |= for a state formula; ∙ (, , ) |= ○ if (, , + 1) |= ; ∙ (, , ) |= 1 2 if ∃. ≥ such that (, , ) |= 2 and ∀. ≤ < we have (, , ) |= 1. Boolean operators are omitted. For a state formula we say that |= if (, ⟨ ⟩) |= for all ∈ . Atl* Model Checking of BitML Games. In the following, we study the problem of model checking an Atl* specification over BitML games. First, observe that {G}C allows for uninteresting outcomes, such as an unfair scheduler, the time never progresses, or the contract is never initialized. To rule out unfair runs (see requirements (b), (c) and (d)), we include a set of fairness constraints in of the form □♢ , one for each possible value of , namely AuthCommitA, ActedA, DoneA for all A ∈ , and Delayed. Let Fair be the conjunction of these constraints, and let |= be defined as |= if |= ⎷ ⌄ (Fair → ). Also, we introduce a suitable set of propositions AP{G}C , and its associated labeling functions {G}C , for {G}C , to provide the alphabet for constructing the Atl* specifications: ∙ initializedC : this proposition is false in every initial state, and it is set to true by action init . Intuitively, initializedC keeps track of whether the contract C has been initialized or not in the current game. ∙ committed (with ∈ ): this type of proposition holds in a state if, after contract initialization, there exists a commitment for secret in Conf(): {A : # } ∈ Conf(), for some ∈ N ∪ ⊥. ∙ revealed (with ∈ ): this proposition holds in a state if secret has been revealed in Conf(). ∙ liquidatedC : the proposition liquidatedC holds whenever there are no contract names, descendant from C , in the current state , i.e. liquidatedC ≡ initializedC ∧ (cn(Conf()) = ∅). Intuitively, since in BitML active contracts always store some funds, this is equivalent to checking that funds deposited in the contract at initialization time have been withdrawn, so there are no frozen funds. The presence of the initializedC is needed to rule out the case in which C has not been initialized yet. ∙ “total-depositsA ∘ ” (where ∘ ∈ { =, <}): this proposition holds in a state if the sum of deposits available to A in Conf() satisfies the condition ∘ against the value , where total-depositsA = ∑︀⟨A,′⟩∈Conf() ′ is the sum of the values of all deposits controlled by A. ∙ expired: this proposition holds in a state if Time() ≥ , meaning that the timeout has expired. The term must occur in some after-clause in C .
According to the smart contract and the Atl specification of interest, there might be other choices of atomic propositions. We designed these propositions based on the criterion that they should capture generic properties of contract execution. Finally, we define the problem of Atl* model checking a specification against a BitML {G}C as the problem of determining whether {G}C |= . Game Abstraction. The main limitation in solving our model checking problem is that {G}C has an infinite state space and an infinite action space. The source of the infiniteness of the state space and the action space comes from (i) the commitment of secrets of arbitrary value, and (ii) the unboundedness of time. Therefore, naively adopting an of-the-shelf Atl* model checking algorithm (see, e.g., [59]) for solving our problem will not work since the termination is guaranteed only when the state space is ifnite. In this section, analogous to the abstract semantics of the BitML semantics introduced in [54], we introduce an abstraction for the (concrete) game {G}C , denoted with {♯G}C , which reduces the state/action space to a finite one, while guaranteeing correctness of Atl* model checking.
To cope with (i), we make the following simplifying assumption: Assumption 1. All the clauses put ⃗ & reveal ⃗ if in BitML contract C are such that = true.
♯ Assumption 1 simplifies the design of {G}C by only considering whether participants have committed to secrets and, if so, whether they are willing to reveal them. In particular, the secret commitment component {A : # }, with ∈ N∪{⊥}, is replaced with an abstract secret commitment {A : # ♯}, with ♯ ∈ {⊤, ⊥}, and ⊤ denoting any valid secret value. The secret commitment action is changed accordingly. While being a restrictive assumption, since it limits the expressivity of the BitML language, it heavily simplifies the treatment and the analysis of the correctness. We will try to relax this assumption in a future work. To address (ii), we redefine the transition rules to prevent the progression of time after all the timeouts in C , if any, have expired. Formally, let ticks(C ) be the set of all timeouts occurring in expressions of the form after : D in contract C , and let max the largest of such timeouts. Then, in {♯G}C , we impose that if Time() = max, the action delay from does not increase the time. Note that we can also simplify the time progression machinery whenever this condition is triggered, but it is ♯ inconsequential to the correctness of the abstraction. Intuitively, {G}C is the same as {G}C except that the participants can only decide whether they want to commit to a secret or not, and that time ♯ cannot increase indefinitely. It is easy to see that, {G}C is a sound and complete abstraction: under the assumption on put-reveal-if-clauses, the actual value of a valid secret does not matter for the execution of the contract, and the evaluation of propositions in AP{G}C , do not depend on time after Time() > max; hence, the construction of {♯G}C does not afect the truth of the Atl* specification. ♯ Theorem 3. Under Assumption 1 and choice of propositions AP{G}C , {G}C |= if {G}C |= .
♯ Note that a diferent choice of propositions for {G}C does not guarantee the validity of Theorem 3, e.g., propositions that check arbitrary conditions on secret values.
Despite Atl* model checking under imperfect information and perfect recall is undecidable in general ♯ [60], it can be shown that {G}C can be cast into a game structure with only public actions [61], for which model checking against Atl* specifications is decidable. Such games satisfy the condition that if ̸= ′ and ∼ ′ then (, ) ̸∼ (′, ′). Although all actions must be public, we can still model private update of an agent’s private state [84]. Formally, we define {G}C as {♯G}C with the following ♯,PA diferences: (i) PA contains (at most) 2|| initial states, one for each possible abstract assignment (⊥ or ⊤) of each secret; (ii) the commitment action is replaced by toggleA, which must be called exactly once; it can either leave a secret value unchanged or change it, e.g., from ⊤ to ⊥ or vice versa; (iii) the state
PA (′, ′), if ∼ ′ and = ′, for (, ), (′, ′) ∈ StPA. records the last joint action; (iv) (, ) ∼ Lemma 4. Under Assumption 1 and choice of propositions AP{G}C , {♯G}C |= if {G}C |= . ♯,PA Proof sketch. Given a strategy for one of the two games, we can compute a strategy for the other game such that, after contract initialization, the secrets of the protagonist coalitions are set to the same values in both games. Moreover, note that in both evaluations, all the possible assignments of the adversaries are considered: in one case because |= if ∀ ∈ .(, ) |= , while in the other because we use subjective semantics and mutual knowledge as collective knowledge relation.
Theorem 5 Under Assumption 1 and choice of propositions AP{G}C , {G}C |= is decidable. Proof. First, we determine whether {♯,GPA}C |= , which is decidable (see Thm. 1 in [61]); then, the result for {G}C |= follows by applying Lemma 4 and Theorem 3.
We conjecture that the problem is decidable also without Assumption 1: intuitively, since the contract is finite, there are a finite number of predicates in put-reveal-if-clauses, meaning that there are only finitely many sets of relevant decisions that the participants can make on secret commitments.
Liquidity [53, 54, 85] is an important security property of smart contracts. Generally speaking, a liquidity analysis of a smart contract aims to determine whether its balance can be decreased or funds remain frozen and under which conditions these scenarios happen. The notion of liquidity is based upon liquidability; here, we use the variant formalized in [85]. Informally, a BitML contract is liquidable by A if, at any point during its execution, A can perform a sequence of transitions eventually leading to a configuration containing no contract names originating from . A contract is liquid in a configuration Γ when, after an arbitrary sequence of moves performed by any participant, the contract names originated by are liquidable by A. In our framework, it can be shown that a BitML contract C is liquid in Γ 0 if {G}C |= ⎷ ⌄ □ ((⋀︀∈A committed(⊤)) → ⎷ A⌄ ♢ liquidatedC ). The constraints of the form committed( ♯), meaning that there exists an abstract commitment ♯ for secret in the current configuration, are required because in the original setup of [ 85] A must be a “honest” participant who always generates valid commitments to her secrets. There are other variants of liquidity [54] that can be formalized in Atl* : ∙ Multiparty liquidity. Instead of a single agent A, we can consider a set ⊆ of collaborative participants [53]. In the Atl* specification, it is enough to replace A with a coalition of participants . ∙ Liquidity under a strategy. We can allow A to follow a specific strategy since the start of the game. This means the original Atl* liquidity specification can be simplified in ⎷ A⌄ ♢ liquidatedC . ∙ Liquidity under assumptions. We can constrain participants’ behavior by working at the specification level. For example, to verify liquidity under the requirement that A always performs the reveal of a secret ∈ A, we can write: ⎷ ⌄ □ (revealed → ⎷ A⌄ liquidatedC ). ∙ Quantitative liquidity. In some cases, A could accept that a portion of the funds remain frozen, e.g. when these funds would be assigned to other participants. We define a contract -liquid for A if a strategy exists for A to withdraw at least bitcoins: ⎷ A⌄ □ (initializedC → ⎷ A⌄ ♢ “total-depositsA ≥ ”).
Our framework can express more general strategic specifications. For example, in a mutual timed commitment contract [54], A and B have to exchange their secrets or pay a 1B penalty. Consider the following BitML contract that specifies the mutual timed commitment (with < ′): reveal .(reveal .split(1B → withdraw A | 1B → withdraw B) + after ′: withdraw A) + after : withdraw B We can check some strategic invariants, e.g. if the secret is not valid, A cannot recover her funds: ⎷ ⌄ □ ((committed(⊥) → ¬⎷ A⌄ ♢ “total-depositsA > 0”); or that, if timeout has expired and secret has not been revealed, then B can recover his funds plus A’s penalty without revealing its secret : ⎷ ⌄ □ ((¬revealed ∧ committed(⊥) ∧ expired) → ⎷ B⌄ ♢ (¬revealed ∧ “total-depositsB = 2”)).
Let us consider the following escrow contract Escrow between two participants A and B, where the precondition requires A to deposit 1B [54]:
Escrow = A : withdraw B + B : withdraw A + A : Resolve + B : Resolve
Resolve = split(0.1B → withdraw M | 0.9B → M : withdraw A + M : withdraw B) After the contract has been stipulated, A can choose to pay B, by authorizing the first branch. Similarly, B can allow A to take her money back, by authorizing the second branch. If they do not agree, any of them can invoke a mediator M to resolve the dispute, invoking a Resolve branch. There, the 1B deposit is split in two parts: 0.1B go to the mediator, while 0.9B are assigned either to A and B, depending on M’s choice. We have that {G}C ̸|= ⎷ A⌄ ♢ liquidatedEscrow , for any ∈ , but {G}C |= ⎷ P ⌄ ♢ liquidatedEscrow for ⊆ with | | ≥ 2, i.e. with at least two cooperative participants, the contract is liquid.
Our technique makes it possible to reason about several strategic abilities of participants of a Bitcoin smart contract under a unifying framework based on Atl* model checking. Indeed, as we have shown, interesting variants of contract liquidity proposed in the literature can be captured by Atl* specifications. Moreover, as we have seen with the mutual time commitment and the escrow contracts, more general strategic interaction can be captured. We proved that the model checking problem for BitML contracts, under reasonable assumptions, is decidable even in the case of perfect recall and imperfect information semantics. There are several future research directions. First, we would like to extend our approach to the analysis of rational players [86] and to quantitative objectives [87, 88, 89]. Then, it would be interesting to analyze the impact of diferent collective knowledge relations (mutual, common, and distributed knowledge) by considering some form of communication mechanisms [83] or information sharing (e.g. via resolution operators [90]). Moreover, we would like to devise a solution method for general BitML contracts (i.e. without Assumption 1) and provide a tool that solves our problem, relying on state-of-the-art tools such as MCMAS [68], or STV [91] with support for asynchronous models [76, 77, 92]. [17] J. Poon, T. Dryja, The bitcoin lightning network: Scalable of-chain instant payments (2016).
https://lightning.network/lightning-network-paper.pdf. [18] W. Banasik, S. Dziembowski, D. Malinowski, Eficient zero-knowledge contingent payments in cryptocurrencies without scripts, in: ESORICS (2), volume 9879 of Lecture Notes in Computer Science, Springer, 2016, pp. 261–280. [19] M. Andrychowicz, S. Dziembowski, D. Malinowski, L. Mazurek, Secure multiparty computations on bitcoin, Commun. ACM 59 (2016) 76–84. [20] R. Kumaresan, I. Bentov, How to use bitcoin to incentivize correct computations, in: CCS, ACM, 2014, pp. 30–41. [21] D. Siegel, Understanding The DAO Attack, 2016. URL: https://www.coindesk.com/learn/ understanding-the-dao-attack/. [22] L. Breidenbach, P. Daian, A. Juels, E. Sirer, An In-Depth Look at the Parity Multisig Bug, ???? URL: https://hackingdistributed.com/2017/07/22/deep-dive-parity-bug/. [23] P. Technologies, A postmortem on the parity multi-sig library self-destruct (2017). URL: https://web.archive.org/web/20231106123811/https://www.parity.io/blog/ a-postmortem-on-the-parity-multi-sig-library-self-destruct/. [24] K. Nelaturu, A. Mavridou, A. G. Veneris, A. Laszka, Verified development and deployment of multiple interacting smart contracts with verisolid, in: IEEE ICBC, IEEE, 2020, pp. 1–9. [25] King of ether throne post-mortem investigation, 2016. URL: https://www.kingoftheether.com/ postmortem.html, https://www.kingoftheether.com/postmortem.html. [26] G. Bigi, A. Bracciali, G. Meacci, E. Tuosto, Validation of decentralised smart contracts through game theory and formal methods, in: Programming Languages with Applications to Biology and Security, volume 9465 of Lecture Notes in Computer Science, Springer, 2015, pp. 142–161. [27] K. Chatterjee, A. K. Goharshady, Y. Velner, Quantitative analysis of smart contracts, in: ESOP, volume 10801 of Lecture Notes in Computer Science, Springer, 2018, pp. 739–767. [28] C. Laneve, C. S. Coen, A. Veschetti, On the prediction of smart contracts’ behaviours, in: From Software Engineering to Formal Methods and Tools, and Back, volume 11865 of Lecture Notes in Computer Science, Springer, 2019, pp. 397–415. [29] R. van der Meyden, On the specification and verification of atomic swap smart contracts (extended abstract), in: IEEE ICBC, IEEE, 2019, pp. 176–179. [30] K. Delmolino, M. Arnett, A. E. Kosba, A. Miller, E. Shi, Step by step towards creating a safe smart contract: Lessons and insights from a cryptocurrency lab, in: Financial Cryptography Workshops, volume 9604 of Lecture Notes in Computer Science, Springer, 2016, pp. 79–94. [31] N. Atzei, M. Bartoletti, T. Cimoli, A survey of attacks on ethereum smart contracts (sok), in: POST, volume 10204 of Lecture Notes in Computer Science, Springer, 2017, pp. 164–186. [32] A. Miller, Z. Cai, S. Jha, Smart contracts and opportunities for formal methods, in: ISoLA (4), volume 11247 of Lecture Notes in Computer Science, Springer, 2018, pp. 280–299. [33] S. Badruddoja, R. Dantu, Y. He, K. Upadhyay, M. A. Thompson, Making smart contracts smarter, in: IEEE ICBC, IEEE, 2021, pp. 1–3. [34] R. Feichtinger, R. Fritsch, L. Heimbach, Y. Vonlanthen, R. Wattenhofer, Sok: Attacks on daos, in:
The 4th Workshop on Decentralized Finance (DeFi), 2024. [35] A. Groce, J. Feist, G. Grieco, M. Colburn, What are the actual flaws in important smart contracts (and how can we find them)?, in: Financial Cryptography, volume 12059 of Lecture Notes in Computer Science, Springer, 2020, pp. 634–653. [36] A. Mense, M. Flatscher, Security vulnerabilities in ethereum smart contracts, in: iiWAS, ACM, 2018, pp. 375–380. [37] S. Sayeed, H. Marco-Gisbert, T. Caira, Smart contract: Attacks and protections, IEEE Access 8 (2020) 24416–24427. [38] D. Harz, W. J. Knottenbelt, Towards safer smart contracts: A survey of languages and verification methods, CoRR abs/1809.09805 (2018). [39] A. Singh, R. M. Parizi, Q. Zhang, K. R. Choo, A. Dehghantanha, Blockchain smart contracts formalization: Approaches and challenges to address vulnerabilities, Comput. Secur. 88 (2020). [40] P. Tolmach, Y. Li, S. Lin, Y. Liu, Z. Li, A survey of smart contract formal specification and verification, ACM Comput. Surv. 54 (2022) 148:1–148:38. [41] R. B. Fekih, M. Lahami, M. Jmaiel, S. Bradai, Formal verification of smart contracts based on model checking: An overview, in: WETICE, IEEE, 2023, pp. 1–6. [42] E. M. Clarke, E. A. Emerson, Design and synthesis of synchronization skeletons using branchingtime temporal logic, in: Logic of Programs, volume 131 of Lecture Notes in Computer Science, Springer, 1981, pp. 52–71. [43] J. P. Queille, J. Sifakis, Specification and verification of concurrent systems in cesar, in: M. DezaniCiancaglini, U. Montanari (Eds.), International Symposium on Programming, Springer Berlin Heidelberg, Berlin, Heidelberg, 1982, pp. 337–351. [44] E. M. Clarke, O. Grumberg, D. A. Peled, Model checking, 1st Edition, MIT Press, 2001. [45] C. Baier, J. Katoen, Principles of model checking, MIT Press, 2008. [46] S. Kripke, Semantical considerations on modal logic, Acta Philosophica Fennica 16 (1963) 83–94. [47] R. M. Keller, Formal verification of parallel programs, Commun. ACM 19 (1976) 371–384. [48] A. Pnueli, The temporal logic of programs, in: FOCS, IEEE Computer Society, 1977, pp. 46–57. [49] E. A. Emerson, J. Y. Halpern, "sometimes" and "not never" revisited: on branching versus linear time temporal logic, J. ACM 33 (1986) 151–178. [50] D. Harel, A. Pnueli, On the development of reactive systems, in: Logics and Models of Concurrent
Systems, volume 13 of NATO ASI Series, Springer, 1984, pp. 477–498. [51] O. Kupferman, M. Y. Vardi, P. Wolper, Module checking, Inf. Comput. 164 (2001) 322–344. [52] M. Bartoletti, Smart contracts contracts, Frontiers Blockchain 3 (2020) 27. [53] P. Tsankov, A. M. Dan, D. Drachsler-Cohen, A. Gervais, F. Bünzli, M. T. Vechev, Securify: Practical security analysis of smart contracts, in: CCS, ACM, 2018, pp. 67–82. [54] M. Bartoletti, R. Zunino, Verifying liquidity of bitcoin contracts, in: POST, volume 11426 of Lecture
Notes in Computer Science, Springer, 2019, pp. 222–247. [55] W. Jamroga, A. Murano, Module checking of strategic ability, in: AAMAS, ACM, 2015, pp. 227–235. [56] Y. Shoham, K. Leyton-Brown, Multiagent Systems - Algorithmic, Game-Theoretic, and Logical
Foundations, Cambridge University Press, 2009. [57] M. J. Wooldridge, An Introduction to MultiAgent Systems, Second Edition, Wiley, 2009. [58] M. Bartoletti, R. Zunino, Bitml: A calculus for bitcoin smart contracts, in: CCS, ACM, 2018, pp.
83–100. [59] R. Alur, T. A. Henzinger, O. Kupferman, Alternating-time temporal logic, J. ACM 49 (2002) 672–713. [60] C. Dima, F. L. Tiplea, Model-checking ATL under imperfect information and perfect recall semantics is undecidable, CoRR abs/1102.4225 (2011). [61] F. Belardinelli, A. Lomuscio, A. Murano, S. Rubin, Verification of multi-agent systems with imperfect information and public actions, in: AAMAS, ACM, 2017, pp. 1268–1276. [62] K. Crary, M. J. Sullivan, Peer-to-peer afine commitment using bitcoin, in: PLDI, ACM, 2015, pp.
479–488. [63] N. Atzei, M. Bartoletti, S. Lande, N. Yoshida, R. Zunino, Developing secure bitcoin contracts with bitml, in: ESEC/SIGSOFT FSE, ACM, 2019, pp. 1124–1128. [64] M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer, J. F. Quesada, Maude: specification and programming in rewriting logic, Theor. Comput. Sci. 285 (2002) 187–243. [65] S. Eker, J. Meseguer, A. Sridharanarayanan, The maude LTL model checker, in: WRLA, volume 71 of Electronic Notes in Theoretical Computer Science, Elsevier, 2002, pp. 162–187. [66] G. Madl, L. A. D. Bathen, G. H. Flores, D. Jadav, Formal verification of smart contracts using interface automata, in: Blockchain, IEEE, 2019, pp. 556–563. [67] W. Nam, H. Kil, Formal verification of blockchain smart contracts via ATL model checking, IEEE
Access 10 (2022) 8151–8162. [68] A. Lomuscio, H. Qu, F. Raimondi, MCMAS: an open-source model checker for the verification of multi-agent systems, Int. J. Softw. Tools Technol. Transf. 19 (2017) 9–30. [69] M. Bartoletti, T. Cimoli, R. Zunino, Fun with bitcoin smart contracts, in: ISoLA (4), volume 11247 of Lecture Notes in Computer Science, Springer, 2018, pp. 432–449. [70] S. Busard, C. Pecheur, H. Qu, F. Raimondi, Reasoning about memoryless strategies under partial observability and unconditional fairness constraints, Inf. Comput. 242 (2015) 128–156. [71] N. Bulling, W. Jamroga, Comparing variants of strategic ability: how uncertainty and memory influence general properties of games, Auton. Agents Multi Agent Syst. 28 (2014) 474–518. [72] R. Fagin, J. Y. Halpern, Y. Moses, M. Y. Vardi, Reasoning About Knowledge, MIT Press, 1995. [73] X. Nicollin, J. Sifakis, An overview and synthesis on timed process algebras, in: CAV, volume 575 of Lecture Notes in Computer Science, Springer, 1991, pp. 376–398. [74] A. Meski, W. Penczek, M. Szreter, B. Wozna-Szczesniak, A. Zbrzezny, Bdd-versus sat-based bounded model checking for the existential fragment of linear temporal logic with knowledge: algorithms and their performance, Auton. Agents Multi Agent Syst. 28 (2014) 558–604. [75] A. Lomuscio, W. Penczek, H. Qu, Partial order reductions for model checking temporal-epistemic logics over interleaved multi-agent systems, Fundam. Informaticae 101 (2010) 71–90. [76] W. Jamroga, W. Penczek, T. Sidoruk, P. Dembinski, A. W. Mazurkiewicz, Towards partial order reductions for strategic ability, J. Artif. Intell. Res. 68 (2020) 817–850. [77] W. Jamroga, W. Penczek, T. Sidoruk, Strategic abilities of asynchronous agents: Semantic side efects and how to tame them, in: KR, 2021, pp. 368–378. [78] F. Laroussinie, N. Markey, G. Oreiby, On the expressiveness and complexity of ATL, Log. Methods
Comput. Sci. 4 (2008). [79] P. Schobbens, Alternating-time logic with imperfect recall, in: LCMAS, volume 85 of Electronic
Notes in Theoretical Computer Science, Elsevier, 2003, pp. 82–93. [80] W. Jamroga, W. van der Hoek, Agents that know how to play, Fundam. Informaticae 63 (2004) 185–219. [81] N. Bulling, W. Jamroga, M. Popovici, Reasoning about strategic abilities: Agents with truly perfect recall, ACM Trans. Comput. Log. 20 (2019) 10:1–10:46. [82] D. P. Guelev, C. Dima, Model-checking strategic ability and knowledge of the past of communicating coalitions, in: DALT, volume 5397 of Lecture Notes in Computer Science, Springer, 2008, pp. 75–90. [83] C. Dima, C. Enea, D. P. Guelev, Model-checking an alternating-time temporal logic with knowledge, imperfect information, perfect recall and communicating coalitions, in: GANDALF, volume 25 of EPTCS, 2010, pp. 103–117. [84] F. Belardinelli, A. Lomuscio, A. Murano, S. Rubin, Verification of multi-agent systems with public actions against strategy logic, Artif. Intell. 285 (2020) 103302. [85] M. Bartoletti, S. Lande, M. Murgia, R. Zunino, Verifying liquidity of recursive bitcoin contracts,
Log. Methods Comput. Sci. 18 (2022). [86] A. Abate, J. Gutierrez, L. Hammond, P. Harrenstein, M. Kwiatkowska, M. Najib, G. Perelli, T. Steeples, M. J. Wooldridge, Rational verification: game-theoretic verification of multi-agent systems, Appl. Intell. 51 (2021) 6569–6584. [87] N. Bulling, V. Goranko, Combining quantitative and qualitative reasoning in concurrent multiplayer games, Auton. Agents Multi Agent Syst. 36 (2022) 2. [88] P. Bouyer, O. Kupferman, N. Markey, B. Maubert, A. Murano, G. Perelli, Reasoning about quality and fuzziness of strategic behaviors, ACM Trans. Comput. Log. 24 (2023) 21:1–21:38. [89] W. Jamroga, M. Mittelmann, A. Murano, G. Perelli, Playing quantitative games against an authority: On the module checking problem, in: AAMAS, International Foundation for Autonomous Agents and Multiagent Systems / ACM, 2024, pp. 926–934. [90] T. Ågotnes, Y. N. Wáng, Resolving distributed knowledge, Artif. Intell. 252 (2017) 1–21. [91] D. Kurpiewski, W. Jamroga, M. Knapik, STV: model checking for strategies under imperfect information, in: AAMAS, International Foundation for Autonomous Agents and Multiagent Systems, 2019, pp. 2372–2374. [92] D. Kurpiewski, W. Pazderski, W. Jamroga, Y. Kim, Stv+reductions: Towards practical verification of strategic ability using model reductions, in: AAMAS, ACM, 2021, pp. 1770–1772.