Daniele Nantes

Jorge A Pérez

Relating Process Languages for Security and Communication Correctness (Extended Abstract)

Process calculi are expressive specification languages for concurrency. They have been very successful in two research strands: (a) the analysis of security protocols and (b) the enforcement of correct message-passing programs. Despite their shared foundations, languages and reasoning techniques for (a) and (b) have been separately developed. Here we connect two representative calculi from (a) and (b): we encode a (high-level) π-calculus for multiparty sessions into a (low-level) applied π-calculus for security protocols. We establish the correctness of our encoding, and we show how it enables the integrated analysis of security properties and communication correctness by re-using existing tools.

Introduction

This paper connects two distinct formal models of communicating systems: a process language for the analysis of security protocols [START_REF] Kremer | Automated analysis of security protocols with global state[END_REF], and a process language for sessionbased concurrency [START_REF] Honda | Language Primitives and Type Discipline for Structured Communication-Based Programming[END_REF][START_REF] Honda | Multiparty asynchronous session types[END_REF]. They are representative of two separate research strands: (a) Process models for security protocols, such as [START_REF] Kremer | Automated analysis of security protocols with global state[END_REF] (see also [START_REF] Cortier | Formal models and techniques for analyzing security protocols: A tutorial[END_REF]), rely on variants of the applied π-calculus [START_REF] Abadi | Mobile values, new names, and secure communication[END_REF] to establish properties related to process execution (e.g., secrecy and confidentiality). These models support cryptography and term passing, but lack support for high-level communication structures. (b) Process models for session-based communication, such as [START_REF] Honda | Multiparty asynchronous session types[END_REF] (see also [START_REF] Hüttel | Foundations of session types and behavioural contracts[END_REF]), use π-calculus variants equipped with type systems to enforce correct message-passing programs. Security extensions of these models target properties such as information flow and access control (cf. [START_REF] Bartoletti | Combining behavioural types with security analysis[END_REF]), but usually abstract away from cryptography.

We present a correct encoding that connects two calculi from these two strands:

-A, a (low-level) applied π-calculus in which processes explicitly describe term communication, cryptographic operations, and state manipulation [START_REF] Kremer | Automated analysis of security protocols with global state[END_REF]; -S, a (high-level) π-calculus in which communication actions are organized as multiparty session protocols [START_REF] Honda | Multiparty asynchronous session types[END_REF][START_REF] Coppo | A gentle introduction to multiparty asynchronous session types[END_REF].

Our aim is to exploit the complementary strenghts of A and S to analyze communicating systems that feature high-level communication structures (as in session-based concurrency [START_REF] Honda | Language Primitives and Type Discipline for Structured Communication-Based Programming[END_REF][START_REF] Honda | Multiparty asynchronous session types[END_REF]) and use cryptographic operations and global state in protocol exchanges.

Our encoding of S into A describes how the structures typical of session-based, asynchronous concurrency can be compiled down, in a behavior-preserving manner, as Work partially funded by FAP-DF 0193.001381/2017. process implementations in which communication of terms takes place exploiting rich equational theories and global state. To our knowledge, ours is the first work to relate process calculi for the analysis of communication-centric programs (S) and of security protocols (A), as developed in disjoint research strands.

We believe our results shed light on both (a) and (b). In one direction, they define a new way to reason about multiparty session processes. Process specifications in S can now integrate cryptographic operations and be analyzed by (re)using existing methods. In fact, since A processes can be faithfully translated into multiset rewriting rules using SAPIC [START_REF] Kremer | Automated analysis of security protocols with global state[END_REF] (which can in turn be fed into the Tamarin prover [START_REF] Meier | The TAMARIN prover for the symbolic analysis of security protocols[END_REF]), our encoding bridges the gap between S processes and toolsets for the analysis of security properties:

Multiset Rewrite Rules

(Input to Tamarin) [START_REF] Meier | The TAMARIN prover for the symbolic analysis of security protocols[END_REF] This paper Interestingly, this connection can help to enforce communication correctness: we show how SAPIC/Tamarin can check local formulas representing local session types [START_REF] Honda | Multiparty asynchronous session types[END_REF].

In the other direction, our approach allows us to enrich security protocol specifications with communication structures based on sessions. This is relevant because the analysis of security protocols is typically carried out on models such as, e.g., Horn clauses and rewriting rules, which admit efficient analysis but that lead to too low-level specifications. Our developments fit well in this context, as the structures intrinsic to session-based concurrency can conveniently describe communicating systems in which security protocols appear intertwined with higher-level interaction protocols. This rest of the paper is organized as follows. § 2 introduces the Two-Buyer Contract Signing Protocol, a protocol that is representative of the kind of systems that is hard to specify using S or A alone. § 3 recalls the definitions of S and A, and also introduces S , which is a variant of S that is useful in our developments. § 4 defines the encoding of S into A, using S as stepping stone, and establishes its correctness (Theorems 1, 2, and 3). § 5 shows how our encoding can be used to reduce the enforcement of protocol conformance in S to the model checking of local formulas for A (Theorems 4 and 5). § 6 revisits the Two-Buyer Contract Signing Protocol: we illustrate its process specification using S minimally extended with constructs from A, and show how key correctness properties can be mechanically verified using SAPIC/Tamarin. The paper closes by discussing related works and collecting concluding remarks ( § 7). Additional technical material and further examples are given in an appendix available online [START_REF] Nantes | Relating Process Languages for Security and Communication Correctness (Full Version)[END_REF].

A Motivating Example: The Trusted Buyers-Seller Protocol

The Trusted Buyers-Seller Protocol extends the Two-Buyer Protocol [START_REF] Honda | Multiparty asynchronous session types[END_REF], and proceeds in two phases. The first phase follows the global session type in [START_REF] Honda | Multiparty asynchronous session types[END_REF], which offers a unified description of the way in which two buyers (B 1 and B 2 ) interact to purchase a book from a seller (S). In the second phase, once B 1 and B 2 agree in the terms of the purchase, the role of S is delegated to a trusted third party (T ), which creates a contract for the transaction and collects the participants' signatures. This second phase relies on the contract signing protocol [START_REF] Garay | Abuse-free optimistic contract signing[END_REF], which may resolve conflicts (due to unfulfilled promises from B 1 and B 2 ) and abort the conversation altogether. In this protocol, one key security property is authentication, which ensures that an attacker cannot impersonate B i , S, or T . Relevant properties of communication correctness include fidelity and safety: while the former ensures that processes for B i , S, and T follow the protocols specified by global/local types, the latter guarantees that such processes do not get into errors at runtime. The protocol is illustrated in Fig. 1 and described next: Clearly, S and A offer complementary advantages in modeling and analyzing the Trusted Buyers-Seller Protocol. On the one hand, S can represent high-level structures that are typical in the design of multiparty communication protocols. Such structures are essential in, e.g., the exchanges that follow session establishment in the first phase (which involves a step of session delegation to bridge with the second phase) and the handling of requests success, abort and resolve in the second phase. Hence, S and its type-based verification techniques can be used to establish fidelity and safety properties. However, S is not equipped with constructs for directly representing cryptographic operations, as indispensable in, e.g., the NSL protocol for session establishment and in the exchanges of signatures/promises in the contract sigining phase. The lack of these constructs prevents the formal analysis of authentication properties. On the other hand, A compensates for the shortcomings of S, for it can directly represent cryptographic operations on exchanged messages, as required to properly model the contract signing phase and, ultimately, to establish authentication. While A can represent the high-level communication structures mentioned above, it offers a too low-level representation of them, which makes reasoning about fidelity and safety more difficult than in S.

First Phase B 1 , B
Our encoding from S into A, given in § 4, will serve to combine the individual strengths of both languages. In § 6, we will revisit this example: we will give a process specification using an extension of S with some constructs from A. This is consistent, because A is a low-level process language, and our encoding will define how to correctly compile S down to A (constructs from A will be treated homomorphically). Moreover, we will show how to use SAPIC/Tamarin to verify that implementations for B 1 , B 2 , S, and T respect their intended local types.

3 Two Process Models: A and S

The Applied π-calculus (A)

Preliminaries As usual in symbolic protocol analysis, messages are modelled by abstract terms (t, t , . . .). We assume a countably infinite set of variables V, a countably infinite set of names N = PN ∪ FN (FN for fresh names, PN for public names), and a signature Σ (a set of function symbols, each with its arity).

M, N ::= x, y | p | n | f (M1, . . . , Mn) (f ∈ Σ) P, Q ::= 0 | out(M, N ); P | in(M, N ); P | P | Q | !P
We denote by T Σ the set of well-sorted terms built over Σ, N , and V. The set of ground terms (i.e., terms without variables) is denoted M Σ . A substitution is a partial function from variables to terms. We denote by σ = {t 1 /x 1 , . . . , t n /x n } the substitution whose domain is Dom(σ) = {x 1 , . . . , x n }. We say σ is grounding for t if tσ is ground. We equip the term algebra with an equational theory = E , which is the smallest equivalence relation containing identities in E, a finite set of pairs the form M = N where M, N ∈ T Σ , that is closed under application of function symbols, renaming of names, and substitution of variables by terms of the same sort. Furthermore, we require E to distinguish different fresh names, i.e., ∀a, b ∈ F N :

a = b ⇒ a = E b.
Given a set S, we write S * and S # to denote the sets of finite sequences of elements and of finite multisets of elements from S. We use the superscript # to annotate the usual multiset operations, e.g., S 1 ∪ # S 2 denotes the union of multisets S 1 , S 2 . Application of substitutions is extended to sets, multisets, and sequences as expected.

The set of facts is

F := {F (t 1 , . . . , t k )| t i ∈ T Σ , F ∈ Σ f act of arity k},
where Σ f act is an unsorted signature, disjoint from Σ. Facts will be used to annotate protocols (via events) and to define multiset rewrite rules. A fixed set of fact symbols will be used to encode the adversary's knowledge, freshness information, and the messages on the network. The remaining fact symbols are used to represent the protocol state. For instance, fact K(m) denotes that m is known by the adversary.

Syntax and Semantics

The grammar for terms (M, N ) and processes (P, Q), given in Table 1, follows [START_REF] Kremer | Automated analysis of security protocols with global state[END_REF]. In addition to usual operators for concurrency, replication, and name creation, the calculus A inherits from the applied π-calculus [START_REF] Abadi | Mobile values, new names, and secure communication[END_REF] input and output constructs in which terms appear both as communication subjects and objects. Also, A includes a conditional construct based on term equality, as well as constructs for reading from and updating an explicit global state:

insert((M, N )); P first binds the value N to a key M and then proceeds as P .

Successive inserts may modify this binding; delete M ; P simply "undefines" the mapping for the key M and proceeds as P . lookup M as x in P else Q retrieves the value associated to M , binding it to variable x in P . If the mapping is undefined for M then the process behaves as Q. lock M ; P and unlock M ; P allow to gain and release exclusive access to a resource/key M , respectively, and to proceed as P afterwards. These operations are essential to specify parallel processes that may read/update a common memory.

