S Hoerder
email: hoerder@cs.bris.ac.uk

K Järvinen
email: kimmo.jarvinen@aalto.fi

D Page
email: page@cs.bris.ac.uk

On secure embedded token design Quasi-looped Yao circuits and bounded leakage

Within a broader context of mobile and embedded computing, the design of practical, secure tokens that can store and/or process security-critical information remains an ongoing challenge. One aspect of this challenge is the threat of information leakage through side-channel attacks, which is exacerbated by any resource constraints. Along these lines, this paper extends previous work on use of Yao circuits via two contributions. First, we show how careful analysis can fix the maximum number of leakage occurrences observed during a DPA attack, effectively bounding leakage from a Yao-based token. To achieve this we use modularised Yao circuits, which also support our second contribution: the first Yao-based implementation of a secure authentication payload, namely HMAC based on SHA-256.

Introduction

A vast range of challenges and opportunities has emerged as a result of the (ongoing) proliferation of mobile and embedded computing. We now routinely and fundamentally depend on a broad range of complex, highly integrated mobile devices and applications and supporting technologies and techniques need to keep pace with such developments. We consider a motivating example within this context, namely the establishment of a secure communication channel between some token and another party. Although we limit our remit to tokens that are more capable than a (basic) smart-card (e.g., a mobile telephone or USB token, with concrete examplars including the IBM ZTIC 3 ), the secure, efficient implementation of such a device is clearly of central importance.

Although well studied cryptographic techniques can satisfy varied requirements at a high level, real-world security guarantees are still difficult to achieve: the field of physical security in particular, including passive side-channel attacks, represents a central concern. In general, a typical side-channel adversary acquires execution profiles by observing a device and, in an ensuing analysis phase, has to recover a security-critical target value (e.g., key material) from the profiles. Although practical bounds on the number of profiles collected or processed may exist, attacker capability in this respect scales over time (e.g., with Moore's law); ideally this should be catered for by any countermeasure.

Our focus is the threat of Simple (SPA) and Differential Power Analysis (DPA) [START_REF] Kocher | Differential Power Analysis[END_REF], including variations thereof such as electro-magnetic emission analysis. We cater for timing side-channels, but explicitly deem (semi-)invasive or active attacks as outside the scope of this paper. In our scenario, profiles acquired take the form of traces that describe power consumption by the token. One broad class of countermeasures aims to produce an implementation of some primitive, and secure it by applying attack-specific countermeasures at an algorithmic, software and hardware level. Selected examples include schemes for hiding [START_REF] Mangard | Power Analysis Attacks: Revealing the Secrets of Smart Cards[END_REF]Chapter 7] and masking [START_REF] Mangard | Power Analysis Attacks: Revealing the Secrets of Smart Cards[END_REF]Chapter 10] input and/or intermediate values. An alternative class aims to formulate then implement a primitive which is secure-by-design. Following a philosophy that says security should be treated as a first-class goal [START_REF] Kocher | Security as a New Dimension in Embedded System Design[END_REF][START_REF] Ravi | Security in Embedded Systems: Design Challenges[END_REF], this is an attractive direction in that robust guarantees can be provided. However, as the emerging field of leakage-resilient primitives (see [START_REF] Standaert | Leakage Resilient Cryptography in Practice[END_REF] for example) illustrates, difficulties remain. Most importantly, leakageresilient cryptography has focused on assuring security provided leakage entropy remains below a certain bound; unfortunately, no practical means of (provably) verifying such a bound for a given device is currently available.

We extend work on Yao circuits [START_REF] Yao | Protocols for secure computations[END_REF][START_REF] Yao | How to generate and exchange secrets[END_REF][START_REF] Malkhi | Fairplay -A Secure Two-Party Computation System[END_REF][START_REF] Ben-David | FairplayMP -A Secure Multi-Party Computation System[END_REF][START_REF] Henecka | TASTY: Tool for Automating Secure Two-partY computations[END_REF][START_REF] Huang | Faster Secure Two-Party Computation Using Garbled Circuits[END_REF][START_REF] Malka | VMCrypt -Modular Software Architecture for Scalable Secure Computation[END_REF], especially their implementation on tokens [START_REF] Järvinen | Garbled Circuits for Leakage-Resilience: Hardware Implementation and Evaluation of One-Time Programs[END_REF][START_REF] Järvinen | Embedded SFE: Offloading Server and Network using Hardware Tokens (short version)[END_REF] as a means of performing leakage-resilient computation within the motivating scenario above. Our focus is practicality: we aim to keep the entire architecture as simple as possible in order to reduce manufacturing and verification cost. Careful analysis of said architecture places a bound τ on the number of useful leakage occurrences an attacker can observe. For a given signal-to-noise ratio, this forces an attacker to develop more effective attacks rather than simply using more traces; when combined with conventional countermeasures, it can effectively prevent such attacks. One can view this process as playing a similar role to key refresh [START_REF] Medwed | Fresh rekeying: Security against side-channel and fault attacks for low-cost devices[END_REF][START_REF] Medwed | Fresh re-keying II: Securing multiple parties against side-channel and fault attacks[END_REF], but without the need for synchronization. In addition, we add the first secure authentication payload, HMAC [START_REF]The Keyed-Hash Message Authentication Code (HMAC)[END_REF], to the list of applications implemented as Yao circuits. The overall result are leakage-bounded implementations of both AES 128 and HMAC.

Background

An important aspect of formalising the ability of a side-channel attack(er) is the selection of a model that describes the form of leakage from a token (and thus exploitable by the attacker). The model proposed by Standaert et al. [START_REF] Standaert | A Unified Framework for the Analysis of Side-Channel Key Recovery Attacks[END_REF] can be directly applied to our scenario with just one minor modification. In said model, adversarial success depends, among other factors, on the number of oracle queries allowed per primitive independent of updates to secret values (e.g., use of key refresh schemes). We therefore replace the number of oracle queries with the number of observable leakage occurrences per secret value.

G E

Select mG

Select mE

Generate Y f [mG ,mE ] Evaluate r = Y f [mG ,mE ] (•) Agree f mE Y f [mG ,mE ]
Fig. 1: A high-level, generic description of Yao circuit generation and evaluation. Note that all inputs and outputs are implicitly defined wrt. f , and that depending on the scenario a) one or more of f , m G and m E could alternatively be provided as input to the protocol, and b) subsequent use of r could be included.

Yao circuits at a high level

An implementation of a functionality f as a standard Boolean circuit, say B f , can be evaluated using an input x to give an output r = B f (x). We use B f x to denote an implementation with an embedded fixed input and retain a similar form for evaluation r = B f x (•). At a high level, Yao circuits simply represent a nonstandard implementation of f , say Y f , which allows the associated evaluation to be secure.

Use of a given Yao circuit can be described formally as a secure two-party computation protocol. The parties involved are a circuit generator G who (given f and x) produces Y f

x , and a circuit evaluator E who (given Y f x ) computes r = Y f x (•); both are illustrated in Figure 1. Thus the side-channel attack surface is shifted away from individual primitives f onto the task of generating a Yao circuit

Y f [m G ,m E ]
where we can give strong bounds on leakage. In contrast to the original usage as a two-party computation protocol, the token is trusted and we do not need oblivious transfer to communicate the circuit inputs m E , m G . Note that in theory G could evaluate Y f

[m G ,m E ] as well as generating it, but we deem it more economic in most cases to let E do the evaluation.

Imagine g k refers to some k-th truth table wlog. describing a 2-input, 1output Boolean function or gate instance within B f . Both the inputs to and outputs from said gate are provided on wires indexed using a unique wire identifier (or wire ID): we write m i for the value carried by the wire with wire ID i. Note that the output wire ID can act to identify a given gate instance (i.e., acts as a gate ID). Figure 2a is a trivial starting point outlining how such a gate can be evaluated.

Yao circuits are constructed by forming a "garbled" Yao gate instance in Y f for each Boolean gate instance in B f . Both inputs to and outputs from the Yao gate are altered to mask their underlying value: this means each m i is replaced by c i , an encryption of the former. Given Enc x (y) denotes the encryption of y under the key x using some symmetric cipher (with a κ-bit key and β-bit block size), Figure 2b illustrates a Yao gate corresponding to the above. Note that the public c i and c j inputs (whose secret underlying values are m i and m j ) are provided on wires with public indices i and j, the public c k output (whose secret underlying value is m k ) is provided on a wire with public index k, mi mj 0 0 mk = gk(mi, mj) 0 1 mk = gk(mi, mj) 1 0 mk = gk(mi, mj)

1 1 mk = gk(mi, mj) mi mj mk (a) An example Boolean gate. ci = mi ⊕ πi cj = mj ⊕ πj 0 0 Enc[0,0,k](ck = gk(mi, mj) ⊕ πk) 0 1 Enc[0,1,k](ck = gk(mi, mj) ⊕ πk) 1 0 Enc[1,0,k](ck = gk(mi, mj) ⊕ πk) 1 1 Enc[1,1,k](ck = gk(mi, mj) ⊕ πk) ci cj ck (b) An illustrative example of the corresponding Yao gate. ci = mi ⊕ πi cj = mj ⊕ πj 0 1 Enc [w 0 i ,w 1 j ,k] (w g(mi,mj )⊕πk k ) 1 0 Enc [w 1 i ,w 0 j ,k] (w g(mi,mj )⊕πk k ) 1 1 Enc [w 1 i ,w 1 j ,k] (w g(mi,mj )⊕πk k ) wi wj wk (c)
The corresponding Yao gate with wire labelling and Garbled Row Reduction (GRR) [START_REF] Naor | Privacy preserving auctions and mechanism design[END_REF] applied (noting that each ci forms part of the associated wi per Equation 1).

Fig. 2: A step-by-step comparison of a 2-input, 1-output Boolean gate (whose function is described by g k ), and the associated Yao gate construction before and after optimisation.

the standard gate functionality is g k , and π i , π j and π k act as secret permutation bits on the rows of the truth table. During evaluation of the gate, E gets c i and c j meaning it cannot recover the underlying values of m i and m j since it does not know π i and π j . However, c i and c j index one entry of the truth table and allow only this entry to be decrypted (since they determine the associated cipher key) and yield c k . The central idea is that a Yao gate reveals nothing about a) the gate functionality nor b) underlying values, iff. it is evaluated at most once.

Abstract realisation of Yao circuits

Wire labels The illustrative example above has a major shortcoming: the effective cipher key size is just two bits (since all wire IDs are public), meaning the key is inherently susceptible to exhaustive search. To combat this, given a security parameter λ one replaces the Boolean value communicated on each wire with a randomised λ-bit wire label. Let

