Sara Capecchi

Ilaria Castellani

Mariangiola Dezani-Ciancaglini

Typing Access Control and Secure Information Flow in Sessions

Keywords: Communication-centred computing, session types, access control, secure information flow

We consider a calculus for multiparty sessions with delegation, enriched with security levels for session participants and data. We propose a type system that guarantees both session safety and a form of access control. Moreover, this type system ensures secure information flow, including controlled forms of declassification. In particular, it prevents information leaks due to the specific control constructs of the calculus, such as session opening, selection, branching and delegation. We illustrate the use of our type system with a number of examples, which reveal an interesting interplay between the constraints of security type systems and those used in session types to ensure properties like communication safety and session fidelity.

Introduction

With the advent of web technologies and the proliferation of programmable and interconnectable devices, we are faced today with a powerful and heterogeneous computing environment. This environment is inherently parallel and distributed and, unlike previous computing environments, it heavily relies on communication. It therefore calls for a new programming paradigm which is sometimes called communication-centred. Moreover, since computations take place concurrently in all kinds of different devices, controlled by parties which possibly do not trust each other, security properties such as the confidentiality and integrity of data become of crucial importance. The issue is then to develop models, as well as programming abstractions and methodologies, to be able to exploit the rich potential of this new computing environment, while making sure that we can contain its complexity and get around its security vulnerabilities. To this end, calculi and languages for communication-centred programming have to be security-minded from their very conception, and make use of specifications not only for data structures, but also for communication interfaces and for security properties.

The aim of this paper is to investigate type systems for safe and secure sessions. A session is an abstraction for various forms of "structured communication" that may occur in a parallel and distributed computing environment. Examples of sessions are a client-service negotiation, a financial transaction, or a multiparty interaction among different services within a web application.

Language-based support for sessions has now become the subject of active research. Primitives for enabling programmers to code sessions in a flexible way, as well as type systems ensuring the compliance of programs to session specifications (session types), have been studied in a variety of calculi and languages in the last decade. Session types were originally introduced in a variant of the pi-calculus [START_REF] Takeuchi | An Interaction-based Language and its Typing System[END_REF]. We refer to [START_REF] Dezani-Ciancaglini | Sessions and Session Types: an Overview[END_REF] for a survey on the session type literature. The key properties ensured by session types are communication safety, namely the consistency of the communication patterns exhibited by the partners (implying the absence of communication errors), and session fidelity, ensuring that channels which carry messages of different types do it in a specific order.

Enforcement of security properties via session types has been studied in [START_REF] Bhargavan | Cryptographic Protocol Synthesis and Verification for Multiparty Sessions[END_REF][START_REF] Planul | Secure Enforcement for Global Process Specifications[END_REF]. These papers propose a compiler which, given a multiparty session description, implements cryptographic protocols that guarantee session execution integrity. A type system assuring that services always comply with the policy regulating data exchange is presented in [START_REF] Lapadula | Regulating Data Exchange in Service Oriented Applications[END_REF]. The question of ensuring access control in binary sessions has been recently addressed in [START_REF] Kolundzija | Security Types for Sessions and Pipelines[END_REF] for the Calculus of Services with Pipelines and Sessions of [START_REF] Boreale | Sessions and Pipelines for Structured Service Programming[END_REF], where delegation is absent. On the other hand, the property of secure information flow has not been investigated within session calculi so far. This property, first studied in the early eighties [START_REF] Goguen | Security Policies and Security Models[END_REF], has regained interest in the last decade, due to the evolution of the computing environment. It has now been thoroughly studied for both programming languages (cf [START_REF] Sabelfeld | Language-Based Information-Flow Security[END_REF] for a review) and process calculi [START_REF] Focardi | Classification of Security Properties (Part I: Information Flow)[END_REF][START_REF] Honda | A Uniform Type Structure for Secure Information Flow[END_REF][START_REF] Kobayashi | Type-Based Information Flow Analysis for the Pi-Calculus[END_REF].

In this paper, we address the question of incorporating mandatory access control and secure information flow within session types. We consider a calculus for multiparty sessions with delegation, enriched with security levels for both session participants and data, and providing a form of declassification for data [START_REF] Sabelfeld | Dimensions and Principles of Declassification[END_REF], as required by most practical applications. We propose a type system that ensures access control, namely that each participant receives data of security level less than or equal to its own. For instance, in a well-typed session involving a Customer, a Seller and a Bank, the secret credit card number of the Customer will be communicated to the Bank, but not to the Seller. Moreover, our type system prevents insecure flows that could occur via the specific constructs of the language, such as session opening, selection, branching and delegation. Finally, we show that it allows controlled forms of declassification during communication, namely those explicitly permitted by the sender and respecting the access control policy in the receiver. Our work reveals an interesting interplay between the constraints of security type systems and those used in session types to ensure properties like communication safety and session fidelity.

The rest of the paper is organised as follows. Section 2 motivates our access control and declassification policies with an example. Sections 3 and 4 introduce the syntax and semantics of our calculus. Section 5 defines the secure information flow property. Section 6 illustrates this property by means of examples. Section 7 presents our type system and Section 8 establishes its soundness. Section 9 discusses future work. Appendix Appendix A discusses a more expressive notion of security (called robust security) and shows that our type system remains sound for this new notion. Appendix Appendix B summarises various features of the running example introduced in Section 2.

This paper is a deeply revised version of [START_REF] Capecchi | Session Types for Access and Information Flow Control[END_REF], with improved definitions, new examples and results and complete proofs. In a companion paper [START_REF] Capecchi | Information Flow Safety in Multiparty Sessions[END_REF] we give a monitored semantics, which only assures secure information flow, for a simplification of the present calculus without declassification and delegation.

An Example on Access Control and Declassification

In this section we illustrate by an example the basic features of our typed calculus, as well as our access control policy and our specific form of declassification. The question of secure information flow will only be briefly touched upon here, while it will be discussed in depth in Sections 5 and 6, once the semantics of the calculus has been formally defined. Suffice it to say, for the time being, that a process has secure information flow if none of its actions depends on some input action of higher or incomparable level.

For the sake of simplicity, in this introductory example we shall only consider binary sessions, and two security levels for data and participants, namely high (secret) and low (public) 1 . In our calculus, the level of data represents their degree of confidentiality, while the level of participants represents their reading rights: thus a high participant can read both high and low data, whereas a low participant can only read low data.

Consider the following scenario, involving a bookseller, a client and a bank. A client C sends the title of a book to a bookseller S. The seller S delegates to a bank B both the reception of C's credit card number and its validity check. This frequently happens in online shopping, when clients are redirected to a new page for a secure payment. Delegation is crucial for assuring the secrecy of the credit card number, which should be read by B but not by S. To express this access control constraint, the typing will assign high security level to the credit card and to B, and low security level to S. Then B notifies S about the result of the validity check: since this result is low and the card is high, for this information flow to be admissible a declassification is needed. Finally, if the credit card is valid, C receives a delivery date from S, otherwise the deal falls through. More precisely, the protocol is as follows:

1. C opens a connection with S and sends a title to S; 2. S opens a connection with B and delegates to B part of his conversation with C; 3. C sends his secret credit card number apparently to the low party S but really -thanks to delegation -to the high party B; moreover C authorises the high recipient of his card number to declassify it (although not knowing B, C knows that a delegation to a high party must take place since S is low); 4. B reads the credit card number and then delegates back to S the conversation with C; 5. B selects the answer or for the low party S depending on the validity or not of the credit card, thus performing a declassification; 6. S sends to C either and a date, or just , depending on the label or chosen by B. Notice that this scenario could not be represented by a unique protocol involving C, S, and B, i.e., by a ternary session, since this would imply that the client knows the bank used by the bookseller for payments.

I = ā[2] | b[2] C = a[1](α 1 ).α 1 ! 2, Title ⊥ .α 1 ! ⊥ 2, . α 1 &(2, {ok : α 1 ?(2, date ⊥ ).0, ko : 0}) S = a[2](α 2 ).α 2 ?(1, x ⊥ ).b[2](β 2 ).β 2 ! 1, α 2 .β 2 ?((1, η)). β 2 &(1, {ok : η ⊕ 1, ok .η! 1, Date ⊥ .0, ko : η ⊕ 1, ko .0}) B = b[1](β 1 ).β 1 ?((2, ζ )).ζ ? (2, cc ⊥ ).β 1 ! 2, ζ . valid(cc ⊥ ) β 1 ⊕ 2, ok .0 β 1 ⊕ 2, ko .0
In our calculus, which is an enrichment with security levels of the calculus in [START_REF] Bettini | Global Progress in Dynamically Interleaved Multiparty Sessions[END_REF], this scenario may be described as the parallel composition of the processes shown in Table 1, where security levels appear as superscripts on both data and operators. Here means "secret" and ⊥ means "public", and a level appears on an I/O operator whenever a declassification is involved. For the sake of simplicity, we omit the security levels on the other operators. They will be filled in later in the paper, and this running example, completed with all security levels, will be recalled in Table 6.

A session is a particular activation of a service, involving a number of parties with predefined roles. Here C and S communicate by opening a session on service a, while S and B communicate by opening a session on service b. The initiators ā [START_REF] Bettini | Global Progress in Dynamically Interleaved Multiparty Sessions[END_REF] and b [START_REF] Bettini | Global Progress in Dynamically Interleaved Multiparty Sessions[END_REF] specify the number of participants of each service. We associate integers with participants in services: here C=1, S=2 in service a and B=1, S=2 in service b.

In process C, the prefix a [START_REF] Almeida Matos | On Declassification and the Non-Disclosure Policy[END_REF](α 1 ) means that C wants to act as participant 1 in service a using channel α 1 , matching channel α 2 of participant 2, who is S. When the session is established, C sends to S a title of level ⊥ and a credit card number of level , indicating (by the superscript ⊥ on the output operator) that the credit card number may be declassified to ⊥. Then he waits for either , followed by a date, or .

Process S receives a value from C in service a and then enters service b as participant 2. Here the output β 2 ! 1, α 2 sends channel α 2 to the participant 1 of b, who is B, thus delegating to B the use of α 2 . This means that B will now act as participant 2 in service a, thus directly interacting with C. Then S waits back for the channel α 2 from B. Henceforth, S communicates using both channels β 2 and α 2 : on channel β 2 he waits for one of the labels or , which he then forwards to C on α 2 , sending also a date if the label is .

Forgetting about session opening and abstracting from values to types, we may represent the whole communication protocol by the global types of Table 2 (where we use B, C, S instead of 1, 2), where the left-hand side and right-hand side describe services a and b, respectively. Line 1 says that C sends a of level ⊥ to S. In line 2, S δ means that the channel from S to C is delegated: this delegation is realised by the transmission of the channel (with type T ) from S to B, as shown on the right-hand side. Line 3 says that C sends a of level to S, allowing him to declassify it to ⊥. Notice that due to the previous delegation the is received by B and not by S. Line 4 describes a delegation which is the inverse of that in Line 2: here the (behavioural) type of the channel has changed to T , since the channel has already been used to receive the . Line 5 says that B sends to S one of the labels or . Finally, line 6 says that S sends to C either the label followed by a of level ⊥, or the label . Since B's choice of the label or depends on a test on the , it is crucial that be previously declassified to ⊥, otherwise the reception of a of level ⊥ by C would depend on a value of level (this is where secure information flow comes into play).

Type T represents the conversation between C and S after the first communication, seen from the viewpoint of S. Convening that ?(-), ! -represent input and output in types, that ";" stands for sequencing and that ⊕ -{-} represents the choice of sending one among different labels, the session type T is:

Π ::= {p} | Π ∪ {p}
Set of participants As hinted previously, to formalise access control we give security levels to service participants, and require that a participant of a given level does not receive data of higher or incomparable level. Since the only secret data in our example is , it is natural to associate ⊥ with participant S in both services a and b, and with participant B in service b. Notice that participant C may indifferently have level or ⊥ in service a, since he only sends, but does not receive, the high data .

ϑ ::= v ↓ | s[p] | λ Message content m ::= (p, Π, ϑ ) Message in transit h ::= m • h | ε Queue H ::= H ∪ {s : h} | / 0 Q-set

Syntax

Our calculus for multiparty asynchronous sessions is essentially the same as that considered in [START_REF] Bettini | Global Progress in Dynamically Interleaved Multiparty Sessions[END_REF], with the addition of runtime configurations and security levels.

Let (S , ≤) be a finite lattice of security levels, ranged over by , . We denote by and the join and meet operations on the lattice, and by ⊥ and its minimal and maximal elements.

We assume the following sets:

• service names, ranged over by a, b,..., each of which has an arity n ≥ 2 (its number of participants) and a security level ,

• value variables, ranged over by x, y,..., all decorated with security levels,

• identifiers, i.e., service names and value variables, ranged over by u, w,..., all decorated with security levels,

• channel variables, ranged over by α, β ,...,

• labels, ranged over by λ , λ ,... (acting like labels in labelled records).

Values v are either service names or basic values (boolean values, integers, etc.). When treated as an expression, a value is decorated with a security level ; when used in a message, it is decorated with a declassified level of the form ↓ , where ≤ . When = , we will write simply instead of ↓ . In this case we will speak of trivial declassification. Let us point out that declassification of services is not allowed in our calculus, for lack of evidence of its usefulness (see Example 6.5). Hence, if v is a service name, its level will always be of the simple form .

Sessions, the central abstraction of our calculus, are denoted with s, s .... A session represents a particular instance or activation of a service. Hence sessions only appear at runtime. We use p, q,. . . to denote the participants of a session. In an n-ary session (a session corresponding to an n-ary service) p, q are assumed to range over the natural numbers 1,...,n. We denote by Π a non empty set of participants. Each session s has an associated set of channels with role s[p], one for each participant. Channel s[p] is the private channel through which participant p communicates with the other participants in the session s. A new session s on an n-ary service a is opened when the initiator ā [n] of the service synchronises with n processes of the form a [1](α 1 ).P 1 ,...,a [n](α n ).P n . We use c to range over channel variables and channels with roles. Finally, we assume a set of process variables X,Y,..., in order to define recursive behaviours.

As in [START_REF] Honda | Multiparty Asynchronous Session Types[END_REF], in order to model TCP-like asynchronous communications (with non-blocking send but message order preservation between a given pair of participants), we use queues of messages, denoted by h; an element of h may be a value message (p, Π, v ↓ ), indicating that the value v is sent by participant p to all participants in Π, with the right of declassifying it from level to level ; a channel message (p, q, s[p ] ), indicating that p delegates to q the role of p with level in the session s; and a label message (p, Π, λ ), indicating that p selects the process with label λ among those offered by the set of participants Π. The empty queue is denoted by ε, and the concatenation of a new message m to a queue h by h • m. Conversely, m • h means that m is the head of the queue. Since there may be nested and parallel sessions, we distinguish their queues by naming them. We denote by s : h the named queue h associated with session s. We use H, K to range over sets of named queues, also called Q-sets.

The set of expressions, ranged over by e, e ,..., and the set of processes, ranged over by P, Q ..., are given in Table 3, together with the runtime syntax of the calculus (sessions, channels with role, messages, queues), which appears shaded for ease of reading. We say that a process is a user process if it can be written without using runtime syntax.

Let us informally comment on the primitives of the language, whose operational semantics will be given in the next section. The primitive for session initiation ū[n] opens a new n-ary session for the shared service u by synchronising with n processes of the form u[p](α p ).P p , for p = 1,...,n. The effect of this synchronisation is to create a new session s with an associated queue s : ε, and to replace the channel α p in each process P p by the channel with role s[p]. This is the only synchronous interaction of the calculus. All the other communications, which take place within an established session, are performed asynchronously in two steps, via push and pop operations on the queue associated with the session, using the next three pairs of primitives: the send and receive of a value; the send and receive of a delegation (where one participant transmits to another one the capability of participating in another session with a given role); and the selection and branching operators (where one participant chooses one of the branches offered by another participant). The send/receive and choice primitives are decorated with security levels, whose use will be justified later.