Moreover, the construct event F ; P adds F ∈ F to a multiset of ground facts before proceeding as P . These facts will be used in the transition semantics for A, which is de- fined by a labelled relation between process configurations of the form (E, S, P, σ, L), where: P is a multiset of ground processes representing the processes executed in parallel; E ⊆ F N is the set of fresh names generated by the processes; S : M Σ → M Σ is a partial function modeling stored information (state); σ is a ground substitution modeling the messages sent to the environment; and L ⊆ M Σ is the set of currently acquired locks. We write S(M ) = ⊥ to denote that there is no information stored for M in S. Also, notation L\M stands for the set L\{M |M = E M }.

a ∈ (FN ∪ PN) \ ñ [Name] ν ñ.σ a ν ñ.σ t t = E t [Eq] ν ñ.σ t x ∈ Dom(σ) [Frame] ν ñ.σ xσ ν ñ.σ t i [App] ν ñ.σ f t
We also require the notions of frame and a deduction relation. A frame ν ñ.σ consists of a set of fresh names ñ and a substitution σ: it represents the sequence of messages that have been observed by an adversary during a protocol execution and secrets ñ generated by the protocol, a priori unknown to the adversary. The deduction relation ν ñ.σ t models the adversary's ability to compute new messages from observed ones: it is the smallest relation between frames and terms defined by the rules in Table 2.

Transitions are of the form (E, S, P, σ, L)

F --→ A (E , S , P , σ , L )
, where F is a set of ground facts (see Table 3). We write

-→ A for ∅ -→ A and f --→ A for {f } ---→ A . As usual, --→ *
A denotes the reflexive, transitive closure of -→ A . Transitions denote either standard process operations or operations on the global state; they are sometimes denoted -→ A P and -→ A S , respectively.

Multiparty Session Processes (S)

Syntax The syntax of processes, ranged over by P, Q, . . . and that of expressions, ranged over by e, e , . . ., is given by the grammar of Table 4, which also shows name conventions. We assume two disjoint countable set of names: one ranges over shared names a, b, . . . and another ranges over session names s, s , . . .. Variables range over x, y, . . .; participants (or roles) range over the naturals and are denoted as p, q, p , . . .; labels range over l, l , . . . and constants range over true, false, . . .. We write p to denote a finite sequence of participants p 1 , . . . , p n (and similarly for other elements). Given a session name s and a participant p, we write s[p] to denote a (session) endpoint.

The intuitive meaning of processes is as in [START_REF] Honda | Multiparty asynchronous session types[END_REF][START_REF] Coppo | A gentle introduction to multiparty asynchronous session types[END_REF]. The processes u[p](y).P and u[p](y).Q can respectively request and accept to initiate a session through a shared name u. In both processes, the bound variable y is the placeholder for the channel that will be used in communications. After initiating a session, each channel placeholder will replaced by an endpoint of the form s[p i ] (i.e., the runtime channel of p i in session s). Within an established session, process may send and receive basic values or session names (session delegation) and select and offer labeled, deterministic choices (cf. constructs c ⊕ p, l .P and c &(p, {l i : P i } i∈I )). The input/output operations (including delegation) specify the channel and the sender or the receiver, respectively.

Standard Operations

