Itsaka Rakotonirina
email: itsakarakotonirina@mpi-sp.org

Gilles Barthe
email: gillesbarthe@mpi-sp.org

Decision and Complexity of Dolev-Yao Hyperproperties (Technical Report)

Keywords: CCS Concepts:, Security and privacy → Logic and verification, Formal security models, • Theory of computation → Cryptographic protocols hyperproperties, security protocols, computational complexity

The formal analysis of cryptographic protocols traditionally focuses on trace and equivalence properties, for which decision procedures in the symbolic (or Dolev-Yao, or DY) model are known. However, many relevant security properties are expressed as DY hyperproperties that involve quantifications over both execution paths and attacker computations (which are constrained by the attacker's knowledge in the underlying model of computation). DY hyperproperties generalise hyperproperties, for which many decision procedures exist, to the setting of DY models. Unfortunately, the subtle interactions between both forms of quantifications have been an obstacle to lifting decision procedures from hyperproperties to DY hyperproperties.

The central contribution of the paper is the first procedure for deciding DY hyperproperties, in the usual setting where the number of protocol sessions is bounded and where the equational theory modelling cryptography is subterm-convergent. We prove that our decision procedure can decide the validity of any hyperproperty in which quantifications over messages are guarded and quantifications over attacker computations are limited to expressing the attacker's knowledge. We also establish the complexity of the decision problem for several important fragments of the hyperlogic. Further, we illustrate the techniques and scope of our contributions through examples of related hyperproperties.

INTRODUCTION

Cryptographic protocols are interactive distributed algorithms designed to achieve a set of security goals in the presence of active adversaries. These protocols are the cornerstone of computer security: they are widely deployed to support authentication and secure communications and emerging applications such as blockchains. They are however complex and error-prone, and hence a prime target for formal verification. In fact, there is already a large body of work developing foundations and practical tools for their analysis, see e.g. [START_REF] Blanchet | Security protocol verification: Symbolic and computational models[END_REF]].

The common substrate of many of these works is the symbolic model of cryptography, rooted in the seminal work of Dolev and Yao [Dolev and Yao 1983]. Its crux is an adversary that can observe protocol executions, carry arbitrary computations from the values learned during observation, and intercept, tamper, or forge messages exchanged across the network. The adversary is embedded into the model by means of an adversarial semantics of protocols, which can then be used as a basis to prove that these protocols achieve a security property for all possible behaviours of adversaries and coalitions of dishonest participants. Traditional security properties are trace properties that are defined as universal quantifications over execution (traces) w.r.t. the semantics, possibly relying on an epistemic temporal logic featuring a modality K for the adversary's knowledge. Surprisingly, despite general undecidability results, their verification for all adversaries is decidable under reasonable restrictions on cryptographic protocols and on the properties. Existing mature tools typically focus on trace properties for the most part [START_REF] Armando | The AVANTSSAR platform for the automated validation of trust and security of service-oriented architectures[END_REF][START_REF] Basin | Tamarin prover manual[END_REF][START_REF] Blanchet | Automatic Cryptographic Protocol Verifier, User Manual and Tutorial[END_REF]]. Still, not all security properties of interest fall into this class.

In a classic setting [START_REF] Alpern | Defining Liveness[END_REF], (trace) properties are defined as sets of traces. As such, they are special instances of hyperproperties, which are defined as properties of the set of traces itself-that is, they are sets of sets of traces [Clarkson and Schneider 2010]. Hyperproperties provide a rich setting for modelling and reasoning about systems because, in short, they display the additional ability to express relations between several executions of a protocol. This is an important ingredient to formalise, typically, strong notions of information leakage or simulability predicates. Notably, the specification and verification of hyperproperties can be achieved through hyperlogics, such as HyperCTL* [Clarkson et al. 2014], which extends CTL* with quantifiers over execution traces. Decidability and complexity of the model-checking and synthesis problems for such hyperlogics have been studied extensively [Clarkson et al. 2014;Coenen et al. 2019;Finkbeiner et al. 2015;Hsu et al. 2023;Mascle and Zimmermann 2019]. However, these results are not applicable to symbolic models of cryptography, as they do not consider adversarial semantics. Meanwhile, tools operating in the symbolic model still do not handle such hyperproperties beyond some fixed notions of process equivalences [START_REF] Basin | Tamarin prover manual[END_REF][START_REF] Blanchet | Automatic Cryptographic Protocol Verifier, User Manual and Tutorial[END_REF]Cheval et al. 2020b].

In a recent work, [START_REF] Barthe | Tidy: Symbolic Verification of Timed Cryptographic Protocols[END_REF]] introduces Hypertidy CTL*, a temporal logic for modelling and reasoning about hyperproperties in (timed) symbolic models of cryptography. Hypertidy CTL* extends HyperCTL* with clauses to reason about, and quantify over, adversarial computations. Unlike HyperCTL* where the model checking of arbitrary hyperproperties is decidable [Clarkson et al. 2014], the presence of the adversary makes the problem undecidable in general in Hypertidy CTL*. Currently, there is no decision procedure for any non-trivial fragment of this logic beyond trace properties, nor even incomplete methods that could serve as the basis of a future automated tool.

Contributions

The main contribution of this paper is a decision procedure for hyperproperties in a symbolic model of protocols including real-time and a global state. We see this as a first theoretical foundation of DY hyperproperty analysis, in the same way as the development of now-mature symbolic tools benefited from a large amount of more theoretical work on decidability and complexity [START_REF] Cheval | Deciding equivalence-based properties using constraint solving[END_REF][Cheval et al. , 2018;;Durgin et al. 2004;Kanovich et al. 2014;[START_REF] Rusinowitch | Protocol insecurity with a finite number of sessions, composed keys is NP-complete[END_REF]. Our procedure takes as input a hyperproperty 𝜑 and a model of the cryptographic protocol 𝑃, and decides whether the hyperproperty holds for all adversaries interacting with 𝑃. Our decision procedure makes two requirements, described below.

First, we require that the hyperproperty 𝜑 is a formula of a fragment of Hypertidy CTL* whose quantifications over adversarial computations are restricted to model the adversary's knowledge. Alternatively, this fragment can be seen as an extension of HyperCTL* with adversarial executions, real-time, predicates to reason about global states, and a standard epistemic knowledge operator K. Similarly to HyperCTL*, this allows unrestricted quantifications over execution paths. Additionally, we require that quantifiers over messages are guarded, i.e., should only be used to make reference to terms appearing in the protocol-and not to express arbitrary first-order formulae. These assumptions are classic in verification tools for trace properties [START_REF] Basin | Tamarin prover manual[END_REF], although notably excluding cryptographic notions of indistinguishability properties [START_REF] Barthe | Tidy: Symbolic Verification of Timed Cryptographic Protocols[END_REF]Cheval et al. 2018]. While this is a serious restriction of our decision procedure, we contend that it delineates the focus of our technical investigation to the interactions between adversarial computations and trace quantifications, which require specific treatment.

Second, we require that the protocol 𝑃 is written in the bounded fragment of (a timed and stateful variant of) the applied 𝜋-calculus [START_REF] Abadi | The Applied Pi Calculus: Mobile Values, New Names, and Secure Communication[END_REF], and that the equational theory used to model cryptography is subterm-convergent. Both assumptions are very common, and are adopted by many decision procedures [START_REF] Cheval | Deciding equivalence-based properties using constraint solving[END_REF][Cheval et al. , 2018;;[START_REF] Rusinowitch | Protocol insecurity with a finite number of sessions, composed keys is NP-complete[END_REF]. In particular, the boundedness assumption imposes an explicit bound on the number of protocol sessions of 𝑃, but the potential interactions with the adversary remain unbounded. It is justified by theoretical reasons (because verification is generally undecidable for arbitrarily many sessions), and by practical reasons (because most security flaws of concrete protocols can be exhibited with a few sessions). Technically, the assumption ensures that protocol executions are bounded in depth, which is the main reason why we can express the validity of 𝑃 |= 𝜑 as a finite set of hyperconstraints, a core notion that we introduce. As a complement, the use of destructor subterm convergent rewriting systems to model cryptography is used to decide adversarial knowledge, i.e., whether a term can be deduced by the adversary at some point in a protocol execution. It encompasses many primitives such as hash functions, encryption, signatures, or zero-knowledge proofs [START_REF] Abadi | Deciding knowledge in security protocols under equational theories[END_REF].

Technical Developments. At a technical level, getting inspiration from other decision procedures for bounded processes in different contexts [START_REF] Cheval | Deciding equivalence-based properties using constraint solving[END_REF][Cheval et al. , 2018;;Liu and Lin 2012], our own approach consists of two interleaving components:

(1) constraint generation: we extract a set C of hyperconstraints from the decision problem 𝑃 |= 𝜑;

(2) constraint solving: we establish the existence of solutions for the constraints of C.

The main challenge and technical innovation lies in the fact that, unlike any related work in this context, the interaction between path quantifications and adversarial computations requires carefully updating the constraints of C whenever a new path quantifier is handled. We deal with these updates by manipulating a stack of hyperconstraints, each stack level representing a different path quantifier. The effect of solving the constraints of the most recent level 𝑛 of the stack is thus propagated to previous levels 𝑖 < 𝑛, typically in the case where the path at level 𝑛 imposes constraints on some adversarial computations introduced at level 𝑖. We establish the soundness and completeness of our constraint generation, and show that the generated constraint set satisfies a small model property, i.e., it has a solution iff it has a solution of size smaller than some 𝑘. Here 𝑘 can be computed effectively and is exponential in the parameters of the problem (𝑃 and 𝜑 among others). Making the link between the extracted constraints and the actual statement 𝑃 |= 𝜑, this naturally translates into a decision procedure whose complexity ranges over the exponential hierarchy of complexity (EXPH(poly)). This complexity bound is tight, as the verification problem for even stricter fragments of the logic are already known to be EXPH(poly) hard [START_REF] Barthe | Tidy: Symbolic Verification of Timed Cryptographic Protocols[END_REF]].

Additional Contributions. A second contribution of the paper is an extensive study of various fragments and extensions of the framework. On the one hand, we provide exact complexity bounds for several fragments of the logic: we target selected equational theories (e.g., empty or limited to one free symbol), and several sub-fragments (e.g., tidy LTL or Hypertidy LTL). This highlights the impact on complexity of the different parameters of the problem, and we hence argue that it contributes to a better theoretical understanding of hyperproperty verification. On the other hand, we establish undecidability for several generalisations of our main theorem, thus illustrating the minimality of our assumptions. A summary of our results can be found in Figure 9 later in the paper, when all necessary notions are introduced (end of Section 4.3). We recall that our results are restricted to a fragment not supporting cryptographic notions of equivalence, and thus leave the case of the full Hypertidy CTL* logic open. We return to this open problem in the conclusion.

In addition to our technical contributions, we detail several case studies of interest of our procedure. They model various (hyper)properties of interest including notions of fairness, simulation, reentrancy freedom, as well as some correctness properties involving several trace quantifications. Although some of these notions have already been studied in the literature, our contribution is the ability to model these properties in scenarios involving coalitions of fully dishonest participants and an active adversary controlling communications. Most of such proofs cannot be handled or supported by any existing approach, highlighting the theoretical interest of our contributions.

MOTIVATING EXAMPLE: FAIR REWARD

To give a general idea of the expressivity of our model and of the scope of our contributions, we first present a prototypical example of a Dolev-Yao hyperproperty, in the context of distributed programs running on top of a blockchain-based cryptocurrency (so-called smart contracts). It will be used throughout the paper as an example support for our technical definitions.

Blockchain and Smart Contract

At a high-level, blockchain-based cryptocurrencies enable networks of mistrusting users to reach a consensus on the execution of financial transactions. A joint transaction log (the blockchain) is gradually extended by ordering authenticated transactions into blocks. However, transactions do not only authorize direct asset transfers but also advanced asset redistribution logics (smart contracts). Users trigger the contract's behaviour by posting a transaction with the call details; it is then executed once this transaction is appended (published) to the blockchain. Notably, between a transaction's submission and its publication, it already constitutes public information-and other transactions leveraging this information may be scheduled in this time window. reduc verify ( sign (x ,y , z ) ,x , pk ( z )) -> ok . formula hyp_publish ( pi : trace ) = G (∀x: bitstring . Publish ( x ) pi = > (G not Publish ( x ) pi ) /\ verify (x. sig ,x. data , x . sender ) = ok ) formula hyp_submit ( pi : trace ) = ∀x: bitstring . F Submit ( x ) pi = > (F Publish (x) pi ) \/ verify (x. sig ,x. data , x . sender ) ≠ ok

Fig. 1. Simple blockchain model

We axiomatise a simplified blockchain in Figure 1. The submissions and publications of transactions tx are represented by events Submit(tx) and Publish(tx), mentioned in the blockchain's properties (formula). These are trace properties, that is, they refer to events happening in a single trace pi, as indicated by the subscripts pi on events. Here, transactions are tuples tx = ((tx.sender,tx.func,tx.args),tx.sig) storing, resp., the public key of the sender, the name of the contract function to invoke, its arguments, and the signature of the transaction's data tx.data = (tx.sender,tx.func,tx.args). Signatures are modelled by a set of uninterpreted symbols pk(skey) (public key) and sign(msg,rnd,skey) (randomised signature), and a rewriting rule (reduc) defining verification. The two formula then formalise the (trace) properties of our simplified blockchain, namely that transactions should be signed and only appended once (hyp_publish), and that well-signed submissions are eventually published (hyp_submit). For hyp_submit, publication may either precede the submission-thus invalidating it due to hyp_publish-or follow it. The two formula notably use the (strict) temporal operators F ("finally") and its dual G ("globally"). In real-time contexts, they intuitively read as "in the strict future, it eventually (resp. always) holds that... ". The axiomatization therefore captures that valid transactions are guaranteed to be published eventually, but not necessarily in the order of their submission.

Fair Reward Contracts

We now describe a smart contract, Puzzle, implementing a simple hash puzzle letting a user who knows the preimage of a specific hash value puzzle = h(sol) claim a (monetary) prize. A user 𝐴 can claim the prize by submitting a transaction invoking a function of the contract (that we call solve) with sol as the argument. Upon inclusion of such a transaction to the blockchain, the contract checks whether sol is the expected preimage, in which case it transfers the prize funds to the sender. Figure 2 describes a blockchain where Puzzle is deployed, prize referring to the numeric prize value. It is written in our framework's calculus, using a more readable programminglike syntax with an intuitive interpretation (detailed in Appendix B for completeness). In line with the terminology of Figure 1, this process therefore receives transactions as inputs tx from the network, and appends them to the blockchain (event Publish, which is notably constrained by the properties of Figure 1). When tx contains a call to the solve function, the process also executes it accordingly. let d = ( pk ( sk ), solve , sol ) in let tx = (d , sign (d , rand (0) , sk )) in out ( tx ): Submit ( tx )

Fig. 3. Honest user submitting to Puzzle

A user 𝐴 submitting a solution sol to this contract is therefore described by the process of Figure 3. We use in particular the previous Submit event and sign signature function. The randomness of the signature is handled by a symbol rand, modelling a (deterministic) pseudo-random generator, called a private function symbol in our framework, passed here with an arbitrary seed 0. Unfortunately, the Puzzle contract is inherently unfair as it is vulnerable to the following attack which allows an adversary to claim the reward without prior knowledge of sol: (1) an honest user computes and submits a transaction tx to fetch sol to the solve function; then (2) before tx gets effectively appended to the blockchain through the consensus mechanism, it becomes public to all network participants. In particular, a dishonest user may read tx to learn sol before computing their own transaction tx'. The transaction tx' may then be published before tx (even though submitted later). This execution is valid in that it complies to the blockchain's axiomatisation of Figure 1 (valid transactions have been published, although delayed). Such attacks are possible in practice because the blockchain consensus mechanism only ensures that (valid) transactions are eventually included but does not guarantee their order within blocks. Note that the attack requires the adversary to perform active transaction computations when interacting with the system, which is the crux of Dolev-Yao models.

Figure 4 describes a process model of a refined contract FairPuzzle preventing such exploits of honest transactions. Users are required to send commitments (under the form of hashes including their identity) to their solution in an initial phase, in turn stored in a table T. The commitment are subsequently opened in a later release phase. The transition into this phase occurs at time timeout, which is indicated by the checks against the current time t, recorded through the timestamping instructions @t.

Proving Fair Reward

Let us call fair reward the resilience of a protocol against the above kind of attacks. We can define it by comparing the possible executions of a smart contract with idealised executions where transactions are included upon submission, i.e., without getting reordered. Rephrasing: "for all executions 𝜋 1 , there exists an execution 𝜋 2 (with the same submissions, but possibly in a different order) whose valid submissions are immediately followed by their publications, and such that 𝜋 1 and 𝜋 2 have the same final balance of all users". formula hyp_block ( pi : trace ) = // blockchain model hyp_publish ( pi ) /\ hyp_submit ( pi ) formula ideal ( pi : trace ) = // ideal executions G (∀x: bitstring . Submit ( x ) pi = > F Publish ( tx

) pi = > silent pi U Publish ( tx ) pi ) formula fair_reward = // security hyperproperty ∀ pi1 : trace . hyp_block ( pi1 ) = > G ( Setup pi1 => ∃ pi2 : trace . hyp_block ( pi2 ) /\ ideal ( pi2 ) /\ (∀x: bitstring .F Submit ( x ) pi1 <= > F Submit ( x ) pi2 ) /\ F ( G silent pi1 /\ G silent pi2 /\ ∀x: bitstring . balance pi1 [ x ] = balance pi2 [ x ]))

Fig. 5. Formalisation of fair reward

This notion is formalised in Figure 5. It assumes in particular that the theoretical model of the protocol involves a setup phase letting the adversary choose the attack parameters (prize value, number of participants, trust scenario...), and whose end is indicated by the Setup event. After the setup phase, the quantification over pi2 requires the existence of the ideal trace simulating pi1. In particular, immediate publication is modelled by the fact that pi2 should satisfy silent until (U) publication, where silent means that no particular action is occurring at the current time. Similarly, the balances of all users are compared in the final states, i.e., once executions are "silent forever".

Note that, despite FairPuzzle being a reasonably simple contract, establishing fair reward is not trivial in that it requires several technical arguments about the commitment management. Typically:

(1) commitments critically include the public key of the sender (tx.sender in Figure 4). Otherwise, an adversary could replay a commitment by an honest user during the commitment phase and then frontrun their release transaction; (2) commitments should only be accepted during a proper commitment phase, here modelled by a timeout. Otherwise, when an honest user submits a release, the adversary learns the solution and may then both commit and release it before the honest one gets through; (3) users should check that their commitment has effectively been published before releasing.

Otherwise, an adversary may get it artificially rejected by swapping the two transactions.

These three examples are typical executions 𝜋 1 which cannot be simulated by any ideal execution 𝜋 2 . Such subtleties highlight the necessity of a careful, exhaustive and systematic reasoning for proving that fair reward is indeed enforced by the contract's code and the honest participants' behaviour. We illustrate, all across the paper, how FairPuzzle is verified in our framework, and how to encode its various programming mechanisms (e.g., mutable tables) in our symbolic model.

PROTOCOL MODEL

We model our protocols in a timed and stateful variant of the bounded applied 𝜋-calculus. The model is a refinement from [START_REF] Barthe | Tidy: Symbolic Verification of Timed Cryptographic Protocols[END_REF]; one difference is that our model features a notion of atomic composition, which eases the modelling of timing aspects, and supports a notion of global state that can be used to model mutable variables.

Cryptographic Primitives and Messages

Term Algebra. The algebraic setting we use to model cryptographic primitives is largely standard. We start with atomic values:

A = N ⊎ X with N = N pub ⊎ N priv R ⊂ N pub X N ⊂ X .
The set N of names is used to model most values used in protocols: public names (N pub ) may for example model identities, public constants, or numeric values such as time (R), while private names (N priv ) model data unknown to the adversary such as large secret cryptographic material. The set X then contains the variables, including a distinguished subset X N of numeric variables used to specifically bind numeric values. We assume that N priv , N pub ∖ R, X N and X ∖ X N are infinite. We write vars (𝑢), (resp. vars 𝑛 (𝑢), names(𝑢)) the set of variables (resp. numeric variables, names) appearing in an arbitrary object 𝑢. Next, we introduce signatures, which are finite sets F = {f/𝑛, g/𝑚, h/𝑝, . . .} used to represent cryptographic primitives. A symbol f/𝑛 models a primitive taking 𝑛 arguments. We consider two partitions of F :

F = F c ⊎ F d = F pub ⊎ F priv .
On the one hand, F c ⊎ F d distinguishes constructors (used to construct messages) from destructors (used to pattern-match constructors, with possible failure). On the other hand, F pub ⊎ F priv separates public symbols from private ones, the latter specifically modelling operations the adversary is not allowed to perform (e.g., protocol-specific oracles). Finally, protocol messages are modelled by: Definition 3.1 (Term). A term is an atomic value 𝑎 ∈ A, or a function symbol f or an arithmetic operator (+, ×, -, . . . ), applied to other terms while respecting arities. We write T (𝑆) the set of terms built from 𝑆 ⊆ A ∪ F ∪ 𝑂, for a given set of arithmetic operators 𝑂. We call a term 𝑢 ∈ T (𝑆):

(1)

constructor if 𝑆 ∩ F d = ∅; (2) public if 𝑆 ∩ N priv = ∅ and 𝑆 ∩ F priv = ∅; (3) ground if 𝑆 ∩ X = ∅; (4) numeric if 𝑆 ⊆ R ∪ X N ∪ 𝑂.
In particular, our model is implicitly typed in that some terms represent numeric values such as time, and others, cryptographic material; our definitions thus often involve related typing conditions. Finally, the notion of substitutions 𝜎 is defined as usual:

𝜎 = {𝑥 1 ↦ → 𝑢 1 , . . . , 𝑥 𝑛 ↦ → 𝑢 𝑛 }
is a mapping where dom(𝜎) = {𝑥 1 , . . . , 𝑥 𝑛 } are pairwise distinct variables forming the domain of 𝜎, and 𝑢 1 , . . . , 𝑢 𝑛 are terms; 𝜎 is then well-typed if, for all 𝑖 such that 𝑥 𝑖 ∈ X N , 𝑢 𝑖 is a numeric term. The application of a substitution 𝜎 to a term 𝑡 is denoted by 𝑡𝜎 which is the term obtained by replacing all occurrences of 𝑥 𝑖 in 𝑡 by 𝑢 𝑖 = 𝑥 𝑖 𝜎. Also, more specifically, we say that a term 𝐶 is a context if, writing vars (𝐶) = {𝑥 1 , . . . , 𝑥 𝑛 }, each 𝑥 𝑖 appears exactly once in 𝐶. In this case, we write:

𝐶 [𝑢 1 , . . . , 𝑢 𝑛 ] instead of 𝐶𝜎, provided 𝜎 = {𝑥 1 ↦ → 𝑢 1 , . . . , 𝑥 𝑛 ↦ → 𝑢 𝑛 } is well-typed.
In particular, we say that 𝑢 is a subterm of 𝑣 if there is a context 𝐶 such that 𝑣 = 𝐶 [𝑢]. It is a strict subterm if, in addition, 𝑣 ≠ 𝑢. Regarding notations, we write 𝜎 ∪ 𝜎 ′ the substitution of domain dom(𝜎) ∪ dom(𝜎 ′ ) that extends both 𝜎 and 𝜎 ′ (provided they coincide on dom(𝜎) ∩ dom(𝜎 ′ )); and 𝜎𝜎 ′ refers to the composition 𝜎 ′ • 𝜎, i.e., for all terms 𝑡, 𝑡 (𝜎𝜎 ′ ) = (𝑡𝜎)𝜎 ′ .

Rewriting. Terms have an operational behaviour modelled by: Definition 3.2 (Rewriting). A rewriting system R is a finite set of rewrite rules ℓ → R 𝑟 , where ℓ, 𝑟 are terms without arithmetic operators, with vars (𝑟 ) ⊆ vars (ℓ). Additionally, we assume that R is:

(1) destructor, i.e., for all (ℓ → R 𝑟 ), ℓ = f(𝑢 1 , . . . , 𝑢 𝑛 ) with f ∈ F d , 𝑢 1 , . . . , 𝑢 𝑛 , 𝑟 constructor terms; (2) subterm, i.e., for all (ℓ → R 𝑟 ), 𝑟 is either a strict subterm of ℓ, or a ground term;

(3) convergent, i.e., for all terms 𝑢, there exists a unique normal form 𝑢 ↓ of 𝑢, namely a term irreducible by

→ R such that 𝑢 → R • • • → R 𝑢 ↓.
Such rewriting systems can model many primitives such as encryption, signature, hash, or zeroknowledge among others [START_REF] Blanchet | Automatic Cryptographic Protocol Verifier, User Manual and Tutorial[END_REF]Cheval et al. 2020b], but not associative-commutative behaviours, such as XOR or group exponentiation [START_REF] Basin | Tamarin prover manual[END_REF]. Rules may also be extended with weights to capture cryptographic primitives relying on time consumption [START_REF] Barthe | Tidy: Symbolic Verification of Timed Cryptographic Protocols[END_REF]], which we omit here to alleviate the presentation of the model. We lift → R to a relation on arbitrary terms that is the closure of R under well-typed substitution and term context, that is, for all ℓ → R 𝑟 , well-typed substitutions 𝜎, and contexts 𝐶

[𝑥] such that 𝑥 ∈ X ∖ X N , we have 𝐶 [ℓ𝜎] → R 𝐶 [𝑟𝜎].
Also, informally, a destructor operation "fails" when, intuitively, its arguments do not match any rewrite rule. A (well-typed) term without such failure is called a message: Definition 3.3 (Message). A term 𝑢 is a message if for all subterms 𝑣 of 𝑢, 𝑣 ↓ is a constructor term; also, if 𝑣 ↓= 𝑓 (𝑣 1 , . . . , 𝑣 𝑛 ) for some arithmetic operator 𝑓 , all terms 𝑣 𝑖 should be numeric terms. We write msg (𝑢) to express that 𝑢 is a message, the notation being extended to sequences, sets... of terms by requiring that all these terms are messages.

Protocols in an Adversarial Environment

Syntax. We model protocols as processes of a timed and stateful variant of the applied 𝜋-calculus. We use events for formalising security properties; these are modelled by a dedicated, finite set of function symbols F 𝑒 . Although the syntax is mostly taken from [START_REF] Barthe | Tidy: Symbolic Verification of Timed Cryptographic Protocols[END_REF], we introduce a novel notion of atomic composition 𝛼 : 𝛽, that executes two instructions 𝛼 and 𝛽 (or more) simultaneously. In addition to improving the model's modularity by allowing for breaking complex instructions into simpler blocks, atomic composition offers fine-grained control over the timestamping of instructions which is useful when modelling timed case studies. We also introduce a global state, i.e., a multiset to which any subprocess may push, pull, or pattern-match terms.

Definition 3.4 (Process). The grammar of (timed) processes is: where 𝑛 ∈ N ∪ {∞}, 𝑢 is a term, ì 𝑢 = 𝑢 1 , . . . , 𝑢 𝑝 is a sequence of terms, Ev/𝑝 ∈ F 𝑒 , 𝑘 ∈ N priv , 𝑥 ∈ X, 𝑡 ∈ X N , and 𝑒 is a numeric term and ∼ ∈ {>, ⩾}. We call a process bounded when all of its replications ! 𝑛 𝑃 are so that 𝑛 ≠ ∞.

𝑃 ::= 0
We comment the syntax below. Processes are structured by the operators 𝑃 | 𝑄 (executing 𝑃 and 𝑄 concurrently), 𝑃 + 𝑄 (executing the first instruction of either 𝑃 or 𝑄), and ! 𝑛 𝑃 (executing up to 𝑛 parallel copies of 𝑃). Process instructions are composed atomically with the syntax 𝑐 1 : 𝑐 2 : 𝑆, meaning that 𝑐 1 and 𝑐 2 are executed simultaneously. An atomic sequence is eventually broken by a skip, which simply lets time elapse. For readability, we often omit the skip when its role is only to break a sequence (and we write a semicolon directly after the previous instruction). Then, new 𝑘 generates a fresh name, i.e., a value unknown to the adversary. Events have no interpretation in concrete protocol implementations and are simply used here to formalise security properties. Timestamps @𝑡 and the "when" operator record the current time 𝑡 and perform arithmetic tests, respectively. Importantly, processes have access to a global state that is a multiset 𝜃 of constructor terms. Terms can be added to 𝜃 using push 𝑢, and searched for (with pattern matching) using pull 𝑢 or unfound 𝑢. That is, pull 𝑢 only proceeds if 𝑢𝜎 ∈ 𝜃 for some 𝜎 (and has for effect to remove one occurrence of 𝑢𝜎 from 𝜃 ), while unfound 𝑢 asserts that no instance of 𝑢 is in 𝜃 . Finally, inputs and outputs handle remote communications. Since the network is compromised, an output out(𝑢) reveals 𝑢 to the adversary, while an input in(𝑥) fetches an arbitrary message 𝑥 from them, possibly forged from previous outputs. Note however that, in an atomic composition out(𝑢) : in(𝑥) : 𝑆, the adversary has no access to 𝑢 when computing 𝑥 as they are emitted simultaneously.

Example 3.1. Despite the minimal form of the grammar, it is expressive enough to make our results relatively independent of the formalism. For example, one may encode the mutable variables used in the motivating example of Section 2. Each such variable 𝑥 is injectively mapped to a public name 𝑐 𝑥 , and the value 𝑢 of 𝑥 is stored in the global state under the form Store(𝑐 𝑥 , 𝑢) for some dedicated symbol Store/2. Given a numeric variable 𝑥, incrementing it could therefore be done by: 𝑥 += 1 : 𝑃 ≜ pull Store(𝑐 𝑥 , 𝑦) : push Store(𝑐 𝑥 , 𝑦 + 1) : 𝑃 .

We detail in Appendix B other common features such as tests (if / else), or communication channels. As a complement, Figure 6 defines the omitted process in Section 2 in this extended syntax, namely, the expected behaviour of an honest user interacting with the patched contract FairPuzzle. let id = pk ( sk ) in let d0 = (id , commit , h (( sol , id ))) in let tx0 = (d0 , sign ( d0 , rand (0) , sk )) in @ t0 : if t0 < timeout : out ( tx0 ): Submit ( tx0 ); let d1 = (id , release , sol ) in let tx1 = (d2 , sign ( d1 , rand (1) , sk )) in @ t1 : if t1 > timeout : out ( tx1 ): Submit ( tx1 ) Fig. 6. Honest user submitting to FairPuzzle

In both scenarios (the broken or the fair puzzle), if we call user the process describing the expected submission process, and P the one defining the contract's behaviour, the process user | !^n P would thus model the scenario consisting of an honest user and the contract which may be invoked up to n times. The Dolev-Yao adversary then models an implicit coalition of arbitrarily-many dishonest users.

Semantics. We now define a labelled transition system describing the execution of processes in an adversarial environment. To model the knowledge obtained by the adversary by interfering with communications (i.e., spying on outputs), we use a standard notion of frame Φ. It is a substitution

Φ = {ax 1 ↦ → 𝑢 1 , . . . , ax 𝑛 ↦ → 𝑢 𝑛 }
where 𝑢 1 , . . . , 𝑢 𝑛 are constructor terms, and ax 𝑖 ∈ AX are special variables (not considered as being part of X) called axioms. They serve as handles to outputs 𝑢 𝑖 intercepted during a protocol execution by the adversary. We write axioms(𝜉) the set of axioms appearing in an object 𝜉. In particular, adversarial computations are modelled by: Definition 3.5 (Recipe). A recipe is a term of the form 𝜉 ∈ T (N pub ∪ F pub ∪ AX) . We say that a recipe 𝜉 deduces a constructor term 𝑢 from a frame Φ if msg (𝜉Φ) and 𝜉Φ↓= 𝑢.

Recipes cannot contain private names or functions because they are not accessible to the adversary a priori. The actual operational semantics (Figure 7) then operates on an extended form of process recording the multiset of subprocesses executed in parallel P, the adversary's knowledge Φ, the global state 𝜃 , and the current time 𝑡. Definition 3.6 (Extended process). An extended process is a tuple 𝐴 = (P, Φ, 𝜃, 𝑡), with P a multiset of processes, Φ a frame, 𝜃 a multiset of constructor terms, and 𝑡 ∈ R + . We write the respective components P (𝐴), Φ(𝐴), 𝜃 (𝐴) and 𝑡 (𝐴), and often interpret a process 𝑃 as ({{𝑃 }}, ∅, ∅, 0) .

The semantics Figure 7 is a labelled transition relation ì 𝑤 -→ , where ì 𝑤 is a (possibly-empty) sequence of so-called actions, that are either event terms Ev( ì 𝑢), Ev ∈ F 𝑒 , or some transition-specific labels (par, repl, in...). Figure 7 introduces two intermediary relations -→ at (atomic semantics) and -→ seq (sequential semantics). They define the behaviour of single instructions: -→ at specifically handles operations that may be composed atomically (it hence operates on single processes instead of multisets), while -→ seq executes consecutive atomic instructions until reaching a skip. The sequential semantics ensures in particular through Rule (Comp) that atomically-composed outputs do not operational semantics:

({{𝑃 }} ∪ Q, Φ, 𝜃, 𝑡) ì 𝑤 -→ (P ∪ Q, Φ ′ , 𝜃 ′ , 𝑡 + 𝛿) if 𝛿 > 0 and (Lift) ({{𝑃 }}, Φ, 𝜃, 𝑡 + 𝛿) ì 𝑤 -→ seq (P, Φ ′ , 𝜃 ′ , 𝑡 + 𝛿)
sequential semantics:

({{skip ; 𝑃 }}, Φ, 𝜃, 𝑡) skip ---→ seq ({{𝑃 }}, Φ, 𝜃, 𝑡) (Skip) ({{𝑃 | 𝑄 }}, Φ, 𝜃, 𝑡) par --→ seq ({{𝑃, 𝑄 }}, Φ, 𝜃, 𝑡) (Par) ({{! 𝑛 𝑃 }}, Φ, 𝜃, 𝑡) repl ---→ seq ({{! 𝑛-1 𝑃, 𝑃 }}, Φ, 𝜃, 𝑡) if 𝑛 > 0 (Repl) ({{𝑃 }}, Φ, 𝜃, 𝑡) 𝛼, ì 𝑤 ---→ seq (P, Φ ′ ∪ Φ ′′ , 𝜃 ′′ , 𝑡) if (𝑃, Φ, 𝜃, 𝑡) 𝛼 -→ at (𝑃 ′ , Φ ′ , 𝜃 ′ , 𝑡) (Comp)
and

({{𝑃 ′ }}, Φ, 𝜃 ′ , 𝑡) ì 𝑤 -→ seq (P, Φ ′′ , 𝜃 ′′ , 𝑡)
atomic semantics (over single processes): update the adversary's knowledge Φ before the end of the rule. Note also that the global clock 𝑡 is entirely managed by Rule (Lift), which defines -→ by letting some time pass from 𝑡 to 𝑡 + 𝛿. We now comment the rules of Figure 7. In the communication rules (Out) and (In), outputs increase the adversary's knowledge (i.e., add the axiom ax to dom(Φ)), and inputs are computed by the adversary using previous outputs (i.e., through a recipe 𝜉). Note also that only valid messages in normal form, namely constructor terms, are allowed to circulate on the network. Rule (Event) triggers an event used to formalise security properties, and may be atomically composed to other instructions to add custom labels to them as well. The three rules (Push), (Pull) and (Unfound) then formalise the behaviour of global state manipulation by adding, removing, or checking the absence of a term in 𝜃 , respectively. Rules (New), (Stamp) and (When) have a straightforward interpretation, while Rule (Par) and (Repl) spawn parallel threads, and (Choice) atomically branches to either of two processes. The semantics then induces the following notion of execution: Definition 3.7 (Trace, Trace state). A trace 𝑇 of an extended process 𝐴 0 is a finite sequence

(out(𝑢) : 𝑆, Φ, 𝜃, 𝑡) out --→ at (𝑆, Φ ∪ {ax ↦ → 𝑢 ↓}, 𝜃, 𝑡) if msg (𝑢) and ax ∈ AX ∖ dom(Φ) (Out) (in(𝑥) : 𝑆, Φ, 𝜃, 𝑡) in -→ at (𝑆 {𝑥 ↦ → 𝜉Φ↓}, Φ, 𝜃, 𝑡) if 𝜉 recipe, msg (𝜉Φ) (In) (new 𝑘 : 𝑆, Φ, 𝜃, 𝑡) new ---→ at (𝑆 {𝑘 ↦ → 𝑘 ′ }, Φ, 𝜃, 𝑡) if 𝑘 ′ ∈ N priv fresh (New) (Ev ( ì 𝑢) : 𝑆, Φ, 𝜃, 𝑡) Ev ( ì 𝑢↓ ) -----→ at (𝑆, Φ, 𝜃, 𝑡) if msg ( ì 𝑢) (Event) (push 𝑢 : 𝑆, Φ, 𝜃, 𝑡) push ---→ at (𝑆, Φ, 𝜃 ∪ {{𝑢 ↓}}, 𝑡) if msg (𝑢) (Push) (pull 𝑢 : 𝑆, Φ, 𝜃 ∪ {{𝑢𝜎 ↓}}, 𝑡) pull --→ at (𝑆𝜎, Φ, 𝜃, 𝑡) if msg (𝑢𝜎) (Pull) (unfound 𝑢 : 𝑆, Φ, 𝜃, 𝑡) unfound ------→ at (𝑆, Φ, 𝜃, 𝑡) if for all 𝜎 such that msg (𝑢𝜎), 𝑢𝜎 ↓∉ 𝜃 (Unfound) (@𝑡 0 : 𝑆, Φ, 𝜃, 𝑡) stamp ----→ at (𝑆 {𝑡 0 ↦ → 𝑡 }, Φ, 𝜃, 𝑡) (Stamp) (when 𝑒 ∼ 0 : 𝑆, Φ, 𝜃, 𝑡) when ----→ at (𝑆, Φ, 𝜃, 𝑡) if 𝑒 ∈ R and 𝑒 ∼ 0 holds (When) (𝑆 0 + 𝑆 1 , Φ, 𝜃, 𝑡) - → at (𝑆 𝑖 , Φ, 𝜃, 𝑡) if 𝑖 ∈ {0, 1} (Choice)
𝑇 : (P 0 , Φ 0 , 𝜃 0 , 𝑡 0 ) ì 𝑤 1 --→ • • • ì 𝑤 𝑛 --→ (P 𝑛 , Φ 𝑛 , 𝜃 𝑛 , 𝑡 𝑛 )
of -→ -transitions as defined in Figure 7. If 𝑡 ⩾ 𝑡 0 , we also define the state of 𝑇 at time 𝑡, written 𝑇 @𝑡, as the following pair, with the convention 𝑡 𝑛+1 = +∞: 𝑇 @𝑡 = ((P 𝑖 , Φ 𝑖 , 𝜃 𝑖 , 𝑡), 𝐸)

with 𝑖 = min{ 𝑗 ⩽ 𝑛 + 1 | 𝑡 𝑗 ⩾ 𝑡 } where 𝐸 = { ì 𝑤 𝑖 } if 𝑡 = 𝑡 𝑖 , 𝑖 ∈ 1, 𝑛
, and 𝐸 = ∅ otherwise. The state 𝑇 @𝑡 = (𝐴, 𝐸) of a trace thus indicates the set 𝐸 of events being triggered at the current time 𝑡, if any, as well as the current state of the process execution 𝐴 (at time 𝑡 but right after the execution of the events of 𝐸).

Example 3.2. Using the notations of Example 3.1, consider the process 𝐴 0 = user | ! 2 P modelling an honest user submitting to the broken Puzzle contract. The trace modelling the attack against fair reward from Section 2 would typically start as a sequence of transitions of the form

𝐴 0 par --→ out,Submit(tx) -----------→𝐴 1 repl ---→ in,Publish(tx ′ ) -----------→𝐴 2 repl ---→ in,Publish(tx) ----------→𝐴 3
for some extended processes 𝐴 1 , 𝐴 2 , 𝐴 3 . The first segment from 𝐴 0 to 𝐴 1 submits the honest transition tx (say, under the axiom ax). The second segment from 𝐴 1 to 𝐴 2 is the adversary's interference. After unfolding one copy of P (Rule (Repl)), the dishonest transaction tx ′ gets published, being fetched through the input recipe 𝜉 = (𝜁 , sign(𝜁 , 𝑟, sk ′ )), where 𝑟 ∈ N pub is fresh, sk ′ ∈ N pub models the signature key of the adversary, and 𝜁 = (pk(sk ′ ), solve, ax.args). The recipe 𝜉 thus models the adversary extracting the solution from tx and then forging their own transaction from it. The final segment from 𝐴 2 to 𝐴 3 then publishes the honest transaction tx to comply with the blockchain axiomatisation (recall hyp_submit in Section 2, Figure 1). This time, the adversary forwards the honest transaction tx, that is, uses the recipe 𝜉 ′ = ax for the publication's input.

VERIFICATION OF HYPERPROPERTIES

Hyperproperties

Guarded Hyperformulae. We present the logic Hypertidy CTL* of [START_REF] Barthe | Tidy: Symbolic Verification of Timed Cryptographic Protocols[END_REF] for specifying hyperproperties, adapted to our context with atomic composition, and restricted to a fragment with some syntactic restrictions (guarded hyperformulae). First, we do not provide a generic operator for what was called "second-order quantifiers" ∀𝑋 in [START_REF] Barthe | Tidy: Symbolic Verification of Timed Cryptographic Protocols[END_REF]], which quantify over all possible recipes 𝑋 that the adversary may compute. Instead, we restrict their use to the atomic formula K 𝜋 (𝑢), stating that the adversary can deduce ("Knows") 𝑢 in the frame of the trace 𝜋. This feature is not crucial to the examples of this paper, but is useful to express, e.g., notions of data secrecy. However, this limitation excludes more complex statements about the view of the adversary, like indistinguishability properties such as static equivalence 𝜋 0 ∼ 𝜋 1 (reading as "there exist no public tests, i.e., recipes 𝜉, that deduce a valid message in 𝜋 𝑖 but fail in 𝜋 1-𝑖 "). We leave such properties aside, as most use cases for them are already studied by dedicated tools [START_REF] Basin | Tamarin prover manual[END_REF][START_REF] Blanchet | Automatic Cryptographic Protocol Verifier, User Manual and Tutorial[END_REF]Cheval et al. 2020b], and as guarded hyperformulae may still express many relevant relational hyperproperties through arbitrary deducibility constraints or term equalities across multiple traces. Naturally, non-adversarial notions of path indistinguishability (e.g., one that compares parts of the global states as in our motivating example) are expressible in our framework.

As a second (natural) restriction, we will impose that first-order quantifiers ∀𝑥, quantifying over messages, are guarded. This is the uplifting of standard assumptions in reachability properties (see, e.g., [START_REF] Basin | Tamarin prover manual[END_REF]) to the Tidy logics. It intuitively requires that such quantifiers should only be used to make reference to terms used by the process, and not to express arbitrary first-order formulae on terms. Rephrasing, the possible instantiations of 𝑥 should always be determined from context when (dis)proving that a subformula ∀𝑥 .𝜑 holds. A similar notion has been introduced in Hypertidy CTL*, but is purposely very strict so that the complexity lower bounds of [START_REF] Barthe | Tidy: Symbolic Verification of Timed Cryptographic Protocols[END_REF]] could be as general as possible. On the contrary, we designed our notion of guard with expressivity in mind, making it naturally more general than the prior version of [START_REF] Barthe | Tidy: Symbolic Verification of Timed Cryptographic Protocols[END_REF]].

Definition 4.1 (guarded hyperformula). The grammar of guarded hyperformulae is: where 𝑢, 𝑣 are terms, 𝛼 is an action (as in the operational semantics), 𝑥 1 , . . . , 𝑥 𝑝 ∈ X (𝑝 ⩾ 0), 𝜋 belongs to a set X 𝑝 of so-called path variables, and 𝐼 = (𝑎, 𝑏) is an open interval with 𝑎, 𝑏 numeric terms (or possibly 𝑏 = +∞). We also require that in ∀ì 𝑥 .𝜑 0 ⇒ 𝜑 1 , the formula 𝜑 0 is a guard for ì 𝑥. Namely, we require that for all 𝑦 ∈ { ì 𝑥 }, 𝑦 should appear with positive polarity (i.e., 1) in 𝜑 0 , polarity being defined as follows assuming a fresh alpha renaming of all quantified variables:

𝜑 ::= ⊥ false GS 𝜋 (𝑢)
• 𝑦 appears with polarity 1 in ⊥, and also in GS 𝜋 (𝑢) (resp. Ev 𝜋 (ì 𝑣)) provided 𝑢 (resp. provided there exists 𝑢 ∈ {ì 𝑣 } which) is a constructor term and 𝑦 ∈ vars (𝑢); • if 𝑦 appears with polarity 𝑝 𝑖 in 𝜑 𝑖 , 𝑖 ∈ {0, 1}, it appears with polarity min(-𝑝 0 , 𝑝 1 ) in 𝜑 0 ⇒ 𝜑 1 ; • if 𝑦 appears with polarity -1 in 𝜑, so does it in ∀𝜔.𝜑, with 𝜔 ∈ X ∪ X 𝑝 ;

• if 𝑦 appears with polarity 1 in 𝜓 , so does it in 𝜑 U 𝐼 𝜓 .

Let us now give an intuition for each constructor of the logic. First of all, the atomic formulae are ⊥ (always false), 𝑢 = 𝑣 ("𝑢 and 𝑣 are messages of same normal form"), 𝛼 𝜋 ("at the current time, 𝜋 performs the action 𝛼"), K 𝜋 (𝑢) ("the adversary can deduce 𝑢 from the current frame of 𝜋"), and GS 𝜋 (𝑢) ("𝑢 belongs to the current global state of 𝜋"). Guarded quantifiers ∀ì 𝑥 .𝜑 0 ⇒ 𝜑 1 instantiate the variables ì 𝑥 as messages, in a way restricted by 𝜑 0 . Without quantification (i.e., { ì 𝑥 } = ∅), this results in a plain implication 𝜑 0 ⇒ 𝜑 1 . In combination with the atomic formula ⊥, this permits to derive negation ¬𝜑 ≜ 𝜑 ⇒ ⊥, "true" ⊤ ≜ ¬⊥, disjunction 𝜑 ∨ 𝜓 ≜ (¬𝜑) ⇒ 𝜓 , and in turn conjunction 𝜑 ∧𝜓 , and existential quantifiers ∃𝜋 .𝜑 and ∃ì 𝑥 .𝜑 0 ∧ 𝜑 1 . We also sometimes consider the silent action 𝜏 𝜋 (silent in Section 2), which is the negation of all other actions 𝛼 𝜋 . The quantifiers over path variables ∀𝜋 .𝜑 specifically quantify over all traces 𝜋 of the process, with nested quantifiers branching from the last path quantifier in scope. Finally, the "until" 𝜑 U 𝐼 𝜓 means that 𝜑 should hold during a time window (𝑡, 𝑡 + 𝛿), where 𝛿 ∈ 𝐼 and 𝑡 is the current time, while 𝜓 holds at time 𝑡 + 𝛿. We often use the typical notation 𝜑 U 𝜓 ≜ 𝜑 U (0,+∞) 𝜓 to refer to a non-time-constrained version of the operator. Other classical temporal operators include F 𝐼 𝜑 ≜ ⊤ U 𝐼 𝜑 ("finally") and G 𝐼 𝜑 ≜ ¬(F 𝐼 ¬𝜑) ("globally"). The non-time-constrained version of these operators F and G , used in Section 2, are also to be understood with 𝐼 = (0, +∞).