When there is no risk of confusion we will omit the set delimiters {, }, particularly around singletons.

Operational Semantics

In this section we define the operational semantics of our calculus, which consists of a reduction relation on configurations, coupled with a structural equivalence.

A configuration is a pair C = < P , H > of a process P and a Q-set H, possibly restricted with respect to service and session names, or a parallel composition C C of configurations. In a configuration of the form (νs) < P , H >, all occurrences of s[p] in P and H and of s in H are bound. By abuse of notation we will often write P instead of < P , / 0 >.

5

P | 0 ≡ P P | Q ≡ Q | P (P | Q) | R ≡ P | (Q | R) (νr)P | Q ≡ (νr)(P | Q)
(νrr )P ≡ (νr r)P (νr)0 ≡ 0 D 0 ≡ 0 D (νr)P ≡ (νr) D P Let qn(H) stand for the queue names of H. Then the structural equivalence ≡ for processes, queues and configurations is given in Table 4, where assuming Barendregt convention no bound name can occur free or in two different bindings. The rules for processes are standard [START_REF] Milner | Communicating and Mobile Systems: the Pi-Calculus[END_REF]. Among the rules for queues, we have one for commuting independent messages and another one for splitting a message for multiple recipients. Modulo ≡ each configuration has the form (ν r) < P , H >, where (ν r)C stands for (νr 1 )