(E, S, P ∪ # {0}, σ, L) -→ A (E, S, P, σ, L) (E, S, P ∪ # {P | Q}, σ, L) -→ A (E, S, P ∪ # {P, Q}, σ, L) (E, S, P ∪ # {!P }, σ, L) -→ A (E, S, P ∪ # {!P, P }, σ, L) (E, S, P ∪ # {νa; P }, σ, L) -→ A (E ∪ {a }, S, P ∪ # {P {a /a}}, σ, L) C0 (E, S, P, σ, L) K(M ) ----→ A (E, S, P, σ, L) C1 (E, S, P ∪ # {out(M, N ); P }, σ, L) K(M ) ----→ A (E, S, P ∪ # {P }, σ∪{N/x}, L) C2 (E, S, P ∪ # {in(M, N ); P }, σ, L) K( M,N τ ) --------→ A (E, S, P ∪ # {P τ }, σ, L) C3 (E, S, P ∪ # {out(M, N ); P, in(M , N ); Q}, σ, L) -→ A (E, S, P ∪ # {P, Qτ }, σ, L) C4 (E, S, P ∪ # {if M = N then P else Q}, σ, L) -→ A (E, S, P ∪ # {P }, σ, L) C5 (E, S, P ∪ # {if M = N then P else Q}, σ, L) -→ A (E, S, P ∪ # {Q}, σ, L) C6 (E, S, P ∪ # {event F ; P }, σ, L) F --→ A (E, S, P ∪ # {P }, σ, L)
Operations on Global State

(E, S, P ∪ # {insert((M, N )); P }, σ, L) -→ A (E, S[M → N ], P ∪ # {P }, σ, L) (E, S, P ∪ # {delete M ; P }, σ, L) -→ A (E, S[M → ⊥], P ∪ # {P }, σ, L) (E, S, P ∪ # {lookup M as x in P else Q}, σ, L) -→ A (E, S, P ∪ # {P {V /x}}, σ, L) C7 (E, S, P ∪ # {lookup M as x in P else Q}, σ, L) -→ A (E, S, P ∪ # {Q}, σ, L) C8 (E, S, P ∪ # {lock M ; P }, σ, L) -→ A (E, S, P ∪ # {P }, σ, L ∪ {M }) C9 (E, S, P ∪ # {unlock M ; P }, σ, L) -→ A (E, S, P ∪ # {P }, σ, L\M )
where: Message queues model asynchronous communication. A message (p q : v) indicates that p has sent a value v to q. The empty queue is denoted by ∅. By h • m we denote the queue obtained by concatenating message m to the queue h. By s[ p] : h we

C0: if a fresh C5: if M = E N C1: if νE.σ M C6: if M = E N C2: if x is fresh, νE.σ M C7: if ∃N.N = E M
| c! p, c .P (Deleg) | c?((q, y)).P (Recep) | c ⊕ p, l .P (Select) | c &(p, {li : Pi}i∈I ) (Branch) | if e then P else Q (Condit.) | P |Q (Parallel) | 0 (Inaction) | (νn)P (N.Hiding) | s[ p] : h (M. Queue) h ::= h•m | ∅ (Queue)
P | 0 ≡ P P | Q ≡ Q | P (P | Q) | R ≡ P | (Q | R) (νa)0 ≡ 0 (νs)(s : ∅) ≡ 0 (νr)P | Q ≡ (νr)(P | Q), if r / ∈ f n(Q) (νr)(νr )P ≡ (νr )(νr)P, where r ::= a | s s[ p] : h • (q p : ζ) • (q p : ζ ) • h ≡ s[ p] : h • (q p : ζ ) • (q p : ζ) • h , if p = p or q = q Table 5. Structural Congruence for S Processes.
denote the queue h of the session s initiated between participants p = p 1 , . . . , p n ; when the participants are clear from the context we shall write s : h instead of s[ p] : h.

Request/accept actions bind channel variables, value receptions bind value variables, channel receptions bind channel variables, hidings bind shared and session names. In (νs)P all occurrences of s[p] and queue s inside P are bound. We denote by f n(Q) the set of free names in Q. A process is closed if it does not contain free variables or free session names. Unless stated otherwise, we only consider closed processes.

Semantics S processes are governed by a reduction semantics, which relies on a structural congruence relation, denoted ≡ and defined by adding α-conversion to the rules of Table 5. Reduction rules are given in Table 6; we write P -→ S P for a reduction step. We rely on the following syntax for contexts:

E ::= [ ] | P | (νa)E | (νs)E | E | E.
We briefly discuss the reduction rules. Rule [Init] describes the initiation of a new session among n participants that synchronize over the shared name a. After session initiation, the participants will share a private session name (s in the rule), and an empty queue associated to it (s[ p] : ∅ in the rule). -Intra-session communication relies on annotated channels, and output prefixes include a sort for the communicated messages (msg for values, chan for delegated sessions, lbl for labels). -While S uses a single queue per session, in S for each pair of participants there will be two queues, one in each direction. This simplifies the definition of structural congruence ≡ for S , which results from that for S as expected and is omitted. -Constructs for session request and acceptance in S depend on a sequence of variables, rather than on a single variable. In these constructs, denoted u[p]( y).P and u[p]( y).P , respectively, y is a sequence of variables of the form y pq , for some p, q. With these differences in mind, the reduction semantics for S , denoted -→ S , follows that for S (Table 6). Reduction rules for S include the following:

a[p 1 ](y)P 1 | . . . | a[p n-1 ](y)P n-1 | a[pn](y).Pn -→ S [Init] (νs)(P 1 {s[p 1 ]/y} | . . . | P n-1 {s[p n-1 ]/y} | Pn{s[pn]/y} | s[ p] : ∅) s[p]! q, e .P | s : h -→ S P | s : h•(p q : v) (e ↓ v) [Send] s[p]! q, s [p ] .P | s : h -→ S P | s : h • (p q : s [p ]) [Deleg] s[p] ⊕ q, l .P | s : h -→ S P | s : h•(p q : l) [Sel] s[p]?(q, x).P | s : (q p : v)•h -→ S P {v/x} | s[ p] : h [Recv] s[p]?((q, y)).P | s : (q p : s [p ]) • h -→ S P {s [p ]/y} | s[ p] : h [SRecv] s[p] &(q, {l i : P i } i∈I ) | s : (q p : l j )•h -→ S P j | s : h (j ∈ I) [Branch] if e then P else Q -→ S P (e ↓ true) [If-T] P ≡ P and P -→ S Q and Q ≡ Q ⇒ P -→ S Q [Str] P -→ S P ⇒ E[P ] -→ S E[P ] [Ctx]
a[1]( y1).P1 | . . . | a[n -1]( yn-1).Pn-1 | a[n]( yn).Pn -→ S [Init * ] (νs)(P1{s/y} | . . . | Pn-1{s/y} | Pn{s/y} | y1{s/y} : ∅ | . . . | yn{s/y} : ∅) ypq! e : msg .P | ypq : h -→ S P | ypq : h • msg, v (e ↓ v) [Send * ] ypq?(x).P | yqp : msg, v • h -→ S P {v/x} | yqp : h [Recv * ]
Notice that in Rule [Init * ], we only need to write P i {s/y}: after reduction, these variables will be of the form s pq . In that rule, each y i {s/y} : ∅ denotes several queues (one for each name y pq ∈ y i ), rather than a single queue. It is straightforward to define an auxiliary encoding ([ • ]) : S → S . For instance:

([s[p]! q, e .P ]) = s pq ! e : msg .([P ]) ([s[p]?(q, x).P ]) = s qp ?(x).([P ]) ([s[p]! q, z p .P ]) = s pq ! z p : chan .([P ]) ([s[p]?((q, x)).P ]) = s qp ?((x

)).([P ])

The full encoding, given in [START_REF] Nantes | Relating Process Languages for Security and Communication Correctness (Full Version)[END_REF], enjoys the following property: Given the encoding ([ • ]) : S → S and Theorem 1 above, we now move on to define an encoding • : S * → A. By composing these encodings (and their correctness results-Theorems 2 and 3), we will obtain a behavioral-preserving compiler of S into A.

Encoding S Into A

We now present our encoding • : S * → A and establish its correctness. The encoding is defined in Table 7; it uses the set of facts F S = {honest, sndnonce, rcvnonce, sndchann, rcvchann, out, inp, dels, recs, sel, bra, close} . Facts will be used as event annotations in process executions, and also for model checking communication correctness via trace formulas in the following section. Our encoding will rely on the equational theory for pairing, which is embedded in Tamarin prover [START_REF] Meier | The TAMARIN prover for the symbolic analysis of security protocols[END_REF], and includes function symbols , , fst and snd, for pairing and projection of first and second parameters of a pair. Communication within a secure established session is expressed by the manipulation of queues, which will be stored in the set of states S. In SAPIC, we implement queues y pq and y qp as q(y, p, q) and q(y, q, p), respectively, where q is a function symbol for queues. Also, s pq : ∅ is implemented as insert((s pq , init)).

Implementing Session Establishment a[3]( y 3 ).P = νs; P 31 ; P 32 ; insert(( s ij , ∅)); event init( s ij ); event sndchann(pk(ska 31 ), pk(y 1 ), s); out(u 1 , s); event sndchann(pk(ska 32 ), pk(y 2 ), s); out(u 2 , s); P P 3i = νska 3i ; out(c, pk(ska 3i )); event honest(pk(ska 3i )); in(c, pk(y i )); νn 31 ; event sndnonce(pk(ska 3i ), pk(y i ), aenc( n 3i , pk(ska 3i ) , pk(y i ))) out(c, aenc( n 3i , pk(ska 3i ) , pk(y i )))); in(c, aenc( n 3i , u i , pk(y i ) , pk(ska 3i ))); event rcvnonce(pk(y i ), pk(ska 3i ), aenc( n 3i , u i , pk(y i ) , pk(ska 3i ))) a[i]( y i ).P = ν ska i ; in(c, pk(x i )); event honest(pk(ska i )); in(c, aenc( y, pk(x i ) , pk(ska i ))); event rcvnonce(pk(x i ), pk(ska i ), aenc( y, pk(x i ) , pk(ska i ))) νn i ; event sndnonce(pk(ska i ), pk(x i ), aenc( y, n i , pk(ska i ) , pk(x i ))) out(c, aenc( y, n i , pk(ska i ) , pk(x i ))); in(n i , z); event rcvchann(pk(x i ), pk(ska i ), z); P event dels(cpq, c ); unlock cpq; P cpq?((x)).P = lock cqp; lookup cqp as zv in (if fst(zv) = chan, z then (insert((cqp, snd(zv))); event recs(cpq, fst(zv)); unlock cqp; P {z/x} ) cpq ⊕ l : lbl .P = lock cpq; lookup cpq as x in (insert((cpq, x • lbl, l ))); event sel(cpq, l); unlock cpq; P cpq&({l i : P i }) = lock cqp; lookup cqp as z l in if fst(z l ) = lbl, l 1 then insert((cqp, snd(z l ))); event bra(cpq, l 1 ); unlock cpq; P 1 else if fst(z l ) = lbl, l 2 then insert((cqp, snd(z l ))); event bra(cpq, l 2 ); unlock cqp; P 2 0 = event close s[ p] : h = 0 (νs)P = νs; P

P | Q = P | Q if e then P else Q = if e then P else Q Table 7. Encoding from S to A.
Session Initiation. The (high-level) mechanism of session initiation of Rule [Init] in S (Table 6) is implemented in A by following the Needham-Schroeder-Lowe (NSL) authentication protocol [START_REF] Lowe | Breaking and fixing the needham-schroeder public-key protocol using FDR[END_REF]; see Table 7 (top). We use NSL because it is simple, and it has already been formalized in SAPIC. For simplicity, we present the implementation for three participants; the extension to n participants is as expected. The encoding creates queues for intra-session communication using processes insert(( s ij , ∅)). The security verification uses the built-in library asymmetric-encryption available in Tamarin [START_REF] Meier | The TAMARIN prover for the symbolic analysis of security protocols[END_REF], and assumes the usual signature and equational theory for public keys pk, secret keys sk, asymmetric encryption aenc and decryption dec.

Intra-session Communication. Process c pq ! e : msg .P first acquires a lock in the queue c pq to avoid interference. Then, a lookup as process checks the state of c pq and enqueues message msg, v at its end. Finally, the encoding signals this operation by executing event out(c pq , v) before unlocking c pq and proceeding as as P . The encoding of session delegation c pq ! c : chan .P is very similar: the only differences are the sort of the communicated object and the event signaled at the end (dels(c pq , c )).

As above, process c pq ?(x).P first acquires a lock and checks the queue c qp . If it is of the form msg,then it stores it in a variable z v : it consumes the first part (fst(z v )) and updates c qp with the second part. The implementation then signals an event event inp(c pq , z v ) before unlocking c qp and proceeding as P . Process c pq ?((x)).P (reception of a delegated session) is similar; in this case, the queue should contain a value of sort chan and the associated event is recs(c pq , fst(z v )).

Process 0 simply executes an event close. In the prototype SAPIC implementation of our encoding, this event mentions the name of the corresponding session c qp .

Finally, process c pq : h is 0 because we implement queues using the global state in A. The implementation of the remaining constructs in A is self-explanatory.

Remark 1. Since our encoding operates on untyped processes, we could have sort mismatches in queues (cf. Rule [If-F]). To avoid this, encodings of input-like processes (e.g., s pq ?(x).P ), use the input of a dummy value that allows processes to reduce.

Correctness of • . We first associate to each ground process P ∈ S * a process configuration via the encoding in Table 7. Below we assume that s, I, and I may be empty, allowing the encoding of communicating processes (obtained after session initiation); we also assume that the set of (free) variables in P (denoted var(P )) can be instantiated with ground terms that can be deduced from the current frame.

Definition 1 Suppose an S process R ≡ (νs)( i∈I P i | j,k∈I s pj q k : h j,k ), with var(R) = {x 1 , . . . , x n }. A process configuration for R, denoted C[ R ], is defined as:

(E ∪{s}, S ∪ {s pj q k : h j,k | j, k ∈ I }, i∈I P i , σ, L),
where var(R) ⊆ dom(σ) and σ is grounding for x i , i = 1, . . . , n.

With some abuse of notation we say that C is a process configuration for R. Observe that different process configurations C, C , . . . can be associated to a same process R ∈ S once one considers variations of E, S, σ, L.

Theorem 2 (Completeness). Let P ∈ S . If P -→ S P then for all process configuration C, there exists a process configuration C such that

C[ P ] --→ * A C [ P ].
Proof. The proof is by structural induction, analyzing the rule applied in P -→ S P via encoding in Table 7 and the rules in Table 3. See [START_REF] Nantes | Relating Process Languages for Security and Communication Correctness (Full Version)[END_REF] for details.

To prove soundness, we rely on a Labeled Transition System for S , denoted P λ -→ P . Such an LTS, and the proof of the theorem below, can be found in [START_REF] Nantes | Relating Process Languages for Security and Communication Correctness (Full Version)[END_REF].

Multiparty Session Types and Their Local Formulas

Using ([ • ]) and • , in this section we connect well-typedness of processes in S [START_REF] Honda | Multiparty asynchronous session types[END_REF] with the satisfiability of local formulas, which model the execution of A processes.

Global and Local Types

Rather than defining multiparty session types for A processes, we would like to model checking local types by re-using existing tools for A: SAPIC [START_REF] Kremer | Automated analysis of security protocols with global state[END_REF] and Tamarin [START_REF] Meier | The TAMARIN prover for the symbolic analysis of security protocols[END_REF].

Concretely, next we shall connect typability for S processes with satifiability for A processes. To formalize these results, we first recall some essential notions for multiparty session types; the reader is referred to [START_REF] Honda | Multiparty asynchronous session types[END_REF][START_REF] Coppo | A gentle introduction to multiparty asynchronous session types[END_REF] for an in-depth presentation.

Global types G, G describe multiparty session protocols from a vantage point; they offer a complete perspective on how two or more participants should interact. On the other hand, local (session) types T, T describe how each participant contributes to the multiparty protocol. A projection function relates global and local types: the projection of G onto participant n is denoted G| n . The syntax for global and local types, given in Table 8 is standard [START_REF] Honda | Multiparty asynchronous session types[END_REF]. A complete description of session types can found in [START_REF] Nantes | Relating Process Languages for Security and Communication Correctness (Full Version)[END_REF].

Example 1. Fig. 2 gives three global types for the protocol in § 2: while G init represents the first phase, both G contract and G sign are used to represent the second. In G sign , we use G resolvei to denote a global protocol for resolving conflicts; see [START_REF] Nantes | Relating Process Languages for Security and Communication Correctness (Full Version)[END_REF] for details.

Typing judgements for expressions and processes are of the form Γ e : S or Γ P ∆, where Γ ::= ∅ | Γ, x : S and ∆ ::= ∅ | ∆, c : T . The standard environment Γ assigns variables to sorts and service names to closed global types; the session environment ∆ associates channels to local types. We write Γ, x : S only if x / ∈ dom(Γ ), where dom(Γ ) denotes the domain of Γ . We adopt the same convention for a : G and c : T , and write ∆, ∆ only if dom(∆) ∩ dom(∆ ) = ∅. Typing rules are as in [START_REF] Honda | Multiparty asynchronous session types[END_REF][START_REF] Coppo | A gentle introduction to multiparty asynchronous session types[END_REF]; as discussed in those works, typability for S processes ensure communication correctness in terms of session fidelity (well-typed processes respect prescribed local protocols) and communication safety (well-typed processes do not feature communication errors), among other properties.

Satisfiability of Local Formulas from A

Following the approach in [START_REF] Kremer | Automated analysis of security protocols with global state[END_REF], properties of processes in A will be established via analysis of traces, which describe the possible executions of a process. This will allow us to prove communication correctness of S processes, using encoding • .

G init : (I.1) 3 → 1 : Title (I.2) 1 → {2, 3} : quote (I.3) 3 → 2 :
quote' Definition 1 (Traces of P [START_REF] Kremer | Automated analysis of security protocols with global state[END_REF]). Given a ground process P ∈ A, we define the set of traces of P , denoted by traces(P ), as

(I.4) 2 → {1, 3} : ok : G contract ¬ok : end G b : (1 ) 1 → 2 : T T = (G contract )| 1 G contract : (c.1) 1 → {2, 3} : contract (c.2) 3 → 2 : promise (c.3) 2 → 3 :        ok : 2 → 3 : promise 3 → 2 : ok : G sign ¬ok : 3 → 1 : abort ¬ok : end G sign : (s.1) 3 → 2 : signature 1 (s.1) 2 → 3 :          ok : 2 → 3 : signature 2 3 → 1 :    success : 3 → 1 : address 1 → 3 : date ¬success : 1 → 3 : G resolve 1 ¬ok : 2 → 1 : G resolve 2
traces(P ) = [F 1 , . . . , F n ] (∅, {P }, ∅, ∅) F 1 = == ⇒ . . . Fn = == ⇒ (En, Sn, Pn, σn, Ln)
We will denote by tr P , a trace from a set traces(P ), for some process P . We will write tr when P is clear from the context. Notice that, tr P = tr Q does not necessarily imply that P = Q: each process may implement more than one session in different ways.

SAPIC and Tamarin [START_REF] Meier | The TAMARIN prover for the symbolic analysis of security protocols[END_REF] consider two sorts: temp and msg. Each variable of sort s will be interpreted in the domain D(s); in particular, we will denote by V temp the set of temporal variables, which is interpreted in the domain D(temp) = Q; also, V msg is the set of message variables, which is interpreted in the domain D(msg) = M. Below, we will adopt a function θ : V → M ∪ Q that maps variables to terms respecting the variable's sorts, that is θ(x : s) ∈ D(s).

Definition 2 (Trace atoms [START_REF] Kremer | Automated analysis of security protocols with global state[END_REF]). A trace atom has of one of the forms:

A ::= ⊥ | t 1 ≈ t 2 | i j | i . = k | F @i
denoting, respectively, false, term equality, timepoint ordering, timepoint equality, or an action for a fact F and a timepoint i. The construction of trace formula ϕ respects the usual first-order convention:

ϕ, ψ ::= A | ¬ϕ | ϕ ∧ ψ | ϕ ∨ ψ | ϕ → ψ | ϕ ↔ ψ | (∃x : s).ϕ | (∀x : s).ϕ
Given a process P , in the definition below, tr denotes a trace in traces(P ), idx(tr) denotes the positions in tr, and tr i denotes the i-th position in tr.

Definition 3 (Satisfaction relation [START_REF] Kremer | Automated analysis of security protocols with global state[END_REF]). The satisfaction relation (tr, θ) ϕ between a trace tr, a valuation θ, and a trace formula ϕ is defined as follows

(tr, θ) ⊥ never (tr, θ) i j iff θ(i) < θ(j) (tr, θ) i . = j iff θ(i) = θ(j) (tr, θ) t 1 ≈ t 2 iff t 1 θ = E t 2 θ
(tr, θ) ¬ϕ iff not (tr, θ) ϕ (tr, θ) ϕ 1 ∧ ϕ 2 iff (tr, θ) ϕ 1 and (tr, θ) ϕ 2 (tr, θ) F @i iff θ(i) ∈ idx(tr) and F θ = E tr θ(i) (tr, θ) (∃x : s).ϕ iff there exists u ∈ D(s) such that (tr, θ[x → u]) ϕ Satisfaction of (∀x : s)ϕ, ϕ ∨ ψ and ϕ ⇒ ψ can be obtained from the cases above.

From Local Types to Local Formulas

Below we assume s is an established session between participants p and q. Given k : temp and a trace formula ϕ, we write ϕ(k) to say that there is a fact F such that F @k is an atom in ϕ. Below we assume that S is a subsort of msg.

Definition 4 (Local Formula). Given a local type T and an endpoint s[p], its local formula Φ s[p] (T ) is defined inductively as follows: Remark 2. Since each local type is associated to a unique local formula, the mapping Φ ( ) is invertible. That said, from a local formula ϕ we can obtain the corresponding type Φ -1 (ϕ). For instance, for the local formula ϕ out := ∃iz.(out(s pq , z)@i ∧ ψ(Φ s[p] (T )), one has Φ -1 (ϕ out ) = s[p] :! q, S .Φ -1 s[p] (ϕ ). The other cases are similar.

Φ s[p] (! q, S .T ) = ∃i, z.(out(s pq , z)@i ∧ ψ(Φ s[p] (T )) Φ s[p] (?(q, U ).T ) = ∃i, z.(inp(s pq , z)@i ∧ ψ(Φ s[p] (T )) Φ s[p] (⊕ q, {l i : T i } i∈I ) = ∃i. j∈I (sel(s pq , l j )@i ∧ ψ(Φ s[p] (T j )) Φ s[p] (&(q, {l i : T i } i∈I )) = ∃i. j∈I (bra(s pq , l j )@i ∧ ψ(Φ s[p] (T j )) Φ s[p] (end) = ∃i.close@i.
The following theorems give a bi-directional connection between (a) well-typednesss and (b) satisfiability of the corresponding local formulas (see [START_REF] Nantes | Relating Process Languages for Security and Communication Correctness (Full Version)[END_REF]): Theorem 4. Let Γ P ∆ be a well-typed S process. Also, let tr ∈ traces( ([P ]) ). Then there exists a θ such that (tr, θ) Φ(∆).

Theorem 5. Let tr and ϕ be a trace and a local formula, respectively. Suppose θ is an instantiation such that (tr, θ) ϕ. Then there is a P ∈ S such that

Γ ϕ P Φ -1 (ϕ)
where The local formula associated is:

Γ ϕ = {θ(x) : sort(x) | x ∈ dom(θ)} Example 2.
Φ s[3] (T ) = ∃i 1 , z 1 .
out(s 31 , z 1 )@i 1 ∧ (∃i 2 z 2 .inp(s 31 , z 2 )@i 2 ∧ (∃i 3 z 3 .out(s 32 , z 3 ))@i 3 ∧ (∃i 4 i 5 z 4 .((bra(s 32 , ok)@i 4 ∧ Φ s[3] (T )) ∨ bra(s 32 , ¬ok)@i 4 ∧ close@i 5 )))

∧ ((i 1 < i 2 < i 3 < i 4 ∧ ψ(Φ s[3] (T ))) ∨ (i 1 < i 2 < i 4 < i 5 ∧ ψ(Φ s[3] (T ))))
where T is the projection of G contract onto participant 3.

6 Revisiting the Two-Buyer Contract Signing Protocol We recall the motivating example introduced in § 2. Using a combination of constructs from S and A, we first develop a protocol specification which is compiled down to A using our encoding; the resulting A process can be then used to verify authentication and protocol correctness properties in SAPIC/Tamarin. Figure 2 shows the corresponding global types, and their associated local types (obtained via projection following [START_REF] Honda | Multiparty asynchronous session types[END_REF]). An alternative approach to specification/verification would be as follows. First, specify the protocol using S only, abstracting away from cryptography, and using existing type systems for S to enforce protocol correctness. Then, compile this resulting S specification down to A, where the resulting specification can be enhanced with cryptographic exchanges and authentication properties can be enforced with SAPIC/Tamarin.

Process Specification

Process specifications for B i and S are as follows:

B 1 = a[3](y).y[3]! 1, "Title" .y[3]?(1, x 1 ).y[3]! 2, x 1 div 2 .y[3]&(2, {ok : B sct 1 , ¬ok : 0}) B 2 = a[2](y).y[2]?(1, x 2 ).y[2]?(3, x 3 ).if x 2 -x 3 ≤ 99 then y[2] ⊕ {1, 3}, ok .B sct 2 else y[2] ⊕ {1, 3}, ¬ok .0 S = a[1](y).y[1]?(3, x 1 ).y[1]! {2, 3}, quote .y[1]&(2, {ok : b[2](z).y[2]! 1, y .z[2]?(1, x 4 ). y[1]! 2, date .0, ¬ok : 0}))
where processes B sct 1 and B sct 2 , which implement the contract signing phase, are as in Tables 9 and10, respectively. The specification for the trusted authority T is as follows:

b[1](z).z[1]?((2, t)).νsk(T ); t[3]! {1, 2}, pk(sk(T )) .y[1]?(3, z 2 ).y[1]?(2, z 3 ).(νs)insert((s, init)). (ν ct)t[3]! {1, 2}, ct .t[3]&({1, 2}, {abort : P T Ab , res 1 : P T R 1 , res 2 : P T R 2 , success : z[1]! 2, ok .0})}
where processes P T Ab , P T R1 , and P T R2 are given in Tables 11 and12. Process T illustrates how we may combine constructs from S (important to represent, e.g., session establishment on b and delegation from S) and features from A (essential to, e.g., manipulate the memory cell s, which records contract information). Indeed, T uses the A construct insert to initialize the cell s and lookup as to update it. Therefore, the sound and complete encoding proposed in § 4 allows us to specify processes in A, while retaining the high-level constructs from S. Process specifications for B 2 , S, and T in A can be obtained similarly. As mentioned in § 4, the communication is done via updating session queues s ij , for i, j = 1, 2, 3.

Using SAPIC/Tamarin to Verify Authentication and Local Session Types

We conclude this section by briefly discussing how to use our developments to verify properties associated to authentication and protocol correctness.

Concerning authentication, we can use SAPIC/Tamarin to check the correctness of the authentication phase implemented by NSL. The proof checks that events honest( ), sndnonce( , , ), rcvnonce( , , ), and rcvchann( , , ) occur in the order specified by the encoding in Table 7. This way, e.g., the following lemma verifies the correctness of the specification of the fragment of NSL authentication with respect to participant B 2 : lemma B2 NSL correctness : existstrace (All pk 12 pk 1s pk 2 pks #i #j #k #l.

honest(pk 12 )@i & honest(pk 1s )@j & honest(pk 2 )@k & honest(pks)@l =⇒ (Ex x y z s #j 1 #k 1 #l 1 .rcvnonce(pk 12 , pk 2 , x, y)@j 1 & sndnonce(pk 2 , pk 12 , z)@k 1 & rcvchann(pk 12 , pk 2 , s)@l 1 &j 1 < k 1 & k 1 < l 1 ))

The lemma below says that the session channel exchanged using NSL is secret. The proof relies on asymmetric-encryption, which is built in the Tamarin library. lemma Chann is secret : (All pk 12 pk 2 pk 1s pks s z n x y w z n 2 #i #j #l #i 1 #i 2 #j 1 #j 2 #k 1 #l 1 #l 2 . (honest(pk 12 )@i& honest(pk 2 )@j & honest(pk 1s )@k & honest(pks)@l & sndnonce(pk 2 , pk 12 , z)@i 1 & rcvnonce(pk 2 , pk 12 , n, z)@j 1 & sndnonce(pk 12 , pk 2 , w)@i 2 & rcvnonce(pk 12 , pk 2 , n 2 , w)@j 2 & sndnonce(pks, pk 1s , x)@i 3 & rcvnonce(pks, pk 1s , y, x)@j 2 & sndchann(pk 12 , k 2 , s)@k 1 & rcvchann(pk12, pk2, s)@k 2 & sndchann(pk 1s , pks, s)@l 1 & rcvchann(pk12, pk2, s)@l 2 ) =⇒ not(Ex #j. KU(s)@j))

We now consider properties associated to fidelity/safety of processes with respect to their local types. The lemma below ensures protocol fidelity of B 1 and B 2 with respect to the corresponding projections of the global type G init , presented in Figure 2. The corresponding local formula can be obtained following Definition 4: Using similar lemmas, we can also prove protocol fidelity for processes S and T with respect to the projections of the global types presented in Figure 2.

Related Works and Concluding Remarks

We have connected two distinct process models: the calculus S for multiparty sessionbased communication [START_REF] Honda | Multiparty asynchronous session types[END_REF] and the calculus A for the analysis of security protocols [START_REF] Kremer | Automated analysis of security protocols with global state[END_REF]. To our knowledge, this is the first integration of sessions (in the sense of [START_REF] Hüttel | Foundations of session types and behavioural contracts[END_REF]) within process languages for security protocol analysis. Indeed, research on security extensions to behavioral types (cf. the survey [START_REF] Bartoletti | Combining behavioural types with security analysis[END_REF]) seems to have proceeded independently from approaches such as those overviewed in [START_REF] Cortier | Formal models and techniques for analyzing security protocols: A tutorial[END_REF]. The work in [START_REF] Corin | Secure implementations for typed session abstractions[END_REF] is similar in spirt to ours, but is different in conception and details, as it uses a session graph specification to generate a cryptographic functional implementation that enjoys session integrity. Extensions of session types (e.g., [START_REF] Capecchi | Typing access control and secure information flow in sessions[END_REF][START_REF] Pfenning | Proof-carrying code in a session-typed process calculus[END_REF]) address security issues in various ways, but do not directly support cryptographic operations, global state, nor connections with "applied" languages for (automated) verification, which are all enabled by our approach.

Our work should be mutually beneficial for research on (a) behavioral types and contracts and on (b) automated analysis of security protocols: for the former, our work enables the analysis of security properties within multiparty session protocols; for the latter, our approach enables protocol specifications enriched with high-level communication structures based on sessions. In ongoing work, we have used SAPIC/Tamarin to implement our encodings and the verification technique for communication correctness, based on local formulas (Def. 4). Results so far are very promising, as discussed in § 6.

In future work, we intend to explore our approach to process specification and verification in the setting of ProVerif [START_REF] Blanchet | Modeling and verifying security protocols with the applied pi calculus and proverif[END_REF], whose input language is a typed applied π-calculus. We also plan to connect our approach with existing type systems for secure information flow and access control in multiparty sessions [START_REF] Capecchi | Typing access control and secure information flow in sessions[END_REF].

  Session π-calculus (S) High-level Protocol Structures Applied π-calculus (A) Term Passing / Global State

Fig. 1 .

 1 Fig. 1. The Trusted Buyers-Seller Protocol.

  and S(N ) = E V C3: if ∃τ.νE.σ M and νE.σ N τ and τ grounding for N C8: if ∀N.N = E M ⇒ S(N ) = ⊥ C4: if M = E M and ∃τ.N = E N τ and τ grounding for N C9: if M / ∈ E L Table 3. Operational Semantics for A. u ::= x | a (Identifiers) n ::= s | a (Names) e ::= v | x | e = e | . . . (Expressions) c ::= s[p] | x (Channels) v ::= a | true | false | s[p] (Values) m ::= (q p : v) | (q p : c) | (q p : l) (Messages) P ::= u[p](y).P (Req) | u[p](y).P (Acc) | c! p, e .P (Send) | c?(p, x).P (Recv)

  Rules [Send], [Deleg] and [Sel] add values, channels and labels, respectively, into the message queue; in Rule [Send], e ↓ v denotes the evaluation of the expression e into a value v. Rules [Recv], [SRecv] and [Branch] perform complementary de-queuing operations. Other rules are self-explanatory.3.3 The Calculus S We now introduce S , a variant of S which will simplify the definition of our encoding into A. The syntax of S processes is as follows: P, Q ::= 0 | u[p]( y).P | u[p]( y).P | P | Q | (νn)P | if e then P else Q | c pq ! e : msg .P | c pq ?((y)).P | c pq ?(x).P | c pq ! c p q : chan .P | | c pq ⊕ l : lbl .P | c pq &({l i : P i } i∈I ) | s pq : h where c pq denotes a channel annotated with participant identities, h ::= h • m | ∅ and m ::= msg, v | chan, s pq | lbl, l . The main differences between S and S are:

Theorem 1 .

 1 Let P ∈ S. Then: (a) If P -→ S P , then ([P ]) -→ S ([P ]). (b) If ([P ]) -→ S R, then there exists P ∈ S such that P -→ S P and ([P ]) = R.

Theorem 3 ( 8 .

 38 Soundness). Let P ∈ S and C be such that C[ P ] -→ A P R. Then there exist P ∈ S , a C , and λ such that R --→ * A C [ P ] and P λ -→ P . S ::= bool | nonce | msg | temp | . . . | G Sorts U ::= S | T Exchange Types (Global Types) G ::= p → q : U .G | p → q : {li : Gi}i∈I | end (Local Types) T ::=! p, U .T | ?(p, U ).T | ⊕ p, {li : Ti} | &(p, {li : Ti}) | endTable Global and Local Types [10].

Fig. 2 .

 2 Fig. 2. Global Types for the Trusted Buyer-Seller Protocol ( § 2).

  where ψ(Φ s[p] (T )) := ∀k.(Φ s[p] (T )(k) ⇒ i k)) the quantified variables have sorts i, j, k : temp and z : S, and variables i and z are fresh. The extension of Φ( ) to session environments, denoted Φ( ), is as expected: Φ(∆, s[p] : T ) = Φ(∆) ∧ Φ s[p] (T ).

  lemma B1 B2 protocol fidelity : existstrace (Ex x y z s #j #j 1 #k #k 1 #l.out(s 31 , x)@j & inp(s 31 , z)@k & out(s 32 , s)@l & j < k & k < l & ((bra(s 32 , ok))@j 1 & l < j 1 ) | (bra(s 32 , ¬ok)@k 1 & l < k 1 & Φ(Gcontract| 3 ))) & (Ex x y z s #j #j 1 #k #k 1 #l. inp(s 21 , z)@k & inp(s 23 , s)@l & j < k & k < l &((sel(s 23 , ok)@j 1 & l < j 1 & Φ(Gcontract| 2 )) | (sel(s 23 , ¬ok)@k 1 & l < k 1 ))

  B 1 tells B 2 how much he can contribute. 2. If the amount is within B 2 's budget, then he accepts to perform the transaction, informs B 1 and S, and awaits the contract signing phase. Otherwise, if the amount offered by B 1 is not enough, B 2 informs S and B 1 his intention to abort the protocol. 3. Once B 1 and B 2 have agreed upon the purchase, S will delegate the session to the trusted party T , which will lead the contract signing phase. Upon completion of this phase, S (implemented by T ) sends B 1 the delivery date for the book. Second Phase At this point, the trusted authority T , B 1 , and B 2 interact as follows: 4. T creates a new contract ct and a new memory cell s, useful to record information about the contract. T sends the contract ct to B 1 and B 2 for them to sign. T can start replying to the following requests: success (in case of successful communication), abort (request to abort the protocol), or resolve (request to solve a conflict). 5. Upon reception of contract ct from T , B 1 sends to B 2 his promise to sign it. Subsequently, B 1 expects to receive B 2 's promise: • If B 1 receives a valid response from B 2 , his promise is converted into a signature ( signature 1 ), which is sent back. Now, B 1 expects to receive a valid signature from B 2 : if this occurs, B 1 sends to T a success message; otherwise, B 1 sends T a resolve request, which includes the promise by B 2 and his own signature. • If B 1 does not receive a valid promise from B 2 , then B 1 asks T to cancel the purchase (an abort request), including his own promise ( promise 1 ) in the request. 6. Upon reception of contract ct from T , B 2 checks whether he obtained a valid promise from B 1 ; in that case, B 2 replies by sending his promise to sign it ( promise 2 ). Now, B 2 expects to receive B 1 's signature on ct: if the response is valid, B 2 sends its own signature ( signature 2 ) to B 1 ; otherwise, B 2 asks T to resolve. If B 2 does not receive a valid promise, then it aborts the protocol.

[START_REF] Bartoletti | Combining behavioural types with security analysis[END_REF]

, and S start by establishing a session, after executing the Needham-Schroeder-Lowe (NSL) authentication protocol. Subsequently, they interact as follows:

1. B 1 sends the book title to S. Then, S replies back to both B 1 and B 2 the quote for the title. Subsequently,

Table 1 .

 1 | νn; P | insert((M, N )); P | delete M ; P | lookup M as x in P else Q | lock M ; P | unlock M ; P | event F ; P | if M = N then P else Q Syntax of A: Terms and Processes.

Table 2 .

 2 Deduction rules for A. In Rule [Appl]: t = (t1, . . . , tn).

Table 4 .

 4 Process syntax and naming conventions for S.

Table 6 .

 6 Reduction rules for S (Rule [If-F] omitted).

  The projection of G init onto participant 3 (Buyer1), under session s is: s[3] : ! 1, string .?(1, int).! 2, int .&(2, {ok : (G contract |3), ¬ok : end}).

  P T res 1 = lock s; y[1]?(3, y 3 ).if m 11 = Epcs true then (if m 12 = Epcs true then (lookup s as y 3 in (if f st(y 3 ) = abort then y[1]! 3, snd(y 3 ) .unlock s)) else (if f st(y 3 ) = res 2 then y[1]! 3, snd(y 3 ) .z[1]! 2, ok ; unlock s)) ); if m 21 = Epcs true then (if m 22 = Epcs true then (lookup s as w 3 in (if f st(w 3 ) = abort then y[1]! 2, snd(w 3 ) ; unlock s)) else (if f st(w 3 ) = res 1 then (y[1]! 2, snd(w 3 ) ; z[1]! 2, ok ; unlock s))

	else y[1]! 3, tconvert(sk(T ), snd(m 1 )) .z[1]! 2, ok .unlock s))
	P T res 2 = lock s; y[1]?(2, w 3 else y[1]! 3, tconvert(sk(T ), f st(m 2 )) ; insert((s, res 2 , snd(w 3 ) ));
	z[1]! 2, ok ; unlock s))

Table 12 .

 12 P T res 1 e P T res 2 : resolve processes executed by T

νs; P 31 ; P 32 ; insert(( s ij , ∅)); event init( s ij ); event sndchann(pk(ska 31 ), pk(y 1 ), s); out(u 1 , s); event sndchann(pk(ska 32 ), pk(y 2 ), s); out(u 2 , s); lock s 31 ; lookup s 31 as x 31 in insert((s 31 , x 31 • msg, "Title" )); event out(s 31 , "Title"); unlock s 31 ; lock s 13 ; lookup s 31 as x in if f st(x) = msg, z then insert((s 31 , snd(x))); event inp(s 31 , z); unlock s 13 lock s 32 ; lookup s 32 as x 32 ; in insert((s 32 , msg, "quote" )); event out(s 32 , "quote"); unlock s 32 ; lock s 23 ; lookup s 23 as x 23 in (if f st(x 23 ) = lbl, ok then insert((s 23 , snd(x 23 ))); event bra(s 23 , accept); unlock s 23 ; B sct 1 else event bra(s 23 , ¬ok); unlock s 23 ; 0)

Table 13 .

 13 Translation of B1 into A.

Acknowledgements We are grateful to the anonymous reviewers for their useful remarks and suggestions. Pérez is also affiliated to the NOVA Laboratory for Computer Science and Informatics (supported by FCT grant NOVA LINCS PEst/UID/CEC/04516/2013), Universidade Nova de Lisboa, Portugal.

B sct 1 = y [START_REF] Blanchet | Modeling and verifying security protocols with the applied pi calculus and proverif[END_REF]?(1, z 1 ).νsk(B 1 ).y [START_REF] Blanchet | Modeling and verifying security protocols with the applied pi calculus and proverif[END_REF]! {1, 2}, pk(sk(B 1 )) .y [START_REF] Blanchet | Modeling and verifying security protocols with the applied pi calculus and proverif[END_REF]?(2, z 3 ).y [START_REF] Blanchet | Modeling and verifying security protocols with the applied pi calculus and proverif[END_REF]? (

Table 10. B sct 2 : B2's contract signing processes.

else (if f st(y 2 ) = abort then y[1]! 3, y 2 ; unlock spq))))

else if f st(y 2 ) = res i then y[1]! 3, y 2 ; unlock spq)))) with function symbols for promises and signatures, and for verifying the validity of exchanged messages. As for constructors: pcs(x, y, w, z) is the promise of x to y to sign contract z given by w; sign(x, y) is the signature of x in z; pk(x) is the public key of x; sk(x) is the secret key of x; aenc(x, y) is the asymmetric encryption of y using key x; and senc(x, y) is the symmetric encryption of y using key x. Destructor sdec(, ) (resp. adec(, )) enforces symmetric (resp. asymmetric) decryption; the other destructors (sconvert, tconvert, pcsver, sverif) are defined from the rules in E pcs :