w ci i = ρ i (m i ⊕ π i ) = ρ i c i (1)
denote the i-th such wire label in the general case where

m i ⊕ π i = c i for c i ∈ {0, 1}, ρ i $ ← Z λ-1 2 and π i $ ← Z 2 .
Note that the combination of ρ i and π i could be viewed as a λ-bit ephemeral key, implying κ = 2λ + where is the number of bits used to encode wire IDs, and that Equation 1 caters for two optimisations outlined below.

The Garbled Row Reduction (GRR) optimisation was introduced by Naor et al. [START_REF] Naor | Privacy preserving auctions and mechanism design[END_REF]. In short, by carefully selecting

w c k k = w g(mi,mj )⊕π k k = Enc [w 0 i ,w 0 j ,k] (γ) (2)
for c i = c j = 0 and a suitable public constant γ, the first truth table entry can be eliminated (as illustrated by Figure 2c). This is attractive since it permits up to a 25% reduction in communication of the Yao circuit from G to E, plus reduces the amount of storage required.

The "free XOR" optimisation introduced by Kolesnikov and Schneider [START_REF] Kolesnikov | Improved Garbled Circuit: Free XOR Gates and Applications[END_REF] realises XOR gates (almost) for free. Given a global (i.e., one for each instance of Y f ), secret constant ∆ ∈ Z λ-1 2 they select w 1 i as in Equation 1, then define

w 0 i = w 1 i ⊕ (∆ 1) = (ρ i ⊕ ∆) (π i ⊕ (m i ⊕ 1)) (3)
to allow computation of XOR gates via the relationships

w 0 i ⊕ w 1 i = w 1 i ⊕ (∆ 1) ⊕ w 1 j = w 1 i ⊕ w 0 j = w 1 k w 0 i ⊕ w 0 i = w 1 i ⊕ (∆ 1) ⊕ w 1 j ⊕ (∆ 1) = w 1 i ⊕ w 1 j = w 0 k = w 1 k ⊕ (∆ 1)

Previous Token implementations of Yao circuits

As far as cryptographic primitives are concerned, previous work (with the exception of [START_REF] Kreuter | Billion-gate secure computation with malicious adversaries[END_REF]) focus on use of AES 128 as the functionality f . Other functionalities considered relate instead to higher level applications, e.g., database search [START_REF] Henecka | TASTY: Tool for Automating Secure Two-partY computations[END_REF][START_REF] Malka | VMCrypt -Modular Software Architecture for Scalable Secure Computation[END_REF] or bioinformatics [START_REF] Huang | Faster Secure Two-Party Computation Using Garbled Circuits[END_REF]. Pinkas et al. [START_REF] Pinkas | Secure Two-Party Computation is Practical[END_REF] provide the first feasibility results (using software) of Yao-based constructions; since they relate more directly to the chosen scenario, we detail work by Järvinen et al. [START_REF] Järvinen | Garbled Circuits for Leakage-Resilience: Hardware Implementation and Evaluation of One-Time Programs[END_REF][START_REF] Järvinen | Embedded SFE: Offloading Server and Network using Hardware Tokens (short version)[END_REF] below which both implement Yao circuits on tokens but do not use modularisation.

Secure computation via One-Time Programs (OTPs): In [START_REF] Järvinen | Garbled Circuits for Leakage-Resilience: Hardware Implementation and Evaluation of One-Time Programs[END_REF], Järvinen et al. consider a scenario wherein E is a hardware token, and G is a trusted party during a setup stage. The idea is that G as token issuer stores One-Time Memories (OTMs) for a fixed number x of OTPs represented by Y f on the token. At run-time, the token owner uses one set of OTMs to form the input labels corresponding to his data, and the token evaluates the Yao circuit before finally releasing the result.

The advantage of this scenario is that very little protection against sidechannel attacks is required. However, the major disadvantage is the limited number of Yao circuits: in most real-life scenarios this is unacceptable. In addition, a generic framework without this disadvantage is given at the cost of loosing the leakage-resilient circuit generation. Our work can be seen as a leakage-resilient, more flexible version of the framework.

Secure computation via out-sourcing: In [START_REF] Järvinen | Embedded SFE: Offloading Server and Network using Hardware Tokens (short version)[END_REF], Järvinen et al. consider a scenario wherein E is a cloud computing provider; the role of G is split between a secure hardware token G S and some other party G U (e.g., a desktop workstation). The idea is for G U to generate B f , which is passed to G S and translated (securely) into Y f . The Y f can then be evaluated by E, with the overall effect of securely out-sourcing computation from G U to E (and the token G S ).

This scenario is advantageous in the sense it allows a flexible choice of f (wrt. the token) and is very speed-and memory-efficient. However, it has a relatively high hardware requirement: in addition to the SHA-256 core it requires at least one AES 128 core, [START_REF] Järvinen | Embedded SFE: Offloading Server and Network using Hardware Tokens (short version)[END_REF] uses two, which all have to be free from leakage.

Supporting alterations to traditional Yao circuits

To support our design in Section 4, we first outline two supporting concepts: detail relating to their realisation and utility is deferred until later. While neither represents a significant change to underlying theory, we posit that both significantly ease the practical task of constructing and using Yao circuits.

Circuit modularisation

Existing limitations Consider a typical iterative block cipher design, with s rounds in total (e.g, AES 128 with s = 10). The functionality for round i is described by f i , which implemented as a Boolean circuit is B fi . The s different round functionalities can be the same or different as required, with the overall cipher thus described by the functionality

f = f s-1 • • • • • f 1 • f 0 .
One can implement this either combinatorially, whereby instances of each B fi are "unrolled" to form the resulting monolithic circuit, or iteratively, whereby instances of each unique B fi are "looped over" with a need for only one circuit instance and some control logic. Traditional Yao circuits must adopt the former approach: no sequential elements (e.g., latches, clock signals) are allowed because each gate can be evaluated at most once (to ensure security). One cannot reuse the resulting Yao circuit unless rerandomisable constructions [START_REF] Gentry | i-Hop Homomorphic Encryption and Rerandomizable Yao Circuits[END_REF] are considered; typically these incur a prohibitive overhead.

One impact of this restriction is that previous work almost exclusively focuses on AES 128 (as far as cryptographic primitives are concerned) which a) has a fixed s and can hence be unrolled, and b) has a fairly compact hardware implementation. We know of only one implementation of another cryptographic primitive [START_REF] Kreuter | Billion-gate secure computation with malicious adversaries[END_REF], wherein an (insecure) implementation of 256-bit RSA is described. Even with such small operands, the resulting Yao circuit is ≈ 8500 times larger than their AES 128 circuit, in part as a result of the requirement to unroll the loop representing a binary, modular exponentiation.

Modularised Yao circuits

To address this issue, we make use of modular Yao circuits. Similar concepts have been used recently4 in [START_REF] Huang | Faster Secure Two-Party Computation Using Garbled Circuits[END_REF][START_REF] Malka | VMCrypt -Modular Software Architecture for Scalable Secure Computation[END_REF] to achieve efficiency gains for large circuits, but only [START_REF] Malka | VMCrypt -Modular Software Architecture for Scalable Secure Computation[END_REF] mentions the possibility of using run-time parameters to control circuit assembly.

Traditionally (right) each monolithic Boolean circuit

B f = B fs-1•••••f1•f0
is stored and must be translated into the corresponding Yao circuit by G each time the latter needs to be evaluated. In our alternative (left), G holds only the static description of each template B fi (and associated meta-data), instantiating them to form Y f without holding the entirety of the (potentially large) B f . This technique permits a quasi-loop: given s, e.g. the number of blocks to be hashed, at run-time (rather than being fixed), the token unrolls one circuit template B fi , to form the resulting Yao circuit. The resulting reduction in resource requirement and increased flexibility allows us to implement HMAC. Generation of the corresponding Y f can be streamed in that G communicates one part at a time to E.

Updating ∆ between template instances

In previous works [START_REF] Pinkas | Secure Two-Party Computation is Practical[END_REF][START_REF] Järvinen | Garbled Circuits for Leakage-Resilience: Hardware Implementation and Evaluation of One-Time Programs[END_REF][START_REF] Järvinen | Embedded SFE: Offloading Server and Network using Hardware Tokens (short version)[END_REF] using the free XOR trick [START_REF] Kolesnikov | Improved Garbled Circuit: Free XOR Gates and Applications[END_REF], the authors argue that for correctness ∆ must remain constant within a given Yao circuit. Indeed, if an XOR gate is evaluated using constants ∆ 1 = ∆ 2 , the result is incorrect as

w 0 i ⊕ w 1 j = (w 1 i ⊕ (∆ 1 1)) ⊕ w 1 j = w 1 i ⊕ (w 1 j ⊕ (∆ 2 1)) = w 1 i ⊕ w 0 j w 0 i ⊕ w 0 j = (w 1 i ⊕ (∆ 1 1)) ⊕ (w 1 j ⊕ (∆ 2 1)) = w 1 i ⊕ w 1 j
shows. Despite this, a crucial observation is that ∆ can be changed if said change is applied consistently. Although doing so has no functional benefit, we use it to directly formulate a leakage bound within Section 5.

In some modularised Yao circuit, imagine the t-th template instance uses ∆ t . The next, (t + 1)-th instance can then use ∆ t+1 (as illustrated by Figure 3) iff. each connecting wire is updated appropriately. The simplest approach is to consider a dedicated 1-input, 1-output update gate with the identity functionality, i.e., g k (x) = x. Given

w c k k = w mi⊕π k k = Enc [w 0 i ,w 0 i ,k] (γ
) by definition, and that m i = m k since the gate updates ∆ rather than change the underlying input value, Equation 2 means the associated wire labels are

w 0 i = w 1 i ⊕ ( ∆ t 1 ) w 0 k = w 1 k ⊕ ( ∆ t+1 1 )
However, this suggests that any non-XOR gate can be used to perform the update without cost: the existing GRR-optimised Yao gate truth table only needs to have ∆ t+1 folded into the label w

g k (mi,mj )⊕π k k
instead of ∆ t where appropriate.

We consider a scenario wherein G is a hardware token that needs to be secured against SPA and DPA attacks, and E is some other party to which computation is outsourced. The idea is to put a bound on the number of times secret values are used for any computation and leakage can be observed before the value -akin to key refresh -is updated. The known, residual leakage can then be accommodated by careful use of conventional countermeasures.

Cipher construction

To instantiate the symmetric cipher required to encrypt wire labels, we follow existing work [START_REF] Pinkas | Secure Two-Party Computation is Practical[END_REF][START_REF] Järvinen | Embedded SFE: Offloading Server and Network using Hardware Tokens (short version)[END_REF][START_REF] Järvinen | Garbled Circuits for Leakage-Resilience: Hardware Implementation and Evaluation of One-Time Programs[END_REF]] by using a one-time pad like construction