The satisfiability relation for guarded hyperformulae is formalised in Figure 8, through judgements of the form Π, 𝑡 |= 𝜑 with Π a substitution from path variables to traces and 𝑡 ∈ R + . We assume a dedicated path variable 𝜀 ∈ dom(Π) used to track the last path quantifier. Definition 4.2 (Satisfiability). A process 𝑃 satisfies 𝜑, written 𝑃 |= 𝜑, when {𝜀 ↦ → 𝜀 𝑃 }, 0 |= 𝜑, with 𝜀 𝑃 the empty trace starting from 𝑃.

Fragments and Restrictions

In this paper, we provide a large range of results, referring in particular to several classical fragments of Hypertidy CTL* whose definitions are recalled below. Definition 4.3 (Fragments). A guarded hyperformula 𝜑 is said to be in:

• Hypertidy LTL if it is of the form 𝜑 = 𝑄 1 𝜋 1 . . . 𝑄 𝑛 𝜋 𝑛 .𝜓 , for 𝑄 𝑖 ∈ {∀, ∃} and 𝜓 a formula without path quantifiers;

Π, 𝑡 ̸ |= ⊥ Π, 𝑡 |= 𝑢 = 𝑣 iff msg(𝑢, 𝑣) and 𝑢 ↓= 𝑣 ↓ Π, 𝑡 |= Ev 𝜋 ( ì 𝑢) iff msg( ì 𝑢)
, and writing Π(𝜋)@𝑡 = (𝐴, 𝐸) for some 𝐴, 𝐸, we have Ev ( ì 𝑢) ↓∈ 𝐸 Π, 𝑡 |= K 𝜋 (𝑢) iff msg(𝑢), and writing Π(𝜋)@𝑡 = (𝐴, 𝐸) for some 𝐴, 𝐸, we have 𝑢 ↓∈ 𝜃 (𝐴) Π, 𝑡 |= GS 𝜋 (𝑢) iff msg(𝑢), and writing Π(𝜋)@𝑡 = (𝐴, 𝐸) for some 𝐴, 𝐸, 𝑢 ↓ deducible from Φ(𝐴) Π, 𝑡 |= ∀𝑥 . 𝜑 iff for all ground constructor terms 𝑢 s. While many properties of our examples will fall into the Hypertidy LTL fragment, the running example (Section 2, Figure 5) typically uses nested quantifiers to express succinctly that the two equivalent trace 𝜋 1 and 𝜋 2 did the same setup phase. Other typical properties that Hypertidy LTL does not capture are liveness properties such as fairness in optimistic fair exchange [START_REF] Barthe | Tidy: Symbolic Verification of Timed Cryptographic Protocols[END_REF], which fall into tidy CTL* (non-relational formulae). Finally, the tidy LTL fragment is restricted to express trace properties such as (weak) secrecy or authentication. The simple blockchain axiomatisation of Section 2 falls into this last class. In protocol analysis, one is then usually interested in the verification problem:

t. 𝜎 = {𝑥 ↦ → 𝑢} is well-typed, Π |= 𝜑𝜎 Π, 𝑡 |= 𝜑 ⇒ 𝜓 iff Π, 𝑡 ̸ |= 𝜑 or Π, 𝑡 |= 𝜓 Π, 𝑡 |= ∀𝜋 . 𝜑 iff writing Π(𝜀)@𝑡 = (𝐴, 𝐸), for all traces 𝑇 of 𝐴, Π[𝜋 ↦ → 𝑇 , 𝜀 ↦ → 𝑇 ] |= 𝜑 Π, 𝑡 |= 𝜑 U 𝐼 𝜓 iff 𝐼 ⊆ R + and ∃𝛿 ∈ 𝐼 . Π, 𝑡 + 𝛿 |= 𝜓 and ∀𝛿 ′ ∈ (0, 𝛿). Π, 𝑡 + 𝛿 ′ |= 𝜑
Decision Problem: Verif ▶ Input: A term algebra (consisting of F , F 𝑒 , R), a process 𝑃 built from it, a guarded hyperformula 𝜑 ▶ Output: Does 𝑃 |= 𝜑 hold?

The analogue of Verif in HyperCTL* is model checking, simpler than satisfiability in that it is decidable for arbitrary hyperproperties [Clarkson et al. 2014]. The problem is however more complex in our context, i.e., undecidable even in tidy LTL [START_REF] Barthe | Tidy: Symbolic Verification of Timed Cryptographic Protocols[END_REF]]. To achieve decidability, our results therefore rely on previously-mentioned restrictions (bounded processes and destructor subterm convergent rewriting). We motivate them below through several undecidability results. First, the problem is undecidable for unbounded processes, even without rewriting.

Proposition 4.1 (Verification of arbitrary processes). Verif is undecidable even when F c = F pub = {h/1}, F d and R are empty, and 𝜑 is a tidy LTL formula.

Although general undecidability is common in protocol analysis, this result emphasises the minimality of the fragment needed to reach it. The proof, in Appendix C, relies on an encoding of two-counter machines, and is done in a restricted setting without real-time, and with global states limited to simulate internal communications. One therefore has to either rely on partial decision procedures or impose restrictions on processes to obtain decidability. We chose to focus on the decidability of bounded processes which, we recall, is still of practical interest as attacks on real protocols rarely require many sessions. However, this does not make the problem trivially decidable due to the adversary, if the term algebra remains unrestricted. Typically [START_REF] Barthe | Tidy: Symbolic Verification of Timed Cryptographic Protocols[END_REF]]: Proposition 4.2 (Verification with arbitrary rewriting). Verif is undecidable for bounded processes and a convergent term algebra, even for tidy LTL formulae.

Technical Overview of the Results

In this section, we state our main decidability and complexity results (summarised at the end of the section, Figure 9) and reference the corresponding sections. Basics of complexity theory can be found in Appendix A but, as a minimal reminder, we give here relations between complexity classes of interest, including EXPH(poly) (polynomially-bounded exponential hierarchy):

P ⊆ NP ⊆ PSPACE ⊆ EXP EXP ⊆ NEXP ⊆ EXPH(poly) ⊆ EXPSPACE
When it comes to complexity, one important aspect of the problem is the numeric constraints that may appear in "when" instructions, or that naturally arise as (discrete-time) scheduling constraints when proving hyperproperties. Our results are largely independent of the details of the solving of numeric constraints; they thus always implicitly assume:

(1) a notion of atomic numeric constraint used in "when" conditions, and that allows at least constraints 𝑡 < 𝑡 ′ for 𝑡, 𝑡 ′ ∈ X N . All of our complexity lower bounds are valid regardless, that is, without "when" instructions; (2) an oracle checking whether a conjunction of atomic time constraints has a solution (that is, an instantiation of the numeric variables satisfying the constraints).

For oracle-free results to hold, the underlying problem should be decidable-and in P, when it comes to complexity. Note that this polynomial bound is at least trivial for the minimal required core of atomic constraints, i.e., in contexts without real-time.

Decidability in Restricted Fragments. As a complement to our main result (stated at the end of the section), we first mention a couple of side complexity results for fragments of the logic (proved in Appendix F). Historically, reachability properties (tidy LTL) benefited from more attention, resulting in a strong theoretical understanding and automated support, compared to wider fragments [Cheval et al. 2020a]. For example, for subterm convergent term algebras and bounded processes, many such properties such as weak secrecy are known to be coNP complete [START_REF] Baudet | Sécurité des protocoles cryptographiques: aspects logiques et calculatoires[END_REF][START_REF] Rusinowitch | Protocol insecurity with a finite number of sessions, composed keys is NP-complete[END_REF]. However surprisingly, verifying generic tidy LTL formulae is also known to be PSPACE hard under the same assumptions [START_REF] Barthe | Tidy: Symbolic Verification of Timed Cryptographic Protocols[END_REF]]. We actually prove that: Theorem 4.3 (Decidability in tidy LTL). Verif is PSPACE complete for destructor subterm convergent term algebras, bounded processes, and tidy LTL guarded hyperformulae.

This gap in complexity compared to practical coNP properties is due to the permissive (guarded) quantifiers over terms ∀𝑥. This easily allows us to encode the satisfaction of quantified boolean formulae, the prototypical PSPACE complete problem-while the above-mentioned coNP complete security properties only exploit such quantifiers in a rather limited way. We introduce here a more restricted notion of safety property, closer to practical examples, where the Verif problem will be coNP complete. For that, we require that only the same type of quantifiers (∀, ∃) is used. Formally: Definition 4.4 (Mono-polarity fragments). We inductively define that a guarded hyperformula has polarity ∀, ∃, or 0 as follows. If 𝑝 ∈ {0, ∀, ∃}, we write ¬𝑝 the opposite polarity, that is, ¬∀ = ∃, ¬∃ = ∀ and ¬0 = 0. Then:

• atomic formulae and their negations have polarity 0;

• if 𝜑 𝑖 has polarity 𝑝 𝑖 , ∀ì 𝑥 .𝜑 0 ⇒ 𝜑 1 has both polarity ¬𝑝 0 and 𝑝 1 , and additionally ∀ if 𝑛 ⩾ 1;

• if 𝜑 has polarity 𝑝, ∀𝜋 .𝜑 has polarity ∀ and 𝑝;

• if 𝜑 𝑖 has polarity 𝑝 𝑖 , 𝜑 0 U 𝐼 𝜑 1 has polarity 𝑝 0 and 𝑝 1 .

We call tidy 𝑄-LTL , 𝑄 ∈ {∀, ∃}, the class of tidy LTL guarded hyperformulae without polarity ¬𝑄.

Many reachability properties do not involve both ∀ and ∃. Weak secrecy (∀𝜋 . G ¬K 𝜋 (𝑢)), event reachability (∃𝜋 . F A 𝜋 ), or correspondence properties (∀𝜋 . ¬A 𝜋 U ? B 𝜋 ) are typical examples.

Theorem 4.4 (Complexity of mono-polarity tidy LTL). Verif is coNP complete (resp. NP complete) for destructor subterm convergent term algebras, bounded processes, in tidy ∀-LTL (resp. tidy ∃-LTL ).

We also provide tight complexity analyses for the pure 𝜋-calculus, that is, with an empty term algebra (F = ∅ and R = ∅), see Figure 9. Although anecdotal in terms of applications, this fragment serves as a baseline for comparison to emphasise which assumptions increase the verification cost.

Decidability in Hypertidy CTL*. Finally, our main result is then that Verif is decidable under the assumptions of this paper. This states three incomparable complexity results for Verif. However, as EXPH(poly) hardness is already established for the three of them [START_REF] Barthe | Tidy: Symbolic Verification of Timed Cryptographic Protocols[END_REF], it suffices to prove that Verif is in EXPH(poly) only for the whole logic Hypertidy CTL*. Our procedure is based on constraint solving, recalling [START_REF] Cheval | Deciding equivalence-based properties using constraint solving[END_REF][Cheval et al. , 2018;;Liu and Lin 2012]. This intuitively replaces the sources of unboundedness of traces (recipes and timestamps), by variables and constraints on their instantiations. This is done through an alternative, finitely-branching symbolic semantics defined in Section 5, used as a basis for a procedure in Section 6. Given a guarded hyperformula 𝜑, it mainly computes two sets of constraints Ω 𝜑 , Ω ¬𝜑 , where solutions of Ω 𝜓 can intuitively be used to reconstruct a proof that 𝜓 holds. Typically, if 𝜑 = 𝜑 0 ⇒ 𝜑 1 , the procedure starts by computing Ω 𝜑 0 , Ω ¬𝜑 0 . Then, as the constraints of Ω ¬𝜑 0 already induce a proof of 𝜑, the constraints of Ω 𝜑 0 are refined w.r.t. to the formula 𝜑 1 through a suitable recursive call, to compute Ω 𝜑 0 ∧𝜑 1 , Ω 𝜑 0 ∧¬𝜑 1 . The final decision criterion is then that 𝜑 holds iff Ω ¬𝜑 = ∅. One technical challenge specific to hyperproperties is the more complex notion of constraints compared to related works [START_REF] Cheval | Deciding equivalence-based properties using constraint solving[END_REF][Cheval et al. , 2018]], as they are to be interpreted across several different traces. Additionally, two constraints characterising two different traces are not independent: 𝜑 expresses relations between them. Therefore, they cannot be solved separately. Our procedure handles nested path quantifiers using a stack structure, to propagate the solving's results from deeper levels to higher ones. Finally, using a small-solution property (i.e., that all constraints of Ω 𝜑 ∪ Ω ¬𝜑 have a solution of at most exponential size), we show that we can derive a naive EXPH(poly) procedure.

SYMBOLIC ABSTRACTION

We give a symbolic semantics for bounded processes, replacing the operational semantics with a finitely-branching relation annotated with constraints, mostly inspired by classical analogue notions [Cheval et al. 2018]. In the following, we always assume that processes only contain bounded replications.

(Refined) Unification Theory

We first introduce some important notions from unification theory that are necessary to formalise the symbolic semantics, and that are central to our decision procedure in general.

Refined Term Algebra. First, we partition the set of variables X in two: first-order variables 𝑥, 𝑦, 𝑧, . . . that we have been using so far in processes and formulae, and second-order variables 𝑋, 𝑌, 𝑍, . . . that will be used to represent adversarial computations (i.e., recipes). Formally, we write: where X 1 ∖ X N , X N and X 2 are infinite. We recall that X 𝑝 is the set of path variables, and write vars 1 (𝑢), vars 2 (𝑢), vars 𝑛 (𝑢) the set of first-order, second-order, and numeric variables, respectively, appearing in an object 𝑢. To reflect the partition X = X 1 ⊎ X 2 , we refine terms:

X = X 1 ⊎ X 2 with X N ⊆ X 1
Definition 5.1 (First-and second-order term). A first-order term is a term 𝑢 ∈ T (F ∪ N ∪ X 1 ), and a second-order term is a term 𝜉 ∈ T (F pub ∪ N pub ∪ AX ∪ X 2 ).

First-order terms are therefore terms representing actual protocol communications, whereas second-order terms represent adversarial computations. We recall in particular from Section 3 that a ground term is a term 𝑢 such that vars (𝑢) = ∅: a ground second-order term is therefore, by definition, a recipe 𝜉 (as axioms are not treated as variables of X). Additionally, we use a form of bookkeeping to record which amount of knowledge was available to the adversary at the time a given adversarial computation 𝑋 ∈ X 2 was introduced. We consider the partition:

X 2 = 𝑀 ⊆ A X, 𝑀 finite X 2 𝑀 Intuitively, variables of X 2
𝑀 represent recipes that only use axioms ax ∈ 𝑀; in this case we say that 𝑋 has multiplicity 𝑀 and write 𝑋: 𝑀 instead of 𝑋 to denote this fact. Concretely, when the symbolic semantics will introduce a new second-order variable to represent a recipe, its multiplicity will be the domain of the current frame. Besides, we adapt the definition of well-typing accordingly: Definition 5.2 (Well-typed substitution). A substitution 𝜎 is well-typed if for all 𝜔 ∈ dom(𝜎):

(1) if 𝜔 ∈ X 1 then 𝜔𝜎 is a first-order term;

(2) if 𝜔 ∈ X N then 𝜔𝜎 is a numeric term;

(3) if 𝜔: 𝑀 ∈ X 2 then 𝜔𝜎 is a second-order term, axioms(𝜔𝜎) ⊆ 𝑀 and vars 2 (𝜔𝜎) ⊆ 𝑁 ⊆𝑀 X 2 𝑁 . Constraints and unifiers. Given a set of equations between terms 𝐸 = (𝑢 𝑖 = ? 𝑣 𝑖 ) 𝑖 ∈𝐼 , a standard problem is unification, i.e., the existence of (well-typed) substitutions 𝜎 such that 𝑢 𝑖 𝜎 = 𝑣 𝑖 𝜎 for all 𝑖 ∈ 𝐼 . When unification is possible, a most general unifier is known to exist. The problem has also been studied modulo the rewriting system [Comon-Lundh and Delaune 2005]. However, numeric terms, due to arithmetic operators, are poorly suited for unification in general. In particular, rather than a substitution, we see in this paper unifiers 𝜎 as conjunctions of equation constraints 𝑢 = ? 𝑣, with 𝑢, 𝑣 constructor terms. They are used to either characterise substitutions 𝜎 (through constraints 𝑥 = ? 𝑥𝜎 for each 𝑥 ∈ dom(𝜎)) or numeric equations (through constraints 𝑒 = ? 0, 𝑒 numeric term). We introduce below a more general notion of constraint, which will be at the core of our symbolic semantics, and of the different components of our decision procedure as a whole.

Definition 5.3 (Constraint). A constraint C is of either of the forms:

C ::= 𝑢 = ? 𝑣 ∀ì 𝑥 . 𝑖 𝑢 𝑖 ≠ ? 𝑣 𝑖 first-order (dis)equation 𝜉 = ? 𝜁 ∀ ì 𝑋 . 𝑖 𝜉 𝑖 ≠ ? 𝜁 𝑖 second-order (dis)equation 𝑒 < ? 0 𝑒 ⩽ ? 0 numeric inequality 𝜉 ⊢ ? 𝑢 ∀𝑋 .𝑋 ⊬ ? 𝑢 (non-)deduction constraint
with 𝑢, 𝑣, 𝑢 𝑖 , 𝑣 𝑖 first-order constructor terms, { ì 𝑥 } ⊆ X 1 , { ì 𝑋, 𝑋 } ⊆ X 2 , 𝜉, 𝜉 𝑖 , 𝜁 𝑖 second-order terms with 𝜉 not having a constructor symbol at its root, and 𝑒 is a numeric term. Note that the case of numeric constraints 𝑒 = ? 0 is covered as a subcase of first-order equations. We usually write ⊤ and ⊥ trivially (un)satisfiable constraints.

Intuitively, equations represent equalities between terms. We insist on the fact that they are syntactic: to express that 𝑢 ↓= 𝑣 ↓, the adequate constraint is not 𝑢 = ? 𝑣 but 𝑥 ∈dom(𝜎 ) 𝑥 = ? 𝑥𝜎 for some 𝜎 such that 𝑢𝜎 ↓= 𝑣𝜎 ↓. More generally, we often see unifiers, or even well-typed substitutions in general, as conjunctions of constraints, with the interpretation:

𝜎 ≜ 𝑥 ∈dom(𝜎 ) 𝑥 = ? 𝑥𝜎 ¬𝜎 ≜ ∀ì 𝑧. 𝑥 ∈dom(𝜎 ) 𝑥 ≠ ? 𝑥𝜎 (ì 𝑧 = img(𝜎) ∖ dom(𝜎)) .
Regarding numeric inequalities, they are similar to their non-symbolic analogue used in protocols in when conditions, and constraints 𝜉 ⊢ ? 𝑢 express that 𝑢 is deducible by the adversary using the computation 𝜉. As stated earlier, we can then use constraints to define unification (possibly modulo rewriting) in our numeric context:

Definition 5.4 (Unification modulo rewriting). A unifier modulo rewriting of a set of equations 𝐸 = (𝑢 𝑖 = ? 𝑣 𝑖 ) 𝑖 ∈𝐼 is a conjunction of constraints 𝛾 = 𝜎 ∧ 𝑁 , with 𝜎 a well-typed substitution (interpreted as a conjunction of constraints as above), 𝑁 a conjunction of numeric equations, s.t.:

(1) dom(𝜎) ⊆ vars (𝐸) and vars 𝑛 (𝑁 ) ⊆ vars 𝑛 (𝐸);

(2) there exists a well-typed substitution 𝜎 𝑁 such that dom(𝜎 𝑁 ) = vars (𝑁 ) and 𝑁 𝜎 𝑁 holds when interpreting = ? as the equality on R;

(3) for all 𝜎 𝑁 verifying Item (2), for all 𝑖 ∈ 𝐼 , we have msg(𝑢 𝑖 𝜎𝜎 𝑁 , 𝑣 𝑖 𝜎𝜎 𝑁 ) and 𝑢 𝑖 𝜎𝜎 𝑁 ↓= 𝑣 𝑖 𝜎𝜎 𝑁 ↓. We say that a set 𝑆 of such unifiers is complete if for all 𝜎 ′ ∧ 𝑁 ′ unifiers modulo rewriting of 𝐸, there exist 𝜎 ∧ 𝑁 ∈ 𝑆 and a well-typed substitution 𝜏 such that 𝜎 ′ = 𝜎𝜏 and such that for all well-typed 𝜎 𝑁 of domain vars (𝑁 , 𝑁 ′ ), 𝑁 ′ 𝜎 𝑁 ⇒ 𝑁 𝜎 𝑁 . We write mgu R (𝐸) such a complete set of unifiers, with the convention mgu R (𝐸) = ⊥ when none exists.

Definition 5.5 (Syntactic unification). A unifier 𝛾 of 𝐸 is a unifier modulo rewriting of 𝐸, for the alternative term algebra interpreting all symbols as constructors, and with an empty rewriting system (i.e., all terms are messages in normal form). Also, 𝛾 is a most general unifier of 𝐸, written mgu (𝐸), if {𝛾 } is a complete set of unifiers of 𝐸 modulo this same theory.

Computing mgu can be done straightforwardly using standard algorithms, adding numeric constraints instead of regular constraints when unifying a numeric term with another term. The set mgu R (𝐸) is also known to be computable for our class of rewriting systems using narrowing [Comon-Lundh and Delaune 2005], up to minor modifications due to the numeric requirements.

Note also that, regardless of numeric aspects, unifying a term 𝑢 with itself is not always immediate due to the requirement that 𝑢 is a valid message. Rephrasing, mgu R (𝑢 = ? 𝑢) ≠ {⊤} in general. In fact, 𝜎 ∈ mgu R (𝑢 = ? 𝑢) means msg (𝑢𝜎). Finally, when it comes to (syntactically) unifying second-order terms, subtle considerations also arise due to the multiplicity of variables. Typically, when unifying, e.g., two variables 𝑋: 𝑀, 𝑌: 𝑁 , one should map them to a common fresh variable 𝑍 whose multiplicity is the most general one not breaking well-typing (i.e., 𝑀 ∩ 𝑁 ). We however omit the details as they are vastly analogue to existing techniques despite the slight differences in contexts. For the unusual case of second-order unification, we refer to the algorithm and proofs of [START_REF] Rakotonirina | Efficient verification of observational equivalences of cryptographic processes: theory and practice[END_REF], Chapter 2, Section 1.2].

Symbolic Semantics

We now introduce the symbolic semantics we use to give a finite characterisation of traces, using constraints to reflect the application conditions of the operational semantics -→ . Concretely:

Definition 5.6 (Constraint system). A constraint system is a constraint D ∧ K ∧ E 1 ∧ E 2 where
(1) D is a set of (non-)deduction constraints of the form 𝑋 ⊢ ? 𝑢 or ∀𝑋 .𝑋 ⊬ ? 𝑢 for 𝑋 ∈ X 2 ;

(2) K is a set of constraints 𝜉 ⊢ ? 𝑢, 𝜉 ∉ X 2 , s.t. the following is a well-defined substitution:

Φ(C) = {ax ↦ → 𝑢 | (ax ⊢ ? 𝑢) ∈ K, ax ∈ AX}
(3) E 1 is a set of first-order (dis)equations and numeric constraints, and E 2 of second-order (dis)equations. Given a constraint system C, the above decomposition is unique and we write D(C), K(C), Φ(C) and E 𝑖 (C) the underlying components. We also use the notations:

mgu (E 𝑖 ) = mgu ((𝑤 = ? 𝑤 ′ ) ∈ E 𝑖 ) .