( D P) | Q ≡ D (P | Q) D ( D P) ≡ D ( D P) h • (p, Π, ϑ ) • (p , Π , ϑ ) • h ≡ h • (p , Π , ϑ ) • (p, Π, ϑ ) • h if Π ∩ Π = / 0 or p = p h • (p, Π, ϑ ) • h ≡ h • (p, Π , ϑ ) • (p, Π , ϑ ) • h if Π = Π ∪ Π and Π ∩ Π = / 0 h ≡ h ⇒ H ∪ {s : h} ≡ H ∪ {s : h } P ≡ Q and H ≡ K ⇒ < P , H > ≡ < Q , K > C ≡ C ⇒ (νr)C ≡ (νr)C (ν r) < P , H > (ν r ) < Q , K > ≡ (ν r r ) < P | Q , H ∪ K > if qn(H) ∩ qn(K) = / 0 (
•••(νr k )C if r = r 1 •••r k .
In a configuration (νa )C, we assume that α-conversion on the name a preserves the level .

The transitions for configurations have the form C -→ C . They are derived using the reduction rules in Table 5. Let us briefly comment on these rules.

Rule [Link] describes the initiation of a new session among n processes, corresponding to an activation of the service a of arity n. After the connection, the participants share a private session name s and the corresponding queue, initialised to s : ε. In each participant P p , the channel variable α p is replaced by the channel with role s [p].

The output rules [Send], [DelSend] and [Label] push values, channels and labels, respectively, into the queue s : h. In rule [Send], e ↓ v denotes the evaluation of the expression e to the value v , where if v is a basic value, is the join of the security levels of the variables and values occurring in e, while if v is a service name, is simply the level associated with the service. The superscript on the output sign indicates that v can be declassified to level when received by an input process s[q]? (p, x ).P. This is why the value needs to be recorded with both levels in the queue. Recall that in case v is a service name, then = (services cannot be declassified).

The rules [Rec], [DelRec] and [Branch] perform the corresponding complementary operations. Rule [ScopC] is a standard contextual rule. In this rule, Barendregt convention ensures that the names in s are disjoint from those in r and do not appear in C . We will often omit the level on the I/O operators s[p]! Π, e .P and s[q]? (p, x ).P when = , using the simpler notation s[p]! Π, e .P and s[q]?(p, x ).P.

As usual, we use -→ * for the reflexive and transitive closure of -→.

Semantics of the Client, Seller, Bank example

We illustrate the use of our reduction rules on the introductory example of Section 2. We start by rewriting in Table 6 the various components equipped with all the required security levels. Then the global process has the reductions shown in Table 7, where the continuation processes P C , P S , P B are given by:

P C = s a [1]& ⊥ (2, {ok : s a [1]? ⊥ (2, date ⊥ ).0, ko : 0}) P S = s b [2]& ⊥ (1, {ok : η ⊕ ⊥ 1, ok .η! ⊥ 1, Date ⊥ .0, ko : η ⊕ ⊥ 1, ko .0}) a [1](α 1 ).P 1 | ... | a [n](α n ).P n | ā [n] -→ (νs) < P 1 {s[1]/α 1 } | ... | P n {s[n]/α n } , s : ε > [Link] < s[p]! Π, e .P , s : h >-→< P , s : h • (p, Π, v ↓ ) > (e↓v ) [Send] < s[q]? (p, x ).P , s : (p, q, v ↓ ) • h > -→< P{v /x } , s : h > [Rec] < s[p]! q, s [p ] .P , s : h >-→< P , s : h • (p, q, s [p ] ) > [DelSend]
< s[q]? ((p, α)).P , s :

(p, q, s [p ] ) • h >-→< P{s [p ]/α} , s : h > [DelRec] < s[p] ⊕ Π, λ .P , s : h >-→< P , s : h • (p, Π, λ ) > [Label] < s[q]& (p, {λ i : P i } i∈I ) , s : (p, q, λ i 0 ) • h >-→< P i 0 , s : h > (i 0 ∈ I) [Branch] e P Q -→ P (e ↓ ) e P Q -→ Q (e ↓ ) [If-T, If-F] X(x , α) = P (X e, s[p] | Q) -→ X(x , α) = P (P{v /x }{s[p]/α} | Q) (e ↓ v ) [Def] < P , H >-→ (ν s) < P , H > ⇒ < D P , H >-→ (ν s) < D P , H > [Defin] C -→ (ν s)C ⇒ (ν r)(C C ) -→ (ν r)(ν s)(C C ) [ScopC]

Information Flow Security in Sessions

Let us turn now to the main concern of this work, namely that of ensuring secure information flow [START_REF] Denning | Cryptography and Data Security[END_REF] within sessions. We shall be interested in the classical property of noninterference (NI) [START_REF] Goguen | Security Policies and Security Models[END_REF], combined with a limited form of declassification [START_REF] Almeida Matos | On Declassification and the Non-Disclosure Policy[END_REF][START_REF] Sabelfeld | Dimensions and Principles of Declassification[END_REF], which is assumed to only take place during the transmission of a basic value. The property of NI requires that there is no dependency or information flow from objects of a given level to objects of lower or incomparable level [START_REF] Volpano | A Sound Type System for Secure Flow Analysis[END_REF][START_REF] Smith | Secure Information Flow in a Multi-threaded Imperative Language[END_REF][START_REF] Sabelfeld | Language-Based Information-Flow Security[END_REF]. Such an information flow is considered insecure since by observing the latter objects one could potentially reconstruct information about the former. To set the stage for our information flow analysis, the first questions to ask are:

1. Which objects of the calculus should carry security levels? 2. Which information leaks can occur and how can they be detected?

As concerns objects, we shall see that besides basic values, also labels, delegated channels and services need security levels. Since this question requires some discussion, which is best understood through examples, we defer it to the next section, just assuming here as a fact that queue messages have the form (p, Π, ϑ ), where ϑ may be of the form v ↓ , λ or s [p] . We shall focus here on the observation model, which will be based on a notion of bisimulation as is now standard for concurrent processes [START_REF] Smith | Secure Information Flow in a Multi-threaded Imperative Language[END_REF][START_REF] Sabelfeld | Probabilistic Noninterference for Multi-threaded Programs[END_REF].

We are looking for a security property which is persistent in the sense of [START_REF] Bossi | Verifying persistent security properties[END_REF], namely which holds in any reachable state of a process, assuming the process may be restarted with fresh Q-sets at each step. This means that we view processes as evolving in a dynamic and potentially hostile environment, where at each step an attacker may change the high context by adding or subtracting messages, or changing their content.

Before formally introducing the security property, let us illustrate by a couple of examples the kinds of insecure flow that may arise in our calculus. Essentially, we have an insecure information flow -or information leak -when a communication action of level depends on an input action of level ≤ .

I = ā⊥ [2] | b⊥ [2] C = a ⊥ [1](α 1 ).α 1 ! ⊥ 2, Title ⊥ .α 1 ! ⊥ 2, . α 1 & ⊥ (2, {ok : α 1 ? ⊥ (2, date ⊥ ).0, ko : 0}) S = a ⊥ [2](α 2 ).α 2 ? ⊥ (1, x ⊥ ).b ⊥ [2](β 2 ).β 2 ! ⊥ 1, α 2 .β 2 ? ⊥ ((1, η)). β 2 & ⊥ (1, {ok : η ⊕ ⊥ 1, ok .η! ⊥ 1, Date ⊥ .0, ko : η ⊕ ⊥ 1, ko .0}) B = b ⊥ [1](β 1 ).β 1 ? ⊥ ((2, ζ )).ζ ? (2, cc ⊥ ).β 1 ! ⊥ 2, ζ . valid(cc ⊥ ) β 1 ⊕ ⊥ 2, ok .0 β 1 ⊕ ⊥ 2, ko .0
I | C | S | B -→ (νs a )(< b⊥ [2] | s a [1]! ⊥ 2, Title ⊥ . • • • | s a [2]? ⊥ (1, x ⊥ ). • • • | b ⊥ [1](β 1 ). ••• , {s a : ε} >) -→ (νs a )(< b⊥ [2] | s a [1]! ⊥ 2, . • • • | s a [2]? ⊥ (1, x ⊥ ). • • • | b ⊥ [1](β 1 ). ••• , {s a : (1, 2, Title ⊥↓⊥ )} >) -→ (νs a )(< b⊥ [2] | s a [1]! ⊥ 2, . • • • | b ⊥ [2](β 2 ). • • • | b ⊥ [1](β 1 ). ••• , {s a : ε} >) -→ (νs a )(νs b )(< s a [1]! ⊥ 2, . • • • | s b [2]! ⊥ 1, s a [2] . • • • | s b [1]? ⊥ ((2, ζ )). ••• , {s a : ε, s b : ε} >) -→ (νs a )(νs b )(< s a [1]! ⊥ 2, . • • • | s b [2]? ⊥ ((1, η)). • • • | s b [1]? ⊥ ((2, ζ )). ••• , {s a : ε, s b : (2, 1, s a [2] ⊥ )} >) -→ (νs a )(νs b )(< s a [1]! ⊥ 2, .P C | s b [2]? ⊥ ((1, η)).P S | s a [2]? (2, cc ⊥ ).P B , {s a : ε, s b : ε} >) -→ (νs a )(νs b )(< P C | s b [2]? ⊥ ((1, η)).P S | s a [2]? (1, cc ⊥ ).P B , {s a : (1, 2, ↓⊥ ), s b : ε} >)
Table 7: Some reductions of the C, S, B example.

A typical information leak occurs when a low action is guarded by a high input, as in the following process P, where s is some previously opened session with three participants:

( * ) P = s[1]?(2, x ).s[1]! 3, e .0
where e↓v ⊥

In process P, participant 1 waits for a high message from participant 2, and then sends a low message to participant 3. This process is insecure because the low output is guarded by a high input whose occurrence depends on whether or not a matching message is offered by the high environment, which is something we do not control. Since input is a blocking operator, the low output will be able to occur in the first case but not in the latter, and the observer will conclude that the low output depends on the high input. Note that in process P the value v ⊥ of the expression e cannot depend on the value received for x , since in this case e should contain x and therefore its value would have level 2 . Hence the leak in P is only due to the presence or absence of a high message in the environment, and not on its value.

Another typical leak occurs when a high input guards a conditional which tests the received value in order to choose between two different low behaviours. Consider the following process:

( * * ) Q = s[2]! 1, .0 | s[1]?(2, x ). x s[1]! 3, ⊥ .0 s[1]! 3, ⊥ .0
Again, session s has three participants. Here participant 1 receives a message from participant 2, and depending on its value sends two different low values to participant 3. This process is insecure because the value of the low message sent by participant 1 to participant 3 depends on the value of the high message received by participant 1 from participant 2.

Here the leak is caused by the value of the high message rather than by its presence or absence.

In fact, Example ( * * ) is not completely correct, since in our persistent notion of security we assume that the attacker can add or withdraw high messages at each step. Hence, after participant 2 has sent the message to participant 1, this message could disappear again from the queue, in which case participant 1 would be blocked just like participant 1 in Example ( * ). However, Example ( * * ) can be easily adapted by rendering both components of process Q recursive, so that the high message is continuously offered by participant 2 and hence the high input of participant 1 is indeed guaranteed to occur (Example 6.4 is the recursive version of this example).

Let us turn now to the definition of security. Security is a behavioural property, based on a notion of observation of processes. In our calculus, what is observable of processes is the way they transform the Q-sets at each step. Moreover, for defining security one uses a set of observers, one for each downward-closed set of security levels L (the intuition being that an observer who can see messages of level should also be able to see all messages of level lower than ). For every L , the L -observer is only able to see Q-set messages whose level belongs to L (in case of a declassified value v ↓ , the observed level is the lowest one). Let us call these messages L -messages, and the complementary ones L -messages. Hence, two Q-sets containing the same L -messages will be indistinguishable for the L -observer. This will be formalised by a notion of L -equality = L on Q-sets. Based on = L , a notion of L -bisimulation L on processes will then formalise indistinguishability of processes by the L -observer: two processes will be L -bisimilar if they transform L -equal Q-sets into L -equal Q-sets. Then, a process will be secure for the L -observer if it is L -bisimilar to itself when run with L -equal Q-sets, namely if it preserves at each step the L -equality of Q-sets. Intuitively, this means that the process cannot exhibit different L -behaviours when fed with equal L -messages but different L -messages (in fact, as we shall see the situation is slightly more complex since Q-sets are not simply multisets of messages, but they have some structure). Finally, a process is secure if it is secure for every L -observer.

In the following, we shall always use L to denote a downward-closed set of levels of S . Formally, a queue s : h is L -observable if it contains some L -message, that is, some message with level in L . Then two Q-sets are L -equal if their L -observable queues have the same names and contain the same L -messages. This equality is based on the following L -projection operation on Q-sets, which discards all messages whose level is not in L . Definition 5.1. Let the functions lev ↑ and lev ↓ be defined by:

lev ↑ (v ↓ ) = lev ↓ (v ↓ ) = lev ↑ (s[p] ) = lev ↑ (λ ) = = lev ↓ (s[p] ) = lev ↓ (λ ).
Definition 5.2. The projection operation ⇓ L is defined inductively on messages, queues and Q-sets as follows:

(p, Π, ϑ ) ⇓ L = (p, Π, ϑ ) if lev ↓ (ϑ ) ∈ L , ε otherwise. ε ⇓ L = ε (m • h) ⇓ L = m ⇓ L • h ⇓ L / 0 ⇓ L = / 0 (H ∪ {s : h}) ⇓ L = H ⇓ L ∪ {s : h ⇓ L } if h ⇓ L = ε, H ⇓ L otherwise.
Notice that the projection operation ⇓ L discards a message (p, Π, v ↓ ) only if ∈ L . This implies that the message containing the (declassified to ⊥) in the C, S, B example is present in all projections.

Definition 5.3 (L -Equality of Q-sets).

Two Q-sets H and K are L -equal, written

H = L K, if H ⇓ L = K ⇓ L .
When L = {⊥}, we shall write = ⊥ instead of = {⊥} (and similarly for ⊥-observer, ⊥-equality, ⊥-security).

We proceed now to introduce our notion of L -bisimulation. The idea is to test processes by running them in conjunction with L -equal Q-sets. However, when combining processes with Q-sets we cannot allow arbitrary queues, otherwise we could rule out processes which are intuitively secure. Indeed, what could be safer than a process which just wants to write a bottom value in a queue or read a bottom value from a queue? However, even these simple processes turn out to be insecure without conditions on Q-sets.

For example, the process P = s[1]! 2, ⊥ .0 does not react in the same way when combined with the two Q-sets {s : ε} = ⊥ / 0. Indeed, while P reduces when combined with {s : ε}, it is stuck when combined with / 0. Formally:

< P , {s : ε} >-→< 0 , {s : (1, 2, ⊥ )} > <P , / 0 > -→
Here the ⊥-observer would detect an insecurity by looking at the resulting Q-sets {s : (1, 2, ⊥ )} = ⊥ / 0. To get around this problem, we require that the Q-sets contain enough queues to enable all outputs of the process to reduce. For this it suffices that in a configuration < P , H >, every session name that occurs free in P has a corresponding queue in H. Let fsn(P) denote the set of free session names in P.

Definition 5.4. A configuration P, H is saturated if all free session names in P have corresponding queues in H, i.e. s ∈ fsn(P) implies s ∈ qn(H).

It is easy to check that saturation is preserved by reduction, since only rule [Link] creates new sessions, always together with the corresponding queues. In particular, starting from a closed user process and the empty Q-set, we always obtain saturated configurations. This is formally established by the following definitions and lemma.

Definition 5.5 (Initial configurations).

A configuration P, H is initial if P is a closed user process and H = / 0.

Definition 5.6 (Reachable configurations).

A configuration C is reachable if there is an initial configuration C 0 such that C 0 -→ * C.

Lemma 1. A reachable configuration is saturated.

A dual phenomenon occurs with inputs. Consider the process

Q = s[2]?(1, x ⊥ ).0 with the Q-sets H 1 = ⊥ H 2 :
H 1 = {s : (1, 2, ⊥ )}, H 2 = {s : (1, 2, ) • (1, 2, ⊥ )} Here we have < Q , H 1 >-→< 0 , {s : ε} >, while < Q , H 2 > -→.
Again, the ⊥-observer would detect a leak since {s : ε} = ⊥ H 2 . What happens here is that the top level message in H 2 is transparent for the ⊥-equality, but it prevents the process from reading the subsequent bottom level message. Note that the problem comes from the fact that both messages have the same receiver and the same sender, since if instead of H 2 we took

H 3 = {s : (3, 2, ) • (1, 2, ⊥ )}, then we would have a matching transition < Q , H 3 >-→< 0 , {s : (3, 2,
)} >, thanks to the structural equivalence on queues given in Table 4.

Our way out of this problem is to ask that queues are monotone, namely that the security levels of messages with the same sender and common receivers can only stay equal or increase along a queue. Intuitively, this means that an attacker can only experiment on a process by providing or not high messages, as well as changing their content, but cannot affect the availability of low messages. In this way we allow the Q-sets H 1 and H 3 in the above example, but forbid H 2 . More formally: Definition 5.7. A queue h is monotone if lev ↓ (ϑ 1 ) ≤ lev ↓ (ϑ 2 ) whenever the message (p, Π 1 , ϑ 1 ) precedes the message (p, Π 2 , ϑ 2 ) in h and

Π 1 ∩ Π 2 = / 0. A Q-set is monotone if it contains only monotone queues.
Unlike saturation, monotonicity is not preserved by reduction, since for example

< s[1]! 2, .s[1]! 2, ⊥ .0 , {s : ε} >-→ * < 0 , {s : (1, 2, ) • (1, 2, ⊥ )} >
This could not be avoided by starting from initial configurations only, since the above process occurs as a subprocess in a configuration that is reachable from the initial configuration:

< ā⊥ [2] | a ⊥ [1](α).α! 2, .α! 2, ⊥ .0 | a ⊥ [2](β ).β ?(1, x ).β ?(1, y ⊥ ).0 , / 0 >
Notice that all the presented processes are typable in standard session type systems, for example in that of [START_REF] Bettini | Global Progress in Dynamically Interleaved Multiparty Sessions[END_REF]. All these processes will also be typable in the type system we will define in Section 7, except for a ⊥ [2](β ).β ?(1, x ).β ?(1, y ⊥ ).0, since a high input will not be allowed to guard a low action. In particular, the process s

[1]! 2, .s[1]! 2,
⊥ .0 will be typable, in spite of the fact that it generates a non monotone queue. In Theorem 14 we will show that our type system assures monotonicity of Q-sets that are generated by well-typed initial configurations.

We are now ready for defining our bisimulation. A relation R on processes is a L -bisimulation if, whenever two related processes are coupled with L -equal monotone Q-sets yielding saturated configurations, then the reduction relation preserves both the relation R on processes and the L -equality of Q-sets: Definition 5.8 (L -Bisimulation on processes).

A symmetric relation R ⊆ (Pr × Pr) is a L -bisimulation if P 1 R P 2 implies, for any pair of monotone Q-sets H 1 and H 2 such that H 1 = L H 2 and each < P i , H i > is saturated:

If < P 1 , H 1 > -→ (ν r) < P 1 , H 1 >, then either H 1 = L H 2 and P 1 R P 2 , or there exist P 2 , H 2 such that < P 2 , H 2 >-→ * (ν r) < P 2 , H 2 > , where H 1 = L H 2 and P 1 R P 2 .
Processes P 1 , P 2 are L -bisimilar, P 1 L P 2 , if P 1 R P 2 for some L -bisimulation R.

Note that r may either be the empty string or a single name, since it appears after a one-step transition. If it is a name, it may either be a service name a (extrusion of a private service) or a fresh session name s (opening of a new session). In the latter case, s cannot occur in P 2 and H 2 by Barendregt convention.

Intuitively, a transition that adds or removes a message with level in L must be simulated in one or more steps, producing the same effect on the Q-set, whereas a transition that only affects messages with level not in L may be simulated by inaction.

The notions of L -security and security are now defined in the standard way: Definition 5.9 (L -Security). A process P is L -secure if P L P.

Notice that each process is S -secure, since for L = S the L -equality of saturated Q-sets reduces to syntactic identity, and hence S reduces to ordinary bisimilarity, which is a reflexive relation.

The soundness of our definition of L -security comes from the observation that for an arbitrary process P the monotone Q-set H P = {s : ε | s ∈ fsn(P)} gives a saturated configuration < P , H P >. Definition 5.10 (Security). A process P is secure if it is L -secure for every L .

The necessity of considering all down-closed sets of levels included in S is justified by the following example. Let S = {⊥, , } where ⊥ ≤ ≤ and

P = s[2]?(1, x ).s[2]! 1, .0
The process P is ⊥-secure (and S -secure), but it is not {⊥, }-secure, as can be seen by taking the two {⊥, }-equal

Q-sets H 1 = {s : (1, 2,
)} and H 2 = {s : ε}.

Examples of Information Flow Security in Sessions

In this section we illustrate the various kinds of information flow that can occur in our calculus, by means of simple examples. Since we aim at justifying the introduction of security levels in the syntax, other than on basic values and participants, we initially omit levels on all other objects. Then, as we go along examining examples, we will find out that other objects need to carry security levels. These levels will be used in the type system to reject processes that are innocuous in isolation but may be dangerous in some contexts. For the sake of simplicity, we use here just two security levels ⊥ and (also called low and high).

Insecurity of high input followed by low action

Consider the process P (which coincides with that of Example (*) at page 8, assuming e = ⊥ ), together with the Q-sets H 1 and H 2 , where H 1 = ⊥ H 2 :

P = s[1]?(2, x ).s[1]! 3, ⊥ .0, H 1 = {s : (2, 1, )} H 2 = {s : ε} Here we have < P , H 1 >-→< s[1]! 3, ⊥ .0 , {s : ε} >=< P 1 , H 1 >, while < P , H 2 > -→. Since H 1 = {s : ε} = H 2 , we can proceed with P 1 = s[1]! 3,
⊥ .0 and P 2 = P. Take now

K 1 = K 2 = {s : ε}. Then < P 1 , K 1 >-→< 0 , {s : (1, 3, ⊥ )} >, while < P 2 , K 2 > -→. Since {s : (1, 3, ⊥ )} = ⊥ {s : ε} = K 2 , P is not ⊥-secure.
With a similar argument we could show that the process s[1]?(2, x ).s [START_REF] Almeida Matos | On Declassification and the Non-Disclosure Policy[END_REF]?(3, y ⊥ ).0 is not ⊥-secure.

Security of declassified high-to-low input followed by low action

Consider the following process Q, which differs from process P in Example 6.1 in that the input action declassifies the received value from high to low:

Q = s[1]? (2, x ⊥ ).s[1]! 3, ⊥ .0, Let H 1 = {s : (2, 1, v ↓⊥ )}.
Note that H 1 = ⊥ {s : ε}. Indeed, for H 2 to be such that H 1 = ⊥ H 2 , it must be the case that

H 2 ≡ {s : (2, 1, v ↓⊥ ) • h} ∪ H, where {s : h} ∪ H = ⊥ {s : ε}. Then, it is easy to see that < Q , H 1 >-→< Q , H 1 > implies < Q , H 2 >-→< Q , H 2 >, with H 1 = ⊥ H 2 .
This is enough to conclude that Q is secure.

Interestingly, an insecure component may be "sanitised" by its context, so that the insecurity is not detectable in the overall process. Clearly, in case the insecure component is wrapped into a deadlocked context such as (νb)b [START_REF] Almeida Matos | On Declassification and the Non-Disclosure Policy[END_REF](β 1 ).[ ], the insecurity disappears simply because the component is not executed. However, the curing context could also be a partner of the component, as shown by the next example.

Insecurity sanitised by recursion and parallel context

Let us consider the unfolded recursive version R of the process P of Example 6.1, in parallel with a process R that continuously emits a matching message.

R = X(x ⊥ , α) = α?(2, y ).α! 3, x ⊥ .X(x ⊥ , α) s[1]?(2, y ).s[1]! 3, ⊥ .X ⊥ , s[1] R = Y (z , β ) = β ! 1, z .Y (z , β ) s[2]! 1, .Y , s[2]
Take the two ⊥-equal Q-sets

H 1 = {s : (2, 1, )} = ⊥ {s : ε} = H 2 . Then the move < R | R , H 1 >-→< R | R , {s : ε} > where R = X(x ⊥ , α) = α?(2, y ).α! 3, x ⊥ .X(x ⊥ , α) s[1]! 3, ⊥ .X ⊥ , s[1] can be simulated by < R | R , H 2 >-→< R | R , {s : (2, 1, )} >-→ * < R | R , {s : ε} >
where R is the folded version of R. Note that it would make no difference if we replaced

H 1 = {s : (2, 1, )} with H 3 = {s : (2, 1,
)}.

Insecurity of high conditional with different low branches

Consider the following process Q, which is the recursive unfolded version of process Q in Example (**) of page 8:

Q = Q 1 | Q 2 Q 1 = X(x ⊥ , α) = Q Q { ⊥ /x ⊥ }{s[1]/α} Q 2 = Y (y , β ) = β ! 1, y .Y (y , β ) s[2]! 1, .Y , s[2]
where The next series of examples justifies the introduction of security levels on services, labels and delegated channels, by showing that they are necessary in the type system to rule out some indirect information flows.

Q = α?(2, z ). z α! 3, x ⊥ .X x ⊥ , α α! 3, x ⊥ .X x ⊥ , α . Take the Q-sets H 1 = {s : (2, 1, )} and H 2 = {s : ε}. We have H 1 = ⊥ H 2 . Now, if < Q , H 1 > starts by reading the message (2, 1, ) from H 1 , then < Q , H

Need for levels on services

Consider the following process:

s[2]?(1, x ). b[2] | b[1](β 1 ).β 1 ! 2, ⊥ .0 | b[2](β 2 ).β 2 ?(1, y ⊥ ).0
This process is insecure since if there is no -message in the Q-set the process is blocked, hence it has a null ⊥behaviour, while if there is a -message in the Q-set the process subsequently exhibits a ⊥-action. To be able to rule out this kind of leak in our type system, we annotate service names with security levels which in a typable process will act as a lower bound for all the actions executed by the service. Then service b will have to be of level since it is guarded by an input of a -value, and hence it will not be allowed to perform the exchange of the value ⊥ . The communication of a service name only makes sense if the name is restricted, and it is used for allowing a set of participants to start a session on that private name. The above example shows that the service name must have the same security level in the initiator and in all participants, otherwise the session could not start. This is why we do not allow service declassification.

Need for levels on selection and branching

Consider the process:

s[2]?(1, x ).s[2] ⊕ 3, λ .0 | s[3]&(2, {λ : s[3]! 4, ⊥ .0}) | s[4]?(3, y ⊥ ).0
As in the previous example, this process is insecure because if there is no -message in the Q-set the process is blocked, while if there is a -message in the Q-set the process subsequently exhibits a ⊥-action. To prevent this kind of leak, the selection and branching operators will be annotated with a security level which acts as a lower bound for all actions executed in the various branches.

Need for levels on delegated channels

Consider the following process:

s[2]?(1, x ).s[2]! 3, s [1] .0 | s[3]?((2, η)).η! 2, ⊥ .0 | s [2]?(1, y ⊥ ).0
This process is insecure since if there is no -message in the Q-set the process is blocked, while if there is a -message in the Q-set the process subsequently exhibits a ⊥-action. This shows that delegation send and receive should also carry a level, which will act as a lower bound for all actions executed in the receiving participant after the delegation.

Need for levels in queue messages

So far, we have identified which objects of the calculus need security levels, namely: basic values, service names, and the operators of selection, branching and delegation. Let us now discuss how levels are recorded into queue messages.

Values are recorded in the queues with both their original level and their declassified level. The reason for recording also the original level is access control: the semantics does not allow a low input process to fetch a high value declassified to low. More formally, a value v ↓⊥ in the queue can only be read by a process s[q]? (p, x ⊥ ).P. Concerning service names a , the level guarantees that the session initiator and all the participants get started in a context of level ≤ (see Example 6.5). Once the session is established, the name a disappears and it is its global type (cf next section) that will ensure that all participants perform actions of levels greater than or equal to . As for the operators of branching/selection and delegation, they disappear after the reduction and their level is recorded respectively into labels and delegated channels within queue messages. This is essential to ensure that the sender and receiver have matching security levels, since in this case the communication is asynchronous and occurs in two steps. In conclusion, queue messages need to be of the form (p, Π, ϑ ), where ϑ is of one of v ↓ , s[p] , or λ .

To conclude this section, note that while

P 1 = s[1]?(2, x ).s[1]?(2, y ⊥ ).0 and P 2 = s[1]?(2, x ).s[1]! 2, ⊥ .0 are insecure, their dual processes Q 1 = s[2]! 1, .s[2]! 1, ⊥ .0 and Q 2 = s[2]! 1,
.s [START_REF] Bettini | Global Progress in Dynamically Interleaved Multiparty Sessions[END_REF]?(1, ⊥ ).0 are secure. Intuitively, this is because output is not blocking.

Finally, we let the reader verify that the process of the C, S, B example in Section 4.1 is secure.

Type system

In this section we present our type system for secure sessions and state its properties. Just like process syntax, types will contain security levels.

Safety Global Types

A safety global type is a pair L, G , decorated with a security level , describing a service where:

• L : {1,...,n} → S is a safety mapping from participants to security levels;

• G is a global type, describing the whole conversation scenario of an n-ary service;

• is the meet of all levels appearing in G, denoted by M(G).

The grammar of global types is:

Global G ::= p → Π : U .G Exchange U ::= S ↓ | T | L, G | p → Π : {λ i : G i } i∈I Sorts S ::= | ... | p δ .G | µt.G | t |
The type p → Π : U .G says that participant p multicasts a message of type U to all participants in Π and then the interactions described in G take place.

Exchange types U may be sort types S ↓ for values (base types decorated with a declassification ↓ ), session types T for channels (defined below), or safety global types for services. If U = T , then Π is a singleton. We use S as short for S ↓ , called a trivial declassification.

Type p → Π : {λ i : G i } i∈I , where ≤ i∈I M(G i ), says that participant p multicasts one of the labels λ i to the participants in Π. If λ j is sent, interactions described in G j take place. Type p δ .G says that the role of p is delegated to another participant; this construct does not appear in the original global types of [START_REF] Honda | Multiparty Asynchronous Session Types[END_REF]. It is needed here to "mark" the delegated part of the type, which is discharged when calculating its join (see below).

Type µt.G is a recursive type, where the type variable t is guarded in the standard way. In the grammar of exchange types, we suppose that G does not contain free type variables. Type represents the termination of a session. The meet of global types is needed for information flow control, and it takes into account the lower level of declassified exchanged values, and the level of all other constructs, including delegation. More precisely the meet of global types is defined as follows, using the meet of session types given in next section.

M(p → Π : S ↓ .G) = M(G) M(p → Π : L, G .G) = M(G) M(p → q : T .G) = M(T ) M(G) M(p → Π : {λ i : G i } i∈I ) = M(p δ .G) = M(G) M(t) = M(µt.G) = M(G) M( ) =
The condition ≤ i∈I M(G i ) (see above) justifies the absence of M(G i ) in the definition of M(G) for the case of label exchanges.

Session Types

While global types represent the whole session protocol, session types correspond to the communication actions, representing each participant's contribution to the session.

Session

T ::

= ! Π, S ↓ ;T send | ! Π, L, G ;T servsend | ! q, T ;T delsend | ⊕ Π, {λ i : T i } i∈I selection | µt.T recursive | δ ; T delegation | ?(p, S ↓ );T receive | ?(Π, L, G );T servreceive | ? (p, T );T delreceive | & (p, {λ i : T i } i∈I ) branching | t variable | end
The send and servsend types ( ! Π, S ↓ ; T and ! Π, L, G ;T ) express the sending to all participants in Π of a value of type S of level , declassified to and of a service of type L, G of level respectively, followed by the communications described in T . The two different types for sending are necessary since services cannot be declassified. The delsend type ! q, T ; T says that a channel of type T is sent to participant q, and then the protocol specified by T takes place.

The selection type ⊕ Π, {λ i : T i } i∈I , represents the transmission to all participants in Π of a label λ j in {λ i | i ∈ I}, followed by the communications described in T j . The delegation type δ ; T , says that the communications described in T will be delegated to another agent. The receive, servreceive, delreceive and branching types are dual to the send, servsend delsend, and selection ones. In all cases, the need for the security level is motivated by one of the examples in Section 6. Recursive types are considered modulo fold/unfold. We say that ! Π, S ↓ , ! Π, L, G , ! q, T , ?(p, S ↓ ), ?(p, L, G ), ? (p, T ) are type prefixes and we use τ to range over them.

A type prefix τ occurs in a session type T if one of the following conditions holds:

• T = τ; T ; • T = τ ; T or T = µt.T or T = δ ; T and τ occurs in T ; • T = ⊕ Π, {λ i : T i } i∈I or T = & (p, {λ i : T i } i∈I )
T i } i∈I ) = M(& (p, {λ i : T i } i∈I )) = M(t) = M(µt.T ) = M(T ) M( δ ; T ) = M(T ) M( ) =
The type system will assure some relations between levels appearing in types and meets of continuations that justify the definition of M(T ) in the cases of inputs, output of a channel, selection and branching, see Proposition 2.