Enc [w c i i ,w c j j ,k] (w c k k ) = SHA-256(w ci i w cj j k) ⊕ w c k k
where the SHA-256 output is implicitly truncated to λ bits to match the wire label size. We reuse SHA-256 as a secure Pseudo-Random Number Generator (PRNG), splitting the SHA-256 into two 128-bit values [x, y] ← SHA-256(seed t-1 ) seed t ← seed t-1 ⊕ y rand ← x so x = rand is used as a wire label for example, while y is used exclusively to update the seed. Note SHA-256 is therefore the only significant cryptographic core required by the token. This construction is certainly secure if the PRNG is modelled as a random oracle which is a weaker model than the one we have for our Yao circuits. Intuitively however, some form of correlation robustness should be sufficient. Research on the correlation robustness of hash functions is still developing, see [START_REF] Kolesnikov | Improved Garbled Circuit: Free XOR Gates and Applications[END_REF][START_REF] Choi | On the Security of the "Free-XOR" Technique[END_REF] for example, and therefore we defer the exact security requirements to future work. Previous work has used domain-specific languages (e.g. SFDL [START_REF] Malkhi | Fairplay -A Secure Two-Party Computation System[END_REF][START_REF] Ben-David | FairplayMP -A Secure Multi-Party Computation System[END_REF]) to implement the payloads. While this may ease implementation, it reduces control over the actual circuit layout. Standard Hardware Description Languages (HDLs) are, in fact, well suited to payload description: they simply lack the protocol aspect of Yao circuits. Therefore we aim to reap benefits of familiarity, design and code portability by using a VHDL dialect and associated compiler, both of our own design, to describe structural and behavioural circuit templates.

Operational protocol and token architecture

The communication between the token G and the evaluator E is shown in Figure 5. E can, for example, be a local untrusted work station or an untrusted but more powerful chip within a mobile phone; in most cases it will not be

Step

G E 0a) 0b) Select mG Select mE while true 1a) 1b) Generate Y fi [m G ,m E ] 1c) Evaluate Y fi [m G ,m E ] (•)
l•i , . . . , mE l•(i+1)-1 Y fi [m G ,m E ]
o0, o1, . . . wo 0 , wo 1 , . . . r Fig. 5: The two-party computation protocol reflecting circuit modularisation. Note that E does not communicate m E in one block, but rather in multiple l-bit blocks. Output wires of the Yao circuit (i.e. the wires carrying results from the functionality) have wire IDs o0, o1, . . .. the authentication partner. We assume a physical connection between the parties, and hence focus on optimising their workload rather than the number of communication rounds.

Initially, in step 0, E requests a functionality f (e.g., HMAC or AES 128 ) and both parties need to have (or generate) corresponding inputs m G and m E . Step 1, from a theoretic perspective, is the same as the monolithic communication in Figure 1 despite now supporting the modularised approach. Specifically, G generates the Yao circuit Y f based on the circuit templates B fi and sends it step-by-step to be evaluated. Note that modularisation forces three important checks:

1. step 1d checks if all input values (from both m G and m E ) have been used, 2. step 1e checks if all gates have evaluated, and 3. step 4 checks if all output values are valid, i.e., if w oj ∈ {w 0 oj , w 1 oj } ∀ o j . When a check condition can not be satisfied the token aborts immediately, meaning in particular that it does not reach step 5 where the result r

= f (m G , m E ) = Y f [m G ,m E ]
is revealed, and that seed values of the PRNG are not accidentally reused.

To support the protocol outlined above, Figure 4 outlines a proposed token architecture. The main components and their roles are as follows:

-A general-purpose micro-controller manages the communication protocol in Figure 5, controlling assembly of Y f from the B fi circuit templates and performing other tasks (such as message padding for HMAC). -A general-purpose memory holds the B fi , micro-controller program and other public run-time variables values which only require correctness.

-Storage of and computation using secret values is limited to the Yao core, which consists of:

• A SHA-256 core, used to encrypt wire labels and also as a PRNG.

• Control logic used for auxiliary operations such as wire label generation.

• A secure memory, split into two parts: a non-volatile part holds m G and seed, while a volatile part holds ∆ t , ∆ t+1 and, for each wire i, the tuple {w 0 i , w 1 i }. Note that ∆ t+1 = 0 unless the token is processing update gates, and that a crucial role of the secure memory as a whole is to prevent read-out or other leaks of values such as m G and seed.

Analysis and results

Security analysis

This section attempts to explore security aspects of the proposal outlined in Section 4. After a statement of general assumptions, we deal specifically with potential attack vectors exploited during an SPA or DPA attack, or by a malicious adversary within the operational protocol.

Security assumptions To be successful, the adversary has to recover the input x G held by the token for which he can either attempt to recover x G directly (e.g., via a DPA attack), or try to "ungarble" the Yao circuit

Y x G ,x f E (or part thereof).
In showing neither strategy is viable, we make some important assumptions:

A-1 An authentication protocol that prevents man-in-the-middle attacks against m E in step 1d of the Yao protocol must be selected (if this threat is relevant). A-2 The control-flow of the token, managed by the micro-controller, is tamperproof which implies integrity of the general-purpose memory. Although this is a strong requirement, it is common for embedded systems. A-3 The hash function used for encryption of wire labels (in our case SHA-256) must be circular-2-correlation robust (see Choi et al. [START_REF] Choi | On the Security of the "Free-XOR" Technique[END_REF]). A-4 The token cannot be reset, and no randomness reused: this prevents an adversary forcing the token to regenerate the same Yao circuit with the same randomness, then reevaluating it with different inputs.

Power analysis adversaries SPA attacks attempt to recover the target value using one (or at least very few) traces and attack capabilities do not scale over time; examination of data-dependent control-flow is one example. There are two possible attack vectors:

SPA-1 For each i-th input wire, the token must send either w 0 i or w 1 i to the evaluator depending on the underlying value of m i . To succeed, the adversary must be able to determine whether m i is 0 or 1 (for all m i ∈ x G ). SPA-2 Gates such as AND and OR are biased towards 0 or 1 in their output:

if the adversary determines during computation of

Enc [w c i i ,w c j j ,k] w g(mi,mj )⊕π k k
which truth table row contains the minority output, they can reverse the permutations (i.e., π i and π j ) and recover the underlying values of almost all output wire labels from non-XOR gates.

For hardware implementations, both SPA attack vectors will be implemented using multiplexers whose data dependency of the power consumption is usually already hidden well enough without countermeasures (e.g., [START_REF] Mangard | Power Analysis Attacks: Revealing the Secrets of Smart Cards[END_REF]Appendix A.3]). Even if this is not the case, traditional countermeasures (e.g., random masking of the select signal with corresponding permutation of the inputs) are efficient.

In contrast, DPA attacks attempt to recover the security-critical target value by applying statistical distinguishers to a large set of traces; issues of signalto-noise ratio, as well as explicit countermeasures, determine the exact number. More formally, let k be the target value, v be a variable value and r the result of some generic operation . A DPA adversary collects traces relating to execution of r i ← k v i for many different v 1 , v 2 , . . . , v σ . The potency of a DPA attack is then judged by σ, the number of traces required to be reliably recover k. Our approach is to have a design-time constant bound τ σ instead of allowing the adversary to control it. Put another way, we bound the leakage such an adversary can utilise in a DPA attack: if the application of conventional countermeasures can prevent attacks with said leakage level, the token is secure.

DPA-1

The token must compute w 0 i ← w 1 i ⊕ (∆ t 1) for every wire. As such we have

τ DPA-1 = max(δ 1 , δ 2 , . . .)
where δ t denotes the number of wires using ∆ t . If the technique in Section 3.2 is used correctly, τ DPA-1 is a constant determined by the token designer. DPA-2 For each gate, the four values of w {0,1} {i,j} are each used twice as input to SHA-256(w {0,1} i w {0,1} j k). Focusing on one label, wlog. w i say, and one external value, wlog. 0 say, the attacker gets two traces for each gate where w 0 i is used as input. Therefore, we have

τ DPA-2 = 2 • max ∀k (G k )
where G k represents the fan-out of the k-th gate (and input wires are also considered as being driven by imaginary gates). Note that a similar attack vector exists when the token processes an XOR gate. Such a gate must compute w 0 k and w 1 k , and one possible approach is to compute

w 0 k ← w 0 i ⊕ w 0 j w 1 k ← w 0 i ⊕ w 1 j (4)
in which case τ DPA-2 conveniently covers this attack vector as well.

Concrete, non-optimised examples for these bounds are given in Section 5.2.

If our design is used to protect against DPA attacks, functionalities that were inherently secure against SPA clearly inherit any SPA vulnerabilities of the underlying Yao circuit approach. We suggest that preventing SPA attacks on our design using conventional countermeasures is, broadly speaking, easier than preventing DPA attacks on the functionality in question: the cost of preventing the former is easily justified by the improvement offered wrt. the latter.

Catering for timing analysis adversaries The execution time associated with generating of a Yao circuit is inherently independent of the inputs to that Yao circuit: it depends only on the circuit size. As far as the architecture is concerned, we do not use a cache for the micro-processor in order to avoid cache-based timing attacks. Working without a cache is a common decision for cryptographic tokens and therefore not an exceptional burden of our design.

Catering for malicious adversaries One advantage of Yao circuits is the availability of related security proofs. For semi-honest adversaries, Figure 5 preserves proofs already given by [START_REF] Kolesnikov | Improved Garbled Circuit: Free XOR Gates and Applications[END_REF][START_REF] Pinkas | Secure Two-Party Computation is Practical[END_REF][START_REF] Järvinen | Embedded SFE: Offloading Server and Network using Hardware Tokens (short version)[END_REF][START_REF] Järvinen | Garbled Circuits for Leakage-Resilience: Hardware Implementation and Evaluation of One-Time Programs[END_REF][START_REF] Choi | On the Security of the "Free-XOR" Technique[END_REF]. This is a direct result of steps 1a to 1e being equivalent to the single generate-evaluate step from previous protocols. However, we also need to consider malicious adversaries. Lindell et al. [START_REF] Lindell | An Efficient Protocol for Secure Two-Party Computation in the Presence of Malicious Adversaries[END_REF] show how a two-party computation protocol using Yao circuits can cover the case of malicious G using a cut-and-choose approach. Our scenario is far less complex, since Y f is generated by the token which is implicitly trusted: we disallow a malicious G. Therefore we only have to consider a malicious E, and show it cannot learn anything about x G not implied by the result r = f (x G , x E ) by deviating from the protocol. E has two options (which we expand on below): it can either a) provide faulty input or b) perform variants on early termination.