sdec(x, senc(x, y)) -→ y adec(sk(x), aenc(pk(x), y)) -→ y sver(pk(x), z, sign(x, z)) -→ true tconvert(w, pcs(x, y, pk(w), z)) -→ sign(x, z) pcsver(pk(x), y, w, z, pcs(x, y, w, z)) -→ true sconvert(x, pcs(x, y, w, z)) -→ sign(x, z)

Table 13 shows the translation of B 1 in A, using our encoding. For simplicity, we omit the details related to the session establishment (using NSL), which follow Table 7.


Henryk Fukś

Francis Kwaku Combert

Evaluating the Quality of Local Structure Approximation Using Elementary Rule 14

Keywords: rule 14, local structure approximation, invariant manifolds

 In spite of the popularity of this approximation in CA research, examples of rigorous evaluations of its accuracy are lacking. In an attempt to fill this gap, we construct a local structure approximation for rule 14, and study its dynamics in a rigorous fashion, without relying on numerical experiments. We then compare the outcome with known exact results.

Introduction

One-dimensional elementary cellular automata (CA) can be viewed as maps in the space of probability measures over bi-infinite binary sequences (to be called configurations). This can be understood as follows. Suppose that we start with a large set of initial configurations drawn from a certain distribution (for example, from the Bernoulli distribution). Let us now suppose that we apply a given cellular automaton rule to all these configurations. The resulting set of configurations is usually no longer described by Bernoulli distribution, but by some other distribution. We can thus say that the CA rule transforms the initial probability measure into some other measure, and when we apply the local rule again and again, we obtain a sequence of measures, to be called the orbit of the initial measure.