Projections

The relation between global types and session types is formalised by the notion of projection [START_REF] Honda | Multiparty Asynchronous Session Types[END_REF]. The projection of G onto q, denoted (G q), gives participant q's view of the protocol described by G.

Definition 7.1. The projection of G onto q (written G q) is defined by induction on G:

(p → Π : S ↓ .G ) q =      ! Π, S ↓ ; (G q) if q = p, ?(p, S ↓ ); (G q) if q ∈ Π, G q otherwise. (p → Π : L, G .G ) q =      ! Π, L, G ; (G q) if q = p, ?(p, L, G ); (G q) if q ∈ Π, G q otherwise. (p → p : T .G ) q =      ! p , T ; (G q) if q = p, ? (p, T ); (G q) if q = p , G q otherwise where = M(T ). (p → Π : {λ i : G i } i∈I ) q =          ⊕ (Π, {λ i : G i q} i∈I ) if q = p & (p, {λ i : G i q} i∈I ) if q ∈ Π G 1 q if q = p
, q ∈ Π and G i q = G j q for all i, j ∈ I.

p δ .G q = δ ; (G q) if q = p, G q otherwise.
(µt.G ) q = µt.(G q) if q occurs in G , otherwise.

t q = t q =
The mapping of the global type for message multicasting assures that the message has sort S and security level declassified to in both the sender and the receivers. The mapping of the global type for delegation assures that the security levels of the projections be the same and equal to the meet of the session type of the delegated channel. From Example 6.7 it is clear that we could choose for the projections also a level less than this meet, but this would render projection a relation instead of a function. The condition G i q = G j q for all i, j ∈ I assures that the projections of all the participants not involved in the branching are identical session types.

Well-formedness of safety global types

To formulate the well-formedness condition for safety global types, we define the join J(T ) of a session type T . Intuitively, while M(T ) is needed for secure information flow, J(T ) will be used for access control. Recall from Section 2 our access control policy, requiring that participants in a session only read data of level less than or equal to their own level. This motivates our (slightly non standard) definition of join: in short, J(T ) is the join of all the security levels decorating the input constructs in T (receive, servreceive, delreceive, branching) and selection:

J( ! Π, S ↓ ; T ) = J(T ) J(?(p, S ↓ ); T ) = J(T ) J( ! Π, L, G ; T ) = J(T ) J(?(p, L, G ); T ) = J(T ) J( ! q, T ; T ) = J(T ) J(? (p, T ); T ) = J(T ) J(⊕ Π, {λ i : T i } i∈I ) = i∈I J(T i ) J(& (p, {λ i : T i } i∈I )) = i∈I J(T i ) J(t) = ⊥ J(µt.T ) = J(T ) J( δ ; T ) = ⊥ J( ) = ⊥
Notice that in the definition of J(T ) we cannot omit in the case of selection, because we could have M(T ) ≤ J(T ).

For example M( ) = M(µt.t) = and J( ) = J(µt.t) = ⊥. Then, if all T i are such that M(T i ) = and J(T i ) = ⊥, we have i∈I J(T i ) = ⊥ and = i∈I M(T i ) = and thus i∈I J(T i ) = ⊥ = = i∈I J(T i ).

The condition of well-formedness for safety global types requires that the security level of the participant p is greater than or equal to the join of the p-th projection of the global type. More formally, the condition of well-formedness is the following, where dom(L) denotes the domain of L:

A safety global type L, G is well formed if for all p ∈ dom(L): L(p) ≥ J(G p).

Henceforth we shall only consider well-formed safety global types.

Typing rules

Typing expressions. The typing judgments for expressions are of the form:

Γ e : S
where Γ is the standard environment which maps variables with security levels to sort types with trivial declassification or to safety global types, service names with security levels to safety global types, and process variables to pairs of sort types with trivial declassification and session types. Formally, we define:

Γ ::= / 0 | Γ, x : S | Γ, x : L, G | Γ, a : L, G | Γ, X : S T
assuming that we can write Γ, x : S or Γ, x : L, G (respectively Γ, a : L, G ) only if there does not exist such that x (respectively a ) belongs to the domain of Γ, that is, Γ should not contain the same variable or service name with two different security levels. Similarly, when writing Γ, X : S T , we assume that X does not belong to the domain of Γ.

An environment Γ is well formed if x : S ∈ Γ, x : L, G ∈ Γ, or a : L, G ∈ Γ implies that = .
In the following we will only consider well-formed environments.

We type values by decorating their type with their security level, and names according to Γ:

Γ , : Γ, u : S u : S
We type expressions by decorating their type with the join of the security levels of the variables and values they are built from. For example a typing rule for is:

Γ e 1 :
1 Γ e 2 :

2 Γ e 1 e 2 :

1 2

Typing processes. The typing judgments for processes are of the form:

Γ P ∆
where ∆ is the process environment which associates session types with channels:

∆ ::= / 0 | ∆, c : T
We decorate the derivation symbol with the security level inferred for the process: this level is a lower bound for the actions and communications performed in the process. The set of typing rules for processes is given in Table 8.

SUBS allows the security level inferred for a process to be decreased.

INACT This rule gives security level to 0 since a terminated process cannot leak any information. The hypothesis assures that there is no further behaviour after inaction.

CONC This rule allows the parallel composition of two processes P, Q to be typed if both processes are typable and their process environments have disjoint domains. The level of the resulting process is the level of both P and Q. If P, Q should have different levels 1 , 2 we can give them the level 1 2 using rule SUBS .

IF This rule requires that the two branches P, Q of a conditional be typed with the same process environment ∆, and with the same security level . Note that the classical requirement that the security level of the tested expression be less than or equal to the security level of the branches is not needed here. This is because the process e P Q can only be executed if the expression e can be evaluated, and this is the case only if all the variables occurring in e have been instantiated by previous inputs. Since these inputs guard the conditional, the join of their levels will be less than or equal to by Rule RCV . This means that the process e P Q is typable whenever P and Q are typable with the same process environment ∆, since the levels of the branches can always be made equal using Rule SUBS . NRES This rule types the restriction of a process: the use of the restricted name a in the process P is constrained by the premise.