Faulty data. The only steps where E can provide faulty data are 1a and 3. As m E in step 1a is the input of the functionality, sending a faulty m E has no impact on the security of the Yao protocol: it can only influence the output of the functionality f . In contrast, sending faulty w oj in step 3 is potentially a problem if the adversary sends labels from intermediate wires instead of the output labels. However, this is prevented by the check in step 4 which ensures that for each output wire o j , exactly one wire label w co j oj ∈ {w 0 oj , w 1 oj } has been sent before the result is revealed. Early termination. Since E can not learn anything from one of the partial circuits (i.e., a given Y fi [m G ,m E ] ) until the protocol is finished (i.e., until G reveals the result), E cannot profit from straight early termination. However, if the functionality f requires s iterations of a loop to form

f = f s-1 • • • • • f 1 • f 0 ,
per the description of AES 128 in Section 3.1 for instance, the adversary could potentially gain information from terminating the loop early, i.e., to get f = f s -1 •• • ••f 1 •f 0 for 0 < s < s: this would be analogous to a reduced-round attack. To prevent this, we require the token to check (in steps 1d and 1c) whether the Yao circuit for f has been completely generated or whether some Y fi [m G ,m E ] is missing.

Experimental results and analysis

Our goal is to study gross, indicative metrics and trade-offs rather than focus on absolute figures that could be improved via incremental optimisation. For the evaluation of our proposed design, we implemented a VHDL compiler (per Section 4.1), a token simulator G, an evaluator E as well as two payload functionalities, namely AES 128 and HMAC SHA-256 . For each payload, we considered variants that differ in their frequency of ∆ update: for AES 128 three variants are used, for HMAC SHA-256 two variants. The variants are as follows:

AES

Baseline AES 128 implementation without updating of ∆. AES U1 AES 128 with a ∆ update after the fifth iteration of the round function. AES U9 AES 128 with a ∆ update after every iteration of the round function. HMAC Baseline HMAC implementation without updating of ∆. HMAC U HMAC with ∆ updates after every iteration of the compression function.

Table 1 details efficiency metrics for implementation of these variants on the platform described and shows the two associated bounds τ DPA-1 and τ DPA-2 . The first three columns specify the payload, the number of input blocks from E and the number of ∆ values being used at run-time.

Efficiency The columns #XOR and #non-XOR in Table 1 give the number of gates in the resultant Yao circuit. Compared to [START_REF] Pinkas | Secure Two-Party Computation is Practical[END_REF][START_REF] Järvinen | Garbled Circuits for Leakage-Resilience: Hardware Implementation and Evaluation of One-Time Programs[END_REF] we have considerably smaller AES 128 circuits, which is mainly due to omission of key scheduling and, to a less extent, use of more optimised S-box formulas of Boyar et al. [START_REF] Boyar | A new combinational logic minimization technique with applications to cryptology[END_REF]. The omission of key scheduling implies a small penalty of having to store all round keys m G,sec in secure ROM.

The column #SHA-256 shows the number of distinct uses of the SHA-256 core, each a one-block hash. Ignoring the absolute simulation time, we feel this metric best represents the execution time of a concrete token since the SHA-256 core will most likely be the throughput bottleneck. [START_REF] Järvinen | Embedded SFE: Offloading Server and Network using Hardware Tokens (short version)[END_REF] use a SHA-256 core which requires 67 cycles per 512 bit block at 66 MHz. Based on these numbers, a crude time estimation (based only on calls to the SHA-256 core) is 24ms for AES and 1418ms for HMAC U with 4 message blocks.

A significant issue is the amount of RAM required at run-time. To assess this, we measured the simulator heap and stack usage using the Valgrind massif tool [START_REF]Massif User Manual[END_REF]. We note that the tool itself is not perfect, and that the result includes overhead of up to 20% relating to performance and security counters. Even so, the indicative RAM requirement is large: it remains within the capability of devices in our remit, but clearly beyond smart-cards or RFID tokens for example. The requirement stems in the most part from storing all wire labels {w 0 i , w 1 i } in RAM. One possible trade-off would be to store only w 0 i and recompute w 1 i when needed, reducing the RAM usage by a factor of two, but increasing the number of traces available by a factor similar to the maximum fan-out. [START_REF] Järvinen | Embedded SFE: Offloading Server and Network using Hardware Tokens (short version)[END_REF] chose a keyed PRNG which allows recomputation of w 0 i when needed, thus reducing the RAM requirements drastically. However, any keyed PRNG is vulnerable to DPA attacks with unlimited τ which negates our aim of bounding the leakage.

An interesting observation can be made about the RAM usage of AES U1 and AES U9. Intuitively, one would expect the RAM usage to always grow in line with the number of ∆ t used. In this case, the opposite happens because AES U1 applies the ∆ updating within the top-level entity (which also accounts for the larger |B fi |), requiring more wires for which RAM is allocated during the entire run-time. AES U9 performs the updating at the end of the round function entity instead, and the RAM for additional wires can be deallocated as soon as each round function instance of has been completed.

The size of the templates, |B fi | (stored in unsecured ROM), profits directly from modularisation. As predicted, the size of |B fi | for HMAC does not depend on the message size as it would have for the traditional approach.

Security Having explained τ DPA-1 and τ DPA-2 in Section 5.1, we note that our ∆ updating technique limits τ DPA-1 as predicted; note esp. the HMAC U payload, where updating ∆ fixes previously unlimited leakage to a constant chosen by the token designer.

The result for τ DPA-2 is an absolute upper bound, i.e., for all output wires we counted how often it gets used while processing the follow-up gates. As explained in Section 5.1, if a wire is used as input to a non-XOR gate each label gets used twice; for XOR gates Equation 4gives the numbers relevant to our implementation. For an attacker it will be very difficult to combine traces from two different operations like this but we prefer to err on the side of security by overestimating the attacker. With numbers this low, DPA-2 is almost irrelevant as an attack vector. But having a low τ DPA-2 was an explicit aim of our work: τ DPA-2 is the only possible attack vector on the SHA-256 core, and therefore τ DPA-2 is crucial to determine the level of conventional countermeasures needed to protect the SHA-256 core. Compared to the SHA-256 core, protecting the XOR from DPA-1 to match a much higher τ DPA-1 is inexpensive.

As a reference one may look at the Power-Trust micro-processor of Tillich et al. [START_REF] Tillich | Implementation and Evaluation of an SCA-Resistant Embedded Processor[END_REF], which has parts of the ALU implemented within a secure zone. For evaluation purposes they implemented the secure zone in three different logic styles (namely CMOS, iMDPL [START_REF] Popp | Evaluation of the Masked Logic Style MDPL on a Prototype Chip[END_REF] and DWDDL [START_REF] Yu | Secure FPGA circuits using controlled placement and routing[END_REF]) and performed a DPA attack against an AES 128 software implementation using the secure zone. While it is difficult to directly extrapolate from a design as different from ours, this at least gives an estimate: there is no reason why secure logic styles such as iMDPL and DWDDL should fare worse for our token. For the DPA attack on the secure zone to be successful, Tillich et al. required 130, 000 traces against the (unprotected) CMOS implementation, 260, 000 traces against the iMDPL implementation and 675, 000 traces against the DWDDL implementation. With τ DPA-1 = 7296 in the worst case for AES 128 and τ DPA-1 = 84040 for HMAC U we surmise that both iMDPL and DWDDL would have successfully thwarted the DPA attack from Tillich et al. against an implementation of our token. It is important to note, that for both bounds we did not yet try to find the absolute minimum. For example it is possible to add additional gates to achieve fan-out = 2 and thus τ DPA-2 ≤ 4 while τ DPA-1 can be easily reduced by updating ∆ more often within the round resp. compression functions, not just at their end.

In essence, this paper has demonstrated that an embedded token can be designed which gives strong bounds on the number of useful traces a power analysis adversary can collect. Our design methodology 1. is generic in that it works for all payloads and use-cases (cf. PIN block), 2. does not impose limits on the token lifetime, 3. does not require synchronization (cf. key update schemes), 4. is easily verifiable, and 5. successfully limits attack capabilities for side-channel adversaries.

In relation to the former point, we have already extended previous work through support for a Yao circuit for HMAC. Exploration of further primitives based on modularisation (including methods and trade-offs to further reduce the leakage bound), plus incremental optimisation of both the token design and operational protocol (especially the RAM requirement) are interesting avenues for further work. In relation to the latter point, the clear next step is to produce experimental results from a concrete implementation of the token. This would, for example, allow investigation of the concrete leakage and whether implementation specific high order moments occur which increase τ for higher order attacks.

Fig. 3 :Fig. 4 :

 34 Fig.3: An example of updating ∆ between two template instances, with the heavy dashed line denoting the boundary between use of ∆t and ∆t+1.

Table 1 :

 1 Efficiency metrics and leakage bounds for our token design and a range of payload implementations. The block size for AES128 is 128 bits, for HMAC it is 512 bits (including the padding in the last block).

		#blocks #∆ #XOR #non-XOR #SHA-256	RAM	|B fi | |mG,sec| |mG,pub| τDPA-1 τDPA-2
	AES	1	1 19088	5760	24578 245.9kB 12318B	176B	-7296	11
	AES U1	1	2 19088	5888	25091 263.4kB 13628B	176B	-3776	11
	AES U9	1 10 19088	6912	29195 262.3kB 12845B	176B	-	960	11
		1	1 148080	129680	556866 1883.6kB 121942B	64B	32B 167824	19
	HMAC	2	1 222120	194520	835170 2489.8kB 121942B	64B	32B 251608	19
		3	1 296160	260384 1113474 3069.0kB 121942B	64B	32B 335392	19
		4	1 370200	324200 1391778 3671.4kB 121942B	64B	32B 419176	19
		1	3 148080	130192	558916 1911.0kB 122981B	64B	32B 84040	19
	HMAC U	2	4 222120	195288	835170 2500.8kB 122981B	64B	32B 84040	19
		3	5 296160	260384 1117574 3113.4kB 122981B	64B	32B 84040	19
		4	6 370200	325480 1396903 3724.6kB 122981B	64B	32B 84040	19

http://www.zurich.ibm.com/ztic/

A year earlier,[START_REF] Henecka | TASTY: Tool for Automating Secure Two-partY computations[END_REF] proposed a different kind of modularity, namely mixing Yao circuits and homomorphic operations. The cost associated with additional hardware required to support homomorphic operations means we do not adopt this approach.