This approach, however, is not without difficulties. In order to fully describe a probability measure over bi-infinite binary sequences, one needs to specify infinitely many block probabilities, that is, probabilities of the occurrence of 0, 1, 00, 01, 10, 11, 000, etc -in short, the probabilities of occurrence of all possible binary words. This means that the CA rule treated as a map in the space of probability measures is an infinitely-dimensional map.

Infinite-dimensional maps are difficult to investigate, even numerically, thus from the early days of CA research, efforts were made to find a way to approximate them by finite-dimensional maps. In a seminal paper [START_REF] Gutowitz | Local structure theory for cellular automata[END_REF], published over 30 years ago, H. Gutowitz et al. proposed such an approximation, which they called the local structure theory. It was an application of a well know idea of Bayesian extension, widely used in statistical physics as a basis of so-called mean-field theories, finite-cluster approximations, and related methods.

Since 1987 the local structure theory has been widely used in CA research, as witnessed by a large number of citations of [START_REF] Gutowitz | Local structure theory for cellular automata[END_REF]. This could be somewhat surprising, given that relatively few rigorous results are known about the local structure theory. Usually, the authors using this method simply construct a finite-dimensional map or recurrence equations following the recipe given in [START_REF] Gutowitz | Local structure theory for cellular automata[END_REF], and declare that these posses orbits approximating the dynamics of the actual CA or related system which they investigate. Judgments on the quality of the approximation are usually made based on numerical iterations of local structure maps and numerical simulations of the CA in question. Numerical results are thus compared with other numerical results.