A constraint system is therefore a collection of constraints organised accordingly to their roles. Constraints of D indicate the deductions required from the adversary to reach a certain state of the proof. Typically, symbolically executing an input in(𝑥) puts a constraint 𝑋 ⊢ ? 𝑥 in D. On the contrary, K is a knowledge base available to the attacker to resolve the constraints of D, thus generalising the notion of a frame. In our procedure, K will undergo a saturation generating (redundant) entries 𝜉 ⊢ ? 𝑢 facilitating deducibility checks. Finally, E 𝑖 adds syntactic constraints to the lot. The set E 2 in particular is not used in the symbolic semantics, but will be at the core of our constraint-solving algorithm to store solutions under the form of mgu (E 2 ). Altogether: Definition 5.7 (Symbolic processes). A symbolic process is a tuple 𝐴 = (P, C, 𝜃, 𝑡) with P a multiset of processes, C a constraint system, 𝜃 a global state, and 𝑡 ∈ X N . The different components are referred to as P (𝐴), C(𝐴), 𝜃 (𝐴) and 𝑡 (𝐴), respectively.

Formally, the symbolic semantics is a relation ì 𝑤 -→ s over symbolic processes, with ì 𝑤 a sequence of actions. Similarly to the operational semantics, it relies on an atomic semantics -→ s-at and sequential semantics -→ s-seq . For space reasons however, their definitions can be found in Figure 14, Appendix D, and we only review a couple of rules here. Most often, symbolic processes contain free variables, as executing inputs in(𝑥) symbolically does not instantiate 𝑥 using a concrete recipe 𝜉. This is formalised by Rule (s-In), which freshly renames the input variable 𝑥 (to avoid naming collisions), and adds a deduction constraint for it:

(in(𝑥) : 𝑆, C, 𝜃, 𝑡) in -→ s-at (𝑆 {𝑥 ↦ → 𝑦}, C ∧ 𝑌 ⊢ ? 𝑦, 𝜃, 𝑡) (s-In)
if 𝑦 ∈ X 1 and 𝑌: dom(Φ(C)) ∈ X 2 are fresh. Most other constraints are of the form mgu R (𝑢 = ? 𝑢), thus expressing that 𝑢 is a message, and are carried out to subsequent transitions by the unifier

𝜇 = mgu (E 1 (C))
. The unifier mgu (E 2 (C)), however, is not considered as no constraints are added to E 2 (C) by the symbolic semantics. Typically, the symbolic rule for outputs is the following:

(out(𝑢) : 𝑆, C, 𝜃, 𝑡) out --→ s-at (𝑆, C ∧ 𝜎 ∧ 𝑁 ∧ ax ⊢ ? 𝑢𝜎 ↓, 𝜃, 𝑡) (s-Out)
if 𝜎 ∧ 𝑁 ∈ mgu R (𝑢𝜇 = ? 𝑢𝜇) and ax ∈ AX is fresh, and 𝜇 = mgu (E 1 (C)) as above.

Soundness and Completeness

We now formalise the link between the symbolic semantics and the operational one. This relies on the following notion of solution, formalising the semantics of constraint systems:

Definition 5.8 (Solution). A solution of a constraint system C is a pair of well-typed substitutions (Σ, 𝜎) such that:

(1) dom(Σ) = vars 2 (C), dom(𝜎) = vars 1 (C), img(Σ) only contains recipes, and img(𝜎) ground constructor terms;

(2) for all (𝑋 ⊢ ? 𝑥) ∈ D (C), 𝑋 ΣΦ(C)𝜎 ↓= 𝑥𝜎;

(3) for all (𝑢 = ? 𝑣) ∈ E 1 (C), 𝑢𝜎 = 𝑣𝜎; (4) for all (𝑒 ∼ ? 0) ∈ E 1 (C) with ∼ ∈ {<, ⩽}, we have 𝑒𝜎 ∈ R and 𝑒𝜎 ∼ 0 in R;

(5) for all (𝜉 = ? 𝜁 ) ∈ E 2 (C), 𝜉 Σ = 𝜁 Σ; (6) the satisfaction of first-order formulae is recursively defined in the natural way, interpreting ∀𝑥 as a quantifier over ground constructor terms, and ∀𝑋 as a quantifier over recipes.

Example 5.1. As an example of constraints, consider again the attack on fair reward introduced in Section 2, and the attack trace in the model mentioned in Section 3. A typical constraint modelling the adversary's constraints during the attack would be the following: C = ax ⊢ ? tx ∧ 𝑋: {ax} ⊢ ? tx ′ ∧ tx ′ = ? (𝑥, sign(𝑥, 𝑟, sk ′ )) ∧ 𝑥 = ? (pk(sk ′ ), solve, sol) .

Paraphrasing, the honest transaction tx is public (and accessible through the axiom ax), and the adversary has to compute a transaction tx ′ from it, whose validity is expressed by the last to equation constraints. A second-order solution of this constraint would be the mapping {𝑋 ↦ → 𝜉 }, with 𝜉 the attack recipe previously detailed in the description of the attack (Section 3, Example 3.2).

We write Sol (C) the set of solutions of C, and refer to Σ and 𝜎 as second-order and first-order solutions. This hence formalises the semantics of constraints. Then if we define a symbolic trace

𝑇 : 𝐴 0 s ì 𝑤 1 --→ s • • • ì 𝑤 𝑛 --→ s 𝐴 𝑛
s ì 𝑤 1 --→ s • • • ì 𝑤 𝑛 --→ s 𝐴 𝑛 s . Then if (Σ, 𝜎) ∈ Sol (C(𝑇 s )), we have: 𝑇 : 𝐴 0 ì 𝑤 1 Σ ---→ • • • ì 𝑤 𝑛 Σ ---→ 𝐴 𝑛 with 𝐴 𝑖 = (P (𝐴 𝑖 s )𝜎, Φ(C(𝐴 𝑖 s ))𝜎, 𝜃 (𝐴 𝑖 s )𝜎, 𝑡 (𝐴 𝑖 s )𝜎).
The proof is a straightforward induction on 𝑛 the length of 𝑇 s . In the following, we will often refer to the trace 𝑇 given by the above proposition as the result of applying the solution 𝑆 = (Σ, 𝜎) to 𝑇 𝑠 , and write it 𝑇 = 𝑇 s 𝑆 . In particular, completeness ("all regular traces can be abstracted by a symbolic trace") is formalised as: Proposition 5.3 (Completeness). Let 𝐴 0 s = (P, C, 𝜃, 𝑡) be a symbolic process, (Σ, 𝜎) ∈ Sol (C), and let us write 𝐴 = (P𝜎, Φ(C)𝜎, 𝜃𝜎, 𝑡𝜎) . Then for all traces 𝑇 of 𝐴, there exists a symbolic trace 𝑇 s and 𝑆 = (Σ ∪ Σ ′ , 𝜎 ′ ) ∈ Sol (C(𝑇 s )) such that 𝑇 = 𝑇 s 𝑆.

VERIFICATION OF DOLEV-YAO HYPERPROPERTIES

In this section, we built on our symbolic semantics to provide a decision procedure for the verification of arbitrary, guarded hyperformulae. For readability, we only outline some ideas of the procedure and leave the full technical details to Appendices D and E.

Hyperconstraints

The first ingredient is a refined notion of constraint. Indeed, although the symbolic semantics introduces (sound and complete) constraints for characterising traces finitely, some adequate form of bookkeeping is required when proving hyperproperties due to the multiple path quantifications. Definition 6.1 (Hyperconstraint system, path projection). A hyperconstraint is defined with the same grammar as that of constraints, except that deductions are labelled by path variables:

𝜉 ⊢ ? 𝜋 𝑢 ∀𝑋 .𝑋 ⊬ ? 𝜋 𝑢 (non-)deduction hyperconstraint
In particular, if 𝜋 ∈ vars 𝑝 (C) we define the projection of C on path 𝜋 as the hyperconstraint proj 𝜋 (C) obtained by removing those labelled 𝜋 ′ ≠ 𝜋. A hyperconstraint system C is then a hyperconstraint such that for all 𝜋 ∈ vars 𝑝 (C), proj 𝜋 (C) is a well-defined constraint system. We also extend the notations D (C), K(C), E 𝑖 (C) in the natural way. Note however that Φ(C) is not a well-defined substitution in general, but Φ(proj 𝜋 (C)) is one for all 𝜋 ∈ vars 𝑝 (C).

A hyperconstraint is therefore a collection of constraints across different traces, more suited than a plain constraint for proving hyperproperties. In particular, we can define: Definition 6.2 (Solution of a hyperconstraint system). A solution of a hyperconstraint system C is a pair of well-typed substitutions (Σ, 𝜎) such that: (1) dom(Σ) = vars 2 (C), dom(𝜎) = vars 1 (C), img(Σ) only contains recipes, and img(𝜎) ground constructor terms; and (2) for all 𝜋 ∈ vars 𝑝 (C), we have (Σ |vars 2 (proj 𝜋 ( C) ) , 𝜎 vars 1 (proj 𝜋 ( C) ) ) ∈ Sol (proj 𝜋 (C)) .

Furthermore, we define a notion of most general solution (mgs) partly inspired by the analogue notion introduced in [Cheval et al. 2018] for verifying equivalence properties. Intuitively, similarly to mgu for terms, mgs' are partial instantiations of the (second-order) variables of a hyperconstraint system C that characterise all solutions of C: instantiating the pending second-order variables by fresh public names results in an actual solution, and all solutions are instances of a mgs. Definition 6.3 (Most general solution). A set of most general solutions of a hyperconstraint system C, written mgs (C), is a set of well-typed second-order substitutions such that:

(1) for all (Σ, 𝜎) ∈ Sol (C), there is Σ 0 ∈ mgs (C) and a well-typed

Σ 1 such that Σ = Σ 0 Σ 1 ; (2) for all Σ 0 ∈ mgs (C), dom(Σ 0 ) ⊆ vars 2 (C). Also let 𝑉 = vars 2 (img(Σ 0 ), C) ∖ (dom(Σ 0 ) ∪ 𝑉 𝑡 ) .
Also let Σ 1 be a mapping from 𝑉 to fresh constants such that 𝑋 Σ 1 = 𝑌 Σ 1 iff there exist 𝑧, 𝜋, 𝜋 ′ such that (𝑋 ⊢ ? 𝜋 𝑧), (𝑌 ⊢ ? 𝜋 ′ 𝑧) ∈ D(C). Then there is a well-typed 𝜎 s.t.

(Σ 0 Σ 1 , 𝜎) ∈ Sol (C) .
In this paper, mgs (C) = ⊥ expresses that Sol (C) = ∅. Note that verifying the existence of 𝜎 in Item 2 is straightforward: since the symbolic semantics generates a deduction constraint 𝑋 ⊢ ? 𝑥 for each newly-introduced variable 𝑥 ∈ X 1 , Σ 0 Σ 1 uniquely determines 𝑥𝜎 provided 𝑥 ∉ X N . The cases 𝑥 ∈ X N can then be handled by the black-box time-solving oracle we assume in our procedure (recall Section 4.3). Ordering constraints are the main difference with the original notion of mgs, taken from [Cheval et al. 2018]. In particular, most general solutions are not unique in general, and mgs (C) refers to one arbitrary such set.

Proof States and Stacks

Hyperconstraints are then part of a bigger structure reflecting the proof skeleton of the desired security property. For that, we define a notion of proof state, intuitively modelling a current point in the proof with a list of pending proof obligations, each corresponding to a missing proof to carry for a certain trace. Proof states are then gathered in proof stacks capturing the interactions between the different trace quantifications of hyperproperties. Definition 6.4 (Proof state). A proof state is a tuple of the form 𝜔 = (Π, C, O), whose components may be written Π(𝜔), C(𝜔), and O (𝜔), and where

• Π is a mapping from X 𝑝 to symbolic traces;

• C is a hyperconstraint system;

• O is a set of proof obligations o = (𝑇 , C ′ ), 𝑇 a symbolic trace, C ′ a hyperconstraint system.

Besides, we call the domain of 𝜔 the following set:

dom(𝜔) = {𝑋 ∈ X 2 | (𝑋 ⊢ ? 𝜋 𝑥) ∈ C(𝜔)} .
This represents, intuitively, a snapshot of the state of a proof of a hyperproperty at a given point of the proof tree. For example, the hyperconstraint system C (resp. the mapping Π) gathers all constraints (resp. symbolic traces) generated along the proof so far. Importantly, the set O contains proof obligations (𝑇 , C ′ ), indicating that after concluding the current proof, it should be carried again with the last quantified trace replaced by 𝑇 , and under the additional constraints C. They are then gathered into stacks: Definition 6.5 (Proof stack). A proof stack is a sequence of proof states written

𝜔 ★ = 𝜔 1 ↣ 𝜔 2 ↣ • • • ↣ 𝜔 𝑛 and such that dom(𝜔 1 ) ⊆ • • • ⊆ dom(𝜔 𝑛 ).
Proof states and stacks will undergo forms of constraint solving in order to determine whether their hyperconstraints have solutions. This includes among others a saturation, relying on the assumptions on the term algebra to decide deduction hyperconstraints. We give a first intuition of the goal and behaviour of this saturation step below.

Example 6.1. Consider again our running example (Example 3.2). Once the honest transaction tx is output to the network, this is reflected as a constraint ax ⊢ ?

𝜋 1 tx meaning that the adversary learns tx. The saturation procedure will then add the new hyperconstraint ax.args ⊢ ?

𝜋 1 sol indicating that the private name sol, modelling the submitted solution, can be extracted using the new recipe ax.args. Other deductions such as ax.func ⊢ ?

𝜋 1 solve are not added as the term solve (a public name) is already deducible.

More generally, the role of the saturation procedure is to apply as destructors as possible to already deducible terms, in order to detect potential new adversarial deductions, as in the above examples. The procedure starts from the outputs leaked during the trace to the adversary, and stops when applying destructors only yields terms that were previously deduced-we call the result a saturated knowledge base. This process is guaranteed to terminate due to our restriction to subterm convergent rewriting systems. The details of this constraint-solving procedure can be found in Appendix D, and are used between each step of our decision procedure.

Once saturation is over, it offers a simple characterisation of deducible terms. It has indeed the immediate property that deducible terms need be composed of constructor symbols applied to entries of the saturated knowledge base-which can easily be checked syntactically. This, in turn, permits to frame an algorithm to compute most general solutions of hyperconstraints.

Main procedure

One key point is that proof states aggregate constraints monotonously during the proof of a hyperproperty. However, some side data are still local during a proof: this is for example the case of the current time 𝑡, or the subformula currently being proved. We gather this pieces of local information under an ephemeral analogue of proof states, discarded when moving on to the next proof obligation. It contains, as hinted above, a variable 𝑡 representing the current timestamp, the formula 𝜑 to be proved, but also a mapping Π @ indicating the state of all quantified traces at time 𝑡 (in reference to the notation 𝑇 @𝑡 of Section 3.2). Formally: Definition 6.6 (Local proof data). A local proof data is a tuple 𝜔 -1 = (Π @ , 𝑡, 𝜑), where:

• Π @ is mapping from X 𝑝 to pairs (𝐴, 𝐸) where 𝐴 is a symbolic process and 𝐸 is a set of events; • 𝑡 ∈ X N and 𝜑 is a guarded hyperformula.

To prove a hyperproperty 𝜑, our main procedure then consists of a function HCompute which computes two sets of proof stacks representing, respectively, all cases resulting in 𝜑 or ¬𝜑 holding. Exactly one of these sets will be empty when 𝜑 has no free variables, which is the core criterion for deriving decidability. Formally, this function takes the following form:

HCompute(𝜔 ★ , 𝜔 -1 ) = (Ω 𝜑 , Ω ¬𝜑 )
where 𝜔 ★ is a proof stack, 𝜔 -1 is a local proof data, and Ω 𝜑 and Ω ¬𝜑 are two sets of proof stacks. We also assume that dom(Π @ (𝜔 -1 )) ⊆ dom(Π(𝜔)) and at least contains 𝜀 and all (non-quantified) path variables appearing in 𝜑 (𝜔 -1 ).

Overview of the technical details. Let us give a more concrete intuition of how HCompute operates. For complete technical details, we refer to Appendix E. Consider for example the handling of atomic formulas. Here the role of HCompute is to rely on the constraint solving procedure to resolve a set of characteristic constraints. Let us study the case of an equality modulo rewriting, namely:

HCompute(𝜔 ★ ↣ 𝜔, 𝜔 -1 )
with 𝜑 (𝜔 -1 ) = (𝑢 = 𝑣) .

The first step of HCompute is to unify 𝑢 and 𝑣 modulo rewriting, that is, to compute 𝐸 = mgu R (𝑢 = ? 𝑣). It then picks a first 𝜎 ∈ 𝐸, and adds it to the constraint of the last stack's state, i.e., C(𝜔). By a call to the constraint solving subroutine, it then computes all possible solutions of the updated hyperconstraint.

The results of this resolution are then applied at each level 𝜔 𝑖 of the whole stack 𝜔 ★ , directly in the hyperconstraint C(𝜔 𝑖 ), or filling a queue of pending proof obligations in o(𝜔 𝑖 ) when several solutions are added. This eventually leads to a new resolved stack 𝜔 ★ + . Analogously, a stack 𝜔 ★ can be obtained by considering the negative constraint ¬𝜎 instead. The sets Ω 𝑢=𝑣 , Ω 𝑢≠𝑣 returned by HCompute are then obtained by computing each of the corresponding stacks 𝜔 ★ + and 𝜔 ★ -, for all different unifiers 𝜎 ∈ 𝐸. The treatment of other atomic formulas follows the same idea: (1) we characterise them by a set of unifiers or constraints, (2) they are then added to the last stack level, and (3) this triggers a constraint solving whose results are propagated to all stack levels.

In the other (non-atomic) cases, HCompute follows the inductive structure of the formula 𝜑 (𝜔 -1 ) to be proved. For example, if 𝜑 (𝜔 -1 ) = 𝜑 ⇒ 𝜓 , one first computes (Ω 𝜑 , Ω ¬𝜑 ) through a recursive call to HCompute. Subsequently, for each proof stack 𝜔 ★ ∈ Ω 𝜑 , another recursive call to HCompute is used to, overall, aggregate the sets Ω 𝜑∧𝜓 and Ω 𝜑∧¬𝜓 . The final result of the procedure is then, using the identity (𝜑 ⇒ 𝜓 ) = ¬𝜑 ∨ 𝜓 :

(Ω 𝜑⇒𝜓 , Ω ¬(𝜑⇒𝜓 ) ) = (Ω ¬𝜑 ∪ Ω 𝜑∧𝜓 , Ω 𝜑∧¬𝜓 ) .
The only notable exception is the case of path quantifiers, which creates, on top of that, a new stack level (and yields an additional recursive call to the next proof obligation once the proof at more recent levels are finished).

Correctness. We now state the main correctness property of HCompute. To obtain the desired EXPH(poly) bound, we consider the naive 𝑛-bounded algorithm NBA 𝑛 (𝑃, 𝜑) ∈ {true, false}, which is the brute force alternating (but incomplete) algorithm for proving 𝑃 |= 𝜑 which bounds the size of adversarial computations by 𝑛 to obtain a finite set of traces. Its definition is straightforward, and similar to HCompute but operates on concrete processes and traces, and hence uses concrete recipes (of size 𝑛 at most) instead of deduction constraints. Proposition 6.2 (Complexity and Soundness of NBA). The procedure NBA 𝑛 (𝑃, 𝜑) runs in alternating polynomial time in 𝑛 and the sizes of 𝑃 and 𝜑, and also involves a polynomial number of alternations. Besides, for some initial parameters 𝜔 ★ , 𝜔 -1 (technically defined in Appendix E), let us write (Ω 𝜑 , Ω ¬𝜑 ) = HCompute(𝜔 ★ , 𝜔 -1 ) and assume

𝑛 ⩾ 𝜇 (Ω 𝜑 ∪ Ω ¬𝜑 ) ≜ max (𝜔 ★ ↣𝜔 ) ∈Ω 𝜑 ∪Ω ¬𝜑 𝜋 ∈vars 𝑝 (𝜔 ) 𝜇 𝜋 (C(𝜔))
where 𝜇 𝜋 (C) refers to the size of a mgs of C projected on path 𝜋, i,e., mgs (C) |vars 2 (proj 𝜋 ( C) ) . Then 𝑃 |= 𝜑 iff NBA 𝑛 (𝑃, 𝜑) accepts.

This states that NBA 𝑛 is a sound procedure provided 𝑛 is greater than all (projections of) mgs generated by HCompute. To justify that the Verif problem is in EXPH(poly) under our assumptions, it therefore remains to establish a small solution property, that is, that 𝜇 𝜋 (C) is bounded by an exponential in the inputs of the problem. These properties are proved in Appendix E.2.

REVIEW OF APPLICATIONS OF DY-HYPERPROPERTIES

To conclude, we review here some potential applications of hyperproperties in the context of security protocols, in addition to the running example. We present these examples in an informal style, the translation of the security property in our logic being often straightforward.

Distribution fairness

We first review a few case studies from [START_REF] Barthe | Tidy: Symbolic Verification of Timed Cryptographic Protocols[END_REF], which lists examples of hyperproperties in real-time contexts. They feature either trace properties (lacking relevance to our paper), equivalence properties (out of our scope), or liveness properties in the tidy CTL* fragment. We will focus on the third kind. Notably, although omitted in this section, similar properties as those listed below arise in the context of optimistic fair exchange, studied for example in [START_REF] Backes | A novel approach for reasoning about liveness in cryptographic protocols and its application to fair exchange[END_REF].

The applications we consider rely on time cryptography, which are primitives that require, by design, a significant amount of time to be computed. This allows to lock sensitive data from the adversary during a time window, and corresponds to notions of cost in our calculus term algebra. We cleared this component from our framework to simplify its already dense presentation, but protocol variants may rely instead on trusted third parties holding data until predetermined deadlines. This is used to enforce notions of (distribution) fairness, meaning that either all participants get the protocol's output, or none does. This typically involves the following core notions.

(1) Stuck: the agent cannot do anything but wait for some event 𝐴 that is, say, out of its control.

(2) Progress: at any point in time, non-stuck agents proceed until being stuck.

(3) Activeness: agents do not get stuck by passively waiting, e.g., that some timeout expires. We define these predicates in Figure 10, sticking to the programming-like syntax of Section 2. Various security properties of the form ∀𝜋 .Progress ⇒ 𝜑, or ∀𝜋 .Progress ⇒ Active 𝜋 ⇒ 𝜑, can then be used to formalise fairness in different contexts. One instance is the organisation of auctions as described in [START_REF] Boneh | Timed commitments[END_REF], where participants lock their bid until a common date 𝑡 in the future. They are then expected to reveal their bid at time 𝑡, but should have backup solutions to recover those of non-cooperating parties (typically forceable time cryptography or a trusted third party). The desired security property is then that, in presence of at least one progressing agent, the protocol always goes through until the end once the bids have all been submitted.

Another example of such properties would be contract signing protocols such as the one of [START_REF] Boneh | Timed commitments[END_REF]. Here two mutually distrusting parties 𝐴 and 𝐵 want to exchange signatures with some guarantee that they will get the other's. The main idea is to rely on a locking mechanism expiring after some (parametric) time 𝑡. Concretely, 𝐴 and 𝐵 exchange their signatures, locked for a prohibitive amount of time (say, 𝑡 = 2 𝜂 for some high security parameter 𝜂). They then repeat this protocol, decrementing 𝜂 at each new round. If both parties cooperate, they get each other's signatures in 𝜂 rounds. If one party aborts during round 𝑝, they will have to wait at least time 2 𝜂-𝑝 to get the signature; meanwhile, the worse-off party waits at most time 2 𝜂-𝑝+1 , i.e., at most twice as much. The desired security property would therefore read as:

for all trace 𝜋, if either participant obtains the other's signature at time 𝑇 , then the other can get it at time 𝑇 + 2𝑇 = 3𝑇 , provided it is actively progressing.