Acknowledgements The work described in this paper has been supported in part by EPSRC grant EP/H001689/1 and by Academy of Finland, project #138358. We would like to thank Elisabeth Oswald for her valuable comments.


Fabio Gadducci

Valentina Giacoma

Monreale

Giacoma Valentina Monreale

Barbed Semantics for Open Reactive Systems

Keywords: Open reactive systems, (saturated) barbed bisimilarities p implies x, p, c p

de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

The most commom technique for specifying the dynamics of a system is based on a reduction semantics: a set representing the states of the system, plus an unlabelled relation among these states, usually built out of a finite set of rules, denoting the evolutions. Despite the advantage of conveying the behaviour with relatively few rules, the main drawback of reduction semantics is that the dynamics of a system is described in a monolithic way, meaning that the evolution is obtained by closing the set of rules under all contexts. Thus, a subsystem can be interpreted only by inserting it inside the contexts where a reduction may take place. To make the analysis simpler, it is often necessary to consider descriptions accounting separately for the behaviour of each single sub-component, thus increasing modularity and enhancing the opportunities for verification.

The theory of reactive systems (RSs) [START_REF] Leifer | Deriving bisimulation congruences for reactive systems[END_REF] offers a framework that allows to distill labelled transition systems (LTSs), hence to obtain behavioural equivalences, for formalisms based on reduction semantics. The idea is simple: a system p has a labelled transition p c -→ p if the system obtained by inserting p inside the (unary) minimal context c may reduce to p . The notion of "minimal" context is expressed via the categorical notion of relative pushout (RPO), which ensures that bisimilarity is a congruence when enough RPOs exist. A grupoidal extension (GRSs) has been proposed [START_REF] Sassone | Deriving bisimulation congruences using 2-categories[END_REF], in order to deal with equationally specified systems (e.g. processes in a calculus with structural congruence).

Should all the possible contexts allowing a reduction be admitted as labels, the resulting bisimilarity would in general be coarser. Despite being better suited in some case studies, such an equivalence (called saturated bisimilarity) is usually intractable, since it has to tackle a potentially infinite set of contexts. The problem has been addressed in [START_REF] Bonchi | Saturated semantics for reactive systems[END_REF] by introducing an "efficient" characterisation of these semantics, where one avoids considering all contexts by using in a cunning way RPOs, at the price of modifying the standard, symmetric presentation of the (either strong or weak) bisimulation equivalences.

Despite their wide range of applicability, saturated and "minimal contexts" bisimilarities still fail to cover all the interesting possibilities: the former is sometimes too fine-grained, while the latter is too coarse. As for process calculi, the standard way out of the impasse is to consider barbs [START_REF] Milner | Barbed bisimulation[END_REF] (that is, predicates on the states of a system) and barbed equivalences (where the check of such predicates is added to the bisimulation game). The flexibility of the definition allows for recasting a variety of observational, bisimulation-based equivalences. Therefore, a suitable notion of barbed saturated semantics for RSs is introduced in [START_REF] Bonchi | Reactive systems, barbed semantics, and the mobile ambients[END_REF], and it is further investigated in [START_REF] Bonchi | On barbs and labels in reactive systems[END_REF][START_REF] Bonchi | Towards a general theory of barbs, contexts and labels[END_REF], where an efficient characterisation for both the strong and weak case is presented, avoiding to consider all contexts.

Even if these extensions witness the vitality of the formalism, one of the fiercest limits suffered by RSs was the restriction to ground rules for describing the dynamics of a system. We are aware of two different attempts to deal with parametric rules in the (G)RS framework. In [START_REF] Di Gianantonio | RPO, second-order contexts, and λcalculus[END_REF], the notion of a category of second-order contexts is introduced and the RPO construction is carried out in this setting, to capture the lazy observational equivalence of λ-calculus. In [START_REF] Klin | Labels from reductions: Towards a general theory[END_REF] term x may evolve into a state p . The notions of minimal context and most general instantiation are captured at once by the notion of (G-)lux. The (strong) bisimilarity induced by the synthesised LTS for open terms is a congruence only under very restrictive conditions, hindering the applicability of the framework. It indeed seems that such conditions are satisfied by simple process calculi with a trivial structural congruence, but that this is not always so for richer calculi.

This paper, along the lines of [START_REF] Bonchi | Reactive systems, barbed semantics, and the mobile ambients[END_REF], proposes a suitable notion of barbed saturated bisimilarity for open GRSs: this is by definition guaranteed to be a congruence and, under certain conditions, it can alternatively be described in a more efficient way via the G-lux LTS and the semi-saturated game. We present the study for both the strong and the weak equivalence and, as it is usual for any newly proposed technique, we test their adequacy against suitable case studies. We thus consider the asynchronous CCS [START_REF] Amadio | On bisimulations for the asynchronous π-calculus[END_REF], whose simplicity allows us to use it as running example, and MAs, whose more complex behaviour highlights the usefulness of open semantics. In both cases, we show that the closed version of our semantics exactly captures the standard ones of the calculus.

The paper is organised as follows. §2 recalls the notion of 2-category on which the one of GRS is based, and shows how it can be used to model the syntax of a calculus. §3 introduces open GRSs and the definition of G-lux LTS. The technical core of the paper is presented in §4, where both the strong and weak barbed saturated semantics for open GRSs are studied, and labelled characterisations of them by means of their semi-saturated counterparts are offered. §5 shows an application of the framework to MAs and §6 concludes the paper.

The appendix recalls the categorical notions of GRPO and GRPB (needed in §3), as well as the proof of our main result.

A categorical representation of process calculi

This section briefly introduces a categorical representation of a process calculus, previously introduced in [START_REF] Klin | Labels from reductions: Towards a general theory[END_REF], and based on the notion of 2-category [START_REF] Bruni | Symmetric monoidal and cartesian double categories as a semantics framework for tile logic[END_REF][START_REF] Kelly | Review of the elements of 2-categories[END_REF]. G-categories can be used to model the syntax of process calculi. We will show an example of this by exploiting a G-category based on the PROP-category [START_REF] Maclane | Categorical algebra[END_REF].

Definition 1 (2-category).

Definition 3 (PROP-category).

A product and permutation category (PROP-category) C has natural numbers 0, 1, 2, . . . as objects and it is equipped with two further structures, as follows for each n, the group of permutations of n elements, S(n), is a subgroup of all the invertible elements of the hom-set C(n, n). The identity permutation is the identity morphism 1 n : n → n; there is a functor ⊗ : C × C → C, called product and written between its arguments, which acts as addition on the objects, i.e., m ⊗ n = m + n, and moreover it is required that 1. it is associative: A G-PROP is a PROP where the underlying category is a G-category.

(f ⊗ f ) ⊗ f = f ⊗ (f ⊗ f ); 2. given σ ∈ S(n) and σ ∈ S(n ), we have σ ⊗ σ = σ × σ : n + n → n + n ,
Q P | R Q | R
Example 1. We now show how the signature of a calculus (modulo term equations) may induce a G-PROP. Inspired by the characterisation of (a fragment of) CCS in [START_REF] Klin | Labels from reductions: Towards a general theory[END_REF], we model here the finite, restriction and summation free fragment of the asynchronous version of the calculus [START_REF] Amadio | On bisimulations for the asynchronous π-calculus[END_REF]. Later on, we will use the same approach for modelling our main case study, i.e., Mobile Ambients (MAs) [START_REF] Cardelli | Mobile ambients[END_REF]. The syntax of ACCS is shown on the left of Fig. 1. We assume a set N of names ranged over by a, b, c, . . . . Also, we let P, Q, R . . . range over the set of processes. The processes are considered up to the structural congruence ≡ induced by the two axioms in the middle of Fig. 1. To keep the example simple, there is no structural rule guaranteeing that is the identity for the parallel composition. The transition relation is defined by the rightmost rules of the same figure: it is going to be used just in the forthcoming sections, even if it is introduced here for the sake of presentation.

The signature for ACCS is Σ = : 0, a. : 1, ā : 0, | : 2. The arrows p : m → n of G-PROP PA2CP represent n-tuples of terms over Σ quotiented by associativity (the leftmost axiom in the middle of Fig. 1) that altogether contain m distinct holes. Permutations in (n, n) are tuples built from holes, ⊗ acts on arrows as tuple juxtaposition, and arrows composition is the standard term composition.

To define the 2-cells of the category, an explicit representation of the arrows of the category is used. A term can be indeed represented as a finite, ordered tree with nodes of any degree, where an immediate child of a node of degree higher than 1 must have degree at most 1. Leaves of such a tree correspond to occurrences either of outputs or of the constants , so they are labelled with names belonging to N or with ; nodes of degree 1 correspond to applications of prefix operators and they are indeed labelled with names belonging to N ; and nodes of higher degree correspond to term fragments built solely of the parallel operator. So, arrows can be represented as tuples of these trees.

A 2-cell from p to q intuitively says that they are equivalent with respect to the commutative axiom. So, it is defined as a family, indexed by the nodes of (the explicit representation of) p, of permutations on the sets of their immediate children, such that the application of all these permutations to p yields q.

Open G-Reactive Systems

This section presents an extension, previously proposed in [START_REF] Klin | Labels from reductions: Towards a general theory[END_REF], of the theory of G-reactive systems (GRSs) [START_REF] Sassone | Deriving bisimulation congruences using 2-categories[END_REF]. In general, the aim of this theory is to derive labelled transition systems (LTSs) and bisimulation congruences for those specification formalisms whose operational semantics is provided by reduction rules.

In [START_REF] Sassone | Deriving bisimulation congruences using 2-categories[END_REF], the technique of LTS derivation is defined for closed GRSs, that is, by considering closed terms and ground reduction rules, while in [START_REF] Klin | Labels from reductions: Towards a general theory[END_REF], open terms and parametric rules are considered. The idea is quite simple A G-category C models the syntax of a formalism. An (open) system is an arrow p : a 1 → a 2 : it can be plugged into q : a 2 → a 3 via arrows composition. Given arrows p, q : a 1 → a 2 , a 2-cell α : p ⇒ q represents an isomorphism (i.e., a proof of equivalence) between systems p and q. The semantics is given via reduction rules: pairs of systems l, r with the same interfaces. The behaviour of an open GRS is given by an unlabelled transition system. To obtain a labelled one, we instantiate an open system p with a sub-term x, plug the result into a context c and observe if a reduction occurs. Categorically, it means that x; p; c is isomorphic to y; l; d (there exists α : x; p; c ⇒ y; l; d) for an instantiation x, a rule l, r , and a reactive context d, as depicted by diagram (i) of Fig. 2. We shall refer to this kind of diagrams as hexagons.