In recent years, however, partial orbits of Bernoulli measures have been computed for some selected elementary CA [START_REF] Fukś | Orbits of Bernoulli measures in cellular automata[END_REF], making a somewhat more rigorous approach possible. The goal of this paper is to provide an example of a CA rule for which some block probabilities are known exactly, and for which local structure equations can be analyzed rigorously, without relying exclusively on numerical iterations. This way, the quality of the approximation could be evaluated in a solid and rigorous fashion, without worrying about numerical errors, finite size effects, etc.

We selected elementary CA rule 14 as the most promising example for such study. It has several interesting features: exact probabilities of blocks of length up to three are known for the orbit of the symmetric Bernoulli measure under this rule, and some of these block probabilities exhibit non-trivial behaviourfor example, convergence toward the steady state as a power law with fractional exponent. At the same time, rule 14 conserves the number of pairs 10 [4], and the existence of this additive invariant provides a constrain simplifying local structure equations, making them easier to analyze. Since block probabilities of length 3 are known for this rule, we will construct local approximation of level 3 and investigate its dynamics not only by simple numerical iterations, but by finding invariant manifolds at the fixed point and determining the nature of the flow on these manifolds.

One should stress here that in what follows we will use only very minimal formalism. More formal details about the construction of probability measures over infinite bisequences and the construction of local structure maps for arbitrary rules (both deterministic and probabilistic) can be found in [START_REF] Fukś | Construction of local structure maps for cellular automata[END_REF], where the reader will also find more references on these subjects.

Preliminary remarks about rule 14

Consider the fully discrete dynamical system (called cellular automaton) where

s i (n) ∈ {0, 1} is the state of site i ∈ Z at time n ∈ N, with dynamics defined by s i (n + 1) = f (s i-1 (n), s i (n), s i+1 (n)). The function f : {0, 1} 3 → {0, 1}
is called the local rule. In this paper, we will consider f which is defined by f (x 0 , x 1 , x 2 ) = x 1 + x 2 -x 1 x 2 -x 0 x 1 -x 0 x 2 + x 0 x 1 x 2 , and we call the above rule 14, following the numbering scheme of Wolfram [START_REF] Wolfram | Cellular Automata and Complexity: Collected Papers[END_REF].

Usually, the initial state at n = 0 is drawn from the Bernoulli distribution, where each site s i (0) is either in state 1 with probability ρ, or in state 0 with probability 1 -ρ, independently of each other, where ρ ∈ [0, 1]. When ρ = 1/2, we call this symmetric Bernoulli distribution.

A classical problem in cellular automata theory is to compute the probability of the occurrence of a given binary string a in a configuration obtained after n iterations of the rule, assuming that the initial configuration is drawn from the Bernoulli distribution. Such probability will be denoted by P n (a) and called block probability. It is easy to show that if the initial distribution is Bernoulli, then the probability of occurrence of a is independent of its position in the configuration. We will call such block probabilities shift invariant.

The set of shift-invariant block probabilities P n (a) for all binary strings a defines a shift-invariant probability measure on the set of infinite binary bisequences, but we will not be concerned with the formal construction of such measures here. Interested reader can find all relevant details and references in [START_REF] Fukś | Construction of local structure maps for cellular automata[END_REF].

Consider now a configuration in which s i (n + 1) = 1. By using the definition of rule f , one can easily figure out that s i (n + 1) is determined entirely by the triple (s i-1 (n), s i (n), s i+1 (n)), and that the only possible values of (s i-1 (n), s i (n), s i+1 (n)) producing s i (n + 1) = 1 are (0, 0, 1), (0, 1, 0) or (0, 1, 1). This means that probability of obtaining 1 at time n + 1 is equal to the sum of probabilities of ocurrence of blocks 001, 010, and 011 at time n, P n+1 (1) = P n (001) + P n (010) + P n (011). One can carry out a similar reasoning for longer blocks. For example, a pair of 1s, that is, s i (n + 1) = 1 and s i+1 (n + 1) = 1, can appear only and only if at the previous time step n the lattice positions i-1, i, i+ 1, i + 2 assumed values 0,0,1,0 or 0,0,1,1, i.e., (

s i-1 (n), s i (n), s i+1 (n), s i+2 (n)) = (0, 0, 1, 0) or (s i-1 (n), s i (n), s i+1 (n), s i+2 (n)) = (0, 0, 1, 1
). This yields P n+1 (11) = P n (0010) + P n (0011).

Obviously, one can write analogous equations for probabilities of any binary block, obtaining an infinite system of difference equations. The complete set of such equations for blocks of length up to 3 for rule 14 is shown below. P n+1 (0) = P n (000) + P n (100) + P n (101) + P n (110) + P n (111), P n+1 (1) = P n (001) + P n (010) + P n (011), P n+1 (11) = P n (0010) + P n (0011), P n+1 (00) = P n (0000) + P n (1000) + P n (1100) + P n (1101) + P n (1110) + P n (1111), P n+1 (01) = P n (0001) + P n (1001) + P n (1010) + P n (1011), P n+1 (10) = P n (0100) + P n (0101) + P n (0110) + P n (0111), P n+1 (000) = P n (00000) + P n (10000) + P n (11000) + P n (11100) + P n (11101) + P n (11110) + P n (11111), P n+1 (001) = P n (00001) + P n (10001) + P n (11001) + P n (11010) + P n (11011), P n+1 (010) = P n (10100) + P n (10101) + P n (10110) + P n (10111), P n+1 (011) = P n (00010) + P n (00011) + P n (10010) + P n (10011), P n+1 (100) = P n (01000) + P n (01100) + P n (01101) + P n (01110) + P n (01111), P n+1 (101) = P n (01001) + P n (01010) + P n (01011), P n+1 (110) = P n (00100) + P n (00101) + P n (00110) + P n (00111),