Γ P ∆ ≤ SUBS Γ P ∆ ∆ only INACT Γ 0 ∆ Γ P ∆ Γ Q ∆ CONC Γ P | Q ∆, ∆ Γ e : Γ P ∆ Γ Q ∆ IF Γ e P Q ∆ Γ, a : L, G P ∆ NRES Γ (
T j j ∈ I ≤ ≤ i∈I M(T i ) SEL Γ c ⊕ Π, λ j .P ∆, c : ⊕ Π, {λ i : T i } i∈I Γ P i ∆, c : T i ≤ i∈I M(T i ) BRANCH Γ c& (p, {λ i : P i } i∈I ) ∆, c : & (p, {λ i : T i } i∈I )
VAR This rule types X e, c with a level which is the meet of the security level of expression e and the security levels of the communications performed on channel c. In this way we take into account the levels of all communications which can be performed by a process bound to X, see also rule DEF .

DEF The process P is typed with the meet of the security levels associated with x and α, in agreement with rule VAR . The levels of P and Q can be unrelated, since X could not occur in Q. Clearly if X occurs in Q we get ≤ .

MINIT In this rule the standard environment must associate with the identifier u a safety global type. The premise matches the number of participants in the domain of L with the number declared by the initiator. The emptiness of the process environment in the conclusion specifies that there is no further communication behaviour after the initiator.

MACC In this rule the standard environment must also associate with u a safety global type. The premise guarantees that the type of the continuation P in the p-th participant is the p-th projection of the global type G of u. Concerning security levels, in rule MACC we check that the continuation process P conforms to the security level associated with the service name u. Note that this condition does not follow from well-formedness of environments, since the process P may participate in other sessions, but it is necessary to avoid information leaks. For example, without this condition we could type

ā [2] | a [1](α 1 ).α 1 ! 2, .0 | a [2](α 2 ).α 2 ?(1, x ). b [2] | b [1](β 1 ).c ⊥ [1](γ 1 ).γ 1 ! 2, ⊥ .0 | b [2](β 2 ).0 c⊥ [2] | c[2](γ 2 ).γ 2 ?(1, y ⊥ ).0
SEND This rule types the sending of the basic value followed by the conversation P. The first hypothesis binds expression e with type S , where is the join of all variables and values in e. The second hypothesis imposes typability of the continuation of the output with security level . The third hypothesis relates levels , and (the level to which e will be declassified), preserving the invariant that is a lower bound for all security levels of the actions in the process. Note that the hypothesis ≤ ≤ is not really constraining, since P can always be downgraded to using rule SUBS and ≤ follows from well-formedness of S ↓ .

RCV This rule is the dual of rule SEND , but it is more restrictive in that it requires the continuation P to be typable with exactly the level .

Notice for instance that we cannot type the reception of a -value followed by a ⊥-action. In particular we cannot type a process which receives a -value and then sends it declassified to ⊥. On the other hand we can type the reception of a ↓ ⊥-value followed by a ⊥-action. For instance, in our introductory example of Section 2, rule [Rcv] allows the delegation send in process B to be decorated by ⊥: this is essential for the typability of process B with the first projection of the global type of service b.

SERVSEND This rule types the sending of a service name followed by the conversation P. The first hypothesis binds expression e with type L, G , where = M(G). The second hypothesis imposes typability of the continuation of the output with security level . The third hypothesis relates levels and preserving the invariant that is a lower bound for all security levels of the actions in the process. As for rule SEND the hypothesis ≤ is not really constraining, since P can always be downgraded to using rule SUBS .

SERVRCV This rule is the dual of rule SERVSEND , but it is more restrictive in that it requires the continuation P to be typable with exactly the level (like RECV ).

DELEG This rule types a delegating process with the meet of the type of the delegated channel, provided the continuation process P is typable with a lower or equal level.

SREC This rule is the dual of the DELEG rule.

SEL This rule types a selecting process with the level associated with the selection operator, which is less than or equal to the meets of the types in the different possible continuations.

BRANCH This rule is the dual of the SEL rule.

We say that a process P is typable in Γ if Γ P ∆ holds for some , ∆.

The following relations between derived types can be easily shown by induction on type derivations.

Proposition 2. Let Γ P ∆ and c : T ∈ ∆.

• T =?(p, S ↓ ); T implies ≤ M(T ),

• T =?(p, L, G ); T implies ≤ M(T ),

• T = ! q, T ; T or T =? (p, T ); T imply = M(T ),

• T =? (p, T ); T implies ≤ M(T ),

• T = ⊕ Π, {λ i : T i } i∈I or T = & (p, {λ i : T i } i∈I ) imply ≤ i∈I M(T i ). Proposition 3. Let Γ P ∆ and c : T ∈ ∆. If τ 1 precedes τ 2 in T , where τ 1 ∈ {?(p 1 , S 1 ↓ 1 ), ?(p 1 , L 1 , G 1 ), ? (p 1 , T 1 )} and τ 2 ∈ {?(p 2 , S 2 ↓ 2 ), ?(p 2 , L 2 , G 2 ), ? (p 2 , T 2 )}, then ≤ .
By way of example, let us consider the typing of a fragment of the component S in our C, S, B example of Section 4.1. Letting:

P = β 2 & ⊥ (1, {ok : η ⊕ ⊥ 1, ok .η! ⊥ Date ⊥ , 1 .0, ko : η ⊕ ⊥ 1, ko .0})
we can derive:

⊥ P {β 2 : & ⊥ (1, { : , :
}), η : T } and hence:

⊥ β 2 ! ⊥ 1, α 2 .β 2 ? ⊥ ((1, η)).P {α 2 : δ ; T, β 2 : ! ⊥ 1, T ;? ⊥ (1, T );& ⊥ (1, { : , : })}
where

T =?(1, ↓⊥ ); T T = ⊕ ⊥ 1, { :! 1, ⊥↓⊥ ;
, : }

Typing queues and Q-sets

We type queues describing the messages they contain: message types represent the messages contained in the queues.

Message T ::= ! Π, S ↓ message value send | ! Π, L, G message service send | ! q, T message delegation | ⊕ Π, λ message selection | T; T message sequence
The message value send type ! Π, S ↓ , the message service send type ! Π, L, G and the message delegation type ! q, T express the communication to all p ∈ Π or to q of a value of type S declassified to level , of a service of type L, G , or of a channel of type T with = M(T ). The message selection type ⊕ Π, λ represents the communication to all p ∈ Π of the label λ with level and T; T represents sequencing of message types (we assume associativity for ;). For example ⊕ ⊥ {1, 3}, is the message type for the message (2, {1, 3}, ⊥ ). In order to take into account the structural congruence on queues given in Table 4, we consider message types modulo the equivalence relation ≈ induced by the rules shown in Table 9 Typing judgments for queues have the shape Γ s : h Θ where Θ is a queue environment associating session types or message types with channels:

(with ∈ {!, ! , ⊕ } and Z ∈ {S ↓ , L, G , T, λ }). Γ s : h Θ QSEL Γ s : h • (p, Π, λ ) Θ; {s[p] : ⊕ Π, λ } Γ s : h Θ Θ≈ Θ QCONG Γ s : h Θ Table 10: Typing rules for single queues. QSINIT Γ / 0 / 0 / 0 Γ Σ H Θ Γ s : h Θ QSUNION Γ Σ,s H ∪ {s : h} Θ, Θ
Θ ::= / 0 | Θ, s[p] : T | Θ, s[p] : T
The equivalence ≈ on message types can be trivially extended to queue environments:

{s[p i ] : T i | i ∈ I} ≈ {s[p i ] : T i | i ∈ I} if T i ≈ T i for all i ∈ I
Typing rules for queues are given in Table 10. The empty queue has an empty queue environment (rule QINIT ). In rules QSEND , QSERVSEND , QDELEG and QSEL , each message adds an output type to the current type of the sending channel. Rule QDELEG also adds a session type for the delegated channel. The composition ";" of queue environments is defined only if no channel has a session type in both environments. This condition is essential for channel linearity, since it assures that the same channel cannot be exchanged in more than one message at time. More precisely:

Θ; Θ = {s[p] : T; T | s[p] : T ∈ Θ and s[p] : T ∈ Θ } ∪ {s[p] : T | s[p] : T ∈ Θ and s[p] ∈ dom(Θ )} ∪ {s[p] : T | s[p] ∈ dom(Θ) and s[p] : T ∈ Θ } ∪ {s[p] : T | s[p] : T ∈ Θ ∪ Θ } if s[p] : T ∈ Θ implies s[p] ∈ dom(Θ ) and s[p] : T ∈ Θ implies s[p] ∈ dom(Θ).
Rule QCONG allows a queue to be typed with equivalent queue environments.

Example: we can derive s : (2, {1, 3}, ) {s [START_REF] Bettini | Global Progress in Dynamically Interleaved Multiparty Sessions[END_REF] : ⊕ {1, 3}, }. Typing judgments for Q-sets have the shape:

Γ Σ H Θ
where Σ is the set of session names which occur free in H.

Typing rules for Q-sets are given in Table 11. As for process environments, Σ, Σ and Θ, Θ are defined only if Σ ∩ Σ = / 0 and dom(Θ) ∩ dom(Θ ) = / 0, respectively. The empty Q-set has an empty queue environment (rule QSINIT ). Rule QSUNION types the addition of a queue to the set H by checking that a queue associated with that session name is not already present.

Typing configurations

Typing judgments for runtime configurations C have the form:

Γ Σ C < ∆ Θ >
They associate with a configuration the environments ∆ and Θ mapping channels to session and message types, respectively. We call < ∆ Θ > a configuration environment. Channel linearity is assured also by forbidding a channel to occur both in the process and in a message as delegated channel. This condition is mirrored by the following definition of well-formedness of configuration environments.

Definition 7.2. A configuration environment < ∆ Θ > is well formed if no channel with a session type in Θ occurs in ∆, i.e. if s[p] : T ∈ Θ implies s[p] ∈ dom(∆).

A configuration type is a session type, or a message type, or a message type followed by a session type:

Configuration T ::= T session | T message | T; T continuation
An example of configuration type is:

⊕ ⊥ {1, 3}, ;! {3}, ;?(3, ⊥ );
It is easy to check that for typable initial configurations the set of session names and the process and queue environments are all empty.

Since channels with roles occur both in processes and in queues, a configuration environment associates configuration types with channels.

Definition 7.3. The configuration type of a channel s[p] in a configuration environment

< ∆ Θ > (notation < ∆ Θ > (s[p]
) ) is defined by: Clearly the configuration types of all channels are defined only for well-formed configuration environments.

< ∆ Θ > (s[p]) =                T; T if s[p] : T ∈ Θ and s[p] : T ∈ ∆, T if s[p] : T ∈ Θ and s[p] ∈ dom(∆), T if s[p] : T ∈ Θ and s[p] ∈ dom(∆), T if s[p] ∈ dom(Θ) and s[p] : T ∈ ∆, if s[p] ∈ dom(Θ) ∪ dom(∆). Γ P ∆ Γ Σ H Θ < ∆ Θ > is coherent CINIT Γ Σ < P , H > < ∆ Θ > Γ Σ 1 C 1 < ∆ 1 Θ 1 > Γ Σ 2 C 2 < ∆ 2 Θ 2 > < ∆ 1 , ∆ 2 Θ 1 , Θ 2 > is coherent CPAR Γ Σ 1 ,Σ 2 C 1 C 2 < ∆ 1 , ∆ 2 Θ 1 , Θ 2 > Γ Σ C < ∆ Θ > GSRES Γ Σ\s (νs)C < ∆ \ s Θ \ s > Γ, a : L, G Σ C < ∆ Θ > GNRES Γ Σ (νa )C < ∆ Θ >
Configuration types can be projected on participants.

Definition 7.4. The projection of the configuration type T onto q , denoted by T q , is defined by:

( ! Π, S ↓ ; T ) q = !S ↓ ; T q if q ∈ Π, T q otherwise. ( ! Π, L, G ; T ) q = ! L, G ; T q if q ∈ Π, T q otherwise. ( ! p, T ; T ) q = ! T ; T q if q = p, T q otherwise. (⊕ Π, λ ; T ) q = ⊕ λ ; T q if q ∈ Π, T q otherwise.
(?(p, S ↓ ); T ) q = ?S ↓ ; T q if q = p T q otherwise. (?(p, L, G ); T ) q = ? L, G ; T q if q = p T q otherwise.

(? (p, T ); T ) q = ? T ; T q if q = p T q otherwise. (µt.T ) q = µt.(T q) if q occurs in T, otherwise.

(⊕ Π, {λ i : T i } i∈I ) q = ⊕ {λ i : T i q} i∈I if q ∈ Π, T 1 q otherwise. (& (p, {λ i : T i } i∈I )) q = & {λ i : T i q} i∈I if q = p, T 1 q otherwise. t q = t ( δ ; T ) q = T q q =
We also define a duality relation between projections of configuration types, which holds when opposite communications are offered (input/output, selection/branching). Definition 7.5. The duality relation between projections of configuration types is the minimal symmetric relation which satisfies:

t t T T =⇒ µt.T µt.T ∀i ∈ I T i T i =⇒ ⊕ {λ i : T i } i∈I & {λ i : T i } i∈I T T =⇒ !S ↓ ; T ?S ; T T T =⇒ ! L, G ; T ? L, G ; T T T =⇒ ! T ; T ? T ; T ∃i ∈ I λ = λ i & T T i =⇒ ⊕ λ ; T & {λ i : T i } i∈I
The above definitions are needed to define coherence of well-formed configuration environments. Informally, this holds when the inputs and the branchings offered by the process agree both with the outputs and the selections offered by the process and with the messages in the queues. More formally:

Definition 7.6. A well-formed configuration environment < ∆ Θ > is coherent if s[p] ∈ dom(∆) ∪ dom(Θ) and s[q] ∈ dom(∆) ∪ dom(Θ) imply < ∆ Θ > (s[p]) q < ∆ Θ > (s[q]) p.
The typing rules for configurations are given in Table 12. Rule CPAR types the parallel composition of two configurations. Rules GSRES and GNRES type restriction on session and service names respectively, where Σ \ s, ∆ \ s and Θ \ s are defined as expected:

• Σ \ s = {s | s ∈ Σ & s = s}

Properties

We are now able to state our main results, namely type preservation under reduction and the soundness of our type system for both access control and noninterference.

Our type system also preserves the fundamental properties ensured by classical session types, i.e. linearity of communications inside sessions and absence of communication mismatches. This is easy to see, once we observe that our type system projects down to the classical session type system of [START_REF] Bettini | Global Progress in Dynamically Interleaved Multiparty Sessions[END_REF] when we ignore security levels and associated type constraints. We shall therefore concentrate here on establishing the security properties.

Subject Reduction

We first state some auxiliary results that are used in the subject reduction proof. The first lemma says that reduction of configuration environments preserves coherence.

Lemma 5. If < ∆ Θ > is coherent and < ∆ Θ > ⇒ < ∆ Θ >, then < ∆ Θ > is coherent.
Proof. Easy by induction on the definition of ⇒ (Definition 7.7).

The next three lemmas are inversion lemmas for processes, Q-sets and configurations, which immediately follow from our typing rules.

Lemma 6 (Inversion Lemma for Processes). Lemma 7 (Inversion Lemma for Queues and Q-sets).

1. If Γ 0 ∆, then ∆ only. 2. If Γ P | Q ∆, then ∆ = ∆ 1 , ∆ 2 and Γ P ∆ 1 and Γ Q ∆ 2 .
1. If Γ s : ε Θ, then Θ = / 0. 2. If Γ s : h • (p, Π, v ↓ ) Θ, then Γ s : h Θ and
L, G . 3. If Γ s : h • (p, q, s [p ]) Θ, then Θ ≈ Θ , s [p ] : T ; {s[p] : ! q, T } and Γ s : h Θ . 4. If Γ s : h • (p, Π, λ ) Θ, then Θ ≈ Θ ; {s[p] : ⊕ Π, λ } and Γ s : h Θ . 5. If Γ Σ / 0 Θ, then Σ = Θ = / 0. 6. If Γ Σ H ∪ {s : h} Θ, then Σ = Σ , s and Θ = Θ 1 , Θ 2 and Γ Σ H Θ 1 , Γ s : h Θ 2 .
Lemma 8 (Inversion Lemma for Configurations).

1. If Γ Σ < P , H > < ∆ Θ >, then Γ P ∆ and Γ Σ H Θ and < ∆ Θ > is coherent.
From (4) by Lemma 6 [START_REF] Boudol | Access Control and Declassification[END_REF] we get Γ = Γ , a : L, G and ∆ = / 0. Since Γ is a well formed environment, this implies = . From (3) by Lemma 6(8) we get

Γ P i ∆ i , α i : G i (1 ≤ i ≤ n)
which implies by Lemma 11(3)

Γ P i {s[i]/α i } ∆ i , s[i] : G i (1 ≤ i ≤ n).
Applying rules CONC and QINIT we derive

Γ P 1 {s[1]/α 1 }|...|P n {s[n]/α n } n i=1 (∆ i , s[i] : G i) (5) Γ s : ε / 0 (6)
From ( 6) using rules QSINIT and QSUNION we derive

Γ {s} s : ε / 0 (7)
Applying rule CINIT to ( 5) and ( 7) we derive

Γ {s} < P 1 {s[1]/α 1 }|...|P n {s[n]/α n } , s : ε > < n i=1 (∆ i , s[i] : G i) / 0 > which implies by rule GSRES , taking into account that ∆ = n i=1 ∆ i Γ / 0 (νs) < P 1 {s[1]/α 1 }|...|P n {s[n]/α n } , s : ε > < ∆ / 0 >
This concludes the proof for this case, since ⇒ is reflexive.

[ From ( 10) by subject reduction on expressions we have:

Γ v : S 0 (12)
which implies 0 = by our assumption on the typing of values. From (9) by Lemma 7( 5) and ( 6) we get Σ = {s} and

Γ s : h Θ (13)
Applying rule QSEND on ( 12) and ( 13) we derive

Γ s : h • (p, Π, v ↓ ) Θ; {s[p] : ! Π, S ↓ }
which implies by rules QSINIT and QSUNION :

Γ {s} s : h • (p, Π, v ↓ ) Θ; {s[p] : ! Π, S ↓ } ( 14
)
Applying rule CINIT on [START_REF] Denning | Cryptography and Data Security[END_REF] and ( 14) we derive From ( 15) by subject reduction on expressions we have:

Γ {s} < P , s : h • (p, Π, v ↓ ) > < ∆ ,
Γ v : L, G 0 (17)
which implies = 0 by our assumption on the typing of values. From ( 9) by Lemma 7( 5) and ( 6) we get Σ = {s} and

Γ s : h Θ (18)
Applying rule QSERVSEND on ( 17) and ( 18) we derive

Γ s : h • (p, Π, v ) Θ; {s[p] : ! Π, L, G }
which implies by rules QSINIT and QSUNION :

Γ {s} s : h • (p, Π, v ) Θ; {s[p] : ! Π, L, G } (19)
Applying rule CINIT on [START_REF] Denning | Cryptography and Data Security[END_REF] and [START_REF] Kolundzija | Security Types for Sessions and Pipelines[END_REF] we derive

Γ {s} < P , s : h • (p, Π, v ) > < ∆ , s[p] : T Θ; {s[p] : ! Π, L, G } >
This concludes the proof, since

< ∆ , {s[p] : ! Π, L, G ; T } Θ > ⇒ < ∆ , s[p] : T Θ; {s[p] : ! Π, L, G } > [Rec] < s[q]? (p, x ).P , s : (p, q, v ↓ ) • h >-→< P{v /x } , s : h > By hypothesis we have Γ Σ < s[q]? (p, x ).P , s : (p, q, v ↓ ) • h > < ∆ Θ > which implies by Lemma 8(1) Γ s[q]? (p, x ).P ∆ (20)
Γ Σ s : (p, q, v ↓ ) • h Θ (21)
Γ v : L 0 , G 0 (24)
By the coherence of < ∆ Θ > only case (a) is possible with S = S 0 , and therefore from ( 22) and ( 23) by Lemma 11 [START_REF] Almeida Matos | On Declassification and the Non-Disclosure Policy[END_REF] we have

Γ P{v /x } ∆ , s[q] : T ( 25
)
From Γ s : h Θ using rules QSINIT and QSUNION we derive:

Γ {s} s : h Θ (26)
Applying rule CINIT on ( 25) and ( 26) we derive 27) and ( 23) by Lemma 11 [START_REF] Bettini | Global Progress in Dynamically Interleaved Multiparty Sessions[END_REF] we have

Γ {s} < P{v /x } , s : h > < ∆ , s[q] : T Θ > This concludes the proof, since < ∆ , s[q] :?(p, S ↓ ); T {s[q] : ! p, S ↓ }; Θ > ⇒ < ∆ , s[q] : T Θ >
Γ P{v /x } ∆ , s[q] : T ( 28
)
From Γ s : h Θ using rules QSINIT and QSUNION we derive:

Γ {s} s : h Θ (29)
Applying rule CINIT on ( 28) and ( 29) we derive

Γ {s} < P{v /x } , s : h > < ∆ , s[q] : T Θ > This concludes the proof, since < ∆ , s[q] :?(p, L, G ); T {s[q] : ! p, L, G }; Θ > ⇒ < ∆ , s[q] : T Θ >.
• [Link] In this case, since Γ P ∆ is deduced using the typing rules MINIT , MACC and CONC , we have

P = ā [n] | ∏ n p=1 a [p](α p ).Q p ,
with Γ a : L, G , and the reduction has the form:

< ā [n] | n ∏ p=1 a [p](α p ).Q p , / 0 >-→ (νs) < n ∏ p=1 Q p {s[p]/α p } , s : ε >
for some fresh name s. Then we may conclude, since / 0 = L s : ε for any L .

• [Send] In this case, since Γ P ∆ is deduced using the typing rule SEND , there exist 1 , 2 such that ≤

2 ≤ 1 and P = s[p]! 2 Π, e .P , with Γ e : S 1 . Here the reduction has the form:

< s[p]! 2 Π, e .P , s : h >-→< P , s : h • (p, Π, v 1 ↓ 2 ) >,
where e ↓ v 1 . Now, ≤ 2 implies 2 / ∈ L . From this we deduce that s :

h = L s : h • (p, Π, v 1 ↓ 2 ).
• [Rec] In this case, since Γ P ∆ is deduced using the typing rule RCV , there exist 1 , P such that ≤ 1 and P = s[q]? 1 (p, x ).P . Then P = P {v /x } and the reduction is:

< s[q]? 1 (p, x ).P , s : (p, q, v 1 ↓ ) • h >-→< P {v /x } , s : h > and s : (p, q, v 1 ↓ ) • h = L s : h. • [DelRec]
In this case, since Γ P ∆ is deduced by the typing rule SREC , there exists P such that P = s[p]? ((q, α)).P . Then P = P {s [p ]/α} and the reduction is: We next define the bisimulation relation that will be used in the proof of soundness.

< s[q]? ((p, α)).P , s : (p, q, s [p ] ) • h >-→< P {s [p ]/α} , s : h > Since / ∈ L , we conclude that s : (p, q, s [p ] ) • h = L s : h.

Definition 8.5 (Bisimulation for soundness proof).

Given a down-closed set of security levels L , the relation R L Γ on processes is defined inductively by: P 1 R L Γ P 2 if P 1 , P 2 are typable in Γ and i) either P 1 , P 2 are L -high in Γ ii) or P 1 , P 2 are L -bounded in Γ and one of the following holds:

1. P 1 = P 2 ; 2. P i = a [p](α p ).Q (i)
p , and ∀ s fresh: Q

(1) 8. P i = s[p] ⊕ Π, λ .Q i , where Q 1 R L Γ Q 2 ; 9. P i = s[p]& (q, {λ j : Q (i) j } j∈J ), where ∀ j ∈ J : Q (1) j R L Γ Q
(2) j ; 10. P i = (νr)P i , where P 1 R L Γ P 2 ; 11. P i = D P i , where P 1 R L Γ P 2 ; 12.

P i = ∏ m j=1 Q (i) j , where ∀ j (1 ≤ j ≤ m) : Q (1) j R L Γ Q (2)
j follows from one of the previous clauses (including the clause of high processes).

For the proof of soundness, it is convenient to use the following alternative definition of L -bisimulation (where we need to put ≡ in the matching reduction sequence for the case where it is the empty sequence and we have to apply ≡ to obtain the same restriction as in the first process): Definition 8.6 (L -Bisimulation on processes (alternative formulation)).

A symmetric relation R ⊆ (Pr × Pr) is a simple L -bisimulation if P 1 R P 2 implies, for any pair of monotone Q-sets H 1 and H 2 such that H 1 = L H 2 and each < P i , H i > is saturated:

If < P 1 , H 1 > -→ (ν r) < P 1 , H 1 >, then there exist P 2 , H 2 such that < P 2 , H 2 >-→ * ≡ (ν r) < P 2 , H 2 > , where H 1 = L H 2 and P 1 R P 2 .
Processes P 1 , P 2 are L -bisimilar, P 1 L P 2 , if P 1 R P 2 for some L -bisimulation R.

Theorem 19 (Noninterference). If P is typable, then P is secure.

Proof. The proof consists in showing that the relation R L Γ presented in Definition 8.5 is a L -bisimulation containing the pair (P, P). Note that we have P R L Γ P by Clause 1. Suppose that P 1 R L Γ P 2 , Γ i P i ∆ i and H 1 , H 2 are two monotone Q-sets such that H 1 = L H 2 and P i , H i is saturated for i = 1, 2. We want to show that each reduction < P 1 , H 1 >-→ (ν r) < P 1 , H 1 > is matched by a possibly empty sequence of reductions < P 2 , H 2 >-→ * ≡ (ν r) < P 2 , H 2 > such that H 1 = L H 2 and P 1 R L Γ P 2 . Typability of the P i , H i will be given by Lemma 12 (Subject Reduction), which we will use without mentioning it. We proceed by induction on the definition of R L Γ . Let us examine the two clauses of Definition 8.5: i) Both P 1 , P 2 are L -high in Γ;

ii) Both P 1 , P 2 are L -bounded in Γ and P 1 R L Γ P 2 by one of the Clauses 1-12 of Definition 8.5. Note that, since L -highness is preserved by execution, as we go along executing processes we can pass from Clause ii) to Clause i), but not vice versa. i) Let P i be L -high in Γ for i = 1, 2. Consider a move < P 1 , H 1 >-→ (ν r) < P 1 , H 1 >. By the Confinement Lemma (Lemma 17) H 1 = L H 1 and P 1 is L -high in Γ. This move can then be matched by the empty move of

< P 2 , H 2 >, namely < P 2 , H 2 > ≡ (ν r) < P 2 , H 2 >, where H 1 = L H 1 = L H 2 .
Then we may conclude, since P 1 R L Γ P 2 by Clause i) again.

ii) Suppose now that the P i 's are L -bounded. We consider some interesting cases.

• Let P i = s[p]! Π, e .P i , where P 1 R L Γ P 2 and ∃ v, ∃ ≥ such that e ↓ v . In this case the reduction is obtained by rule [Send]. Applicability of rule [Send] assures that there is a queue s : h 1 in H 1 . Since P 2 , H 2 is saturated, there will be a queue s : h 2 in H 2 . Then, assuming

H i = K i ∪ s : h i , we have H 1 = K 1 ∪ s : h 1 • (p, Π, v ↓ )
, and the matching move will be <

P 2 , H 2 >-→ (ν r) < P 2 , H 2 >, where H 2 = K 2 ∪ s : h 2 • (p, Π, v ↓ ). Indeed, if / ∈ L then H 1 = L H 1 = L H 2 = L H 2 . If ∈ L then H 1 = L H 2 follows from K 1 = L K 2 and s : h 1 = L s : h 2 .
• If P i = s[q]? ((p, α i )).P i , then the reduction is obtained by rule [DelRec]. Since Γ i P i ∆ i is deduced by the typing rule SREC , we know that = i . Moreover i ∈ L because P i is L -bounded, hence ∈ L . Applicability of rule [DelRec] ensures that a message (p, q, s [p ] ) must occur at the head of queue s in H 1 .

Given that H 1 = L H 2 , the same message must occur in H 2 . Since H 2 is monotone, the message (p, q, s [p ] ) must occur at the head of queue s also in H 2 . Then, assuming H i = K i ∪ s : (p, q, s [p ] ) • h i , we get:

< P 1 , K 1 ∪ s : (p, q, s [p ] ) • h 1 >-→< P 1 {s [p ]/α 1 } , K 1 ∪ s : h 1 > < P 2 , K 2 ∪ s : (p, q, s [p ] ) • h 2 >-→< P 2 {s [p ]/α 2 } , K 2 ∪ s : h 2 >
We may then conclude since by hypothesis

P 1 {s [p ]/α 1 } R L Γ P 2 {s [p ]/α 2 }, and H 1 = L H 2 implies K 1 ∪ s : h 1 = L K 2 ∪ s : h 2 .
We conclude with an observation about the compositionality of our notion of security. It is clear that security is not preserved by input prefixing in case the input is "high". In the absence of restrictions on the application of our semantic rules, our security notion is not preserved by parallel composition either. Indeed, the three processes discussed in Section 6.5, Section 6.6, Section 6.7, are not secure, although all their components are secure. Let us just recall here the first of these examples, completed with security levels on services:

Consider the following process:

s[2]?(1, x ). b [2] | b [1](β 1 ).β 1 ! 2, ⊥ .0 | b [2](β 2 ).β 2 ?(1, y ⊥ ).0
As argued in Section 6.5, this process is insecure while all its components are secure. Note that this process is untypable, whatever the choice of . Indeed, in a well-formed environment Γ, the service b must be given a safety global type L, G and then the typing rule MACC requires both participant bodies β 1 ! 2, ⊥ .0 and β 2 ?(1, y ⊥ ).0 to be typable at level . This is only possible if = ⊥. But then the first component cannot be typed, since the typing rule RCV requires b [START_REF] Bettini | Global Progress in Dynamically Interleaved Multiparty Sessions[END_REF] to be typable at level .

On the other hand, if we swapped the levels and ⊥ in the above process, then we would obtain: which is both secure and typable for = (recall that the level of a service is the meet of its global type).

Indeed, as an easy consequence of our soundness Theorem, security is preserved by parallel composition if the components are typable with respect to the same standard environment:

Corollary 20 (Security compositionality for typable processes).

Let P and Q be typable with respect to the same standard environment. If P and Q are secure, then also P | Q is secure.

Proof. If P and Q are typable with respect to the same standard environment, then also P | Q is typable with respect to that environment, hence by the previous theorem it is also secure.

Conclusion and future work

In this work, we have investigated the integration of security requirements into session types. Interestingly, there appears to be an influence of session types on security.

For instance, it is well known that one of the causes of insecure information flow in a concurrent scenario is the possibility of different termination behaviours in the branches of a high conditional. In our calculus, we may distinguish three termination behaviours: (proper) termination, deadlock and divergence. Now, the classical session types of [START_REF] Takeuchi | An Interaction-based Language and its Typing System[END_REF] already exclude some combinations of these behaviours in conditional branches. For instance, a non-trivial divergence (whose body contains some communication actions) in one branch cannot coexist with a non-trivial termination in the other branch. Moreover, session types prevent local deadlocks due to a bad matching of the communication behaviours of participants in the same session. By adding to classical session types the interaction typing of [START_REF] Bettini | Global Progress in Dynamically Interleaved Multiparty Sessions[END_REF], we would also exclude most of the global deadlocks due to a bad matching of the protocols of two interleaved sessions. However, this typing still does not prevent deadlocks due to inverse session calls (for instance, a partner that calls service a and then service b, while the dual partner calls first b and then a). We plan to study a strengthening of interaction typing that would rule out also this kind of deadlock taking inspiration from [START_REF] Kobayashi | A Type System for Lock-Free Processes[END_REF].

The form of declassification considered in this work is admittedly quite simple. To justify our choice, let us first remark that a local declassification construct, such as that proposed in [START_REF] Boudol | Access Control and Declassification[END_REF] for a classical language with sequential composition, would not be appropriate for our calculus. Indeed, such a construct specifies which additional information flows -with respect to the security policy in force -are authorised within its scope. If we adopted this construct in our calculus, where the only form of sequential composition is prefixing, the scope of a declassification for an input process would span over its whole continuation. In other words, after a declassification it would never be possible to restore the original policy. This is why we chose here a simpler and more punctual form of declassification, which applies to single values rather than to whole subprocesses. On the other hand, we retained from [START_REF] Boudol | Access Control and Declassification[END_REF] the idea that declassification should be constrained by the access control policy, since a declassified value may only be received by a trusted participant, namely one whose security level is greater than or equal to the original level of the value.

A specificity of our declassification mechanism is that a value v is declassified from to while being transmitted from one participant to another. Moreover, this value is treated as an -value by the sender (the value v ↓ is Lobservable for any L containing ) while it is treated in a mixed way by the receiver, who receives it as if it were a -value but then uses it freely as a -value. It might be objected that this is a rather abstract and implicit way to perform declassification, and that the role played by the bisimulation in controlling declassification is not obvious. Indeed, in the receiver the usage of the declassified value is not constrained by the bisimulation (since v ↓ is already an -value when it is read from the queue4 ); it is only constrained by the access control mechanism, which requires the receiver to be -trusted, and therefore assumed to make good use of the original -value by processing it with a function that safely downgrades it to level (what is sometimes called a "permitted function" or a "downgrading policy" [START_REF] Li | Downgrading policies and relaxed noninterference[END_REF]). A more explicit solution would consist in replacing v ↓ by f ↓ (v) in the queue, where f is some permitted function (say, an encryption function) used by the sender to safely transmit the value as an -level one -here the subscript ↓ indicates that f takes an -level argument and yields an -level result. Then the trusted receiver could retrieve v as an -level value (using the decryption function), and subsequently process it with his own permitted function g ↓ to produce the declassified -level result. Here the function f would be used by the sender to protect the value v while it transits in the queue, whereas the function g would be used by the receiver to actually perform the declassification.). On the other hand, in the sender the usage of v ↓ is constrained by the bisimulation (and a fortiori by the type system), since by observing v ↓ as an -level value in the queue we prevent the sender to receive any -level value before performing the declassified send. This means in particular that the sender cannot have previously received v from some other participant. In other words, the sender must own the high value v in order to be able to transmit it to the receiver with the authorisation to declassify it. Moreover, since the declassified send of v cannot depend on any other high value, the bisimulation ensures that the sender discloses no more than the value v itself. To conclude, declassification is controlled by a combined effect of the bisimulation in the sender and of access control in the receiver. The bisimulation itself has no specific clause to deal with declassification. Indeed, we take here the stand that, since our declassification applies to single values and not to security levels, it can be implemented without modifying the definition of bisimulation, thus departing from other approaches ([27], [START_REF] Almeida Matos | On Declassification and the Non-Disclosure Policy[END_REF]).

Our notion of security could be strengthened by allowing empty queues corresponding to low services to be observed. Then the initiation of a low session would always be observable, no matter whether a low message is exchanged or not in the session. In this way we could avoid requiring saturation of Q-sets, since the empty Q-set would no longer be L -equal to a Q-set consisting of an empty queue corresponding to a low service. Indeed, let us look back at the example that motivated the introduction of the saturation condition, at page 9. If low empty queues were observable, the bisimulation would never test the process P = s[1]! 2, ⊥ .0 in combination with the two Q-sets / 0 and {s : ε}, since these would no more be equivalent for the low observer. However, notice that this would require adding security levels to queues, since the empty queue that is created for a high service should remain unobservable. As a matter of fact, we did explore this alternative definition, in the hope to obtain compositionality for our security property (in its robust variant defined in the Appendix). However, it turned out that adding levels to queues was still not sufficient for compositionality. This is why we adopted the simpler (and weaker) form of observation here.

To enhance the practical use of the present calculus we plan to develop a type inference algorithm, which applied to a typable process returns its type together with the required security levels of session participants in order to guarantee access control.

  ? C, ↓⊥ ; ⊕ C, { :! C, ⊥ ; , : } where the communication partner of S (namely C) is explicitly mentioned. The session type T is the rest of type T after the first communication has been done: ⊕ C, { :! C, ⊥ ; , : }