Clearly, the resulting LTS is often infinite-branching, since all contexts and all instantiations allowing reductions may occur as labels. Moreover, it has redundant transitions: the ACCS open process a.1 would have both transitions

a.1 1|a --→ 1 1 and a.1 1|a|p ---→ 1|q 1 | q | p
, yet neither p nor q "concur" to the reduction.

In order to remove this kind of redundancy, we thus consider only "minimal contexts allowing a reduction" and the "most general instantiations", both modelled by the categorical notion of G-locally universal hexagons (G-luxes). The explicit definition of G-lux is found in [START_REF] Klin | Labels from reductions: Towards a general theory[END_REF], here we use a simpler characterisation of it in terms of the better known notions of groupoidal-idem pushouts (GIPOs) and

a6 a4 c ; ; x x x x x x a5 d c c F F F F F F α + 3 a2 p O O a3 l O O a1 x c c F F F F F F y ; ; x x x x x x a6 a4 c ; ; x x x x x x a5 d c c F F F F F F a1 x;p O O y;l O O a6 a2 p;c 0 0 a3 l;d n n a1 x c c F F F F F F y ; ; x x x x x x a6 β ' F F F F a4 c ; ; x x x x x x c / / a8 γ 7 ? x xx x e O O a5 d c c F F F F F F d o o ψ + 3 a2 p O O a7 x o o ϕ ' F F F F y / / a3 l O O δ 7 ? x xx x a1 z O O x c c F F F F F F y ; ; x x x x x x (i) (ii) (iii) (iv)
Fig. 2. Hexagon and G-lux.

groupoidal-idem pullbacks (GIPBs) in G-categories (see [START_REF] Klin | Labels from reductions: Towards a general theory[END_REF]Lemma 10]). We refer to [START_REF] Sassone | Deriving bisimulation congruences using 2-categories[END_REF] for the notion of GIPO, the one of GIPB being symmetric. For the convenience of the reader we report both definitions in Appendix A.

Definition 5 (G-lux). The hexagon (i) in Fig. 2 is a G-locally universal hexagon (G-lux) if (ii) is a GIPO and (iii) is a GIPB.

We say that a GRS has G-luxes if in its underlying category every hexagon as diagram (i) in Fig. 2 has an inner G-lux hexagon as diagram (iv) such that Example 3. As for the synchronous version [START_REF] Klin | Labels from reductions: Towards a general theory[END_REF], it can be shown that the GRS C ACCS has G-luxes. The leftmost diagram of Fig. 3 shows the derived transition a.ā 1|ā --→ ā (the instantiation 0 is usually omitted). Here the initial state offers a closed process with an input on the channel a at top level, while the environment provides an output action on the same channel, so the communication on it can occur. Note instead that no instantiation is provided. The rightmost diagram of Fig. 3 shows instead the transition a. | 1 1 -→ ā . Also in this case the initial state offers an input on a at top level but here it is in parallel with a hole, which is going to be replaced with the output action on the same channel provided by the instantiation. So, also in this case, the communication on the same channel can occur. Note however that here the environment does not offer anything.

α = δ * 1 p * β • 1 z * ψ * 1 e • ϕ * 1 l * γ.
In [START_REF] Klin | Labels from reductions: Towards a general theory[END_REF], (strong) bisimilarity on LLTS is referred to as GLUX-bisimilarity ∼ L : despite the flexibility of the G-luxes framework, ∼ L is a congruence (i.e., if p ∼ L q, then p; c ∼ L q; c, ∀c ∈ C) under some (restrictive) assumptions on C. In particular, a 2-categorical version of the requirement that all arrows of C are mono must be satisfied. These conditions hold for simple process calculi with a trivial structural congruence, such as the choice-free fragment of CCS (as proved in [START_REF] Klin | Labels from reductions: Towards a general theory[END_REF]) and thus apparently also by its asynchronous version considered here, even if it is doubtful for richer calculi such as Mobile Ambients.

1 1 1|ā 9 9 s s s s s 1 1 e e K K K K K 0 a.ā O O 1 a.1|ā O O 0 0 e e K K K K K ā 9 9 s s s s s 1 1 1 9 9 s s s s s 1 1 e e K K K K K 1 a. |1 O O 1 a.1|ā O O 0 ā e e K K K K K 9 9 s s s s s
Remark 1. The standard notion of GRS [START_REF] Sassone | Deriving bisimulation congruences using 2-categories[END_REF] is very similar to the one presented in Definition 4. One difference is that in the G-category C the existence of a chosen object 0 is required, which can never be the codomain of any arrow and which is used to denote the lack of holes. So, arrows having 0 as domain are deemed to represent closed terms. Building on this, the main difference is that the rules are ground, that is, they are pairs of closed terms, and also the states of the reduction relation and of the derived (GIPO) LTS are so. The reduction relation is thus defined by taking p p if there exist l, r ∈ R, d ∈ D, α : p ⇒ l; d and α : q ⇒ r; d. In the LTS, instead, p c -→ p if for d ∈ D and l, r ∈ R, the square p, c, l, d is a GIPO and p = r; d.

It is easy to see that if we specialise the theory of open GRSs to consider closed terms and closed rules, it subsumes the standard theory of GRSs. Indeed, being both terms and rules ground, in the definition of the reduction relation the x will trivially be the identity on 0, so the definition coincides with the one for closed GRSs. Let us now look at the derived LTS. If we consider again closed states and rules, the definition of transition coincides: since both the instantiations x and y will be the identity on 0, the requirement that diagram (i) of Fig. 2 is a G-lux, by definition, means that the square p, c, l, d is a GIPO and the square 0, p; c, 0, l; d a GIPB. So, it is easy to see that p c -→ p is a GLUX transition if and only if it is also a GIPO one.

If instead open rules and closed are considered, then in the definition of the reduction relation the instantiation x of l can be different from 0, and an equivalent, closed GRS is obtained by instantiating all the open rules, i.e., if it contains the ground rule x; l, x; r for any x. Instead, as far as the definition of LTS is concerned, in diagram (i) of Fig. 2 the x has to be the identity on 0 (since p is ground). By definition, the hexagon is a G-lux if and only if p, c, y; l, d is a GIPO and the square 0, p; c, y, l; d is a GIPB, therefore, it is easy to check that p c -→ p is a GLUX transition if and only if the corresponding closed GRS containing the ground rule y; l, y; r has the same GIPO transition.

Barbed bisimulation represents a general technique for generating bisimulationbased equivalences. Intuitively, a barb is just a predicate on the states of a system, which detects the possibility of performing some observable action. We write P ↓ o if P satisfies the predicate o. Barbed equivalences add the check of such predicates in the bisimulation game: every time that a system shows a barb, the equivalent system has to show the same barb, and vice-versa. For instance, ACCS barbs express the ability of a process to perform an output over a channel. Formally, for a closed process P , P ↓ ā if P ≡ ā | Q, for some Q. In [START_REF] Amadio | On bisimulations for the asynchronous π-calculus[END_REF] this notion is used to give the definition of barbed equivalence for the calculus.

In general, the advantage of this kind of semantics is that the flexibility of the definition allows for recasting a wide variety of observational, bisimulationbased equivalences. For example, in [START_REF] Amadio | On bisimulations for the asynchronous π-calculus[END_REF], the authors prove that the standard bisimilarity for ACCS, (weak) asynchronous bisimilarity, coincides with (weak) barbed equivalence. In [START_REF] Bonchi | Reactive systems, barbed semantics, and the mobile ambients[END_REF], instead, a suitable notion of (weak) barbed semantics for closed RSs is introduced, showing that it can be characterised via the LTS labelled with minimal contexts and the semi-saturated game, and that the proposal captures the behavioural semantics for MAs.

Along the lines of [START_REF] Bonchi | Reactive systems, barbed semantics, and the mobile ambients[END_REF], we introduce suitable notions of strong and weak barbed saturated semantics for open GRSs and characterise them via the GLUX LTS.

Strong Open Barbed Saturated Semantics

As for closed systems, barbs for open ones are state predicates. In the following, we fix a 2-cells respected family O of barbs on open systems, and we write p ↓ o if p satisfies o ∈ O. By 2-cells respected, we mean that p ↓ o and α : p ⇒ q implies q ↓ o . For example, if we consider tuples of open terms, ACCS barbs can observe the presence of an output action at top level of a term.

Definition 7 (Open Barbed Saturated Bisimulation).

A symmetric relation R is an open barbed saturated bisimulation if whenever p R q then ∀x, c if x; p; c ↓ o then x; q; c ↓ o ; if x; p; c p then x; q; c q and p R q .

Open barbed saturated bisimilarity ∼ OBS is the largest such bisimulation.

Note that ∼ OBS is a congruence by definition. It can be efficiently characterised through the GLUX transition system via the semi-saturated game.

Definition 8 (Open Barbed Semi-Saturated Bisimulation). A symmetric relation R is an open barbed semi-saturated bisimulation if whenever

p R q then -∀x, c, if x; p; c ↓ o then x; q; c ↓ o ; -if p c -→
x p then x; q; c q and p R q .

Open barbed semi-saturated bisimilarity ∼ OBSS is the largest such bisimulation.

Proposition 1.

In an open GRS having G-luxes, ∼ OBSS =∼ OBS .

As an immediate test of the adequacy of our framework, we apply it to ACCS. We know that the standard bisimilarity for ACCS coincides with the barbed equivalence, which in turn is equivalent to the open barbed saturated bisimilarity defined only over closed ACCS processes [START_REF] Fournet | A hierarchy of equivalences for asynchronous calculi[END_REF]. Now we can define the open barbed semi-saturated bisimilarity for ACCS by using the GLUX LTS for the calculus, and since the open GRS has G-luxes, thanks to Proposition 1, we can say that it coincides with the open barbed saturated bisimilarity. Therefore, if we consider only closed ACCS processes, we can conclude that barbed semisaturated bisimilarity is equivalent to asynchronous bisimilarity.

Proof. Clearly ∼ OBS ⊆∼ OBSS : it suffices to note that p c -→ x p implies x; p; c p .

We then focus on ∼ OBSS ⊆∼ OBS . We prove it by showing that the closure S of the strong open barbed semi-saturated bisimilarity with respect to instantiations, contexts and 2-cells S = { u, v |u ⇒ x; p; c, v ⇒ x; q; c, p ∼ OBSS q, x ∈ C, c ∈ C} is a strong open barbed saturated bisimulation.

Suppose that x ; u; c ↓ o . By hypothesis barbs are respected by 2-cells, thus x ; x; p; c; c ↓ o . Since p ∼ OBSS q also x ; x; q; c; c ↓ o and so x ; v; c ↓ o .