As a side note, [START_REF] Barthe | Tidy: Symbolic Verification of Timed Cryptographic Protocols[END_REF] proposes a semi-automated approach to prove real-time properties specified in their framework, which is however only sound for trace properties. The examples mentioned above typically fall into the scope of our decidability result but escape the one of the tool of [START_REF] Barthe | Tidy: Symbolic Verification of Timed Cryptographic Protocols[END_REF]. Albeit for our lack of experimental results, this highlights the improvements induced by our procedure in terms of theoretical contributions.

Atomicity in Smart Contracts

We now give other examples inspired by the domain of smart contracts. Some of the presented hyperproperties may have some verification support in the literature, but most of them do not account for scenarios involving an active Dolev-Yao adversary (see related work, Section 8).

Smart contracts are often written in a quasi-Turing-complete language, meaning here that the language itself is Turing-complete but the number of computation steps for the execution of each contract is bounded by a resource called gas. When invoking a contract, the caller specifies an upper bound on the gas to be consumed by the execution. Each instruction consumes (a positive amount of) gas and halts with an exception when running out of gas, reverting the effects of the contract execution. However, widely used smart contract languages do not support exception propagation, meaning that a caller actively needs to read the error code returned by the failed contract invocation and handle the exception appropriately. This subtlety causes a lot of issues in practice since contract developers forget to implement checks to ensure that calls have been finished successfully, resulting in unhandled exceptions and potentially inconsistent state. To give a semantic characterisation of this property, [Grishchenko et al. 2018] defines a notion called atomicity which intuitively states:

for all executions 𝜋 1 , 𝜋 2 of the contract 𝐶, if the initial states of 𝜋 1 , 𝜋 2 only differ in the amount of gas given to them then either 𝜋 1 and 𝜋 2 have the same final state, or either 𝜋 1 or 𝜋 2 fully rolled back to the initial state of their executions.

This ensures that no problematic state can arise due to unhandled out-of-gas exceptions. In our framework, gas can easily be modelled as part of the global state, and thus even referenced in security properties through the GS atomic formula.

Reentrancy

Reentrancy bugs are a prominent class of smart contract bugs that have caused tremendous financial losses in practice. Intuitively, a smart contract is considered reentrant if it can be called again during its execution-which is usually not part of the desired program logic. It typically occurs if a smart contract 𝐶 invokes another contract 𝐶 ′ and this one calls 𝐶 back. This is often not anticipated by contract developers and may lead to inconsistent states and unwanted behaviours.

For characterising the absence of reentrancy bugs, different approaches have been taken. One approach, taken in [Grishchenko et al. 2018] is to consider the absence of reentrancy bugs as an integrity property focusing on the additional power that an external contract may gain over the execution of a contract 𝐶 through reentering the contract. Intuitively, call integrity states that no other contract should be able to influence how contract 𝐶 spends money (money transfer transactions are considered security-critical actions in the contract setting). Assuming such critical transactions are identified in the process using an event Critical/1, the property can intuitively be stated by the hyperproperty, in a non-interference style fashion:

for all executions 𝜋 1 , 𝜋 2 of the contract 𝐶 reaching a final state, 𝜋 1 and 𝜋 2 should trigger the same events Critical(𝑥) simultaneously.

A different approach is taken in [Grossman et al. 2017]. Here, notions from concurrency theory (serialisability/linearisability) are leveraged to distinguish between benign and reentrancies and such that may expose problematic behaviour. The authors introduce the notion of effective callback freedom that states that a contract 𝐶 is effectively callback free if: for all executions 𝜋 1 that may involve reentering executions (callbacks), there exists an execution 𝜋 2 of 𝐶 not involving any callbacks and with the same initial and final states.

A model of this property in our framework would typically require to model a callstack, which again can easily be embedded in our notion of global state.

Virtual Channel Stability

Payment channels [Poon and Dryja 2016] are cryptographic protocols that help blockchain scalability. They enable two users to conduct fast payments (called offchain payments) between each other without registering every single payment on the blockchain. Instead, the parties initially lock the funds they may want to exchange in a shared account and conduct payments by exchanging cryptographic guarantees that enable them to withdraw the corresponding amounts from the shared account upon channel closure. The channel parties can decide to close the channel at any time using the guarantees obtained before, retrieving their rightful amount from the shared account.

Virtual channels [Dziembowski et al. 2019] generalise payment channels to create new channels upon existing ones. This comes with the advantage that users do not need to individually lock funds with each party with who they want to perform off-chain payments. Instead, a user 𝐴 can use a portion of the funds locked with user 𝐵 in channel ch 𝐴𝐵 to open a new virtual payment channel ch 𝐴𝐶 with party 𝐶 (given that parties 𝐵 and 𝐶 also have a payment channel ch 𝐵𝐶 ). This construction can be used recursively to build hierarchies of virtual channels as depicted in Figure 11. Some virtual channel constructions [START_REF] Aumayr | Bitcoin-compatible virtual channels[END_REF]] can only guarantee security if the closure of a virtual payment channel also initiates the closure of all underlying channels. This property has been identified in [START_REF] Aumayr | Breaking and Fixing Virtual Channels: Domino Attack and Donner[END_REF] to give rise to the Domino Attack: an attacker can create a hierarchy of virtual channels and make the whole channel hierarchy collapse-forcing also the closure of channels between honest users. In the example, in Figure 11, user 𝐴 and 𝐷 can collude to close the channel ch 𝐵𝐷 between honest users 𝐵 and 𝐶. To this end they first create ch 𝐴𝐶 based on ch 𝐴𝐵 and then channel ch 𝐴𝐷 leveraging ch 𝐴𝐶 . Closing ch 𝐴𝐷 1 will force party 𝐶 to close ch 𝐴𝐶 (and ch 𝐶𝐷 ) 2 and this again will force 𝐵 to close ch 𝐵𝐶 (and ch 𝐴𝐵 ) 3 . Even though honest users are guaranteed not to lose channel funds in such an attack, they still need to cover the cost of closing and reopening their channels-both of which require the publication of transactions.

The absence of the domino attack, hence, is a desirable property that can be achieved by the virtual channel construction presented in [START_REF] Aumayr | Breaking and Fixing Virtual Channels: Domino Attack and Donner[END_REF]]. It can be formulated as a hyperproperty that we call here virtual channel stability: for all channels ch and all executions 𝜋 1 where ch is closed, there exists an execution 𝜋 2 closing ch where all channels ch ′ (ch ≠ ch ′ ) between honest users remain open.

In our model, at a high level of abstraction, a virtual channel can be seen as a local blockchain only readable by some participants. We, therefore, refer to the axiomatisation provided in Section 2.

RELATED WORK

Dolev-Yao Models. Symbolic models, inspired by early works of Dolev and Yao [Dolev and Yao 1983], support a large range of languages for specifying protocols and security properties. Among the most popular protocol languages, one may cite:

(1) the applied 𝜋-calculus as in the ProVerif tool [START_REF] Blanchet | Automatic Cryptographic Protocol Verifier, User Manual and Tutorial[END_REF] which is a calculus of communicating concurrent processes; and (2) multiset rewrite rules as in the Tamarin tool [START_REF] Basin | Tamarin prover manual[END_REF] which is a formalism defining protocols as transition systems.

To make our results mostly independent of the specification language, we designed our framework to subsume most of their features. Existing tools also usually focus on reachability properties formalised in variants of (temporal) first-order logics, commonly including a notion of guarded quantifiers as ours [START_REF] Basin | Tamarin prover manual[END_REF]. The notable exception is indistinguishability properties, formalising security as an equivalence between two processes, modelling strong flavours of privacytype properties [START_REF] Rakotonirina | Efficient verification of observational equivalences of cryptographic processes: theory and practice[END_REF]]. They may be seen as a variant of the non-interference of HyperCTL* [Clarkson et al. 2014], although significantly more complex due to non-determinism, and as the notion is defined for an adversary actively controlling communications. Regarding automation, the bounded case has seen numerous decidability and complexity results [START_REF] Chadha | Automated verification of equivalence properties of cryptographic protocol[END_REF][START_REF] Cheval | Deciding equivalence-based properties using constraint solving[END_REF]Cheval et al. , 2018Cheval et al. , 2020a;;Durgin et al. 2004;Kanovich et al. 2014;Liu and Lin 2012;[START_REF] Rusinowitch | Protocol insecurity with a finite number of sessions, composed keys is NP-complete[END_REF]. The underlying procedures often rely on an abstraction of the system using a symbolic semantics, similarly to us. One may also mention different lines of work such as the DY ★ framework [START_REF] Bhargavan | DY ★ : A Modular Symbolic Verification Framework for Executable Cryptographic Protocol Code[END_REF]. It proposes a method to specify and prove symbolic properties in the F ★ proof assistant.

Although some approaches exist to handle relational properties within F ★ [START_REF] Barthe | Probabilistic relational verification for cryptographic implementations[END_REF], it is unclear how to adapt this to DY ★ whose proof machinery (relying on establishing trace invariants) is heavily specialised in trace properties.

Hyperproperties. Hyperproperties have been increasingly popular in the context of verification, often expressed in variants of the temporal logic HyperCTL* [Clarkson et al. 2014]. It considers finite-state systems whose traces are infinite sequences of transitions. The logic can then perform arbitrary quantifications over traces, and then expresses properties through a classical temporal logic. This contrasts with standard Dolev-Yao frameworks, which consider traces that are finite in length, but where each step may branch to infinitely-many potential states due to unbounded adversary operating in parallel to the system. Our framework is rooted in the latter, but we use a logic, Hypertidy CTL* [START_REF] Barthe | Tidy: Symbolic Verification of Timed Cryptographic Protocols[END_REF]], whose design is heavily inspired by HyperCTL*.

An important aspect of logics for specifying protocol properties is how to state facts about the adversary, typically to express properties such as secrecy ("in any trace of the system, the adversary has no way to compute a certain secret piece of data 𝑠"). This is usually done using a "knowledge" predicate K(𝑠) as in this paper. Notions of knowledge have also been considered in finite-state systems using, e.g., epistemic-logic approaches [START_REF] Balliu | Epistemic temporal logic for information flow security[END_REF]Coenen et al. 2019], but they do not account for the active adversary. One may still note that epistemic models of knowledge have also been marginally studied in Dolev-Yao models [START_REF] Mario | Tableaux Calculus for Dolev-Yao Multi-Agent Epistemic Logic[END_REF].

Several other extensions of temporal logics somehow bring them closer to the adversarial setting needed for our applications, although never accounting for all necessary features. A recent extension considers for example quantifications over sets of traces [START_REF] Beutner | Second-order hyperproperties[END_REF], thus capturing more complex epistemic properties as the previously-cited references, such as common knowledge (which is orthogonal to our contributions). Other extensions also consider limited parts of what is the basis of Dolev-Yao models. Typically, [START_REF] Beutner | A Logic for Hyperproperties in Multi-Agent Systems[END_REF] formalises hyperproperties in the presence of multiple agents (natively included by the concurrent nature of Dolev-Yao models); [Coenen et al. 2022;[START_REF] Beutner | Second-order hyperproperties[END_REF]] introduce forms of function symbols (but do not support mechanisms for specifying cryptographic properties); and [Hsu et al. 2023] adds support for asynchronous communications (the standard mode of communication in Dolev-Yao models) and de-synchronised behaviours across multiple traces (implicitly captured by the fact that the Hypertidy CTL* logic for Dolev-Yao hyperproperties supports real-time). They thus capture applications from concurrency theory such as linearisability, or security properties in the presence of an adversarial scheduler, but do not support the standard adversary in protocol analysis which fully controls communications by intercepting, forging, and injecting messages.

Finally, let us mention that existing work on the proof automation of hyperproperties in Hy-perCTL* tends to be limited to the fragment HyperLTL [START_REF] Beutner | Second-order hyperproperties[END_REF]Coenen et al. 2022;[START_REF] Beutner | Second-order hyperproperties[END_REF]. Some approaches also commonly struggle with quantifier alternation, the fragment ∀ * ∃ * being a common limit [START_REF] Beutner | Second-order hyperproperties[END_REF]]. Our results are not subject to these restrictions, and support in particular arbitrary alternation of (nested) quantifiers.

Verification of Smart Contracts. As we show several application cases of our decidability result in the field of blockchain and smart contracts, we briefly review some related results on their verification. Most existing work on smart contract verification is concerned with functional contract correctness usually phrased as trace properties [START_REF] Ahrendt | Functional Verification of Smart Contracts via Strong Data Integrity[END_REF]Marescotti et al. 2020;Permenev et al. 2020;[START_REF] Stephens | SmartPulse: Automated Checking of Temporal Properties in Smart Contracts[END_REF]]. [Grishchenko et al. 2018] defines multiple generic non-interference-style integrity properties for smart contracts that aim at ruling out prominent attack classes (see call integrity in Section 7.3). Some of them can be verified with the help of a local dependency analysis of the contract code that soundly models the contract's control and data dependencies [Holler et al. 2023]. The call integrity property does not fall into this class of properties but is shown in [Grishchenko et al. 2018] to be soundly over-approximated by a reachability property and two other local dependency properties. Correspondingly, it can be verified using tools supporting sound local dependency analysis [Holler et al. 2023] and sound reachability analysis [START_REF] Schneidewind | eThor: Practical and Provably Sound Static Analysis of Ethereum Smart Contracts[END_REF]] for smart contracts. [Grossman et al. 2017] presents an alternative approach to characterising the absence of reentrancy attacks by defining effective callback freedom (ECF) (see Section 7.3). [START_REF] Albert | Taming callbacks for smart contract modularity[END_REF] shows a verification technique for ECF that relies on the exploitation of commutative properties of contract code segments. The verification approaches for local dependency properties, call integrity and ECF have in common that they are tailored to the concrete properties and correspondingly narrow in scope. These techniques, in particular, overapproximate only those aspects of the attacker's behaviour that are relevant to the property under verification. Further, they do not account for the usage of cryptography.

[ Coenen et al. 2022] provides examples of hyperproperties in the context of smart contracts, and presents a procedure for synthesising contracts satisfying them. Hyperproperties are expressed in HyperTSL, a generalisation of temporal stream logic (TSL) to support hyperproperties. Examples include symmetry and determinism notions for voting and auction contracts. Even though Hy-perTSL supports uninterpreted function symbols and predicates, there is no support for symbolic cryptography or real-time. Also, this synthesis technique is restricted to all-quantified formulae.

CONCLUSION AND FUTURE WORK

We provided the first decidability and (tight) complexity results for a large fragment of hyperproperties in contexts involving active adversaries. Our results apply to an expressive class of processes supporting arithmetic computations, cryptography, concurrency and stateful programs. The main open problem left by our contribution is the generalisation of our decidability result to the full Hypertidy CTL* logic, as our fragment (guarded hyperformulae) excludes classical notions of adversarial indistinguishability. Although such properties are already well-studied, and got a certain automated support [START_REF] Blanchet | Automatic Cryptographic Protocol Verifier, User Manual and Tutorial[END_REF]Cheval et al. 2020b], it is still open how existing proof techniques would interact with our decision procedure and its complexity.

Another point would be the implementation of our procedure, as we focused here on pinpointing its exact complexity using a theoretical alternating algorithm. As practical examples (see Section 7) rarely involve more than 2 or 3 path quantifications, we conjecture the theoretical EXPH(poly) to be rather pessimistic, compared to how actual verifiers could perform in practice when implementing our HCompute function. Similarly, the EXPH(poly) hardness proved in [START_REF] Barthe | Tidy: Symbolic Verification of Timed Cryptographic Protocols[END_REF]] relies on rather degenerate examples, whose term algebra model binary trees to force the adversary into performing computations of exponential size. On the contrary, although attacks on practical protocols are tedious to find by hand, the adversarial computations they involve are arguably rather of linear size in the protocol's description. The reason is that, most of the time, their objective is precisely to impersonate or imitate some actions of honest instances of the specification, and this is done by combining messages from a small number of sessions. Similar observations arose in related tools such as DeepSec [Cheval et al. 2020b] which, although exhibiting a prohibitive coNEXP theoretical complexity, performs surprisingly well by relying on practical optimisations exploiting the relative simplicity of practical examples compared to the fully-general case [Cheval et al. 2019]. However, at this point, our contribution is mostly theoretical and a non-negligible engineering effort would still be necessary to design and implement such techniques, leaving the experimental evaluation of our procedure as a challenging future work.

A COMPLEXITY THEORY (PRELIMINARIES)

In this section, we recall standard notions of computational complexity theory, used across the paper. We focus in this paper on worst-case complexity.

A.1 Basic Notions

Time and Space. Given 𝑓 : N → N, we define TIME(𝑓 (𝑛)) (resp. SPACE(𝑓 (𝑛))) to be the class of problems decidable by a deterministic Turing machine running in time (resp. in space) at most 𝑓 (𝑛) for input tapes of length 𝑛. In particular:

• P = 𝑝 ∈N TIME(𝑛 𝑝 ) is the class of problems decidable in polynomial time;

• PSPACE = 𝑝 ∈N SPACE(𝑛 𝑝 ) is the class of problems decidable in polynomial space;

• their exponential analogues are

EXP = 𝑝 ∈N TIME(2 𝑛 𝑝 ), EXPSPACE = 𝑝 ∈N SPACE(2 𝑛 𝑝 ).
When considering non-deterministic Turing machines instead of deterministic ones as above, we add a "N" prefix to the name of the class, leading, e.g., to NP (non deterministic polynomial time) and NEXP (non deterministic exponential time). Given a (non-deterministic) class C, we call coC the class of problems whose negation is in C.

Complete Problems. We say that a problem is complete for a class C if any problem of C can be reduced to this problem. In this paper, the notion of reduction used is the standard many-to-one polynomial-time reduction. We assume some familiarity of the reader with the underlying notions, and with the prototypical complete problem for NP (SAT or 3-SAT).

Alternation. We also recall that alternating Turing machines are non-deterministic Turing machines whose states are partitioned between universal states (or ∀-states) and existential states (or ∃-states). An execution from a universal (resp. existential) state is then accepting iff any (resp. at least one) execution from this state accepts. In particular, non-deterministic Turing machines are alternating Turing machines with only existential states, whereas arbitrary alternation of types of states is allowed in general. We add a "A" prefix to express that we consider alternating Turing machines, e.g., AP is the class of problems decidable in alternating polynomial time. Typical known relations between these classes include:

P ⊆ NP,coNP ⊆ PSPACE = NPSPACE = AP ⊆ EXP EXP ⊆ NEXP,coNEXP ⊆ EXPSPACE = AEXP A.

Polynomial and Exponential Hierarchies

The gap between NP and PSPACE = AP is intuitively alternation, as NP may be seen as the class of problems decidable in polynomial time by alternating machines with only existential states. Intermediary levels of alternation characterise a whole hierarchy of alternation-bounded complexity classes between NP and PSPACE, called the polynomial hierarchy PH. We reference in this paper in the analogue hierarchy between NEXP and EXPSPACE (exponential hierarchy), the highest level of which being however more refined (depending on whether arbitrary, or only a polynomial number of, alternations are allowed). For simplicity, we only provide here the usual characterisation of the class we are interested in, EXPH(poly):

Proposition A.1. EXPH(poly), called the polynomially-bounded exponential hierarchy, is the class of problems decidable in exponential time by alternating Turing machines with a polynomial number of alternations. We have:

EXP ⊆ EXPH(poly) ⊆ EXPSPACE

B EXPRESSIVITY OF THE FRAMEWORK

Our presentation focuses on expressivity with minimal syntax, to simplify our proofs while making our decidability results applicable to a large class of protocol features. However, for readability, the concrete examples presented throughout the paper relied on additional convenient features that can be encoded in our minimal theoretical core. for two events Equal and NotEqual. When proving a hyperproperty phi, it then suffices to replace all path quantifiers forall pi:trace. psi appearing in phi by forall pi:trace. PEq(pi) => PNotEq(pi) => psi where PEq and PNotEq are defined in Figure 12. Also, as detailed in Section 3.2, Example 3.1, our original syntax for global state can encode notions of mutable cells or arrays. Simple note that, given for example a mutable table 𝑇 encoded this way as in the running example, the state of 𝑇 can be accessed in hyperproperties by using the GS atomic formula of the logic. It can also be used to perform pattern matching; given a dedicated symbol match taking two arguments, the following process: new k : push match(u,k) : pull match(f(x),k) : P only proceeds to execute P if the term u is of the form f(x) (assuming a unary function symbol f in the term algebra), and binds x to the corresponding term in P. This can easily be generalised to arbitrary pattern matchings of constructors or to patterned let bindings, see [START_REF] Cheval | Sapic+ : protocol verifiers of the world, unite![END_REF] for details of such encodings.

By composing push and pull instructions atomically, one can more generally encode multiset rewrite rules as used in, e.g., the Tamarin prover. Such rules constitute an alternative specification formalism for processes, operating on a global state similar to ours through rules of the form:

[𝑢 1 , . . . , 𝑢 𝑛 ] -[Ev 1 , . . . , Ev 𝑝 ]→ [𝑣 1 , . . . , 𝑣 𝑞 ] .
Here 𝑢 𝑖 , 𝑣 𝑗 can be seen as terms (except for special cases representing inputs, outputs, or new operations), and Ev 𝑘 event terms. This rule as the effect of removing all terms 𝑢 𝑖 from the multiset, adding all terms 𝑣 𝑗 afterwards, and flagging this operation with the Ev 𝑘 events. This can be simulated in our framework by: pull 𝑢 1 :

• • • : pull 𝑢 𝑛 : Ev 1 : • • • : Ev 𝑝 : push 𝑣 1 : • • • push 𝑣 𝑞 .
In case of special instructions, pull may be substituted by inputs or new instructions, and push by outputs. Using this, any feature encodable using multiset rewrite rules can be encoded, e.g. referring to [START_REF] Cheval | Sapic+ : protocol verifiers of the world, unite![END_REF]Kremer and Künnemann 2016], associative maps or state passing. Going further, dialects of the applied 𝜋-calculus [START_REF] Blanchet | Automatic Cryptographic Protocol Verifier, User Manual and Tutorial[END_REF]] usually offer more communication features such as explicit communication channels, and internal communications (synchronous message transfer without adversarial interference). Channels can easily be encoded in our framework by atomically composing events to inputs or outputs. Internal communications can also be simulated by sending messages through the global state, and thereafter pulling an acknowledgment of receipt before proceeding. This multiple-step encoding is equivalent to fully synchronous variants, at least in models without real time (see, e.g., the correct translation of [Kremer and Künnemann 2016]). In our framework, it yields time-desynchronised internal communications, that is, the output and the input are not executed at the same timestamp. This is however, in our opinion, arguably more realistic as it avoids artificial time synchronisations between parallel processes. One may then also encode within security properties, thanks to our atomic-composition syntax, various channel and communication features of interest. This includes, e.g., public communications only allowed on compromised channels, internal communications only with matching channels, resilient channels [START_REF] Backes | A novel approach for reasoning about liveness in cryptographic protocols and its application to fair exchange[END_REF], or variations of the semantics of internal communications [START_REF] Babel | On the semantics of communications when verifying equivalence properties[END_REF]]. This makes our decidability results largely independent of the framework's details.

C PROOF OF UNDECIDABILITY C.1 Reduction From Two-Counter Machines

Restricted Model. In this section, we study the general undecidability of the Verif problem stated in Section 4.1: Proposition 4.1 (Verification of arbitrary processes). Verif is undecidable even when F c = F pub = {h/1}, F d and R are empty, and 𝜑 is a tidy LTL formula.

We prove that under the restrictions of the above proposition, the model can be used to encode two-counter machines, a classical Turing-complete computation model [Minsky 1967]. In particular, the verification of tidy LTL will easily encode (undecidable) reachability problems such as the halting problem. This may however be seen as a shallow statement, as our calculus notably supports shared global states (which can trivially encode counters, even without a free symbol h/1). To emphasise the minimality of this undecidability result, in particular in common models not supporting global states, real-time, or atomic composition [Cheval et al. 2018], we will strengthen it with the following restrictions:

(1) we use an untimed model, that is, no when instructions nor timestamps @𝑡;

(2) we do not use global states except for simulating internal communications (see, e.g., [Kremer and Künnemann 2016] for a detailed encoding). We therefore do not use push, pull, and unfound instructions, except to encode instructions of the form out(𝑒, 𝑢); 𝑃 ≜ Out(𝑒) : push 𝑢; Ack : 𝑃 in(𝑒, 𝑥); 𝑃 ≜ In(𝑒) : pull 𝑥; 𝑃 where 𝑒 ∈ N priv is called a private channel (and should appear in any output messages), and Out, In ∈ F 𝑒 . This models the sending of a message 𝑢 on a private communication channel 𝑒, synchronously received as a variable 𝑥, only after what the outputting process may proceed (event Ack). Synchronicity is in particular modelled by the following formula:

𝜑 sync = G (∀𝑒.Out(𝑒) ⇒ 𝜏 𝜋 U In(𝑒) 𝜋 )
for some path variable 𝜋 (always clear from context in the tidy LTL fragment). In particular, in reference to naming conventions for internal communications [START_REF] Barthe | Tidy: Symbolic Verification of Timed Cryptographic Protocols[END_REF][START_REF] Blanchet | Automatic Cryptographic Protocol Verifier, User Manual and Tutorial[END_REF]Cheval et al. 2018], we call "Rule (Comm)" the execution of a Out(𝑒) : push 𝑢, followed by a In(𝑒) : pull 𝑥 and see it, for simplicity, as a single transition step;

(3) we do not make use of atomic composition, that is, all non-skip instructions are always followed by a semi-column (i.e., an implicit skip), except in the above encoding.

Reduction. Intuitively, two-counter machines consist of:

• two counters that can be seen as two (unbounded) registers, by convention initialised to 0, and that may contain arbitrary natural numbers; • a finite set of labelled instructions, that may increment or decrement counters, test whether its content is zero, and/or jump to the label of a subsequent instruction.

We use the following formalisation of two-counter machines.

Definition C.1 (Two-counter machines). A two-counter machine 𝑀 = (𝐿, 𝐼, ℓ 0 ) consists of a finite set of so-called labels 𝐿 including the initial label ℓ 0 ∈ 𝐿, and a finite set of instructions 𝐼 that may be of either of the following three forms: halt incr(𝑐, ℓ) zdecr(𝑐, ℓ 0 , ℓ -)

where ℓ, ℓ 0 , ℓ -∈ 𝐿 and 𝑐 is either of the two so-called registers c 1 , c 2 . We assume an implicit bijective mapping between 𝐿 and 𝐼 , and write 𝑀 [ℓ] to refer to the instruction mapped to the label ℓ.

Intuitively, halt is a terminated program and incr(𝑐, ℓ) increments the counter 𝑐 and then executes 𝑀 [ℓ]. The instruction zdecr(𝑐, ℓ 0 , ℓ -) is a compact construction that tests whether the content of the counter 𝑐 is zero (in which case 𝑀 [ℓ 0 ] is executed), or not (in which case the counter 𝑐 is decremented, and 𝑀 [ℓ -] is executed). This is formalised by the following notion of execution: Definition C.2 (Termination of a two-counter machine). A state of a two-counter machine 𝑀 = (𝐿, 𝐼, ℓ 0 ) is a tuple (𝑛 1 , 𝑛 2 , ℓ) ∈ N × N × 𝐿. We then define a transition relation → 𝑀 over states of 𝑀 as the smallest binary relation such that for all ℓ ∈ 𝐿 and 𝑛 1 , 𝑛 2 ∈ N:

• if 𝑀 [ℓ] = incr(c 1 , ℓ ′ ) then (𝑛 1 , 𝑛 2 , ℓ) → 𝑀 (𝑛 1 + 1, 𝑛 2 , ℓ ′ ); • if 𝑀 [ℓ] = incr(c 2 , ℓ ′ ) then (𝑛 1 , 𝑛 2 , ℓ) → 𝑀 (𝑛 1 , 𝑛 2 + 1, ℓ ′ ); • if 𝑀 [ℓ] = zdecr(c 1 , ℓ 0 , ℓ -) then -(0, 𝑛 2 , ℓ) → 𝑀 (0, 𝑛 2 , ℓ 0 ); -(𝑛 1 + 1, 𝑛 2 , ℓ) → 𝑀 (𝑛 1 , 𝑛 2 , ℓ -); • if 𝑀 [ℓ] = zdecr(c 2 , ℓ 0 , ℓ -) then -(𝑛 1 , 0, ℓ) → 𝑀 (𝑛 1 , 0, ℓ 0 ); -(𝑛 1 , 𝑛 2 + 1, ℓ) → 𝑀 (𝑛 1 , 𝑛 2 , ℓ -);
We say that 𝑀 terminates if there exists a sequence of → 𝑀 -transitions from (0, 0, ℓ 0 ) to a state of the form (𝑛 1 , 𝑛 2 , ℓ), 𝑀 [ℓ] = halt.

The undecidability of the termination of two-counter machines easily follows from the Turingcompleteness of this computation model. We will then prove the Proposition 4.1 by constructing, given a two-counter machine 𝑀, a process 𝑃 𝑀 and a tidy LTL formula 𝜑 such that 𝑃 𝑀 |= 𝜑 iff 𝑀 does not terminate. Let thus 𝑀 = (𝐿, 𝐼, ℓ 0 ) be an arbitrary two-counter machine. We recall that the term algebra contains a unary symbol h. For readability, we will write multiple applications of h to a term h 𝑛 (𝑢), that is, h 0 (𝑢) = 𝑢 and h 𝑛+1 (𝑢) = h(h 𝑛 (𝑢)). Intuitively, we will encode each counter c 𝑖 by two terms of the form, respectively, h 𝑛 and h 𝑝 , 𝑛 ⩾ 𝑝, the value of the counter being the difference 𝑛 -𝑝. Therefore, applying h to the first term increments the counter, applying h to the second term decrements the counter, and testing the equality of the two terms tests whether the counter is null. The four terms (two for each of the two counters) are then carried over the execution of the program using private channels ℓ corresponding to the labels of 𝐿.

Formally, for each label ℓ ∈ 𝐿, we associate a fresh name 𝑐 ℓ ∈ N priv . We also construct, for each ℓ ∈ 𝐿, a process (using the previous syntactic sugar for internal communications) 𝑃 ℓ = in(𝑐 ℓ , 𝑥 + 1 ); in(𝑐 ℓ , 𝑥 - 1 ); in(𝑐 ℓ , 𝑥 + 2 ); in(𝑐 ℓ , 𝑥 - 2 ); 𝑄 ℓ where the process 𝑄 ℓ is defined in Figure 13, assuming three events Zero/2, Pos/2, Halt/0.

We also define an initialisation process, given a 𝑧 ∈ F 0 :

𝑃 0 = out(𝑐 ℓ 0 , 𝑧); out(𝑐 ℓ 0 , 𝑧); out(𝑐 ℓ 0 , 𝑧); out(𝑐 ℓ 0 , 𝑧); 0

The overall process is then:

𝑃 𝑀 = 𝑃 0 | ℓ ∈𝐿 ! 𝑃 ℓ 𝑇 𝑖 = 𝑇 1 𝑖 • 𝑇 2
𝑖 where 𝑇 1 𝑖 ,𝑇 2 𝑖 are non-empty, 𝑇 1 𝑖 contains no (Repl) transitions, and 𝑇 2 𝑖 contains only (Repl) transitions. Note that this decomposition, when it exists, is unique.

The first step of the proof is to reduce the analysis to normal traces, which is done by the following result. We write 𝜓 the formula such that 𝜑 = ∀𝜋 . 𝜓 , that is,

𝜓 = 𝜑 sync ⇒ 𝜑 Zero ⇒ 𝜑 Pos ⇒ G ¬Halt 𝜋
In the following, we also let P 𝑀 = (P, ∅) be a normal extended process of the form:

P = {{𝑄 ℓ 0 𝜎 0 }} ∪ P 0 ∪ {{! 𝑃 ℓ ′ }} ℓ ′ ∈𝐿
= {𝜀 ↦ → 𝑇 , 𝜋 ↦ → 𝑇 }.
Proof. First of all, note that all processes of the form P 𝑀 are obtained from 𝑃 𝑀 by applying, up to reordering, Rule (Par) as many times as possible, Rule (Repl) at least |𝐿| + 1 times, and Rule (Comm) four times between 𝑃 0 and a copy of 𝑃 ℓ 0 . Conversely, all processes obtained after applying such transitions from 𝑃 𝑀 in any order are of the same form as P 𝑀 , up to the addition of enough (Repl) transitions (and adding such transitions does not prevent subsequent independent transitions from being executed). We hence obtain that 𝑃 𝑀 |= 𝜑 iff for all traces 𝑇 of P 𝑀 , Π 𝑇 |= 𝜓 . Without loss of generality, we only consider traces 𝑇 that does not start with a (Repl) transition (as initial (Repl) transitions only yield normal extended processes of the same form as P 𝑀 ).

Our goal is to prove that it is sufficient to limit this quantification to normal traces P 𝑀 . For that, given an arbitrary normal extended process 𝐴 0 , let us assume par contraposition that there exists a trace 𝑇 , non-necessarily normal but not starting with a (Repl) transition, written

𝑇 : 𝐴 0 𝛼 1 --→ • • • 𝛼 𝑛 --→ 𝐴 𝑛 such that Π 𝑇 |= 𝜑 sync ∧ 𝜑 Zero ∧ 𝜑 Pos ∧ F Halt 𝜋 .
We then have to show that there exists a normal trace 𝑇 𝑁 of 𝐴 0 (also not starting with a (Repl) transition) such that

Π 𝑇 𝑁 |= 𝜑 sync ∧ 𝜑 Zero ∧ 𝜑 Pos ∧ F Halt 𝜋 .
We prove the result by well-founded induction on 𝑛 -𝑖 ⩾ 0, where 𝑛 is the length of the trace, and 𝑖 is the maximal index such that 𝐴 0 ---→ 𝐴 𝑖+1 is derived by Rule (Repl). Indeed in this case, either 𝑖 = 0 and this is in contradiction with the assumption that 𝑇 does not start with a (Repl) transition, or 𝑖 > 0 and we write the decomposition

𝛼 1 --→ • • • 𝛼 𝑖 -→ 𝐴 𝑖 that
(𝐴 0 𝛼 1 --→ • • • 𝛼 𝑖 -→ 𝐴 𝑖 ) = 𝑇 1 • • •𝑇 𝑘 obtained by Definition C.4, then 𝑇 1 • • •𝑇 𝑘 -1 • 𝑇 ′ 𝑘 with 𝑇 ′ 𝑘 = 𝑇 𝑘 • (𝐴 𝑖 𝛼 𝑖+1 ---→ 𝐴 𝑖+1 )
would be a decomposition of 𝐴 0

𝛼 1 --→ • • • 𝛼 𝑖+1
---→ 𝐴 𝑖+1 proving that it is also a normal trace, which is in contradiction with the maximality of 𝑖. Let us thus assume that this transition is derived by any other rule than (Repl). Additionally, we also emphasise that no event Halt could have been executed during the normal trace 𝐴 0

𝛼 1 --→ • • • 𝛼 𝑖 -→ 𝐴 𝑖 .
Otherwise, due to the form of normal traces, no further 𝛼 -→ transitions should have been possible after the execution of this event, except by Rule (Repl)-case excluded above.

Note that this also excludes the case S = ∅ (blank normal process), since only (Repl) transitions are possible from such a process. Therefore S = {{𝑄 ℓ 𝜎 }} (regular normal process), and we perform a case analysis on 𝑀

[ℓ]. ▶ Case 1: 𝑀 [ℓ] = halt.
Since the transition 𝐴 𝑖 𝛼 𝑖+1

---→ 𝐴 𝑖+1 is not derived by Rule (Repl), and due to the form of normal extended processes, this transition must be the instance of Rule (Event) executing the event Halt of 𝑄 ℓ . In particular, 𝐴 𝑖+1 would be a (blank) normal extended process, in contradiction with the maximality of 𝑖. ▶ Case 2: 𝑀 [ℓ] = zdecr(c 1 , ℓ 0 , ℓ -).

Since 𝐴 𝑖 𝛼 𝑖+1

---→ 𝐴 𝑖+1 is not derived by Rule (Repl), and due to the form of normal extended processes, this transition must be the instance of Rule (Choice) executing either event at toplevel of 𝑄 ℓ 𝜎 (Zero(𝑥 + 1 𝜎, 𝑥 - 1 𝜎) or Pos(𝑥 + 1 𝜎, 𝑥 - 1 𝜎)). Let us assume that the event Zero is executed by this transition (the argument in the case of Pos is analogue). In this case we have 𝐴 𝑖+1 = (Q, ∅), with

Q = {{𝑄𝜎 }} ∪ P 0 ∪ {{! 𝑃 ℓ ′ }} ℓ ′ ∈𝐿
where 𝑄 is defined by 𝑄 0 ℓ = event Zero(𝑥 + 1 , 𝑥 - 1 ); 𝑄. In particular, 𝑄𝜎 has four outputs at toplevel (on the private channel 𝑐 ℓ 0 ), while all other processes of Q are either 0, or have either four inputs or a replication followed by four inputs, all on private channels. In particular, in the trace

𝐴 𝑖 𝛼 𝑖+1 ---→ • • • 𝛼 𝑛 --→ 𝐴 𝑛 , if
the outputs of 𝑄𝜎 are either not all used in internal communications, or used in internal communications with inputs of two different processes of Q, it is straightforward to see that this trace may only contain up to three instances of Rule (Comm) and an arbitrary number of Rule (Repl) (in particular, no Halt event). This would be in contradiction with the hypothesis that Π 𝑇 ⊨ F Halt 𝜋 since, as discussed before case 1, the Halt event cannot occur in the prefix trace

𝐴 0 𝛼 1 --→ • • • 𝛼 𝑖 -→ 𝐴 𝑖 .
But in addition, we already excluded the case where the transition 𝐴 𝑖 𝛼 𝑖+1 ---→ 𝐴 𝑖+1 is derived by Rule (Repl), meaning that it must be an internal communication, necessarily between 𝑄𝜎 and a copy of 𝑃 ℓ 0 ∈ P 0 . As a conclusion, we obtain that there exist four internal communications between 𝑃 ℓ and 𝑄𝜎 in the trace 𝐴

𝑖 𝛼 𝑖+1 ---→ • • • 𝛼 𝑛 --→ 𝐴 𝑛 . Therefore, we can write 𝐴 ′ 𝑖 𝛽 𝑖+1 ---→ • • • 𝛽 𝑛+|𝐿| ----→ 𝐴 ′ 𝑛+|𝐿 | the trace obtained from 𝐴 𝑖 𝛼 𝑖+1 ---→ • • • 𝛼 𝑛 --→ 𝐴 𝑛 by:
(1) moving the four internal communications between 𝑃 ℓ and 𝑄𝜎 in front, i.e., as the first four actions;

(2) adding, as the 5 th to 5 + |𝐿| th actions, instances of Rule (Repl) unfolding one copy of each 𝑃 ℓ , ℓ ∈ 𝐿; (3) from the 6 + |𝐿| th action onwards, leave all remaining transitions of 𝐴

𝑖 𝛼 𝑖+1 ---→ • • • 𝛼 𝑛 --→ 𝐴 𝑛 in the same order.
Note that the permutation done in the first step is possible due to the form of the processes (see discussion right above Case 2.1). Overall, we writing 𝑇 ′ the reordered trace We omit the proofs for all remaining cases, as they are either analogue to case 2 (decrement of c 2 ), or only require a similar but much simpler argument (increment). □

𝑇 ′ : 𝐴 0 𝛼 1 --→ • • • 𝛼 𝑖 -→ (𝐴 𝑖 = 𝐴 ′ 𝑖 ) 𝛽 𝑖+1 ---→ • • • 𝛽 𝑛+|𝐿| ----→ 𝐴 ′ 𝑛+|𝐿 | we have Π 𝑇 ′ |= 𝜑 sync ∧ 𝜑 Zero ∧ 𝜑 Pos ∧ F
Building on this characterisation of 𝜑 restricted to normal traces, we prove the proposition by double implication. For that we introduce a natural mapping between regular normal extended processes and two-counter-machine states. With the notations of Definition C.3, if 𝐴 = (P, ∅) is a regular normal extended process with

P = {{𝑄 ℓ 𝜎 }} ∪ P 0 ∪ {{! 𝑃 ℓ ′ }} ℓ ′ ∈𝐿
then we associate to it the tuple

𝐴 = (𝑛 + 1 -𝑛 - 1 , 𝑛 + 2 -𝑛 - 2 , ℓ) with 𝑥 𝑠 𝑖 𝜎 = h 𝑛 𝑠 𝑖 (𝑧)
Note that such a tuple is not necessarily a well-formed two-counter machine state (it is one iff

𝑛 + 1 ⩾ 𝑛 - 1 and 𝑛 + 2 ⩾ 𝑛 - 2 ). Lemma C.3 (Proposition C.1, forward direction). If 𝑃 𝑀 |= ∃𝜋 .𝜑 Zero ∧ 𝜑 Pos ∧ F Halt 𝜋 then 𝑀 terminates.
Proof. Let us assume that there exists a trace 𝑇 of 𝑃 𝑀 such that Π 𝑇 |= 𝜑 Zero ∧ 𝜑 Pos ∧ F Halt 𝜋 . By lemma C.2, we can assume that 𝑇 is a normal trace without loss of generality. Let us thus consider the decomposition 𝑇 = 𝑇 1 • • •𝑇 𝑛 with the notations of Definition C.4, with in particular 𝐴 𝑖 -1 the first extended process of 𝑇 1 𝑖 . We then prove that for all 𝑖 ∈ 0, 𝑛 -1 , 𝐴 𝑖 is a (well-defined) two-counter machine state that is → 𝑀 -reachable from (0, 0, ℓ 0 ). This will conclude the proof since 𝐴 𝑛-1 is a halting configuration.

The conclusion is immediate in the case 𝑖 = 0, since 𝐴 0 = (0, 0, ℓ 0 ). In the case 𝑖 > 0, we know by induction hypothesis that 𝐴 𝑖 -1 is → 𝑀 -reachable from (0, 0, ℓ 0 ), and it therefore suffices to prove that 𝐴 𝑖 -1 → 𝐴 𝑖 . Since 𝐴 𝑖 -1 is a by definition a (regular) normal extended process, we can write 𝐴 𝑖 -1 = (P, ∅) with

P = {{𝑄 ℓ 𝜎 }} ∪ P 0 ∪ {{! 𝑃 ℓ ′ }} ℓ ′ ∈𝐿
with the notations of Definition C.3. The conclusion then follows from a quick case analysis on the instruction 𝑀 [ℓ] (using in particular that Π

𝑇 |= 𝜑 Zero ∧ 𝜑 Pos ). □ Lemma C.4 (Proposition C.1, converse direction). If 𝑀 terminates then 𝑃 𝑀 |= ∃𝜋 .𝜑 Zero ∧ 𝜑 Pos ∧ F Halt 𝜋 .
Proof. Let us consider a halting run of 𝑀, that is, a sequence 𝑠 0 , . . . , 𝑠 𝑛-1 of states of 𝑀 such that 𝑠 0 = (0, 0, ℓ 0 ) and 𝑠 𝑛-1 is a halting state. It is then straightforward to construct, by induction on 𝑖, a (normal

) trace 𝑇 = 𝑇 1 • • •𝑇 𝑛 (notations of Definition C.4) such that for all 𝑖 ∈ 0, 𝑛 -1 , Π 𝑇 1 •••𝑇 𝑖+1 |= 𝜑 Zero ∧ 𝜑 Pos
and, if 𝐴 𝑖 is the first (normal) extended process of 𝑇 𝑖+1 , 𝐴 𝑖 is regular and 𝐴 𝑖 = 𝑠 0 . In particular, we also have Π 𝑇 |= F Halt 𝜋 since 𝐴 𝑛-1 = 𝑠 𝑛-1 is a halting state and, as such, the first instruction of 𝑇 𝑛 need be the execution of a Halt event.

□

D SYMBOLIC CONSTRAINT SOLVING

As a first point of this section, we refer to the full symbolic semantics, which can be found in Figure 14. We then define in this section the data structures at the core of our decision procedure, uplifting the notion of constraint systems to a stack of proof states. It intuitively represents a state of a hyperproperty's proof in presence of several nested path quantifications. We also then present various constraint solving algorithm for computing (most general) solutions and a saturated representation of the attacker's knowledge. If C is a hyperconstraint system, we may write 𝜉 ⊩ C,𝜋 𝑢 instead of 𝜉 ⊩ D ( C)∪K ( C),𝜋 𝑢. We also write

conseq 𝜋 (C) = {𝜉 | 𝜉 ⊩ C,𝜋 𝑢} .
Recalling that, by definition of deduction hyperconstraints 𝜉 ⊢ ? 𝜋 𝑢, 𝜉 does not have a constructor symbol at its root, the context 𝐶 of the above definition is uniquely determined. The saturation of a hyperconstraint system C then means that ⊩ C,𝜋 coincides with deducibility from Φ(proj 𝜋 (C)).

The algorithm for solving constraints itself then proceeds by successively computing partial solutions modelling case analyses. For example, consider a hyperconstraint system C and (𝑋 ⊢ ? 𝜋 f (𝑘)) ∈ C, f ∈ F c ∩ F pub and 𝑘 ∈ N priv . The constraint solver therefore has to compute a recipe (𝑋 Σ) deducing f(𝑘) in 𝜋 (i.e., such that 𝑋 Σ ⊩ 𝜋 f(𝑘), assuming C is saturated). The solver will, among others, perform a case analysis on whether the recipe in question has the symbol f at its root or not. For that, it will generate the substitution

Σ f = {𝑋 ↦ → f (𝑌 )}
with 𝑌 ∈ X 2 fresh and of same multiplicity as 𝑋 . Indeed, interpreted as a second-order constraint, this results in the following, effectively modelling the expected case analysis:

Σ f = 𝑋 = ? f (𝑌 ) ¬Σ f = ∀𝑌 .𝑋 ≠ ? f (𝑌 ) .
The solver will then attempt to solve two instances of C, one where Σ f has been applied, and C ∧¬Σ f . In the first case, applying Σ f to C will remove the initial constraint 𝑋 ⊢ ? 𝜋 f(𝑘) from C, replace it by a fresh deduction constraints 𝑌 ⊢ ? 𝜋 𝑦, and add "linking equations" expressing the relations between 𝑋, 𝑌, 𝑦, namely 𝑋 = ? f (𝑌 ) and 𝑦 = ? 𝑘. We formalise this custom notion of application below. Definition D.2 (Solution application). Let C be a hyperconstraint system and Σ be a second-order substitution such that for all 𝑋 ∈ dom(Σ), there exists (𝑋 ⊢ ?

𝜋 𝑢) ∈ D(C), and also for all such (𝑋 ⊢ ?

𝜋 𝑢) ∈ D (C), 𝑋 Σ ∈ conseq 𝜋 (C). The hyperconstraint system C : Σ is called the application of Σ to C, and is defined as follows:

D (C : Σ) = D ′ E 1 (C : Σ) = E 1 (C) ∧ 𝐸 Σ K (C : Σ) = K (C)Σ E 2 (C : Σ) = E 2 (C)Σ ∧ Σ
where we have D ′ = (D (C) ∖ 𝐷 dom ) ∪ 𝐷 fresh as well as the following sets:

(1) deduction constraints resolved by Σ:

𝐷 dom = {(𝑌 ⊢ ? 𝜋 𝑢) ∈ D | 𝑌 ∈ dom(Σ)}
(2) deduction constraints introduced by Σ:

𝐷 fresh = 𝑌 ⊢ ? 𝜋 𝑦 | (𝑋 ⊢ ? 𝜋 𝑢) ∈ 𝐷 dom , 𝑦 fresh, 𝑌 ∈ vars 2 (𝑋 Σ) ∖ vars 2 (C)
(3) linking equations:

𝐸 Σ = 𝑢 = ? 𝑣 | (𝑌 ⊢ ? 𝜋 𝑢) ∈ 𝐷 dom , 𝑌 Σ ⊩ C : Σ,𝜋 𝑣

D.2 Solving Rules

In our procedure, we will then use several sets of constraint-solving procedure:

• solving rules that are used to compute most general solutions of a hyperconstraint system, and more generally put them in a simple form and discard trivial and unsatisfiable constraints; • case analysis rules, that build on solving rules to formalise case analyses in proof stacks.

They typically test whether some combinations of constraints have a solution or not, and saturate the knowledge base of the adversary. The overall procedure will then proceed by induction on the formula to be verified, using case analysis rules at each step to introduce all necessary constraints and solve them.

Simplification Rules. We define solving rules in this section. They build on a preliminary set of simplification rules, defined in Figure 15. These basic set of rules are rather standard, albeit from the one for numeric constraints (which removes deduction constraints involving a numeric variables, as they are always implicitly quantified in the system). Otherwise, the rules simply put (dis)equational constraints into a simple form by computing unifiers. Note that no rules are needed for second-order equations, as they will be specifically handled by the parts of the procedure computing solutions. The simplification rules are then lifted to hyperconstraint systems C in the natural way, by applying the rules to all compatible hyperconstraints of C.

Basic simplifications C ∧ ⊤ ⇝ C C ∧ ⊥ ⇝ ⊥ ded. constraints C ∧ 𝑋 ⊢ ? 𝜋 𝑡 ⇝ C if 𝑡 ∈ X N C ∧ (∀𝑋 .𝑋 ⊬ ? 𝜋 𝑢) ⇝ ⊥ if there is a recipe 𝜉 such that {𝑋 ↦ → 𝜉 } is well-typed, and 𝜉 ⊩ C,𝜋 𝑢 1 st order equations C ∧ 𝑢 = ? 𝑣 ⇝ C ∧ mgu (𝑢 = ? 𝑣) C ∧ 𝑥 = ? 𝑢 ⇝ C𝜎 ∧ 𝑥 = ? 𝑢 assuming 𝜎 = {𝑥 ↦ → 𝑢} is well-typed and 𝑥 ∈ vars 1 (C) ∖ vars 1 (𝑢) 1 st order disequations C ∧ ∀𝑆. 𝜙 ⇝ C ∧ ∀𝑆. ¬𝜎 with 𝜎 = mgu (¬𝜙) ≠ ⊥ C if mgu (¬𝜙) = ⊥ 2 nd order disequations C ∧ ∀𝑆. 𝜙 ⇝          C ∧ ∀𝑆 ∪ 𝑆 ′ .¬Σ with Σ = mgu (¬𝜙) ≠ ⊥ and 𝑆 ′ = vars 2 (img(Σ)) ∖ vars 2 (𝜙) C if mgu (¬𝜙) = ⊥ Time constraints C ∧ C 𝑡 ⇝ ⊥ if C 𝑡 is a conjunction of numeric constraints with no 𝜎 such that C 𝑡 𝜎 holds
Mgs Rules. Building on this set of simplification rules, we define another set of rules used to compute a complete set of most general solutions of a hyperconstraint system C. The overall procedure will typically alternate between such mgs computations (which assume that C has been saturated up to a certain point), and the case analysis rules (using the mgs to perform the said saturation, among others). The goal of the mgs rules is to resolve all deduction constraints 𝑋 ⊢ ? 𝜋 𝑢, i.e., to find a recipe 𝜉 deducing the constructor term 𝑢 (with the correct multiplicity). Assuming saturation, we only consider direct deduction instead of arbitrary deductions; there are therefore only two possible cases:

(1) 𝜉 has a constructor symbol at its root, i.e., is of the form 𝜉 = f(𝜉 1 , . . . , 𝜉 𝑛 ) for some f/𝑛 ∈ F pub ∩ F c ; or

(2) 𝜉 is an entry of the knowledge base, that is, 𝜉 ⊢ ? 𝜋 𝑢 ∈ C. Each of these cases will be formalised by a rule of the form:

C Σ ---→ mgs C : Σ (★)
for some adequate second-order substitution Σ modelling the case in question (with some conditions on C). The first rule for example models the constructor case by using (★) with:

Σ = {𝑋 ↦ → f(𝑋 1 , . . . , 𝑋 𝑛 )} (Mgs-Cons)
if there exists a deduction hyperconstraint 𝑋: 𝑀 ⊢ ? 𝜋 𝑢 ∈ D(C), 𝑢 ∉ X 1 , and with f/𝑛 ∈ F c ∩ F pub , and 𝑋 𝑖 : 𝑀 fresh. Then, the case where the deduction is a direct entry of the knowledge base corresponds to the instantiation of (★) with:

Σ = mgu (𝑋 = ? 𝜉) ≠ ⊥ (Mgs-Res)
if there exists two deduction hyperconstraints 𝑋 ⊢ ? 𝜋 𝑢 ∈ D(C), 𝑢 ∉ X 1 , and 𝜉 ⊢ ? 𝜋 𝑣 ∈ K (C). The set of all most general unifiers of C is then obtained by considering all hyperconstraint systems reachable using these two rules, each application of which being separated by as many simplification rules as possible. Formally: Definition D.3 (Solved form). We say that a hyperconstraint system C is solved when it cannot be reduced by ⇝ or ---→ mgs , and when for all 𝑋 ⊢ ? 𝜋 𝑢 ∈ D (C), 𝑢 ∈ X 1 .

Definition D.4 (Direct solution). We say that a solution (Σ, 𝜎) ∈ Sol (C) is a direct solution of C if for all 𝑋 ⊢ ? 𝜋 𝑢 ∈ D(C), 𝑋 Σ ∈ conseq 𝜋 (C). A set of most general direct solutions of C is defined analogously to the set of most general solutions of C, replacing solutions by direct solutions.

In the following proposition, we write ⇝ the relation applying as many ⇝ steps as possible (which is terminating). The proposition can be proved by a straightforward induction on the size of the first-order terms appearing in deduction hyperconstraints of C. Proposition D.1 (Correctness of mgs computations). Let C be a hyperconstraint system. If we assume that mgu (E 2 (C)) ≠ ⊥, writing 𝑆 the set of most general direct solutions of C:

(1) If C is irreducible by ⇝ and ---→ mgs , then 𝑆 = {mgu (E 2 (C))} if C is solved, and 𝑆 = ∅ otherwise; (2) otherwise:

{(Σ 1 • • • Σ 𝑛 ) |vars 2 ( C) | C ⇝ Σ 1 ---→ mgs ⇝ • • • Σ 𝑛 ---→ mgs ⇝ C ′ , C ′ solved} .
Solving Rules. Finally, relying on the ability to compute most general solutions described in the previous paragraphs, we can define the set of solving rules solve ⇝ , that are used to solve hyperconstraints in general. They are defined below, and enhance the previous rules by adding ways to remove some unsatisfiable constraints. Resolution. The next rule applies uses most general solutions to perform case analyses in a proof stack. Given a state 𝜔 ★ = 𝜔 1 ↣ • • • ↣ 𝜔 𝑛 , the algorithm will first attempt to compute the solutions Σ of 𝜔 𝑛 . Then, in case Σ imposes additional conditions on previous states 𝜔 𝑖 , 𝑖 < 𝑛, a case analysis will occur, that is, ¬Σ will be added as a proof obligation as well at different levels. Formally, the rule takes the following form: Saturation. This last rule is then used to saturate the knowledge base of the adversary, i.e., to ensure that direct deductions (used in particular in the computation of most general solutions) coincide with regular adversarial deductions. To define the rule, we first introduce a couple of preliminary notions. First of all, we define the origination property, which is a straightforward invariant verified by our decision procedure. It intuitively states that we only consider adversarial computations whose multiplicities are consistent with an actual protocol execution. Definition D.5 (Origination property). We say that a hyperconstraint system C verifies the origination property if for all 𝜋 ∈ vars 𝑝 (C), the domain of Φ = Φ(proj 𝜋 (C)) can be ordered as dom(Φ) = {ax 1 , . . . , ax 𝑛 } in a way that for all 𝑖 ∈ 1, 𝑛 , for all 𝑥 ∈ vars 1 (ax 𝑖 ), there exists 𝑋: 𝑀 ⊢ ?

(𝜔 1 ↣ • • • ↣ 𝜔 𝑛 ) ---→ case (𝜔 ′ 1 ↣ • • • ↣ 𝜔 ′ 𝑛 ) (Case-
𝜋 𝑥 ∈ D(C) such that {ax 𝑗 } 𝑗 <𝑖 ⊆ 𝑀.

In the following, we will always assume that hyperconstraint systems verify the origination property. Then, we define the following notion, which characterises the possibility to perform a new deduction from the knowledge base. Definition D.6 (New deduction). Let C be a hyperconstraint system. We call (Σ, 𝜁 ⊢ ?

𝜋 𝑣) a new deduction for C if there exists a rewrite rule f(ℓ 1 , . . . , ℓ 𝑛 ) → 𝑟 and 𝜉 ⊢ ?

𝜋 𝑢 ∈ K(C) such that the following conditions are satisfied.

(1) There should not exist 𝜉 ′ such that 𝜉 ′ ⊩ C,𝜋 𝑣.

(2) Consider a hyperconstraint of the form

C ′ = C ∧ 𝑛 𝑖=1
𝑋 𝑖 : 𝑀 ⊢ ? 𝜋 ℓ 𝑖 ∧ ℓ ′ = ? 𝑢 where ℎ ⊥ (𝜔 ★ ) = (∅, {𝜔 ★ }). Similarly, we can define: ℎ 0 ∨ ℎ 1 = (¬ℎ 0 ) ⇒ ℎ 1 ℎ 0 ∧ ℎ 1 = ¬(¬ℎ 0 ∨ ¬ℎ 1 ) .

Case-By-Case Computation. We can finally formalise the definition of HCompute. In all incoming cases, we will use the notations (Ω 𝜑 , Ω ¬𝜑 ) = HCompute(𝜔 ★ , 𝜔 -1 ), with 𝜔 ★ and 𝜔 -1 = (Π @ , 𝑡, 𝜑). First of all, HCompute(𝜔 ★ , 𝜔 -1 ) only applies if 𝜔 ★ is a non-empty proof stack, and starts by applying the constraint solving procedure to it, i.e., we write 𝜔 ★ cs ⇝ 𝜔 ★ 𝑠 , where

𝜔 ★ 𝑠 = 𝜔 1 ↣ • • • ↣ 𝜔 𝑛 𝑛 ⩾ 1 .
We then perform the following case analysis. In several cases, we also use the function Analogue to the previous case. ▶ State membership case: 𝜑 = GS 𝜋 (𝑢).

Let us write: Π @ (𝜋) = (𝐴, 𝐸) and 𝜇 = mgu (E 1 (C)) .

Using these notations, we return Ω 𝜑 = {HRefine(𝜎, 𝜔 ★ 𝑠 ) | 𝑣 ∈ 𝜃 (𝐴), 𝜎 ∈ mgu R (𝑢𝜇 = ? 𝑣𝜇)} Ω ¬𝜑 = {HRefine(¬𝜎, 𝜔 ★ 𝑠 ) | 𝑣 ∈ 𝜃 (𝐴), 𝜎 ∈ mgu R (𝑢𝜇 = ? 𝑣𝜇)} ▶ Equality modulo R case: 𝜑 = (𝑢 = 𝑣).

In this case, it suffices to add a (dis)equality constraint to C and to resolve it using the oracle. That is, we let: This case is mostly similar to the equality-modulo case, except that we use (non-)deduction constraints instead of (dis)equations. We therefore let, this time:

𝜇 = mgu (E 1 (C))
𝑀 = mgu R (𝑢𝜇 = ? 𝑢𝜇) .

We first let Π @ (𝜀) = (𝐴, 𝐸), and T be a mapping from fresh path variables to symbolic traces, where img(T) is the set of all symbolic traces of 𝐴. We also consider the hyperconstraint C(𝜋 ′ ), 𝜋 ′ ∈ dom(T), obtained from C(T(𝜋 ′ )) by labelling (non-)deduction constraints by 𝜋 ′ . We then define a function ℎ 𝜋 ′ , 𝜋 ′ ∈ dom(T), which intuitively attempts to prove 𝜓 for the symbolic trace T(𝜋), assuming this symbolic trace has a solution (otherwise ℎ 𝜋 ′ skips the proof). I.e.:

(Ω 𝜑 , Ω ¬𝜑 ) = HCompute(•, (Π ′ @ , 𝑡,𝜓 ′ )) ∧ RecCall(•) (𝜔 ′ )

where:

𝜓 ′ = 𝜓 {𝜋 ↦ → 𝜋 ′ } Π ′ = Π[𝜀 ↦ → T(𝜋 ′ )] ∪ {𝜋 ′ ↦ → T(𝜋 ′ )} Π ′ @ = Π @ [

E.2 Correctness and Complexity

Decidability. We state in this section the main properties for the correctness of our decision procedure, thus leading to the decidability (and tight complexity analysis) of Verif, given as before an oracle to solve the numeric constraints. The characterisation of HCompute is in particular the following. First, given a statement 𝑃 |= 𝜑 to prove or disprove, we consider the following parameters to give as an initial argument to HCompute: Definition E.1 (Initial parameters of HCompute). Given a process 𝑃 and a guarded hyperformula 𝜑, let 𝑡 ∈ X N , and 𝑃 s be the symbolic process: 𝑃 s = ({{𝑃 }}, (𝑡 = 0), ∅, 𝑡) .

We call initial parameters of HCompute for 𝑃 and 𝜑 a tuple (𝜔 ★ , 𝜔 -1 ), where 𝜔 ★ is a proof stack consisting of the single proof state (Π, (𝑡 = 0), ∅), 𝜔 -1 = (Π, (𝑡 = 0), ∅), Π = {𝜀 ↦ → 𝜀 𝑃 s } with 𝜀 𝑃 s the empty symbolic trace starting from 𝑃 s , and Π @ = {𝜀 ↦ → (𝑃 s , ∅)}.

The specification of HCompute can then be formally stated as the following proposition. Note that it is only a partial correctness statement, i.e., it proves that HCompute is correct when it terminates but does not prove termination yet.

Proposition E.1 (Correctness of HCompute). Let 𝑃 be a ground bounded process, and 𝜑 a ground guarded hyperformula. Given 𝜔 ★ , 𝜔 -1 some initial parameters of HCompute for 𝑃 and 𝜑, if we have (Ω 𝜑 , Ω ¬𝜑 ) = HCompute(𝜔 ★ , 𝜔 -1 ) then 𝑃 |= 𝜑 iff Ω ¬𝜑 = ∅.

(1) the size of the formula 𝜑 to prove (polynomial);

(2) the multiset of the numbers of instructions of symbolic processes appearing in the proof stack (polynomial); (3) the multiset of the numbers of deducible term that are not a direct consequence of some proof state. This parameter is of polynomial size since, for destructor subterm convergent rewriting systems, all deducible terms from a frame Φ are of the form 𝐶 [𝑢], for 𝐶 a public constructor context and 𝑢 a subterm of some axΦ ∈ img(Φ) (and there are polynomiallymany in the size of 𝑃); (4) the multiset of the numbers of most general direct solutions of the constraint system of some proof stack (polynomial, as we consider only direct solutions); (5) the multiset of the numbers of proof obligations at each level of the stack (one multiset for each level, lexicographically ordered by increasing stack level order). This parameter is polynomial in the number of traces of 𝑃, which is exponential in the size of 𝑃 and A.

In the case of tidy LTL, 𝜑 = ∀𝜋 .𝜓 contains only one trace quantification at the head of the formula. Therefore, the verification of 𝜑 using NBA can be done by initially guessing a trace nondeterministically, and then verify for the guessed trace that 𝜓 holds (which thus does not involve proof obligations). In particular, in the above measure, only polynomial parameters remain, hence the result. □

In particular, a trivial combination of the previous two propositions gives the following corollary, using NBA 𝑛 as a decision procedure with some exponential value of 𝑛.

Theorem E.4 (Complexity of Verif). Verif is in EXPH(poly) for destructor subterm term algebras, bounded processes, and guarded hyperformulae.

F COMPLEXITY OF SUB-FRAGMENTS

Upper Bounds. We prove in this section the side complexity results we provided in Figure 9, and that apply to sub-fragments of the logic.

First of all, using the polynomial-solution property of the previous section (Theorem E.3), we already obtain the complexity of the fragments of tidy LTL, again using the naive NBA procedure: Corollary F.1 (Complexity of tidy LTL). For a destructor subterm convergent term algebra, bounded processes and guarded hyperformulae, the Verif problem is in PSPACE (resp. NP, coNP) for tidy LTL (resp. tidy ∃-LTL , tidy ∀-LTL ).

Exhibiting complexity upper bounds for bounded processes of the pure 𝜋-calculus, i.e., with an empty term algebra, is also straightforward, since there are this time finitely-many traces up to bijective renaming of fresh public names. The naive NBA 𝑛 procedure is therefore trivially sound for 𝑛 = 1. Proposition F.2 (Complexity in the pure calculus). For bounded processes and guarded hyperformulae, the Verif problem is in PSPACE (resp. NP, coNP) in general (resp. for tidy ∃-LTL , tidy ∀-LTL ).

Lower Bounds. We now prove that all the complexity results of this paper are tight. We already proved the undecidability results in Section 4.1. Also, the hardness results for the main decision procedure are already proved in [START_REF] Barthe | Tidy: Symbolic Verification of Timed Cryptographic Protocols[END_REF]]: Theorem F.3 (Hardness of Verif). For a destructor subterm convergent term algebra, bounded process, and guarded hyperformulae, the Verif problem is EXPH(poly) hard in tidy CTL* and Hypertidy LTL.

Fig. 2 .

 2 Fig. 2. Model of the contract Puzzle

Fig

  Fig. 4. Contract FairPuzzle

Fig. 7 .

 7 Fig. 7. Operational semantics of the calculus

Fig. 8 .

 8 Fig. 8. Satisfiability relation for formulae

  Theorem 4.5 (Decidability in Hypertidy CTL*). The Verif problem is EXPH(poly) complete for destructor subterm convergent term algebras, bounded processes, and guarded hyperformulae of either tidy CTL*, Hypertidy LTL or Hypertidy CTL*.

  process term algebra tidy ∀-LTL tidy LTL tidy CTL* Hypertidy LTL/

Fig. 9 .

 9 Fig. 9. Summary: Complexity of Verifying Guarded Hyperformulae (with oracle to a numeric solver)

s

  as a sequence of -→ s transitions, and C(𝑇 s ) = C(𝐴 𝑛 s ), we can formalise the first property linking the symbolic semantics with the operational one. It is soundness, intuitively stating that all symbolic traces yield valid regular traces when instantiating their variables w.r.t. their constraints.Proposition 5.2 (Soundness). Consider a symbolic trace 𝑇 s : 𝐴 0

  Fig. 10. Progress-related notions

Fig. 11 .

 11 Fig. 11. Recursive construction of virtual payment channels

formula

  Fig. 12. Axiomatisation of tests

  is a normal trace. If 𝑖 = 𝑛, the conclusion follows by choosing 𝑇 𝑁 = 𝑇 . If 𝑖 < 𝑛, let us write the normal process 𝐴 𝑖 = (P, ∅) with the notations of Definition C.3, in particular, P = S ∪ P 0∪ {{! 𝑃 ℓ ′ }} ℓ ′ ∈𝐿 for S = {{𝑄 ℓ 𝜎 }} or S = ∅.First of all, let us exclude the case where the next transition 𝐴 𝑖 𝛼 𝑖+1

Fig. 15 .

 15 Fig. 15. Simplification rules for hyperconstraint systems

  Resolve)where the following conditions are met. First of all, either Σ ∈ mgs (C(𝜔 𝑛 )) or Σ ∈ mgs (C ′ ∧ mgu (¬𝜙)), writing C(𝜔 𝑛 ) = C ′ ∧ ∀ì 𝑥 .𝜙. Then for all 𝑖, writing 𝜔 𝑖 = (Π 𝑖 , C 𝑖 , O 𝑖 ):𝜔 ′ 𝑖 = (Π 𝑖 , C + 𝑖 , O 𝑖 ∪ {(Π(𝜀), C - 𝑖 )})where, with the convention dom(𝜔 -1 ) = ∅:C + 𝑖 = C 𝑖 : Σ |dom(𝜔 𝑖 ) ∧ C 𝑡 C - 𝑖 = C 𝑖 ∧ (¬Σ |dom(𝜔 𝑖 )∖dom(𝜔 𝑖 -1 ) ∨ ¬C 𝑡 )where C 𝑡 refers to the numeric constraints of C 𝑛 : Σ |dom(𝜔 𝑛 ) .

  HRefine, defined byHRefine(𝜎,𝜔 ★ ) = 𝜔 ★ 𝑠 ′ with 𝜔 ★ [C(𝜔) ↦ → C(𝜔) ∧ 𝜎] cs ⇝ 𝜔 ★ 𝑠 ′ , with 𝜔 ★ = 𝜔 ★ pref ↣ 𝜔. ▶ Non-concretisable case: C(𝜔 𝑛 ) = ⊥.Then we simply return Ω 𝜑 = {𝜔 𝑛 } and Ω ¬𝜑 = ∅. ▶ Event case: 𝜑 = Ev ( ì 𝑢) 𝜋 . In this case, we interpret event functions F 𝑒 as constructor symbols of F c . We thus consider the term 𝑣 = Ev( ì 𝑢), and:Π @ (𝜋) = (𝐴, 𝐸) and 𝜇 = mgu (E 1 (C)) .Using these notations, we returnΩ 𝜑 = {HRefine(𝜎, 𝜔 ★ 𝑠 ) | 𝑤 ∈ 𝐸, 𝜎 ∈ mgu R (𝑣𝜇 = ? 𝑤 𝜇)} Ω ¬𝜑 = {HRefine(¬𝜎, 𝜔 ★ 𝑠 ) | 𝑤 ∈ 𝐸, 𝜎 ∈ mgu R (𝑣𝜇 = ?𝑤 𝜇)} ▶ Non-event action case: 𝜑 = 𝛼 𝜋 (𝛼 ∈ {in, out, repl, . . .}).

𝜇

  = mgu (E 1 (C)) 𝑀 = mgu R (𝑢𝜇 = ? 𝑣𝜇)and then returnΩ 𝜑 = {HRefine(𝜎, 𝜔 ★ 𝑠 ) | 𝜎 ∈ mgu R (𝑢𝜇 = ? 𝑣𝜇)} Ω ¬𝜑 = {HRefine(¬𝜎, 𝜔 ★ 𝑠 ) | 𝜎 ∈ mgu R (𝑢𝜇 = ? 𝑣𝜇)} ▶ Adversarial deduction case: 𝜑 = K 𝜋 (𝑢).

  𝜀 ↦ → (𝐴, ∅)] ∪ {𝜋 ′ ↦ → (𝐴, ∅)} 𝜔 ′ = 𝜔 ★ 𝑠 ↣ (Π ′ , C(𝜋 ′ ), {(T(𝜋), C(𝜋)) | 𝜋 ∈ dom(T), 𝜋 ≠ 𝜋 ′ }) and RecCall(𝜔 ★ ↣ 𝜔 prelast ↣ 𝜔 last ) is defined as ({𝜔 ★ ↣ 𝜔 prelast }, ∅) when O (𝜔 prelast ) = ∅;otherwise, for a given (T(𝜋 ′′ ), C) ∈ O (𝜔 prelast ):RecCall(𝜔 ★ ↣ 𝜔 prelast ↣ 𝜔 last ) = HCompute(𝜔 ★ ↣ 𝜔 ′′ , (Π ′ @ , 𝑡,𝜓 ′′ )) with 𝜓 ′′ = 𝜓 {𝜋 ↦ → 𝜋 ′′ } Π ′′ = Π ′ [𝜀 ↦ → T(𝜋 ′′ )] ∪ {𝜋 ′′ ↦ → T(𝜋 ′′ )} 𝜔 ′′ = 𝜔 prelast [O ↦ → O ∖ {(T(𝜋 ′′ ), C)}]

  global state membership 𝑢 = 𝑣 equality modulo theory ∀𝑥 1 , . . . , 𝑥 𝑝 .𝜑 ⇒ 𝜑 guarded quantifier 𝛼 𝜋

	action	∀𝜋 .𝜑	path quantifier
	K 𝜋 (𝑢) adversary deduction	𝜑 U 𝐼 𝜑