P n+1 (111) = 0. ( 1
)
One thing which is immediately obvious is that not all of these equations are independent because the block probabilities themselves are not independent. Block probabilities must satisfy so-called Kolmogorov consistency conditions, which are in fact just additivity conditions satisfied by a measure induced by block probabilities. For example, we must have P n (1) + P n (0) = 1, P n (01) + P n (00) = P n (0), etc. Consistency conditions can be used to express some block probabilities by others. One can show that for binary strings, among probabilities of blocks of length k, only 2 k-1 are independent [START_REF] Fukś | Construction of local structure maps for cellular automata[END_REF], in the sense that one can choose 2 k-1 block probabilities which are not linked to each other via consistency conditions. For blocks of length up to 3, there are 14 block probabilities, P n (0), P n (1), P n (00), P n (01), P n (10), P n (11) P n (000), P n (001), P n (010), P n (011), P n (100), P n (101), P n (110), and P n (111). Among them only 2 3-1 = 4 are independent.

While there is some freedom in choosing which ones are to be treated as independent, we will choose the following four, P n (0), P n (00), P n (000), and P n (010). This is called the short block representation, and a detailed algorithm for choosing block this way is described in [START_REF] Fukś | Construction of local structure maps for cellular automata[END_REF]. Here it is sufficient to say that short block representation ensures that the blocks selected as independent are the shortest possible ones.

Using consistency conditions, one can now express the remaining blocks of length up to 3 in terms of P n (0), P n (00), P n (000), and P n (010), as follows:

P n (1) = 1 -P n (0), P n (01) = P n (0) -P n (00), P n (10) = P n (0) -P n (00), P n (11) = 1 -2 P n (0) + P n (00), P n (001) = P n (00) -P n (000), P n (011) = P n (0) -P n (00) -P n (010), P n (100) = P n (00) -P n (000), P n (101) = P n (0) -2 P n (00) + P n (000), P n (110) = P n (0) -P n (00) -P n (010),

P n (111) = 1 -3 P n (0) + 2 P n (00) + P n (010). ( 2
)
Using the above substitutions one can reduce eqs. (1) to the following set of four equations,

P n+1 (0) = 1 -P n (0) + P n (000), (3)
P n+1 (00) = 1 -2P n (0) + P n (00) + P n (000), P n+1 (000) = 1 -3P n (0) + 2P n (00) + P n (000) + P n (010) -P n (01000), P n+1 (010) = P n (0) -2P n (00) + P n (000).

Note that the above cannot be iterated, because on the right hand side, in addition to the four aforementioned independent probabilities, we have probability P n (01000), the probability of the block of length 5.

Fortunately, in spite of the above problem, if the initial Bernoulli measure is symmetric, exact expressions for probabilities P n (0), P n (00), P n (000) and P n (010) for rule 14 (that is, the solution of eqs. ( 3)) can be obtained by combinatorial methods. We will quote the relevant results below, omitting the proof, which can be found in [START_REF] Fukś | Catalan numbers and power laws in cellular automaton rule 14[END_REF].

Proposition 1 [START_REF] Fukś | Catalan numbers and power laws in cellular automaton rule 14[END_REF]). For elementary rule 14, if the initial configuration is drawn from symmetric Bernoulli distribution, the probabilities of block of length up to 3 are given by

P n (0) = 1 2 1 + 2n -1 4 n C n-1 , (4)
P n (00) = 2 -2-2 n (n + 1)C n + 1 4 , (5)
P n (000) = 2 -2n-3 (4 n + 3) C n , (6)
P n (010) = 2 -2-2 n (n + 1) C n , (7)
where C n is the n-th Catalan number, C n = 1 n+1 2n n . Note that although the above proposition provides probabilities of P n (0), P n (00), P n (000) and P n (010) only, the remaining probabilities of blocks of length up to 3 can be easily computed using eqs. [START_REF] Devaney | An Introduction to Chaotic Dynamical Systems[END_REF].

Although we know exact solution of eqs.

(3), we can also attempt to obtain an approximate solution by approximating the "problematic" block probability P n (01000). There exists a method for approximating longer block probabilities by probabilities of shorter blocks. This method is called the Bayesian extension, and it is known to produce block probabilities satisfying consistency conditions [START_REF] Fukś | Construction of local structure maps for cellular automata[END_REF]. Applying the Bayesian extension to P n (01000), one obtains P n (01000) ≈ P n (010)P n (100)P n (000) P n (10)P n (00) .

In the above, by definition, the fraction on the right hand side is considered to be zero whenever its denominator is equal to zero. Using eqs.

(2) we can now express P n (01000) in terms of our four independent block probabilities, P n (01000) ≈ P n (010) (P n (00) -P n (000)) P n (000) (P n (0) -P n (00)) P n (00) .

If we replace P n (01000) in eqs. (3) by the above approximation, we will obtain the system of four coupled difference equations,

x n+1 = -x n + z n + 1, (10)
y n+1 = -2 x n + y n + z n + 1, (11)
z n+1 =1 + z n + v n -3 x n + 2 y n - v n (y n -z n ) z n y n (x n -y n ) , (12)
v n+1 =x n -2 y n + z n , (13)
where for brevity we introduced variables x n = P n (0), y n = P n (00), z n = P n (000). and v n = P n (010). Equations ( 10)-(13) will be referred to as local structure equations of level 3, following nomenclature of [START_REF] Gutowitz | Local structure theory for cellular automata[END_REF][START_REF] Fukś | Construction of local structure maps for cellular automata[END_REF]. The designation "level 3" pertains to the fact that we used block probabilities of length up to 3.

Exact solutions vs. local structure approximation

How does the orbit of local structure equations ( 10)-( 13) compare with known exact solutions given by eq. ( 4)-( 7)? In order to find this out, we will assume that the initial probability measure is symmetric Bernoulli, meaning that x 0 = P 0 (0) = 1/2, y 0 = P 0 (00) = 1/4, z 0 = P 0 (000) = 1/8, and v 0 = P 0 (010) = 1/8. Figure 1 shows differences between exact probabilities obtained from eq. ( 4)- (7) and values obtained by iterating local structure equations ( 10)-(13). Two differences are shown, P n (00) -y n (lower curve) and P n (000) -z n (upper curve).

In both cases we can see that the difference tends to zero as n → ∞. Values of P n (0) -x n and P n (010) -v n (not shown) exhibit similar behaviour. This indicates that even though the local structure approximation of level 3 does not produce exact values of block probabilities at finite n, it seems to become exact in the limit n → ∞. To verify this, let us first note that from eq. ( 4)-( 7) we obtain

lim n→∞ P n (0) = 1 2 , lim n→∞ P n (00) = 1 4
, lim n→∞ P n (000) = 0, lim n→∞ P n (010) = 0.

We will denote these values by (x , y , z , v ) = ( 1 2 , 1 4 , 0, 0). One can easily verify that (x , y , z , v ) is a fixed point of eqs. ( 10)-( 13). In what follows, we will investigate stability of this fixed point. We will prove that the following property holds.

Proposition 2. If the dynamical system given by eqs. ( 10)-( 13) is iterated starting from initial conditions x 0 = 1/2, y 0 = 1/4, z 0 = 1/8, and v 0 = 1/8, then lim n→∞ (x n , y n , z n , v n ) = (x , y , z , v ) = 1 2 , 1 4 , 0, 0 . This means that the local structure map approximates the exact probabilities remarkably well, converging to the same fixed point as the exact values. We will prove Proposition 2 by reducing local structure equations to two dimensions and by computing local manifolds at the fixed point.

Reduction to two dimensions

Close examination of equations ( 10)-(13) reveals some obvious symmetries. First of all, it is easy to check that x n+1 -y n+1 = x n -y n . Since x 0 -y 0 = 1 4 , we have x n -y n = 1 4 for all n, thus

x n = y n + 1 4 . ( 14
)
Further simplification is possible. Note that v n+1 -

y n+1 = 3(x n -y n ) -1 = 3• 1 4 -1 = -1 4
. This implies that for any n > 0, v n+1 = y n+1 -1 4 , or, equivalently, that for any n > 1,

v n = y n - 1 4 . ( 15
)
Note that this does not hold for n = 0, because in this case v 0 = y 0 -1/8. Now, using eqs. ( 14) and ( 15), we can reduce our dynamical system to two dimension, as eqs. ( 11) and ( 12) become

y n+1 = -2 (y n + 1 4 ) + y n + z n + 1, z n+1 =1 + z n + (y n - 1 4 ) -3 (y n + 1 4 ) + 2 y n - (y n -1 4 ) (y n -z n ) z n y n (y n + 1 4 ) -y n .
where the components of the new variable X will be denoted by Y and Z. Eq. ( 20) thus yields

Y = y - 1 4 - z 2 , (21)
Z = z. ( 22
)
Change of variables from x to X transforms the dynamical system x n+1 = F(x n ) into the system

X n+1 = P -1 F(P X n + x ) -P -1 x . ( 23
)
This yields, after simplification,

Y n+1 = -Y n + 1 2 (4Y n + 2Z n ) Y n -1 2 Z n + 1 4 Z n Y n + 1 2 Z n + 1 4 , (24)
Z n+1 = Z n - (4Y n + 2Z n ) Y n -1 2 Z n + 1 4 Z n Y n + 1 2 Z n + 1 4 . ( 25
)
One can immediately see that the above system has (0, 0) as a fixed point, and that its linear part is given by Y n+1 = -Y n , Z n+1 = Z n . As mentioned earlier, there is nothing we can say about the stability of (0, 0) by examining the linear part alone, except that in the vicinity of (0, 0) the Y variable is changing its sign at each iteration. We will use the method outlined in [START_REF] Perko | Differential Equations and Dynamical Systems[END_REF] to find the invariant manifold corresponding to -1 eigenvalue. We will call this manifold the flip manifold and denote it by W f . Let us assume that W f has the equation Z = h(Y ), where h in the vicinity of 0 is given by the series h(Y ) = a 2 Y 2 +a 3 Y 3 +a 4 Y 4 +a 5 Y 5 +. . .. Note that the series starts from the quadratic term, and this is because the manifold Z = h(Y ) must be tangent to the Y axis (we already diagonalized our dynamical system).

The condition for invariance of W f requires that the relationship Z n = h(Y n ) remains valid in the next time step, meaning that Z n+1 = h(Y n+1 ). Let us rewrite eqs. ( 24) and (25) as

Y n+1 = G 1 (Y n , Z n ), (26)
Z n+1 = G 2 (Y n , Z n ), (27)
where

G 1 (Y, Z) = -Y + 1 2 (4Y + 2Z) Y -1 2 Z + 1 4 Z Y + 1 2 Z + 1 4 , (28)
G 2 (Y, Z) = Z - (4Y + 2Z) Y -1 2 Z + 1 4 Z Y + 1 2 Z + 1 4 . ( 29
) Condition Z n+1 = h(Y n+1 ) now becomes G 2 (Y, Z) = h(G 1 (Y, Z))
, and, by taking

Z = h(Y ), it yields G 2 (Y, h(Y )) = h(G 1 (Y, h(Y ))). (30)
This means that if we expand

G 2 (Y, h(Y )) -h(G 1 (Y, h(Y ))
) into the Taylor series with respect to Y , all coefficient of the expansion should be zero. Such expansion, done by the Maple symbolic algebra system, yields