2 >

 2 could try to reply by letting first Q 2 output the message (2, 1, ) and then Q 1 read this message. In both cases we would be left with the Q-set H 1 = H 2 = {s : ε}. However this would result in the replacement of different values for z in the conditional, leading in the next steps to the output of two different low values from participant 1 to participant 3, yielding the non ⊥-equal Q-sets H 1 = {s : (1, 3, ⊥ )} and H 2 = {s : (1, 3, ⊥ )}.

  and τ occurs in T i for some i ∈ I. A type prefix τ precedes a type prefix τ in a session type T if one of the following conditions holds: • T = τ; T and τ occurs in T ; • T = τ ; T or T = µt.T or T = δ ; T and τ precedes τ in T ; • T = ⊕ Π, {λ i : T i } i∈I or T = & (p, {λ i : T i } i∈I ) and τ precedes τ in T i for some i ∈ I. As for M(G), we denote by M(T ) the meet of all security levels appearing in T . M( ! Π, S ↓ ; T ) = M(T ) M(?(p, S ↓ ); T ) = M( ! Π, L, G ; T ) = M(T ) M(?(p, L, G ); T ) = M( ! q, T ; T ) = M(T ) M(? (p, T ); T ) = M(⊕ Π, {λ i :

  νa )P ∆ Γ e : S = M(T ) ∆ only VAR Γ, X : S T X e, c ∆, c : T Γ, X : S T, x : S P {α :T } = M(T ) Γ, X : S T Q ∆ DEF Γ X(x , α) = P Q ∆ dom(L) = {1,...,n} MINIT Γ, u : L, G ū[n] / 0 Γ, u : L, G P ∆, α : G p MACC Γ, u : L, G u[p](α).P ∆ Γ e : S Γ P ∆, c : T ≤ ≤ SEND Γ c! Π,e .P ∆, c : ! Π, S ↓ ; T Γ, x : S P ∆, c : T ≤ RCV Γ c? (p, x ).P ∆, c :?(p, S ↓ ); T Γ e : L, G Γ P ∆, c : T ≤ SERVSEND Γ c! Π, e .P ∆, c : ! Π, L, G ; T Γ, x : L, G P ∆, c : T SERVRCV Γ c? (p, x ).P ∆, c :?(p, L, G ); T Γ P ∆, c : T ≤ = M(T ) DELEG Γ c! q, c .P ∆, c : ! q, T ; T, c : δ ; T Γ P ∆, c : T, α : T = M(T ) SREC Γ c? ((p, α)).P ∆, c :? (p, T ); T Γ P ∆, c :

3 .

 3 If Γ e P Q ∆, then Γ e : and Γ P ∆ and Γ Q ∆. 4. If Γ (νa )P ∆, then Γ, a : L, G P ∆. 5. If Γ X e, c ∆, then Γ = Γ , X : S T and ∆ = ∆ , c : T and Γ e : S and ≤ M(T ) and ∆ only. 6. If Γ X(x , α) = P Q ∆, then Γ, X : S T, x : S M(T ) P {α : T } and Γ, X : S T Q ∆. 7. If Γ ū[n] ∆, then Γ = Γ , u : L, G and dom(L)={1,...,n} and ∆ = / 0. 8. If Γ u[p](α).P ∆, then Γ = Γ , u : L, G and Γ P ∆, α : G p. 9. If Γ c! Π, e .P ∆, then (a) either ∆ = ∆ , c : ! Π, S ↓ ; T and Γ e : S and Γ P ∆ , c : T and ≤ ≤ ; (b) or ∆ = ∆ , c : ! Π, L, G ; T and Γ e : L, G and Γ P ∆ , c : T and ≤ = . 10. If Γ c? (p, x ).P ∆, then (a) either ∆ = ∆ , c :?(p, S ↓ ); T and Γ, x : S P ∆ , c : T and = ≤ ; (b) or ∆ = ∆ , c :?(p, L, G ); T and Γ, x : L, G P ∆ , c : T and = = . 11. If Γ c! q, c .P ∆, then ∆ = ∆ , c : ! q, T ; T, c : δ ; T and Γ P ∆ , c : T and ≤ = M(T ). 12. If Γ c? ((p, α)).P ∆, then ∆ = ∆ , c :? (p, T ); T and Γ P ∆ , c : T, α : T and = = M(T ). 13. If Γ c ⊕ Π, λ j .P ∆, then ∆ = ∆ , c : ⊕ Π, {λ i : T i } i∈I and j ∈ I and Γ P ∆ , c : T j and ≤ ≤ i∈I M(T i ). 14. If Γ c& (p, {λ i : P i } i∈I ) ∆, then ∆ = ∆ , c : & (p, {λ i : T i } i∈I ) and Γ P i ∆ , c : T i for all i ∈ I and = ≤ i∈I M(T i ).

  (a) either Θ ≈ Θ ; {s[p] : ! Π, S ↓ } and Γ v : S ; (b) or v = a and Θ ≈ Θ ; {s[p] : ! Π, L, G } and Γ a :

  s[p] : T Θ; {s[p] : ! Π, S ↓ } > This concludes the proof, since < ∆ , {s[p] : ! Π, S ↓ ; T } Θ > ⇒ < ∆ , s[p] : T Θ; {s[p] : ! Π, S ↓ } > 2. or ∆ = ∆ , c : ! Π, L, G 0 ; T and ≤ = 0 and Γ e : L, G 0 (15) Γ P ∆ , c : T (16)

From ( 20 )

 20 by Lemma 6(10) we get 1. either ∆ = ∆ , s[q] :?(p, S ↓ ); T and = ≤ and Γ, x : S P ∆ , s[q] : T (22) From (21) by Lemma 7(5) and (6) we get Σ = {s} and Γ s : (p, q, v ↓ ) • h Θ which implies by Lemma 9(1) Γ s : h Θ and : (a) either Θ ≈ {s[p] : ! Π, S ↓ }; Θ and Γ v : S 0 (23) (b) or Θ ≈ {s[p] : ! Π, L 0 , G 0 }; Θ and

2 .

 2 or ∆ = ∆ , c :?(p, L, G ); T and = and Γ, x : L, G P ∆ , c : T (27) From (21) by Lemma 7(5) and (6) we get Σ = {s} and Γ s : (p, q, v ↓ ) • h Θ which implies by Lemma 9(1) Γ s : h Θ and (a) either Θ ≈ {s[p] : ! Π, S ↓ }; Θ and (23) (b) or Θ ≈ {s[p] : ! Π, L 0 , G 0 }; Θ and (24). By the coherence of < ∆ Θ > only case (b) is possible with L 0 = L and G 0 = G, and therefore from (

s[ 2 ]

 2 ?(1, x ⊥ ). b [2] | b [1](β 1 ).β 1 ! 2, .0 | b [2](β 2 ).β 2 ?(1, y ).0

Table 1 :

 1 Processes of the C, S, B example.

Table 2 :

 2

1. C → S : ⊥ 2. S δ S → B : T 3. C → S : ↓⊥ 4. B → S : T 5. B → S : { : , : } 6. S → C : { : S → C : ⊥ ; , : } Global types of the C, S, B example.

Table 3 :

 3 Syntax of processes, expressions and queues.

Table 4 :

 4 Structural equivalence.

νrr )C ≡ (νr r)C (νr)(< P , H >) ≡ < (νr)P , H > (νr)(< P , H >) ≡ < P , (νr)H >

Table 5 :

 5 Reduction rules.

Table 6 :

 6 Processes of the C, S, B example with all security levels.

Table 8 :

 8 Typing rules for processes.

Table 11 :

 11 Typing rules for Q-sets.

Table 12 :

 12 Typing rules for configurations.

However, our formal treatment will cover the general case of a finite lattice of security levels, and a number of examples involving multiparty sessions will be discussed in Section 6.

P B = s b [1]! ⊥ 2, s a [2] . valid(cc ⊥ ) s b [1] ⊕ ⊥ 2, ok .0 s b [1] ⊕ ⊥ 2, ko .0

Recall that the level of an expression value is the join of the levels of the variables and values occurring in the expression.

T; Π, Z ; Π , Z ; T ≈ T; Π , Z ; Π, Z ; T if Π ∩ Π = / 0 T; Π, Z ; T ≈ T; Π , Z ; Π , Z ; T if Π = Π ∪ Π , Π ∩ Π = / 0Table 9: Equivalence relation on message types.QINIT Γ s : ε / 0Γ s : h Θ Γ v : S QSEND Γ s : h • (p, Π, v ↓ ) Θ; {s[p] : ! Π, S ↓ } Γ s : h Θ Γ v : L, G QSERVSEND Γ s : h • (p, Π, v ↓ ) Θ; {s[p] : ! Π, L, G } Γ s : h Θ QDELEG Γ s : h • (p, q, s [p ] ) Θ, s [p ] : T ; {s[p] : ! q, T }

We refer to[START_REF] Pierce | Types and Programming Languages[END_REF], Section 3.3, for the difference between computational and contextual rules.

p {s[p]/α p } R L Γ Q (2)p {s[p]/α p }; 3. P i = s[p]! Π, e .P i , where P 1 R L Γ P 2 and ∃ v, ∃ ≥ such that e ↓ v ; 4. P i = s[q]? (p, x ).P i , where ∀v: P 1 {v /x } R L Γ P 2 {v /x }; 5. P i = s[p]! q, s [p ] .P i , where P 1 R L Γ P 2 ; 6. P i = s[q]? ((p, α i )).P i , where ∀p , ∀ s fresh: P 1 {s [p ]/α 1 } R L Γ P 2 {s [p ]/α 2 }; 7. P i = e P i P i where P 1 R L Γ P 2 and P 1 R L Γ P 2 ;

Note that this is an obliged choice, given our definition of bisimulation. If v ↓ were treated as an -value in the queue, then the bisimulation would systematically fail in the receiver, as soon as the value is actually declassified and used as an -value.

Acknowledgments We would like to thank Nobuko Yoshida for her encouragement to engage in this work, Bernard Serpette for enlightening remarks and the anonymous referees for insightful comments, which allowed us to improve the presentation of the paper and to clarify some important points.

$ Work partially funded by the EU Project 257414 ASCENS, by the ICT COST Action IC1201 BETTY, by the MIUR PRIN Project CINA Prot. 2010LHT4KM and by the Torino University and Compagnia San Paolo Project SALT.

Typing rules assure that configurations are always typed with coherent environments.

Reduction of configuration environments

Since process and queue environments represent future communications, by reducing processes we get different configuration environments. This is formalised by the notion of reduction of configuration environments, denoted by < ∆ Θ > ⇒ < ∆ Θ >. < {s[q] :?(p, S ↓ ); T } { s[p] : ! q, S ↓ }; Θ > ⇒ < {s[q] : T } Θ > 6. < {s[q] :?(p, L, G ); T } { s[p] : ! q, L, G }; Θ > ⇒ < {s[q] : T } Θ > 7. < {s[q] :? (p, T ); T } { s[p] : ! q, T , s [p ] : T }; Θ > ⇒ < {s[q] : T , s [p ] : T } Θ > 8. < {s [q] : & (p, {λ i :

where message types are considered modulo the equivalence relation of Table 9.

The first four rules correspond to participant p putting a value, a session name, a channel or a label in the queue. The following four rules correspond to participant p reading a value, a session name, a channel or a label from the queue. Notice that in the rules for delegation the type of the delegated channel is only moved from ∆ to Θ and vice versa. All these rules are computational. 3 The last rule is contextual: notice that we add only statements to the process environments, since only one statement is considered in the first eight reduction rules, while we do not need to add statements to the queue environments, which are always arbitrary.

We say that a queue is generated by service a, or a-generated, if it is created by applying rule [Link] to the parallel composition of a's participants and initiator.

If

The next lemma characterises the types due to messages occurring as heads of queues.

Lemma 9.

1.

The proof of this Lemma is standard, by induction on the length of queues.

Theorem 10 (Type Preservation under Equivalence

Proof. By induction on the definition of ≡.

Lemma 11 (Substitution Lemma).

Proof. By standard induction on P.

(Subject Reduction

Proof. We prove the simpler statement (of which Theorem 12 is an immediate corollary):

by induction on the derivation of C -→ C , with a case analysis on the final rule. We only consider some paradigmatic cases. For simplicity we write only the part of the configuration which is reduced, omitting processes and queues that can be needed to type the configuration.

[Link]

From ( 2) by Lemma 7 [START_REF] Bossi | Verifying persistent security properties[END_REF] we get Σ = Θ = / 0. From (1) by Lemma 6 [START_REF] Bettini | Global Progress in Dynamically Interleaved Multiparty Sessions[END_REF]

Properties of T-reachable configurations

The definition of coherence (Definition 7.6) does not require that each input has a corresponding output, each branching has a corresponding selection and vice versa. On the other hand, as usual for session types, this holds for configurations reachable from a typable initial configuration.

Definition 8.1 (T-reachable configurations)

.

Following [START_REF] Pierce | Types and Programming Languages[END_REF], Section 3.3, notice that in Table 5 the first nine rules are computational rules and the last two rules are contextual.

Consider the last computational rule applied to infer the transition (ν s )C n-1 -→ (ν s)C. We distinguish two cases, depending on whether the transition creates or not a new queue s. Suppose s = s • s. Then the last computational rule applied is [Link], and the result holds by definition of projection of global type.

Suppose now s = s . Then the last computational rule applied cannot be [Link] and < ∆ Θ > is obtained from < ∆ n-1 Θ n-1 > using the reduction relation of Definition 7.7. More precisely the reduction < ∆ n-1 Θ n-1 > ⇒ < ∆ Θ > is obtained by applying one of the eight computational rules and the contextual rule of Definition 7. [START_REF] Boudol | Access Control and Declassification[END_REF]. In all cases it is easy to check that if < ∆ n-1 Θ n-1 > is complete, then < ∆ Θ > is complete too. Theorem 14. The Q-set of a T-reachable configuration is monotone.

Proof. Toward a contradiction assume that lev ↓ (ϑ 1 ) ≤ lev ↓ (ϑ 2 ) and the message (p, Π 1 , ϑ 1 ) precedes the message (p, Π 2 , ϑ 2 ) in a queue belonging to a T-reachable configuration C and Π 1 ∩ Π 2 = / 0. We only consider the case Π 1 = Π 2 = {q} and ϑ i = v i ↓ i i where v i is not a service name for i = 1, 2, since the proof for the other cases is similar. In this case lev ↓ (ϑ i ) = i for i = 1, 2. Suppose C = (ν s)C , where C does not contain session restrictions, and let C 0 be the typable initial configuration from which C is T-reachable.

By Theorem 12 and Lemma 8(3) we get Γ { s} C < ∆ Θ > for some Γ, ∆, Θ. Then, by Lemma 7(2) and Lemma 9(1), the queue environment Θ must contain s[p] : T; ! q, S 1 ↓ 1 ; T ; ! q, S 2 ↓ 2 ; T for some S, T, T , T . Lemma 13 ensures completeness of the configuration environment < ∆ Θ >. We know that < ∆ Θ > is also coherent by Proposition 4; this implies that the process environment ∆ will contain s[q] : T for some session type T such that ?(p, S 1 ↓ 1 ) precedes ?(p, S 2 ↓ 2 ) in T . Proposition 3 requires 1 ≤ 2 , and this contradicts 1 ≤ 2 .

Soundness for Access Control

We introduce a notion of join for message types and configuration types. The join of message types is always ⊥. Since a configuration type is a message type, or a session type, or a message type followed by a session type, the join of a configuration type is defined to be the join of its building types. More formally:

Notice that the join of a configuration type is well defined also if output prefixes and message types cannot be always distinguished, since outputs do not contribute to the join.

Lemma 15. Let C 0 be an initial configuration, and suppose

Proof. The proof is by induction on the length n of the reduction sequence -→ * , and then by induction on the inference of the last transition.

In the basic case, for n = 1, we have C 0 -→ (νs)C. Then the last computational rule applied is necessarily [Link], and since < ∆ Θ > (s[p]) = G p, we may immediately conclude.

Consider now the inductive case. Let C 0 -→ * C n-1 -→ (νs)C. We distinguish two cases, according to whether the queue s is created in the last step (in which case it does not appear in C n-1 ) or not.

If C n-1 does not contain the queue s then, as in the basic case, the last computational rule applied is [Link] and the result follows from the fact that

Otherwise let C n-1 = (νs)C . By Theorem 12 and Lemma 8(3), we have

. Now, if the last applied rule does not involve the queue s, we are done by induction. Otherwise, the last computational rule applied cannot be [Link]. In this case < ∆ Θ > ⇒ < ∆ Θ > by applying one of the eight computational rules and the contextual rule of Definition 7. [START_REF] Boudol | Access Control and Declassification[END_REF]. In all cases it is easy to verify that J

)), and we may conclude.

Theorem 16 (Access Control). Let C 0 be an initial configuration, and suppose that

, where the queue of name s in C is a-generated and contains the message (p, q, ϑ ), then lev ↑ (ϑ ) ≤ L(q). Proof. We only consider the case ϑ = v ↓ where v is not a service name, since the proof for the other cases is similar. By Theorem 12 and Lemma 8(3) we get Γ {s} C < ∆ Θ > for some ∆, Θ. Then, by Lemma 7(2) and Lemma 9(1), the queue environment Θ must contain s[p] : T; ! q, S ↓ ; T for some S, T, T . Lemma 13 ensures completeness of the configuration environment < ∆ Θ >. We know that < ∆ Θ > is also coherent by Proposition 4; this implies that the process environment ∆ will contain s[q] : T for some session type T such that ?(p, S ↓ ) occurs in T . By definition of join and of configuration type (Definition 7.3) we have then ≤ J(< ∆ Θ > (s[q])) and by Lemma 15 we get J(< ∆ Θ > (s[q])) ≤ J(G q). Then we may conclude, since the well-formedness of safety global types implies J(G q) ≤ L(q).

If we changed the C, S, B example by avoiding delegation and sending the (declassified)

to the seller, we would incur a violation of access control, since lev ↑ ( ↓⊥ ) = and L(S) = ⊥. In fact such a process would not be typable, as may be checked directly or derived from Theorem 16.

Soundness for Noninterference

In this section we prove the soundness of our type system for the security property. This result is based, as usual, on a Confinement Lemma, which states that if a process is typable with a "high" type, then it cannot affect any "low" queue. For each L ⊆ S , it is useful to distinguish the class of typable processes which are "essentially L -typed", that is, which can only be typed with levels ∈ L . Following the terminology of [START_REF] Boudol | Noninterference for Concurrent Programs and Thread Systems[END_REF], we call these processes L -bounded. The following definitions and Lemmas are then quite standard.

Definition 8.3 (L -Boundedness).

On the set of typable processes, we call L -highness the complement of non L -boundedness.

Definition 8.4 (L -highness).

A process P is L -high in Γ if Γ P ∆ for some ∈ L .

Lemma 17 (Confinement).

Let P be a L -high process in Γ. Then, for any Q-set H: P, H -→ * (ν r) P , H implies H = L H and P L -high in Γ.

Proof. We prove the result for a one-step reduction < P , H >-→ (ν r) < P , H >, by induction on the inference of the transition. Then the general result will follow as a simple corollary, observing that Γ P ∆ by Theorem 12 (Subject Reduction). We consider the most interesting base cases, leaving out the inductive cases which are easy.

• If P i = D P i , then either < P 1 , H 1 > reduces by applying rule [Def] or < P 1 , H 1 > reduces. In the first case let D be X(x , α) = Q and P 1 = X e, s[p] | Q 1 . From P 1 R L Γ P 2 , by Clauses 12 and 1 of Definition 8.5 we get

, H 2 >, and we may conclude using Clause 12. In the second case we can apply the induction hypothesis to P 1 R L Γ P 2 .

j follows from one of the previous clauses (including the clause of high processes). Then the move of < P 1 , H 1 > comes either from a single component Q 1 moves alone, then we have a move

1 , by induction we have a move

and H 1 = L H 2 , whence we may infer

j , H 2 >, and thus we conclude by Clause 12 again.

(b) Let now

j and suppose that a new session is created through a synchronisation of all processes in ā

p j {s[p j ]/α p j } , H 1 ∪ {s : ε} >. We distinguish two cases, according to whether ∈ L or ∈ L : * If ∈ L , by the typing rule MACC each Q

(1)

1 follows from Clause 1 and for each j such that 2 ≤ j ≤ n+1 Q

p j and R (1)

(2)

(2)

(2)

p j {s[p j ]/α p j } for 2 ≤ j ≤ n + 1, we may conclude by Clause 12 again. * If ∈ L , then by the typing rule MACC each Q

(1)

j follows necessarily from Clause i) (since in all the other clauses both processes must be L -bounded). Hence < ∏ n+1 j=1 Q

(2)

(1)

because empty queues are not observed) and by Lemma 17 we know that ∏ n+1 j=2 R

(1)

(1)

by Clause i). Then, recomposing with the remaining components, < P 2 , H 2 > may also reply by the empty move to the move:

(1)

(1)

j by Clause 12 again.

Note that in the proof of non-interference we used both the saturation and the monotonicity conditions as defined in Section 5. We claim that these conditions are reasonable, since they hold for all T-reachable configurations, i.e. for all configurations that can be obtained by reducing typable user processes with the empty Q-set, as shown in Lemma 1 and Theorem 14.

Appendix Appendix A. Robust security

We define an alternative notion of L -bisimulation, which leads to a more discriminating security property, which is closer to typability. We call these new notions robust. The idea of robust L -bisimulation stems from the observation that, while the asynchronous communications among participants can be observed by looking at the changes they induce on the Q-sets, there is no means to observe the behaviour of a potential session participant, as long as it is not triggered by the initiator together with a complete set of matching participants. This means that an "incomplete process" like a ⊥ [1](α).α! 2, ⊥ .0 is always considered bisimilar to 0. However, it is clear that it behaves differently when plugged into a complying context. For instance, if we put a ⊥ [1](α).α! 2, ⊥ .0 in parallel with the initiator and the missing partner we get:

while if we put 0 in the same context we get

Since session initiation is a synchronous interaction, which is blocking for all session participants, it would not make sense to use the Q-sets to keep track of it. We therefore introduce a notion of tester, a sort of behaviourless process which triggers session participants in order to reveal their potential behaviour. Intuitively, testers play the same role as "high contexts" in previous work on security. They also bear a strong analogy with the notion of test introduced by De Nicola and Hennessy in the 80's [START_REF] De Nicola | Testing Equivalence for Processes[END_REF], although they are much simpler in our case, since they are only used to explore potential participant behaviours, and not to test active processes. Moreover, they are not aimed at establishing a testing equivalence, but merely at rendering the bisimulation more contextual.

Formally, a tester is a parallel composition of session initiators and degenerate session participants, which cannot reduce by itself.

A tester is an irreducible pre-tester.

To run processes together with testers, we introduce an asymmetric (non commutative) triggering operator P M, whose behaviour is given by the two new "external link" rules [ExtLink1] and [ExtLink2] in Table A.13, which only differ for the presence or not of the initiator inside the process. Note that rule [ExtLink1] also allows P M to move alone, in case k = n. From now on we denote by -→ the reduction obtained by adding the rules [ExtLink1] and [ExtLink2] to those in Table 5. Then the moves of P M can take place in any static context. Let us stress that in all cases the tester M disappears after the reduction. This is because testers are not interesting in themselves but only insofar as they may reveal the ability of processes to contribute to a session initiation. A term P M is read "P triggered by M".

We are now ready for defining our bisimulation. A relation R on processes is a robust L -bisimulation if, whenever two related processes are put in parallel with the same tester and then coupled with L -equal monotone Q-sets yielding saturated configurations, then the reduction relation preserves both the relation R on processes and the L -equality of Q-sets: Let us illustrate the use of testers with some examples. Note that although "complete processes" may reduce autonomously without the help of any tester, we do not allow the empty process as a tester. Indeed, its use may be simulated by any tester whose names are disjoint from those of the tested process, what we shall call a fresh tester. In fact, in Definition Appendix A.2, the quantification over M may be restricted in practice only to those testers that make the process react, by triggering some of its waiting participants, together with one fresh tester that forces the process to progress by itself, if possible, and get stuck otherwise.

Example 21. Consider the three processes:

It is easy to see that no pair of P i is in the L -bisimilarity relation. Assume in all cases the starting Q-sets to be / 0. To distinguish P 2 from P 3 , which is a complete process and thus can progress by itself, we may use the fresh tester b⊥ [START_REF] Bettini | Global Progress in Dynamically Interleaved Multiparty Sessions[END_REF], which will just stay idle in parallel with P 3 while this moves to a state P 3 by opening a session s, generating the Q-set {s : ε}. Since the tester b⊥ [START_REF] Bettini | Global Progress in Dynamically Interleaved Multiparty Sessions[END_REF] cannot make P 2 react, P 2 will respond by staying put, thus keeping unchanged the Q-set / 0 = L {s : ε}. So far so good. But now, if P 2 and P 3 are tested again with b⊥ [2] and coupled with the Q-set {s : ε}, then P 3 will produce the Q-set {s : (1, 2, ⊥ )} while P 2 remains stuck on the Q-set {s : ε} = L {s : (1, 2, ⊥ )}. To distinguish P 1 from P 2 , we may use the tester ā⊥ [2] | a ⊥ [2](β ).0, which produces no effect on P 1 but will activate P 2 , allowing it to move to a new state P 2 by opening a session s, generating the Q-set {s : ε}. From this point onwards, we proceed as for P 3 above.

To distinguish P 1 from P 3 we may use the same fresh tester b⊥ [2] and a similar argumentation.

Testers may also be used to explore some deadlocked processes, when the deadlock is caused by inverted service calls to different services in dual components, for instance. However, as expected, the bisimulation will not equate such a deadlocked process with a correct process where the two calls occur in the same order in the two components.

Example 22. Consider the following processes, where s is a previously opened session on some service:

Process P 1 is deadlocked because the "service calls" to a and b occur in reverse order in its two components. Instead, the calls occur in the same order in the components of P 2 . Hence P 2 may progress by itself and thus, as above, it is sufficient to test it with a fresh tester to distinguish it from the blocked process P 1 .

The notions of robust L -security and robust security are now defined as usual: Definition Appendix A.3 (Robust L -Security). A process P is robustly L -secure if P L P. Definition Appendix A.4 (Robust Security). A process P is robustly secure if it is robustly L -secure for every L .

It is easy to see that robust L -bisimilarity is more discriminating than L -bisimilarity, as shown by the process a ⊥ [1](α 1 ).s[1]! 2, ⊥ .0, which is L -bisimilar to 0 but not robustly L -bisimilar to 0. As a consequence, the property of robust security is stronger than security, as shown by the following example.

Example 23. Consider the process: s[1]?(2, x ).a [1](α).s[1]! 2,

⊥ .0

This processes is secure but not robustly secure. Note that when put in parallel with the initiator and the missing partner of a [START_REF] Almeida Matos | On Declassification and the Non-Disclosure Policy[END_REF](α).0, then it becomes insecure too. Note that this process is not typable.

We prove now that typability implies robust security. The proof will make use of the same relation R L Γ used for security and presented in Definition 8.5. Note that it is not possible here to use an alternative definition of Lbisimulation similar to Definition 8.6, since in case P 2 M does an empty move, then M does not disappear. Hence we need to use the original Definition Appendix A.2 in the proof.

Lemma 24 (Robust confinement).

Let P be a L -high process in Γ. Then, for any Q-set H: P M, H -→ * (ν r) P , H implies H = L H and P L -high in Γ.

Proof. Simple variation of the proof of Lemma 17 (Confinement Lemma). Note that the residual of P M, H after the first step of the reduction is a pure process.

Theorem 25 (Soundness for robust security). If P is typable, then P is robustly secure.

Proof. The proof consists in showing that the relation R L Γ presented in Definition 8.5 is a L -bisimulation containing the pair (P, P). Note that we have P R L Γ P by Clause 1. Suppose that P 1 R L Γ P 2 , Γ i P i ∆ i and H 1 , H 2 are two monotone Q-sets such that H 1 = L H 2 and P i , H i is saturated for i = 1, 2. We want to show that for any tester M, and for each reduction

, where H 1 = L H 2 and P 1 R L Γ P 2 (typability of the P i , H i will be given by Lemma 12 (Subject Reduction), which we will use without mentioning it). We proceed by induction on the definition of R L Γ . Let us examine the two clauses of Definition 8.5: i) P 1 , P 2 are L -high in Γ (i.e. both P 1 , P 2 are not L -bounded in Γ);