Suppose that x ; u; c p . Then, also x ; x; p; c; c p . This means that for some l, r ∈ R, y ∈ C and d ∈ D, we have that there exists α : x ; x; p; c; c ⇒ y; l; d (diagram (i)) and p = y; r; d.

; ; w w w w β ' G G G G G G G G c ; ; w w w w c / / γ 7 ? w w w w w w w w e O O d c c G G G G G G G G G d o o ψ + 3 p O O x o o ϕ ' G G G G G G G G y / / l O O x c c G G G G δ 7 ? w w w w w w w w z O O x c c G G G G y ; ; w w w w w w w w w c ; ; w w w w β ' G G G G G G G G c ; ; w w w w c / / γ 7 ? w w w w w w w w e O O d ;e c c G G G G G G G G G d o o q O O x o o ϕ ' G G G G G G G G y / / l O O x c c G G G G δ 7 ? w w w w w w w w z O O x c c G G G G z;y ; ; w w w w w w w w w (i) (ii)
Since the GRS has G-luxes, we can construct a G-LUX as the inner hexagon of diagram (i). This means that p c --→ x y ; r; d and since p ∼ OBSS q, then x ; q; c q and y ; r; d ∼ OBSS q . Therefore, there exists an hexagon as the inner one of diagram (ii) shown above, with l , r ∈ R and q = y ; r ; d . Thanks to the fact that D is 2-cell closed and composition reflecting, we know that e is reactive, hence z; x ; q; c ; e z; q ; e. Since x ; x; q; c; c ⇒ z; x ; q; c ; e and x ; v; c ⇒ x ; x; q; c; c also x ; x; q; c; c z; q ; e (external hexagon of diagram (ii)) and x ; v; c z; q ; e. Moreover, since y ; r; d ∼ OBSS q and p = y; r; d ⇒ z; y ; r; d ; e, we can conclude that p S z; q ; e. As usual, * denotes the transitive and reflexive closure of .

Weak Open Barbed Saturated Semantics

Definition 10 (Weak Open Barbed Saturated Bisimulation). A symmetric relation R is a weak open barbed saturated bisimulation if whenever p R q then ∀x, c if x; p; c ⇓ o then x; q; c ⇓ o ; if x; p; c * p then x; q; c * q and p R q .

Weak open barbed saturated bisimilarity ∼ W OBS is the largest such bisimulation.

As for the strong case, it can be efficiently characterised through the GLUX transition system via the semi-saturated game.

Definition 11 (Weak Open Barbed Semi-Saturated Bisimulation

). A symmetric relation R is a weak open barbed semi-saturated bisimulation if whenever p R q then -∀x, c, if x; p; c ↓ o then x; q; c ⇓ o ; -if p c -→ x p then x; q; c * q and p R q .
Weak open barbed semi-saturated bisimilarity ∼ W OBSS is the largest such bisimulation.

The correspondence result is stated below: its proof is shown in Appendix B.

Proposition 2.

In an open GRS having G-luxes, ∼ W OBSS =∼ W OBS .

As for the strong case, also for the weak one we can immediately test our proposal against ACCS. In particular, by following the reasoning used in the previous section for the strong case, we can analogously conclude that if we consider only closed ACCS processes, weak barbed semi-saturated bisimilarity is equivalent to weak asynchronous bisimilarity.

An Open G-Reactive System for Mobile Ambients

In this section we apply the framework of open GRSs to a richer calculus, that is, the calculus of Mobile Ambients (MAs) [START_REF] Cardelli | Mobile ambients[END_REF], in order to show the adequacy of the results presented in §4. After a quick introduction of the calculus, we present the corresponding open GRSs and we test our framework on it.

P |Q]|m[R] m[n[P |Q]|R] if P Q then n[P ] n[Q] m[n[out m.P |Q]|R] n[P |Q]|m[R] if P Q then P |R Q|R open n.P |n[Q] P |Q if P ≡ P, P Q, Q ≡ Q then P Q Fig. 4
. Syntax, structural congruence and reduction relation of MAs.

Mobile Ambients

We consider the finite, restriction free fragment of MAs. The syntax is shown on the left of the upper row of Fig. 4. We assume a set N of names ranged over by m, n, u, . . . We let P, Q, R, . . . range over the set P of closed processes. The semantics of the calculus is given by the combination of an equivalence between processes and a relation among them. The structural congruence ≡ is induced by the two axioms on the right of the first row of Fig. 4. It is used to define the reduction relation , which is inductively generated by the set of axioms and inference rules shown in the lower rows of Fig. 4.

As said in the previous section, a barb o is a predicate over the states of a system, with P ↓ o denoting that P satisfies o. In MAs, P ↓ n denotes the presence at top-level of an ambient n. Formally, for a closed process P , P ↓ n if P ≡ n[Q]|R for some closed processes Q and R. A closed process P satisfies the weak barb n (denoted as P ⇓ n ) if there exists a process P such that P * P and P ↓ n . The notions of strong and weak barb above are respectively used to define the strong and weak reduction barbed congruences [START_REF] Merro | Behavioral theory for mobile ambients[END_REF].

Definition 12 (Reduction Barbed Bisimulation

). A symmetric relation R is a reduction barbed bisimulation if whenever P R Q then ∀C[-] contexts -if C[P ] ↓ o then C[Q] ↓ o ; -if C[P ] P then C[Q] Q and P R Q . A symmetric relation R is a weak reduction barbed bisimulation if whenever P R Q then ∀C[-] contexts -if C[P ] ⇓ o then C[Q] ⇓ o ; -if C[P ] * P then C[Q] * Q and P R Q .
Reduction barbed congruence ∼ = and weak reduction barbed congruence ∼ = W are the largest such bisimulations.

Labelled characterisations of reduction barbed congruences over MAs processes are presented in [START_REF] Rathke | Deriving structural labelled transitions for mobile ambients[END_REF][START_REF] Bonchi | Reactive systems, barbed semantics, and the mobile ambients[END_REF] for the strong case, and in [START_REF] Merro | Behavioral theory for mobile ambients[END_REF][START_REF] Bonchi | Reactive systems, barbed semantics, and the mobile ambients[END_REF] for the weak one. In the following, we are going to provide an alternative characterisation of them by using the GLUX LTS and the semi-saturated game.

An open GRS for Mobile Ambients

As for ACCS, in order to define the open GRS for MAs, we exploit the G-PROP PA2CP induced from the signature corresponding to the grammar for the calculus modulo the associativity equation. The signature is Σ = : 0, n[ ] : 1, M. : 1, |: 2, where M stands for in n, out n and open n.

For the definition of 2-cells, we consider an analogous representation for the terms and consequently for the arrows of the category. The main difference with respect to the representation used for ACCS is that here leaves only correspond to occurrences of the constants , while a node of degree 1 corresponds to an application of either an ambient operator or a capability. In the former case it is labelled with a name belonging to N , while in the latter case it is labelled with the capability followed by an ambient name. Now, we use this G-PROP to define the open GRS C M As for MAs. We take as reduction rules the set , which is going to replace the hole inside the ambient n, while the environment provides an ambient m with a hole inside it (which will be replaced by n) in parallel with a closed process R. These transitions show the importance of using instantiation and context at the same time. In both cases, indeed, we can note the interaction of three parts intervening in the reduction: the initial state, the instantiation and the context. 1|m

n,m∈N { n[in m.1 | 2] | m[3], m[n[1 | 2] | 3] , m[n[out m.1 | 2] | 3], n[1 | 2] | m[3] , open n.1 | m[2], 1 | 2 },
1 1 1|m[Q] 9 9 s s s s s 1 1 e e K K K K K 1 n[1] O O 3 n[in m.1|2]|m[3] O O 2 in m.1|2 e e K K K K K 1,2,Q 9 9 s s s s s 1 1 m[1|R] 9 9 s s s s s 1 1 e e K K K K K 1 n[1] O O 3 m[n[out m.1|2]|3] O O 1 out m.1|2 e e K K K K K 1,2,R 9
[Q] -----→ in m.1|2 m[n[1 | 2] | Q] and n[1] m[1|R] ------→ out m.1|2 n[1 | 2] | m[R].
This never happens in ACCS, where we only have the synchronization between two terms in parallel which thus can be offered by just two of these three parts.

Open Barbed Semantics for Mobile Ambients

Here we show that the labelled characterisations of ∼ = and ∼ = W via the GIPO LTS and the semi-saturated game presented in [START_REF] Bonchi | Reactive systems, barbed semantics, and the mobile ambients[END_REF] are an instance of our results stated in Propositions 1 and 2.

We begin by observing that if we consider only closed terms and the standard notion of strong (respectively weak) barb for them, the notion of strong (respectively weak) open barbed saturated bisimilarity for MAs coincides with the one of strong (respectively weak) reduction barbed congruence, where C[P ] stands for P ; C [-]. Therefore, as shown in § 4, since the open GRS has G-luxes, we can efficiently characterise the strong and weak reduction barbed congruence by instantiating respectively Definitions 8 and 11 for closed MAs processes, with the standard notion of strong and weak MAs barb and the GLUX LTS for the calculus. As shown in [START_REF] Bonchi | Reactive systems, barbed semantics, and the mobile ambients[END_REF], the quantification over all contexts can be removed from the first condition of both definitions.

Definition 13 (MAs Closed Barbed Semi-Saturated Bisimulation

). A symmetric relation R is a MAs closed barbed semi-saturated bisimulation if whenever P R Q then -if P ↓ n then Q ↓ n ; -if P C[-] ---→ P then C[Q] Q and P R Q .
A symmetric relation R is a MAs weak closed barbed semi-saturated bisimulation if whenever P R Q then According to Remark 1, the results above subsume the ones presented in [4, Theorem 5], thus providing a labelled characterisation for both congruences ∼ = and ∼ = W via the GIPO LTS.

-if P ↓ n then Q ⇓ n ; -if P C[-] ---→ P then C[Q] * Q and P R Q .

Conclusions and Further Works

We introduced the notions of (strong and weak) barbed saturated bisimilarity for open GRSs, and we showed that it can be efficiently characterized via the GLUX LTS by employing the semi-saturated game. Moreover, in order to show the adequacy of our proposal, we tested it on ACCS and, most importantly, on MAs. In both cases we proved that the framework captures the standard semantics of these calculi. More precisely, we showed that, for both the strong and the weak variant, the open barbed semi-saturated bisimilarity defined on closed ACCS terms coincides with asynchronous bisimilarity, and that on closed MAs terms it coincides with reduction barbed congruence.