(time-constrained) until

  with the notations of Definition C.3, and 𝑥𝜎 0 = 𝑧 for all 𝑥 {𝑥 + 1 , 𝑥 - 1 , 𝑥 + 2 , 𝑥 - 2 }. Lemma C.2 (Reduction to normal traces). 𝑃 𝑀 |= 𝜑 iff for all normal traces 𝑇 of P 𝑀 , Π 𝑇 |= 𝜓 with Π 𝑇

  and deduction hyperconstraints 𝜉 1 ⊢ ? 𝜋 𝑢 1 , . . . , 𝜉 𝑛 ⊢ ? 𝜋 𝑢 𝑛 ∈ 𝑆 such that 𝜉 = 𝐶 [𝜉 1 , . . . , 𝜉 𝑛 ] and 𝑢 = 𝐶 [𝑢 1 , . . . , 𝑢 𝑛 ] .

. DEEPSEC: Deciding equivalence properties in security protocols theory and practice. In IEEE Symposium on Security and Privacy (S&P). Vincent Cheval, Steve Kremer, and Itsaka Rakotonirina. 2019. Exploiting symmetries when proving equivalence properties for security protocols. In ACM Conference on Computer and Communications Security (CCS). Vincent Cheval, Steve Kremer, and Itsaka Rakotonirina. 2020a. The hitchhiker's guide to decidability and complexity of equivalence properties in security protocols. In Logic, Language, and Security. Essays Dedicated to Andre Scedrov on the Occasion of His 65th Birthday (ScedrovFest65). Vincent Cheval, Steve Kremer, Itsaka Rakotonirina, and Victor Yon. 2020b. DeepSec user manual. https://deepsecprover.github.io/. Michael R Clarkson, Bernd Finkbeiner, Masoud Koleini, Kristopher K Micinski, Markus N Rabe, and César Sánchez. 2014. Temporal logics for hyperproperties. In International Conference on Principles of Security and Trust (POST). Springer, Grenoble, France, 265-284. Michael R Clarkson and Fred B Schneider. 2010. Hyperproperties. Journal of Computer Security 18, 6 (2010), 1157-1210. Norine Coenen, Bernd Finkbeiner, Christopher Hahn, and Jana Hofmann. 2019. The hierarchy of hyperlogics. In ACM/IEEE Symposium on Logic in Computer Science (LICS). Norine Coenen, Bernd Finkbeiner, Jana Hofmann, and Julia Tillman. 2022. Smart Contract Synthesis Modulo Hyperproperties. arXiv preprint arXiv:2208.07180 (2022). Hubert Comon-Lundh and Stéphanie Delaune. 2005. The finite variant property: How to get rid of some algebraic properties. In International Conference on Rewriting Techniques and Applications (RTA). Springer, Poland, 294-307. Danny Dolev and Andrew Yao. 1983. On the security of public key protocols. IEEE Transactions on information theory 29, 2 (1983), 198-208. Nancy A. Durgin, Patrick Lincoln, and John C. Mitchell. 2004. Multiset rewriting and the complexity of bounded security protocols. Journal of Computer Security 12, 2 (2004), 247-311. Stefan Dziembowski, Lisa Eckey, Sebastian Faust, and Daniel Malinowski. 2019. Perun: Virtual payment hubs over cryptocurrencies. In 2019 IEEE Symposium on Security and Privacy (SP). IEEE, 106-123. Bernd Finkbeiner, Hadar Frenkel, Jana Hofmann, and Janine Lohse. 2023. Automata-based software model checking of hyperproperties. In NASA Formal Methods Symposium. Springer, 361-379. Bernd Finkbeiner, Markus N. Rabe, and César Sánchez. 2015. Algorithms for Model Checking HyperLTL and HyperCTL*. In Computer Aided Verification (CAV). Springer, San Fransisco, CA, USA, 30-48. Ilya Grishchenko, Matteo Maffei, and Clara Schneidewind. 2018. A Semantic Framework for the Security Analysis of Ethereum Smart Contracts. In Principles of Security and Trust (POST). Springer. Shelly Grossman, Ittai Abraham, Guy Golan-Gueta, Yan Michalevsky, Noam Rinetzky, Mooly Sagiv, and Yoni Zohar. 2017. Online detection of effectively callback free objects with applications to smart contracts. Proceedings of the ACM on Programming Languages (2017). Sebastian Holler, Sebastian Biewer, and Clara Schneidewind. 2023. HoRStify: Sound Security Analysis of Smart Contracts. In 2023 2023 IEEE 36th Computer Security Foundations Symposium (CSF)(CSF). IEEE Computer Society, 347-362. Tzu-Han Hsu, Borzoo Bonakdarpour, Bernd Finkbeiner, and César Sánchez. 2023. Bounded Model Checking for Asynchronous Hyperproperties. arXiv preprint arXiv:2301.07208 (2023). Max I. Kanovich, Tajana Ban Kirigin, Vivek Nigam, and Andre Scedrov. 2014. Bounded memory protocols. Computer Languages, Systems & Structures (2014). Steve Kremer and Robert Künnemann. 2016. Automated analysis of security protocols with global state. Journal of Computer Security (JCS) (2016). Jia Liu and Huimin Lin. 2012. A complete symbolic bisimulation for full applied pi calculus. Theoretical Computer Science 458 (2012), 76-112. Matteo Marescotti, Rodrigo Otoni, Leonardo Alt, Patrick Eugster, Antti E. J. Hyvärinen, and Natasha Sharygina. 2020. Accurate Smart Contract Verification Through Direct Modelling. In Leveraging Applications of Formal Methods, Verification and Validation: Applications -9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020, Proceedings, Part III (Lecture Notes in Computer Science, Vol. 12478), Tiziana Margaria and Bernhard Steffen (Eds.). Springer, 178-194. https://doi.org/10.1007/978-3-030-61467-6_12 Corto Mascle and Martin Zimmermann. 2019. The keys to decidable hyperltl satisfiability: Small models or very simple formulas. arXiv preprint arXiv:1907.05070. Marvin Lee Minsky. 1967. Computation. Prentice-Hall Englewood Cliffs, USA. p.255-258. Anton Permenev, Dimitar K. Dimitrov, Petar Tsankov, Dana Drachsler-Cohen, and Martin T. Vechev. 2020. VerX: Safety Verification of Smart Contracts. In 2020 IEEE Symposium on Security and Privacy, SP 2020, San Francisco, CA, USA, May 18-21, 2020. IEEE, 1661-1677. https://doi.org/10.1109/SP40000.2020.00024 Joseph Poon and Thaddeus Dryja. 2016. The bitcoin lightning network: Scalable off-chain instant payments. (2016).

𝑄 ℓ = out(𝑐 ℓ ′ , h(𝑥 + 1 )); out(𝑐 ℓ ′ , 𝑥 - 1 ); out(𝑐 ℓ ′ , 𝑥 + 2 ); out(𝑐 ℓ ′ , 𝑥 - 2 ); 0

If 𝑀 [ℓ] = incr(c 2 , ℓ ′ ):

𝑄 ℓ = out(𝑐 ℓ ′ , 𝑥 + 1 ); out(𝑐 ℓ ′ , 𝑥 - 1 ); out(𝑐 ℓ ′ , h(𝑥 + 2 )); out(𝑐 ℓ ′ , 𝑥 - 2 ); 0

If 𝑀 [ℓ] = zdecr(c 1 , ℓ 0 , ℓ -):

𝑄 ℓ = 𝑄 0 ℓ + 𝑄 - ℓ with 𝑄 0 ℓ = event Zero(𝑥 + 1 , 𝑥 - 1 ); out(𝑐 ℓ 0 , 𝑥 + 1 ); out(𝑐 ℓ 0 , 𝑥 - 1 ); out(𝑐 ℓ 0 , 𝑥 + 2 ); out(𝑐 ℓ 0 , 𝑥 - 2 ); 0 and 𝑄 - ℓ = event Pos(𝑥 + 1 , 𝑥 - 1 ); out(𝑐 ℓ -, 𝑥 + 1 ); out(𝑐 ℓ -, h(𝑥 - 1 )); out(𝑐 ℓ -, 𝑥 + 2 ); out(𝑐 ℓ -, 𝑥 - 2 ); 0

If 𝑀 [ℓ] = zdecr(c 2 , ℓ 0 , ℓ -):

𝑄 ℓ = 𝑄 0 ℓ + 𝑄 - ℓ with 𝑄 0 ℓ = event Zero(𝑥 + 2 , 𝑥 - 2 ); out(𝑐 ℓ 0 , 𝑥 + 1 ); out(𝑐 ℓ 0 , 𝑥 - 1 ); out(𝑐 ℓ 0 , 𝑥 + 2 ); out(𝑐 ℓ 0 , 𝑥 - 2 ); 0 and 𝑄 - ℓ = event Pos(𝑥 + 2 , 𝑥 - 2 ); out(𝑐 ℓ -, 𝑥 + 1 ); out(𝑐 ℓ -, 𝑥 - 1 ); out(𝑐 ℓ -, 𝑥 + 2 ); out(𝑐 ℓ -, h(𝑥 - 2 )); 0 13. Encoding of two-counter-machine operations as processes

Let us then define the tidy LTL formula 𝜑 that formalises several properties. First, it expresses the assumptions behind the events Zero and Pos, namely that Zero(𝑢, 𝑣) should only be triggered when the terms 𝑢 and 𝑣 are equal (modulo theory), and conversely that Pos(𝑢, 𝑣) can only be triggered when 𝑢 and 𝑣 are different. This way, the non-deterministic choices in the definition of 𝑄 ℓ (cases zdecr) effectively emulate a conditional testing. Additionally, 𝜑 requires that the halting event never holds, thus encoding non-termination. Formally, 𝜑 = ∀𝜋 . 𝜑 sync ⇒ 𝜑 Zero ⇒ 𝜑 Pos ⇒ G ¬Halt 𝜋 with:

The correctness of the overall reduction is then stated by: Proposition C.1 (Correctness of the reduction). 𝑀 does not terminate iff 𝑃 𝑀 ⊨ 𝜑.

C.2 Proof

The rest of this section is dedicated to the proof of Proposition C.1, which will conclude the proof of Proposition 4.1. For that we establish a correspondence between two-counter machine executions and a restricted type of trace that we call normal.

Definition C.3 (Normal process). We call a extended process normal when it is of the form (P, ∅),

(blank normal proc.)

• 𝑃 ℓ , 𝑄 ℓ still refer to the previously defined processes;

• P 0 only contain processes that are 0 or 𝑃 ℓ ′ , ℓ ′ ∈ 𝐿, but at least one copy of each process

and

symbolic semantics:

Fig. 14. Symbolic semantics for verifying timed bounded processes

D.1 Solution Management

We give here some key notions to define the various solving algorithm detailed in the next sections; these notions are adapted from the algorithm of [Cheval et al. 2018] for computing solutions of (plain) constraint systems. First of all, computing the solutions of a hyperconstraint system C is done under the assumption that a saturation procedure has been carried out at a previous step, ensuring that a the deducibility of a term 𝑢 can be checked syntactically from K(C). Formally:

Definition D.1 (Direct consequence). Given a set of deduction hyperconstraints 𝑆, a direct consequence of 𝑆 in path 𝜋 is a statement 𝜉 ⊩ 𝑆,𝜋 𝑢, such that there exists a public constructor context C, with ℓ ′ subterm of some ℓ 𝑖 , and 𝑟 is a subterm of ℓ ′ . Then Σ ∈ mgs (C ′ ), 𝜁 = f (𝑋 1 Σ, . . . , 𝑋 𝑛 Σ) and 𝑣 = 𝑟𝜎, with 𝜎 the non-numeric constraints of mgu (E 1 (C ′ : Σ)).

(3) In the above item, 𝑀 is of the form {ax 1 , . . . , ax 𝑛 }, with these axioms numbered as in the definition of origination property. Besides, there should not exist other new deductions for a multiplicity 𝑀 ′ ⊂ 𝑀.

Using this notion, the rule can be formalised as follows:

where the following conditions are met. First of all, there should exists (Σ, 𝜁 ⊢ ? 𝜋 𝑣) a new deduction for C(𝜔 𝑛 ). Then for all 𝑖, writing 𝜔 𝑖 = (Π 𝑖 , C 𝑖 , O 𝑖 ):

where, with the convention dom(𝜔 -1 ) = ∅:

Constraint Solving. Putting everything together, the constraint solving relation

E VERIFICATION OF HYPERPROPERTIES E.1 Decision Procedure

Setting. We now present the decision procedure itself, relying on the constraint solving relation cs ⇝ introduced in the previous section. We describe the behaviour of HCompute in the rest of this section, by induction on 𝜑. However, to lighten the presentation of some cases, we first introduce notations to compose recursive calls to HCompute in a way that reflects logical connectives. First, we give a notation ⊕ for component-by-component union:

. Another, more involved notion of composition is the one reflecting the verification of implications 𝜑 ⇒ 𝜓 . First, a split (Ω 𝜑 , Ω ¬𝜑 ) is computed for 𝜑, and Ω 𝜑 is then refined to obtain a split Ω 𝜑∧𝜓 , Ω 𝜑∧¬𝜓 . Formally, we let ℎ + 𝑖 , ℎ - 𝑖 be functions mapping proof stacks to sets of proof stacks, and let ℎ 𝑖 : 𝜔 ↦ → (ℎ + 𝑖 (𝜔), ℎ - 𝑖 (𝜔)). In our below definition of HCompute, we will typically have ℎ 𝑖 = HCompute(•, 𝜔 -1 ) .

Then the logical composition of ℎ 0 and ℎ 1 is defined as the following function:

Using a similar construction, the negation composition of ℎ 0 can be defined from it, doing a swap:

One subtlety, however, is that (non-)deduction constraints of a term 𝑢 require that 𝑢 is a constructor term. In particular, 𝜑 does not hold when either 𝑢 is a message but not deducible, or if it is not instantiated as a message. With this in mind, we let 𝑋 ∈ X 2 be a fresh variable, and:

. Note that the quantified variables ì 𝑥 do not need to be taken into account in the constraint computation. Indeed, due to the requirement that they are guarded, they can be left as free variables as they will be unified with process variables during the recursive call ℎ 0 . ▶ Until case: 𝜑 = 𝜑 0 U 𝜑 1 .

Since timestamps are abstracted by time variables, all possible time projections (notation 𝑇 @𝑡 in the non-symbolic case, Definition 3.7) induce a collection of ordering constraints. These constraints intuitively represent all potential schedulings of the different traces of Π.

Formally, if 𝑇 is a symbolic trace and 𝑡 ′ ∈ X N , we define the following set 𝑇 @𝑡 ′ , intuitively representing all possible symbolic abstractions of a time projection of 𝑇 . Each entry of 𝑇 @𝑡 ′ is thus a triple (𝛾, 𝐴 ′ , 𝐸 ′ ), where 𝛾 models a scheduling constraint for 𝑡 ′ , and (𝐴 ′ , 𝐸 ′ ) is the corresponding trace state Π @𝑡 ′ for this trace. Formally, if 𝑇 :

and with convention 𝑡 (𝐴 𝑛+1 ) = +∞:

with 𝐴[𝑡 (𝐴) ↦ → 𝑡 ′ ] the symbolic process 𝐴 with 𝑡 (𝐴) replaced by 𝑡 ′ . We generalise this notation to the whole mapping Π by computing a cartesian product:

We then consider two sets 𝑅 𝜑 0 and 𝑅 𝜑 1 : 𝑅 𝜑 1 = Π@𝑡 1 for some fresh 𝑡 1 ∈ X N , and 𝑅 𝜑 0 is the set Π@𝑡 ′ where in each 𝑎 ∈ Π@𝑡 ′ , 𝑡 ′ is substituted by a different fresh numeric variable 𝑡 𝑎 . We also consider the two functions ℎ

With all these notations, the returned value in this case is finally (Ω 𝜑 , Ω ¬𝜑 ) = ℎ(𝜔), where:

▶ Path quantification case: 𝜑 = ∀𝜋 .𝜓 .

Proof. The proof follows from a straightforward, although technical, induction on the formula 𝜑 to be proved. The actual invariant considered during this induction is the following. Given parameters 𝜔 ★ , 𝜔 -1 that are not necessarily initial, but with

then for all (non-empty) proof stacks (𝜔 ★ ↣ 𝜔) ∈ Ω 𝜓 , for all solutions 𝑆 = (Σ, 𝜎) of C(𝜔), Π(𝜔)𝑆, 𝑡 (𝜔 -1 )𝜎 |= 𝜑𝜎 .

In particular, in the case of a ground process 𝑃 and formula 𝜑, the emptiness of Ω ¬𝜑 is equivalent to 𝑃 |= 𝜑. □

Complexity. Albeit for the missing termination arguments, the above proposition justifies that Verif is decidable for bounded processes and guarded hyperformulae with oracle to numericconstraint solving. However, different arguments are necessary to obtain the expected complexity. Indeed, we recall that EXPH(poly) is a class typically characterised by alternating Turing machines (the class of problems decidable in exponential time by an alternating procedure with a polynomial number of alternations), while HCompute is purely deterministic and may run in double-exponential time.

To obtain an EXPH(poly) bound, we consider the naive 𝑛-bounded algorithm NBA 𝑛 (𝑃, 𝜑) ∈ {true, false}, which is the bruteforce alternating (but incomplete) algorithm for proving 𝑃 |= 𝜑 which bounds the size adversarial computations by 𝑛 to obtain a finite set of traces. Its definition is straightforward, and similar to HCompute but operates on concrete processes and traces, and hence uses concrete recipes (of size 𝑛 at most) instead of deduction constraints.

Proposition E.2 (Complexity and Soundness of NBA). The procedure NBA 𝑛 (𝑃, 𝜑) runs in alternating polynomial time in 𝑛 and the sizes of 𝑃 and 𝜑, and also involves a polynomial number of alternations. Besides, let (Ω 𝜑 , Ω ¬𝜑 ) = HCompute(𝜔, 𝜔 -1 ) for initial parameters of HCompute for 𝑃 and 𝜑 with

𝜇 𝜋 (C(𝜔)) .

where 𝜇 𝜋 (C) refers to the size of a mgs of C projected on path 𝜋, i,e., mgs (C) |vars 2 (proj 𝜋 ( C) ) . Then 𝑃 |= 𝜑 iff NBA 𝑛 (𝑃, 𝜑) accepts.

This states that NBA 𝑛 is a sound procedure provided 𝑛 is greater than all (projections of) mgs generated by HCompute. This last property directly follows from the correctness of HCompute and the definition of mgs.

Proposition E.3 (Small-solution property). We assume a destructor subterm term algebra A. There is a polynomial 𝑝 such that for all processes 𝑃, for all (Ω 𝜑 , Ω ¬𝜑 ) = HCompute(𝜔, 𝜔) obtained with initial parameters of HCompute for 𝑃,

in general

Proof. The proof follows again from an induction on the structure of 𝜑, proving that a wellfounded (exponential) measure decreases at each recursive call of HCompute and solving and case analysis rules. The measure itself is simply a lexicographic product of the following parameters: This result of [START_REF] Barthe | Tidy: Symbolic Verification of Timed Cryptographic Protocols[END_REF]] is proved in a slightly different context, which however does not affect the validity of the proof. First, it defines a notion of guard that is much more restrictive than ours (which even makes the result stronger than what we stated here). Second, the hardness was only stated for subterm convergent term algebras, i.e., not necessarily destructor. However, the reduction used to prove the result was trivially verifying the constructor-destructor property. The corresponding proof of correctness of the reduction can then easily be kept up to minor modifications to match the destructor setting (i.e., to account for the fact that events and outputs are only executed when their arguments are messages).

It thus remains to prove tight lower bounds for tidy LTL (PSPACE) and tidy ∀-LTL (coNP) in the pure 𝜋 calculus. The two reductions are conducted below.

Proposition F.4 (Hardness of tidy LTL). For an empty term algebra, bounded processes and guarded hyperformulae, the Verif problem is PSPACE hard in tidy LTL.

Proof. We prove this result by a reduction from QBF. The encoding is pretty straightforward as guarded quantifiers easily allow to encode boolean quantifications. Formally, we let 0, 1 ∈ N pub and:

𝑃 = Bool(0); Bool(1) Given a quantified boolean formula ∀𝑥 1 .∃𝑦 1 . . . . ∀𝑥 𝑛 .∃𝑦 𝑛 .𝜙, we define the guarded hyperformula:

𝜙

where 𝜙 is the interpretation of the boolean formula 𝜙 as a guarded hyperformulae, i.e., interpreting ∧ and ∨ as the same symbols of our logic, and interpreting a literal 𝑥 as the hyperformula 𝑥 = 0, and ¬𝑥 as 𝑥 = 1. It is then straightforward that 𝑃 |= 𝜑 iff ∀𝑥 1 .∃𝑦 1 . . . . ∀𝑥 𝑛 .∃𝑦 𝑛 .𝜙 holds. □ Proposition F.5 (Hardness of tidy ∀-LTL and tidy ∃-LTL ). For an empty term algebra, bounded processes and guarded hyperformulae, the Verif problem is coNP hard (resp. NP hard) in tidy ∀-LTL (resp. tidy ∃-LTL ).

Proof. It suffices to prove the NP hardness of tidy ∃-LTL , as 𝜑 is in tidy ∃-LTL iff ¬𝜑 is in tidy ∀-LTL . We proceed by reduction from SAT. Let us thus consider a boolean formula in CNF, 𝜙 = 𝑝 𝑖=1 𝐶 𝑖 , whose variables are written ì 𝑥 = 𝑥 1 , . . . , 𝑥 𝑛 . As before, we let two names 0, 1 ∈ N pub modelling booleans. For each clause 𝐶 𝑖 , we consider an event Sat 𝑖 , and we define the following process:

𝑃 𝑖 = (Eq(𝑥 𝑖 1 , 𝑏 𝑖 1 ) : Sat 𝑖 ) | • • • | (Eq(𝑥 𝑖 ℓ , 𝑏 𝑖 ℓ ) : Sat 𝑖 ) where 𝑥 𝑖 1 , . . . , 𝑥 𝑖 ℓ are the variables of 𝐶 𝑖 (they are here free variables in Sat 𝑖 ) and 𝑏 𝑖 1 , . . . , 𝑏 𝑖 ℓ ∈ {0, 1} are their respective negation bits. Intuitively, interpreting the event Eq as an equality predicate, 𝑃 𝑖 can emit the event Sat 𝑖 iff the variables 𝑥 1 , . . . , 𝑥 𝑛 are instantiated in a wy that 𝐶 𝑖 holds. In particular, the satisfiability of the whole boolean 𝜙 is characterised by the following process 𝑃 and guarded hyperformula 𝜑: 𝑃 = in(𝑥 1 ) : • • • : in(𝑥 𝑛 ); (𝑃 1 | • • • 𝑃 𝑛 ) 𝜑 = ∃𝜋 .(G ∀𝑥, 𝑦.Eq(𝑥, 𝑦) ⇒ 𝑥 = 𝑦) ∧ 𝑛 𝑖=1 F Sat 𝑖 . We then observe that 𝑃 |= 𝜑 iff 𝜙 is satisfiable. □