ii) Both P 1 and P 2 are L -bounded in Γ and P 1 R L Γ P 2 by one of the Clauses 1-12 of Definition 8.5. Note that, since L -highness is preserved by execution, as we go along executing processes we can pass from Clause ii) to Clause i), but not vice versa. i) Let P 1 , P 2 be L -high in Γ. Consider a move < P 1 M , H 1 >-→ (ν r) < P 1 , H 1 >. By Lemma 24, we know that H 1 = L H 1 = L H 2 and P 1 is L -high in Γ. Then we conclude, since P 1 R L Γ P 2 by Clause i) again. ii) Suppose now that P 1 and P 2 are L -bounded. We consider some interesting cases. Note that a tester can only interact with the process in Clauses 2, 11 and 12. Hence we do not need to consider testers in the other cases. Indeed, we will omit these cases here, since they are treated exactly as in the proof of Theorem 19.

..,n},q =p a [q](α q ).0, where n is the arity of a. Then we can only apply rule [Link], so we get

p {s[p]/α p } , H 1 ∪ {s : ε} >, where s is fresh. Now, this move can be matched by

p {s[p]/α p }, and

j follows from one of the previous clauses (including the clause of high processes). Then the move of < P 1 M , H 1 > comes either from a single component Q (1) j , or from a group of components synchronising among themselves and possibly with the tester to open a session. Without loss of generality, we may assume that in the first case the moving component is Q

1 , and in the second case the group of moving components is ∏ k j=1 a [p j ](α p j ).R

(1)

p j , for some k ≤ n. Let us examine the two cases.

1 moves alone, then the move

1 , by induction we have either

1 , and therefore

1 and H 1 = L H 2 , whence we infer

j , H 2 > and we may conclude by Clause 12 again.

39

(b) Here we assume that P

j and that all the processes in ∏ k j=1 Q

(1) j synchronise, possibly with the help of the tester.

Let us consider the case where Q

p j for 1 ≤ j ≤ k (the case that includes the initiator is similar, and would use the rule [ExtLink1] instead of [ExtLink2]). Let M be a tester which allows the application of rule [ExtLink2]. Suppose that the move of

(1)

p j {s[p j ]/α p j } , H 1 ∪ {s : ε} >. We distinguish two cases, according to whether ∈ L or ∈ L : * If ∈ L , then by the typing rule MACC no Q

(1) j with 1 ≤ j ≤ k can be high. In this case, for each j such that 1 ≤ j ≤ k, we know that Q

j follows from Clause 2, and hence

p j {s[p j ]/α p j } (note that if we were in the case including an initiator Q (1)

1 would follow from Clause 1 instead). In this case,

(2)

(2)

p j {s[p j ]/α p j }, we may conclude by Clause 12 again. * If ∈ L , then the typing rule MACC requires that each component Q

(1)

j follows necessarily from Clause i) (since in all the other clauses both processes must be L -bounded). In this case, in reply to the move

p j {s[p j ]/α p j } , H 1 ∪{s : ε} >, by Lemma 24 we have H 1 ∪ {s : ε} = L H 1 = L H 2 and ∏ k j=1 R

(1)

j . Then, recomposing with the remaining components, in reply to the move:

(1)

j , H 1 > we have H 1 ∪ {s : ε} = L H 1 = L H 2 and, by Clause 12 again: ∏ k j=1 R

(1)

Appendix B. The Client, Seller, Bank example at a glance

We recap here the definition, semantics and typing of our Client, Seller, Bank example, introduced in Section 2 and used as a running example throughout the paper.

Syntax: process definition

.