However, albeit we showed that the framework is general enough to capture the abstract semantics of well-known formalisms, it parametric with respect to the choice of the set of barbs: the choice of the "right" barb is left to the ingenuity of the researcher, and often it is not a trivial task [START_REF] Rathke | Semantic barbs and biorthogonality[END_REF][START_REF] Honda | On reduction-based process semantics[END_REF]. So, it would be interesting to extend our framework by considering an automatically derived notion of barb for (open) GRSs. An alternate route would instead be to abstract away from the use of state predicates by providing an efficient labelled characterization of the barbed semantics, as shown for closed GRSs in [START_REF] Bonchi | On barbs and labels in reactive systems[END_REF][START_REF] Bonchi | Towards a general theory of barbs, contexts and labels[END_REF].

Our proposal of a semantics for open GRSs builds on [START_REF] Klin | Labels from reductions: Towards a general theory[END_REF]. The authors there study only strong bisimilarity, showing that it is a congruence under rather restrictive conditions, hindering the applicability of the framework. Our work aims at partly solving this problem, in order to relax the conditions for proving a congruence property. However, we did not address the issue of the intrinsic redundancy of the G-lux mechanism: the intertwining of context and instantiation may sometimes end up in the offering of components that are not necessary for the reduction. Consider for example the transition represented by the leftmost G-lux in Fig. 5. It is easy to note that Q is not necessary for this reduction, since it appears both in the context on the left and in the instantiation on the right.

Concerning future works, a relatively simpler one should be a comparison with the proposal for parametric rules in GRSs in [START_REF] Di Gianantonio | RPO, second-order contexts, and λcalculus[END_REF]. A more challenging issue would be to investigate the connections with [START_REF] Baldan | A semantic framework for open processes[END_REF][START_REF] Rensink | Bisimilarity of open terms[END_REF]: both works propose a semantic framework for open processes, adopting suitable LTS and alternative behavioural semantics, which is however far removed from the GRSs formalism. In general terms, and stimulated by the latter contributions, we plan to investigate the issue of adequacy for open semantics, and the connection between our proposal and the standard definition of bisimilarity for open terms, considering the standard bisimilarity lifted from closed to open terms by instantiating these ones in all possible ways. It is clear that the latter bisimilarity is included in the former one, and for simpler calculi the two might often coincide. However, the connection between open GRSs and the tile model [START_REF] Gadducci | The tile model[END_REF] established in [START_REF] Gadducci | A modular lts for open reactive systems[END_REF] suggests us that the bisimilarity that we obtain is finer, as it is proved already for simple CCS variants and argued for richer calculi in [START_REF] Rensink | Bisimilarity of open terms[END_REF][START_REF] Bruni | Bisimilarity congruences for open terms and term graphs via tile logic[END_REF].

  , a general theory for open (G)RSs is developed, by considering open terms and rules. So, now the transitions are labelled not only with the minimal context but also with the most general instantiation allowing a reduction. More explicitly, p c -→ x p if p inserted into the context c and instantiated with the (possibly open)

  A 2-category C is a category such that, given any two objects a and b, the hom-set of a and b (the collections of arrows between them) is the class of objects of some category C(a, b) and, correspondingly, whose composition functions * : C(a, b) × C(b, c) → C(a, c) are functors. Arrows of C(a, b) are called 2-cells and are denoted by α : f ⇒ g : a → b, the composition in C(a, b) is instead denoted by •. Definition 2 (G-category). A groupoidal category (G-category) is a 2category whose 2-cells are invertible.

Fig. 1 .

 1 Fig. 1. Syntax, structural congruence and reduction relation of ACCS.

  : a system specified by an open term p has a labelled transition p c -→ x p if p instantiated with the (open) term x and inserted into the context c may evolve into a state p .

Definition 4 (Example 2 .

 42 Open GRS). An open G-reactive system C consists of 1. a G-category C; 2. a composition-reflecting, 2-cell closed subcategory D of reactive contexts; 3. a set R ⊆ a1,a2∈|C| C(a 1 , a 2 ) × C(a 1 , a 2 ) of reduction rules. Intuitively, reactive contexts are those arrows inside which a reduction can occur. By 2-cell closed we mean that d ∈ D and α : d ⇒ d in C implies d ∈ D, while by composition-reflecting we mean that d ; d ∈ D implies d, d ∈ D. Given an open GRS C, the reduction relation over the terms of C is generated by closing the reduction rules under all reactive contexts, instantiations and 2cells. Formally, the reduction relation is defined by taking p p if there exist l, r ∈ R, d ∈ D, x ∈ C, α : p ⇒ x; l; d and α : p ⇒ x; r; d. Consider the G-PROP PA2CP category shown in §2. An open GRS C ACCS over it takes as reduction rules the set a∈N { a.1 | ā , 1 }, and as the subcategory of reactive contexts the smallest composition-reflecting, 2-cell closed subcategory including arrows of the shape 1 | p : 1 → 1. Note that it contains no context with a hole after the input operator.

Definition 6 (

 6 GLUX Transition System). Let C be an open GRS and C its underlying G-category. The GLUX LTS (llts(C)) is defined as follows states: p : a 1 → a 2 in C, for arbitrary a 1 and a 2 ; transitions: p c -→ x p if there exist d ∈ D, y ∈ C, rule l, r ∈ R and 2-cell α : x; p; c ⇒ y; l; d such that diagram (i) of Fig. 2 is a G-lux and p = y; r; d.

Fig. 3 .

 3 Fig. 3. G-luxes representing the transitions a.ā 1|ā --→ ā and a. | 1 1 -→ ā .

  c

  This section introduces the weak case of open barbed (semi-)saturated bisimilarity. We begin by introducing the notion of weak barb on open states. Definition 9 (Weak Barb). Let o ∈ O be a barb. An open state p satisfies the weak barb o (in symbols p ⇓ o ) if there exists p such that p * p and p ↓ o .

P

  ::= , n[P ], M.P, P |P M ::= in n, out n, open n (P |Q)|R ≡ P |(Q|R) P |Q ≡ Q|P n[in m.

1 | 2 ]n[ 1 | 2 ]

 1212 and as the subcategory of reactive contexts the smallest composition-reflecting, 2-cell closed subcategory including arrows of the shapes 1 | p : 1 → 1 and n[1] : 1 → 1. Note that it does not contain contexts with a hole after a capability. Fig. 5 shows two interesting labelled transitions derived by applying the synthesis mechanism based on G-luxes. The leftmost G-lux represents n[1] | Q]. The initial open term offers an ambient n with a hole inside it, the instantiation provides the open term in m.1 | 2, which is going to replace the hole inside the ambient n, while the environment provides an ambient m[Q] which is going to be in parallel with n. The rightmost G-lux instead represents | m[R]. Also in this case the initial open term offers an ambient n with a hole inside it, the instantiation instead provides the open term out m.1 | 2

Fig. 5 .

 5 Fig.5. The transitions n[START_REF] Amadio | On bisimulations for the asynchronous π-calculus[END_REF]

  MAs closed barbed semi-saturated bisimilarity ∼ BSS M As and MAs weak closed barbed semi-saturated bisimilarity ∼ W BSS M As are the largest such bisimulations. Proposition 3. Closed barbed semi-saturated bisimilarity for MAs ∼ BSS M As coincides with reduction barbed congruence ∼ = and weak closed barbed semi-saturated bisimilarity ∼ W BSS M As coincides with weak reduction barbed congruence ∼ = S .

Research partially supported by the EU FP7-ICT IP ASCEns (IP 257414). z; q ; e and x ; v; c *

A GIPO and GIPB

The first section of the Appendix recalls the notions of GIPO and GIPB. Definition 14 (GRPO, GIPO). Let the diagrams in Fig. 6 be in a G-category C. A candidate for the diagram (i) is a tuple a 5 , n, o, p, β, γ, δ such that 1 h * γ • β * 1 p • 1 g * δ = α. This means that the 2-cells γ, β, and δ, as illustrated in diagram (ii), paste together to give α. A groupoidal-relative-pushout (GRPO) is a candidate which satisfies the universal property, i.e., for any other candidate a 6 , n , o , p , β , γ , δ there exists a mediating morphism: a quadruple q : a 5 → a 6 , ϕ : n ⇒ n; q, ψ : o; q ⇒ o , τ : q; p ⇒ p illustrated in diagrams (iii) and (iv). The equations to be satisfied are

Such a mediating morphism must be essentially unique, i.e., for any other mediating morphism q , ϕ , ψ , τ there exists a unique 2-cell ξ : q ⇒ q that makes the two mediating morphisms compatible, i.e., 1)ϕ

This means that the 2-cells γ, β, and δ, as illustrated in diagram (ii), paste together to give α. A groupoidal-relative-pullback (GRPB) is a candidate which satisfies the universal property, i.e., for any other candidate a 6 , n , o , p , β , γ , δ there exists a mediating morphism: a quadruple q : a 6 → a 5 , ϕ : q; n ⇒ n , ψ : q; o ⇒ o , τ : p ; q ⇒ p illustrated in diagrams (iii) and (iv). The equations to be satisfied are 1)γ

Such a mediating morphism must be essentially unique, i.e., for any other mediating morphism q , ϕ , ψ , τ there exists a unique 2-cell ξ : q ⇒ q that makes the two mediating morphisms compatible, i.e., 1)ϕ

A square such as diagram (i) of Fig. 7 is called G-idem pullback (GIPB) if a 1 , h, g, id a1 , α, 1 h , 1 g is its GRPB.

Fig. 7. GRPB

B Proof of Proposition 2

We first give an alternate definition of weak open barbed saturated bisimulation.

Lemma 1 (Revising Barbed Saturation). A symmetric relation R is a weak open barbed saturated bisimulation if whenever p R q then ∀c, x if x; p; c ↓ o then x; q; c ⇓ o ; if x; p; c p then x; q; c * q and p R q .

Let us now move on to the proof of Proposition 2.

We prove that ∼ W OBSS ⊆∼ W OBS by showing that the closure S of the weak open barbed semi-saturated bisimilarity with respect to instantiations, contexts and 2-cells S = { u, v |u ⇒ x; p; c, v ⇒ x; q; c, p ∼ W OBSS q, x ∈ C, c ∈ C} is a weak open barbed saturated bisimulation according to Lemma 1.

Suppose that x ; u; c ↓ o . By hypothesis barbs are respected by 2-cells, therefore x ; x; p; c; c ↓ o . Since p ∼ W OBSS q, then x ; x; q; c; c ⇓ o and so x ; v; c ⇓ o . Now, assume that x ; u; c p . Then, x ; x; p; c; c p . This means that for some l, r ∈ R, y ∈ C and d ∈ D there exists α : x ; x; p; c; c ⇒ y; l; d (the exterior hexagon of the diagram below) and p = y; r; d.