G 2 (Y, h(Y )) -h(G 1 (Y, h(Y ))) = (2 a 3 -4 a 2 ) Y 3 + -4 a 3 -4 4 + 1 2 a 2 a 2 + 16 a 2 + 4 a 2 2 Y 4 + 2 a 5 -4 a 4 -4 4 + 1 2 a 2 a 3 -8 a 2 a 3 + 16 a 2 2 + 16 a 3 --4 a 3 -4 4 + 1 2 a 2 a 2 + 16 a 2 a 2 Y 5 + O Y 6 .
Coefficients in front of Y 3 , Y 4 , Y 5 , . . . must be zero, yielding the system of equations for a 2 , a 3 , a 4 , . . .,

0 = 2 a 3 -4 a 2 , 0 = -4 a 3 -4 4 + 1 2 a 2 a 2 + 16 a 2 + 4 a 2 2 , 0 = 2 a 5 -4 a 4 -4 4 + 1 2 a 2 a 3 -8 a 2 a 3 + 16 a 2 2 + 16 a 3 (31)
--4 a 3 -4 4 + 1 2 a 2 a 2 + 16 a 2 a 2 , . . . Solving the above system one obtains a 2 = 4, a 3 = 8, a 4 = 32, a 5 = -32, etc. The flip manifold W f is, therefore, given by

Z = h(Y ) = 4Y 2 + 8Y 3 + 32Y 4 -32Y 5 + O(Y 6 ). (32)
By substituting Z n by h(Y n ) on the right hand side of eq. ( 24) and Taylor expanding again one obtains the equation describing the dynamics on the flip manifold W f ,

Y n+1 = -Y n + 8 Y 3 n + 32 Y 4 n + O Y 5 n . (33)
The above equation has 0 as a fixed point, and we need to determine its stability.

Recall that a fixed point x of x n+1 = f (x) is said to be asymptotically stable if there exist δ > 0 such that for any x 0 satisfying |x 0 -x| < δ we have lim n→∞ x n = x. We will use the following general test for asymptotic stability [START_REF] Murakami | Stability for non-hyperbolic fixed points of scalar difference equations[END_REF].

Theorem 1 [START_REF] Murakami | Stability for non-hyperbolic fixed points of scalar difference equations[END_REF]). Let x be a fixed point of x n+1 = f (x n ). Suppose that f ∈ C 2k-1 (R), f (x) = -1, f j (x) = 0 for j ∈ {2, 3, . . . , k -1}, and that f (k) (x) = 0. If k is odd and f (k) (x) > 0, then x is asymptotically stable.

In our case, for eq. (33), f (x) = -x + 8 x 3 + 32 x 4 + O x 5 , x = 0, f (x) = -1, f (x) = 0, and f (3) (x) = 48, thus the theorem applies, meaning that zero is asymptotically stable fixed point of eq. (33). We need to perform a similar analysis for the eigenvalue 1 and the corresponding center manifold W c . Let us assume that W c has equation Y = g(Z), where g in the vicinity of 0 is given by the series g

W c W f W c W f
(Z) = b 2 Z 2 + b 3 Z 3 + b 4 Z 4 + b 5 Z 5 + . . .. The condition for invariance of W c requires that Y n = g(Z n ) remains valid at the next time step, Y n+1 = g(Z n+1 ). Using our previous notation this means that G 1 (Y, Z) = g(G 2 (Y, Z)), which, by substituting Y = g(Z), yields G 1 (g(Z), Z) = g(G 2 (g(Z), Z)). (34)
As before, by expanding G 1 (g(Z), Z) = g(G 2 (g(Z), Z)) into the Taylor series and setting all coefficient of the expansion to be zero we obtain, using Maple,

b 2 = 1 2 , b 3 = -1 2 , b 4 = -4, b 5 = -3 2 , etc. The equation of the center manifold is, therefore, Y = 1 2 Z 2 - 1 2 Z 3 -4Z 4 - 3 2 Z 5 + O Z 6 . (35)
By substituting Y n by g(Z n ) on the right hand side of eq. ( 25) and Taylor expanding again one obtains the equation describing the dynamics on the center manifold W c ,

Z n+1 = Z n -2Z 2 n + 6Z 3 n -6Z 4 n + O Z 5 n . (36)
In order to determine the stability of 0 in the above difference equation, let us first define semistability. A fixed point x of x n+1 = f (x) is said to be asymptotically semistable from the right if there exist δ > 0 such that for any x 0 satisfying x 0 -x < δ we have lim n→∞ x n = x. One can show [START_REF] Elyadi | An Introduction to difference equations[END_REF] that if f (x) = 1 and f (x) < 0 then x is assymptotically stable from the right. In our case, for eq. ( 36), we have f (x) = x -2x 2 + 6x 3 -6x 4 + O x 5 , x = 0, f (x) = 1 and f (x) = -4 < 0, thus for eq. ( 36), zero is asymptotically semistable from the right.

Figure 2 shows manifolds W f and W c together with sample orbits generated numerically by iterating eqs. ( 24) and (25). Direction of the flow is indicated by arrows. Note that W c is asymptotically semistable only on the right (for Z > 0), and unstable on the left (for Z < 0). The left-sided instability is irrelevant for us, since Z represents the probability of 000 block, thus it must always be positive.

Since 0 is asymptotically stable on W f , and asymptotically semistable on W c , we conclude that for Z 0 > 0, lim n→∞ (X n , Z n ) = (0, 0), or, equivalently, lim n→∞ (x n , z n ) = (1/4, 0), as claimed in Proposition 3. Proposition 2 follows automatically.

Quality of local structure approximation

We have demonstrated so far that for rule 14, the local structure approximation of level 3 reproduces correctly the limiting values of probabilities of blocks of length up to 3. What about the rate of convergence to these limiting values? In order to find this out, let us consider rates of convergence to zero of P n (000) and its approximation z n . We know that P n (000) = 2 -2n-3 (4 n + 3) C n , where

C n = 1 n+1 2n n = (2n)! n!(n+1)! . Using Stirling's formula for large n, n! ∼ √ 2πn n e
n , the Catalan number C n can be approximated as

C n = 1 n + 1 (2n)! (n!) 2 ∼ 1 n + 1 √ 4πn 2n e 2n √ 2πn n e n 2 = 1 n + 1 2 2n √ πn = 1 n + 1 4 n √ πn ,
meaning that P n (000) converges toward zero as a power law P n (000) ∝ n -1/2 , where x ∝ y means the ratio x/y tends to a positive number as n → ∞.

Let us now examine convergence of z n to 0. We do not have a formula for z n , but we can generate z n numerically, by iterating the local structure equations. Figure 3 shows the graph of z n vs. n in log-log coordinates together with the graph of P n (000) vs. n. We can see that both graphs appear to be almost straight lines, confirming that both z n and P n (000) behave as n α for large n. The difference is in the value of the exponent α. For P n (000) the exponent (computed as a slope of the upper line in Figure 3) is α ≈ -1/2, whereas for z n the exponent (computed as a slope of the lower line) is α ≈ -1. The value of the exponent α ≈ -1 can be explained as follows. The starting point of the local structure approximation orbit, y 1 = 3/8, z 1 = 7/32, lies almost on the center manifold W c . The convergence toward the fixed point is, therefore, dominated by eq. ( 36), which, if we keep only leading terms, becomes Z n = Z n -2Z 2 n . Although this equation is not solvable in a closed form, we can obtain its asymptotic solution using the standard technique used in the theory of iterations of complex analytic functions. We can namely conjugate the map Z → Z -2Z 2 with appropriate Möbius transformation, which moves the fixed point to ∞ [START_REF] Beardon | Iteration of Rational Functions[END_REF][START_REF] Devaney | An Introduction to Chaotic Dynamical Systems[END_REF]. In our case, the Möbius map will simply be the inverse, meaning that we change variables in the equation Z n = Z n -2Z 2 n to u n = 1/Z n , obtaining

u n+1 = u n + 2 + 4 u n -2 . ( 37
)
Since u n → ∞, the above can be approximated for large n by u n+1 = u n + 2, which has the solution u n = 2t + u 0 , or, going back to the original variable, Z n = 1 2t+1/z0 . The result z n = Z n ∝ t -1 immediately follows. In conclusion, one could thus say that the local structure approximation correctly reproduces not only the coordinates of the the fixed point but also the type of convergence toward the fixed point (as a power law). It fails, however, to reproduce the correct value of the exponent in the power law. This in agreement with the commonly reported results of investigations of critical phenomena: mean-field type theories cannot reproduce values of fractional exponents in power laws.

It would be interesting and beneficial to extend results of this paper to nonsymmetric initial Bernoulli measures. Numerical evidence suggests that local structure approximation remains exact in the limit of n → ∞ in such cases, but to be sure one would need to generalize eqs. ( 4)- [START_REF] Fukś | Orbits of Bernoulli measures in cellular automata[END_REF] to non-symmetric initial measure. This, in principle, should be possible, and will be attempted in the future.

Fig. 1 .

 1 Fig. 1. Differences between exact and approximate values of block probabilities as a function of n. Two differences are shown, Pn(00) -yn (lower curve) and Pn(000) -zn (upper curve).

Fig.

  Fig. The flip manifold W f and the center manifold W c in transformed (Y, Z) coordinates (top) and original (y, z) coordinates (bottom). Points represent numerically computed orbits of a sample point on W c (•) and W f (•).

Fig. 3 .

 3 Fig. 3. Plot of Pn(000) (upper line) and its local structure approximation zn (lower line) as a function of n in log-log coordinates.

Acknowledgement: H.F. acknowledges financial support from the Natural Sciences and Engineering Research Council of Canada (NSERC) in the form of Discovery Grant.

After simplification we obtain, for n ≥ 1,

where we start the recursion at n = 1, taking y 1 = 3/8, z 1 = 7/32. The last two values were obtained by direct computation of y 1 and z 1 from eqs. ( 11) and ( 12) for n = 0, by substituting x 0 = 1/2, y 0 = 1 4 , z 0 = v 0 = 1/8 on the right hand side.

We will prove the following result.

Proposition 3. If the dynamical system described by eqs. ( 16) and ( 17) is iterated starting at

In order to prove the above proposition let us first denote x = y z . In this notation, eqs. ( 16) and ( 17) define two-dimensional map

It is easy to check that the map F has the fixed point x = 1 4 0 . In order to prove Proposition 3, all we need is to show that x is asymptotically stable (or at least semi-stable in the relevant domain).

The Jacobian matrix of F evaluated at the fixed point x is given by

and its eigenvalues are -1 and 1. Since these eigenvalues have an absolute value equal to 1, the fixed point x * is a non-hyperbolic fixed point and one cannot determine its stability by eigenvalues alone. We will investigate its stability by resorting to the center manifold theory.

Let P be the matrix of column eigenvectors of A, and let P -1 be its inverse,

We will first move the fixed point to the origin and simultaneously diagonalize the linear part of F. The following change of variables accomplishes this task,