Keywords: Concurrence, calcul centré sur la communication, types de session, contrôle d'accès, sécurité du flux d'information

Types de session pour le contrôle d'accès et la sécurité du flux d'information Résumé : Nous étudions un calcul pour modéliser des sessions à partenaires multiples, avec délégation, où les données et les partenaires sont équipés de niveaux de sécurité. Nous présentons un système de types pour ce calcul, garantissant à la fois la sûreté des sessions, une forme de contrôle d'accès et la sécurité du flux d'information, tout en permettant la déclassification des données lors de leur transmission. En particulier, ce système de types permet de prévenir les fuites d'information dues aux primitives spécifiques du langage, que sont l'ouverture de session, la sélection, le branchement et la délégation. Nous illustrons l'utilisation de notre système de types par une série d'exemples, qui révèlent une interaction intéressante entre les contraintes apparaissant dans les systèmes de types classiques pour la sécurité et celles utilisées dans les types de session pour assurer des propriétés telles que l'absence d'erreurs de communication au cours d'une session et la conformité d'une session à un protocole donné.

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 harness 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. 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 RR n°7368 specific constructs of the language, such as session opening, selection, branching and delegation. Finally, we show that it allows controlled forms of declassification, namely those permitted by the access control policy. Our work reveals an interesting interplay between the constraints of security type systems and those of 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. The Appendix summarises various features of the running example introduced in Section 2.

This paper is the full version of [START_REF] Capecchi | Session Types for Access and Information Flow Control[END_REF], including complete definitions and proofs.

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 its use for declassification. The question of secure information flow will only be marginal here. It will be discussed in Sections 5 and 6.

A client C sends the title of a book to a bookseller S. Then S delegates to a bank B both the reception of the credit card number of C and the control of its validity. This delegation is crucial for assuring the secrecy of the credit card number, which should be read by B but not by S. Then B notifies S about the result of the control: for this 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 untrusted party S but really -thanks to delegation -to the trusted party B;

4. B delegates back to S the conversation with C;

5.

B selects the answer ♦❦ or ❦♦ for S depending on the validity 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.

I = ā[2] | b[2]
C = a [START_REF] Almeida Matos | On Declassification and the Non-Disclosure Policy[END_REF](α 1 ).α 1 ! 2, Title ⊥ .α 1 ! ⊥ 2, ❈r❡❞✐t❈❛r❞ ⊤ . 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 we omit unnecessary levels on operators and use ⊥ to mean "public" and ⊤ to mean "secret"). A session is a particular activation of a service, involving a number of parties with predefined roles. Here processes C and S communicate by opening a session on service a, while processes 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.

α 1 &(
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 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 . Then S waits for a channel ζ from B. Henceforth, S communicates using both channels β 2 and ζ : on channel β 2 he waits for one of the labels ♦❦ or ❦♦, which he then forwards to C on ζ , sending also a date if the label is ♦❦.

Forgetting 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 ❙tr✐♥❣ 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 ◆✉♠❜❡r of level ⊤ to S, allowing him to declassify it to ⊥. Notice that due to the previous delegation the ◆✉♠❜❡r 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, since the channel has already been used to receive the ◆✉♠❜❡r. 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 ❙tr✐♥❣ of level ⊥, or the label ❦♦. Since B's choice of the label ♦❦ or ❦♦ depends on a test on the ◆✉♠❜❡r, it is crucial that ◆✉♠❜❡r be previously declassified to ⊥, otherwise the reception of a ❙tr✐♥❣ 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, it is easy to see that the session type T is:

? C, ◆✉♠❜❡r ⊤↓⊥ ; ⊕ C, {♦❦ :! C, ❙tr✐♥❣ ⊥ ; ❡♥❞,❦♦ : ❡♥❞}
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, ❙tr✐♥❣ ⊥ ; ❡♥❞,❦♦ : ❡♥❞}
To formalise access control, we will 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 ❈r❡❞✐t❈❛r❞, it is natural to associate ⊥ with S in both services a and b, and ⊤ with B in service b. Notice that C may indifferently have level ⊤ or ⊥, since it only sends, but does not receive, the high data ❈r❡❞✐t❈❛r❞.

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 ℓ ′ ≤ ℓ (in case ℓ ′ = ℓ, we will write simply ℓ instead of ℓ ↓ ℓ). Let us point out that declassification of services is not allowed in our calculus, both for technical reasons (to be explained in some detail in Section 7) and for lack of evidence of its usefulness. 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 nary 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.

P ::= ū[n] n-ary session initiator | u[p](α).P p-th session participant | c! ℓ Π, e .P Value sending | c? ℓ (p, x ℓ ′ ).P Value receiving | c! ℓ q, c ′ .P Delegation sending | c? ℓ ((p, α)).P Delegation reception | c ⊕ ℓ Π, λ .P Selection | c& ℓ (p, {λ i : P i } i∈I ) Branching | ✐❢ e t❤❡♥ P ❡•s❡ Q Conditional | P | Q Parallel | 0 Inaction | (νa ℓ )P Name hiding | ❞❡❢ D ✐♥ P Recursion | X e, c
Process call

r ::= a ℓ | s Service/Session Name c ::= α | s[p] Channel u ::= x ℓ | a ℓ Identifier v ::= a | tr✉❡ | ❢❛•s❡ | . . . Value e ::= x ℓ | v ℓ | e ❛♥❞ e ′ | ♥♦t e | . . . Expression D ::= X(x ℓ , α) = P Declaration Π ::= {p} | Π ∪ {p} Set of participants ϑ ::= v ℓ↓ℓ ′ | s[p] ℓ | λ ℓ Message content m ::= (p, Π, ϑ ) Message in transit h ::= m • h | ε Queue H ::= H ∪ {s : h} | / 0 Q-set
Table 3: Syntax of processes, expressions and queues.

As in [START_REF] Honda | Multiparty Asynchronous Session Types[END_REF], in order to model TCP-like asynchronous communications (with nonblocking 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 by in Table 3, together with the runtime syntax of the calculus (sessions, channels with role, queues etc.), 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 : h, and to replace the channel α in each process P p by the channel with role s[p]. This is the only synchronous interaction of the calculus, since all the communications that 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 input/output 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 (νs) < P , H >, all occurrences of s[p] in P and H and of s in H are bound. By abuse of notation we often write P instead of < P , / 0 >.

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.

Note that modulo ≡, each configuration has the form (ν r) < P , H >, where (ν r)C stands for (νr

1 ) • • • (νr k )C, if r = r 1 • • • r k .
In (ν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 e=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

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 (❞❡❢ D ✐♥ P) | Q ≡ ❞❡❢ D ✐♥ (P | Q) ❞❡❢ D ✐♥ (❞❡❢ D ′ ✐♥ P) ≡ ❞❡❢ D ❛♥❞ D ′ ✐♥ P (p, Π, ϑ ) • (p ′ , Π ′ , ϑ ′ ) • h ≡ (p ′ , Π ′ , ϑ ′ ) • (p, Π, ϑ ) • h if Π ∩ Π ′ = / 0 or p = p ′ (p, Π, ϑ ) • h ≡ (p, Π ′ , ϑ ) • (p, Π ′′ , ϑ ) • h if Π = Π ′ ∪ Π ′′ and Π ′ ∩ Π ′′ = / 0 h ≡ h ′ ⇒ H ∪ {s : h} ≡ H ∪ {s : h ′ } P ≡ Q and H ≡ K ⇒ < P , H > ≡ < Q , K > (ν r) < P , H > (ν r′ ) < Q , K > ≡ (ν r r ′ ) < P | Q , H ∪ K > if qn(H) ∩ qn(K) = / 0 (νrr ′ )C ≡ (νr ′ r)C (νr)(< P , H >) ≡ < (νr)P , H > (νr)(< P , H >) ≡ < P , (νr)H > Table 4: Structural equivalence.
is why the value needs to be recorded with both levels in the queue. Recall that in case v is a service, then ℓ ′ = ℓ (services cannot be declassified).

The rules [Rec], [DelRec] and [Branch] perform the corresponding complementary operations. Rules [ScopP] and [ScopC] are standard contextual rules. In the latter, Barendregt convention ensures that the names in s are disjoint from those in r and do not appear in C ′′ . 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: RR n°7368

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 t❤❡♥ P ❡•s❡ Q -→ P (e ↓ tr✉❡ ℓ ) ✐❢ e t❤❡♥ P ❡•s❡ Q -→ Q (e ↓ ❢❛•s❡ ℓ ) [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 -→ P ′ ⇒ ❞❡❢ D ✐♥ P -→ ❞❡❢ D ✐♥ P ′ [Defin] P -→ P ′ ⇒ (νa ℓ )P -→ (νa ℓ )P ′ [ScopP] C -→ (ν s)C ′ ⇒ (ν r)(C C ′′ ) -→ (ν r)(ν s)(C ′ C ′′ ) [ScopC]
Table 5: Reduction rules.

I = ā⊥ [2] | b[⊥]2 C = a ⊥ [1](α 1 ).α 1 ! ⊥ 2, Title ⊥ .α 1 ! ⊥ 2, ❈r❡❞✐t❈❛r❞ ⊤ . α 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 ⊥ ) t❤❡♥ β 1 ⊕ ⊥ 2, ok .0 ❡•s❡ β 1 ⊕ ⊥ 2, ko .0
Table 6: Processes of the B, C, S example with all security levels.

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}) P B = s b [1]! ⊥ 2, s a [2] .✐❢ valid(cc ⊥ ) t❤❡♥ s b [1] ⊕ ⊥ 2, ok .0 ❡•s❡ s b [1] ⊕ ⊥ 2, ko .0 RR n°7368 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, ❈r❡❞✐t❈❛r❞ ⊤ . • • • | s a [2]? ⊥ (1, x ⊥ ). • • • | b ⊥ [1](β 1 ). • • • , {s a : (1, 2, Title ⊥↓⊥ )} >) -→ (νs a )(< b⊥ [2] | s a [1]! ⊥ 2, ❈r❡❞✐t❈❛r❞ ⊤ . • • • | b ⊥ [2](β 2 ). • • • | b ⊥ [1](β 1 ). • • • , {s a : ε} >) -→ (νs a )(νs b )(< s a [1]! ⊥ 2, ❈r❡❞✐t❈❛r❞ ⊤ . • • • | s b [2]! ⊥ 1, s a [2] . • • • | s b [1]? ⊥ ((2, ζ )). • • • , {s a : ε, s b : ε} >) -→ (νs a )(νs b )(< s a [1]! ⊥ 2, ❈r❡❞✐t❈❛r❞ ⊤ . • • • | 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, ❈r❡❞✐t❈❛r❞ ⊤ .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, ❈r❡❞✐t❈❛r❞ ⊤↓⊥ ), s b : ε} >)
Table 7: Some reductions of the C, S, B example.

Information Flow Security in Sessions

We turn now to the question of ensuring secure information flow [START_REF] Denning | Cryptography and Data Security[END_REF] within sessions.

We shall be interested in the 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], which may only take place during the transmission of a basic value. The property of NI requires that there is no flow of information 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]. 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 v ℓ↓ℓ ′ , λ ℓ or s[p] ℓ . In the rest of this section, we will focus on the observation model, which will be based on 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 assume that the observer can see the content of messages in session queues. To fix ideas, one may view the observer as a kind of buffer through which messages may transit while reaching or leaving a session queue. We do not want to go as far as allowing an observer to take part in a session, since that could affect the behaviour of other processes. In other words, we assume a passive rather than an active observer.

What matters for security is observation relative to a given set of levels. Given a downward-closed subset L of S , a L -observer will only be able to see messages whose level belongs to L . A notion of L -equality = L on Q-sets is then introduced, representing indistinguishability of Q-sets by a L -observer. Based on = L , a notion of L -bisimulation ≃ L will formalise indistinguishability of processes by a L -observer.

Formally, a queue s : h is L -observable if it contains some message with a level in L . Then two Q-sets are L -equal if their L -observable queues have the same names and contain the same messages with a level in L . This equality is based on a Lprojection 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. 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 .
The idea of L -bisimulation is to test processes by running them in conjunction with L -equal queues. Now, when testing processes with queues we cannot allow arbitrary queues, otherwise we could get insecurity for 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, tr✉❡ ⊥ .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, tr✉❡ ⊥ )} > < P , / 0 > -→
Hence a L -observer with L = {⊥} would detect an insecurity by looking at the resulting Q-sets {s : (1, 2, tr✉❡ ⊥ )} = {⊥} / 0. A natural requirement is that the Q-sets always 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 which occurs in P has a corresponding queue in H. We use fsn(P) to denote the set of free session names which occur in P.

Definition 5.4 A configuration P, H is saturated if P does not contain restrictions of session names and all 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 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 is initial if the process is a closed user process, and the Q-set is empty.

Definition 5.6 (Reachable configurations)

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

RR n°7368

Lemma 1 A reachable configuration is saturated.

A dual phenomenon happens with inputs. For example if

Q = s[2]?(1, x ⊥ ).0, H 1 = {s : (1, 2, tr✉❡ ⊥ )}, H 2 = {s : (1, 2, tr✉❡ ⊤ ) • (1, 2, tr✉❡ ⊥ )} we have < Q , H 1 >-→< 0 , {s : ε} >, while < Q , H 2 > -→. Note that H 1 = {⊥} H 2 and {s : ε} = {⊥} H 2 .
The problem here is that the top level message is transparent for the {⊥}-equality, but it prevents the process from reading the bottom level message. Note that the problem comes from the fact that both messages have the same receiver and the same sender, since for example if

H 3 = {s : (3, 2, tr✉❡ ⊤ ) • (1, 2, tr✉❡ ⊥ )} then < Q , H 3 >-→< 0 , {s : (3, 2, tr✉❡ ⊤ )} >,
thanks to the structural equivalence on queues defined in Table 4.

Our way out for this problem is to ask that the security levels of messages with the same sender and common receivers never decrease along a sequence. In this way we allow the Q-sets H 1 and H 3 , but forbid H 2 . More formally:

Definition 5.7 A queue is monotone if lev ↓ (ϑ 1 ) ≤ lev ↓ (ϑ 2 ) whenever the message (p, Π 1 , ϑ 1 ) precedes the message (p, Π 2 , ϑ 2 ) in the queue and Π 1 ∩ Π 2 = / 0. A Q-set is monotone if it contains only monotone queues.
Since a queue can contain the same message more than once, a message can precede an identical message. Also, it may be that each of two messages precedes the other, since an occurrence of one of them may be placed between two occurrences of the other. Note that in this case monotonicity implies that the two messages have the same level.

Notice that monotonicity is not preserved by reduction, since for example

< s[1]! 2, tr✉❡ ⊤ .s[1]! 2, tr✉❡ ⊥ .0 , {s : ε} >-→ * < 0 , {s : (1, 2, tr✉❡ ⊤ )•(1, 2, tr✉❡ ⊥ )} >
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, tr✉❡ ⊤ .α! 2, tr✉❡ ⊥ .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 the process a [START_REF] Bettini | Global Progress in Dynamically Interleaved Multiparty Sessions[END_REF](β ).β ?(1, x ⊤ ).β ?(1, y ⊥ ).0, since a high input will not be allowed to be followed by a low action, as will be explained in detail in the next section. In particular, the process s[1]! 2, tr✉❡ ⊤ .s[1]! 2, tr✉❡ ⊥ .0 will also 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 the desired process bisimulation. A relation on processes is a L -bisimulation if, whenever two related processes are coupled with L -equal monotone Q-sets yielding saturated configurations, both the relation and the L -equality of Q-sets are preserved by execution: RR n°7368 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 onestep transition. If it is a name, it may either be a service name a ℓ (in case of extrusion of the private service a ℓ ) or a fresh session name s (if the last applied rule is [Link]), and in the last 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.

Security is now defined, as usual, to be the reflexive kernel of ≃ L : Definition 5.9 (L -Security)

A process P is L -secure if P ≃ L P.
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 >.

Examples of Information Flow Security in Sessions

In this section we illustrate the various kinds of flow that can occur in our calculus, through 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 in all other objects. In queues, we will use v ℓ as a shorthand for v ℓ↓ℓ . For the sake of simplicity, we assume here just two security levels ⊥ and ⊤ (also called low and high).

In all examples, we suppose

H 1 = {s : (1, 2, tr✉❡ ⊤ )} and H 2 = {s : (1, 2, ❢❛•s❡ ⊤ )}.

High input should not be followed by low actions

A simple example of insecure flow, which is not specific to our calculus but arises in all process calculi with values and a conditional construct, is the following (assuming session s has four participants):

s[2]?(1, x ⊤ ).✐❢ x ⊤ t❤❡♥ s[2]! 3, tr✉❡ ⊤ .0 ❡•s❡ 0 | s[3]?(2, z ⊤ ).s[3]! 4, tr✉❡ ⊥ .0 | s[4]?(3, y ⊥ ).0
This process is insecure because, depending on the high value received for x ⊤ on channel s [START_REF] Bettini | Global Progress in Dynamically Interleaved Multiparty Sessions[END_REF], that is, on whether the Q-set is H 1 or H 2 , the low value tr✉❡ ⊥ will be emitted or not on channel s [START_REF] Bhargavan | Cryptographic Protocol Synthesis and Verification for Multiparty Sessions[END_REF], leading to

H ′ 1 = {s : (3, 4, tr✉❡ ⊥ )} = L H ′ 2 = {s : ε} if L = {⊥}.
This shows that a high input should not be followed by a low output. Note that the reverse is not true, since output is not blocking: if we swapped the polarities of input and output in the third participant (and adjusted them accordingly in the other participants), then the resulting process would be secure.

Let us point out that this process is not typable in a classical session type system, since the session types of the conditional branches are not the same (as we shall see in the next section, this is a classical requirement in session types). However, it would become typable if the second branch of the conditional were replaced by the deadlocked process (νb)b [START_REF] Almeida Matos | On Declassification and the Non-Disclosure Policy[END_REF](β 1 ).s[2]! 3, tr✉❡ ⊤ .0. The expert reader will notice that by adding to our type system the interaction typing of [START_REF] Bettini | Global Progress in Dynamically Interleaved Multiparty Sessions[END_REF] (which enforces global progress) we would rule out also this second process. On the other hand, the interaction typing does not prevent deadlocks due to inverse session calls, as for instance:

b[2] | b[1](β 1 ).c[1](γ 1 ).s[2]! 3, tr✉❡ ⊤ .0 c[2] | c[2](γ 2 ).b[2](β 2 ).0
Clearly, this deadlock could be used to implement the insecure flow in our example.

Need for levels on services.

Consider the following process:

s[2]?(1, x ⊤ ).✐❢ x ⊤ t❤❡♥ b[2] ❡•s❡ 0 | b[1](β 1 ).β 1 ! 2, tr✉❡ ⊥ .0 | b[2](β 2 ).β 2 ?(1, y ⊥ ).0
This process is insecure because, depending on the high value received for x ⊤ , it will initiate or not a session on service b, which performs a low value exchange. To rule out this kind of leak we annotate service names with security levels which 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 appears in the branch of a ⊤-conditional, and hence it will not be allowed to perform the exchange of the value tr✉❡ ⊥ .

Need for levels on selection and branching

Consider the following process:

s[2]?(1, x ⊤ ).✐❢ x ⊤ t❤❡♥ s[2] ⊕ 3, λ .0 ❡•s❡ s[2] ⊕ 3, λ ′ .0 | s[3]&(2, {λ : s[3]! 4, tr✉❡ ⊥ .0, λ ′ : s[3]! 4, ❢❛•s❡ ⊥ .0}) | s[4]?(3, y ⊥ ).0
This process is insecure because a selection in one participant, which depends on a high value, causes the corresponding branching participant to emit two different low values. 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 branches.

Need for levels on delegated channels.

Consider the following process:

s[2]?(1, x ⊤ ).✐❢ x ⊤ t❤❡♥ s[2]! 3, s ′ [1] .s[2]! 4, s ′′ [1] .0 ❡•s❡ s[2]! 3, s ′′ [1] .s[2]! 4, s ′ [1] .0 | s[3]?((2, η)).η! 2, tr✉❡ ⊥ .0 | s[4]?((2, η ′ )).η ′ ! 2, ❢❛•s❡ ⊥ .0 | s ′ [2]?(1, x ⊥ ).0 | s ′′ [2]?(1, y ⊥ ).0
This process is insecure because, depending on the high value received for x ⊤ , the participants 3 and 4 of s will be delegated to participate in sessions s ′ and s ′′ , or viceversa, feeding the queues of s ′ and s ′′ with different low values. 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 level and their declassified level. The reason for recording also the declassified 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 5.2). 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 ℓ↓ℓ ′ , λ ℓ or s[p] ℓ .

Examples of secure processes

It is easy to check that both the processes P = s[1]! 2, tr✉❡ ⊤ .s[1]! 2, tr✉❡ ⊥ .0 and Q = s [START_REF] Bettini | Global Progress in Dynamically Interleaved Multiparty Sessions[END_REF]?(1, x ⊤ ).s [START_REF] Bettini | Global Progress in Dynamically Interleaved Multiparty Sessions[END_REF]?(1, y ⊥ ).0 are secure, as well as their parallel composition P | Q. We let the reader verify that our C, S, B process of Section 4.1 is also 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 | ❡♥❞ RR n°7368
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 {q}. 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 ) 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.3. Recursive types are considered modulo fold/unfold. We say that ! Π, S ℓ↓ℓ ′ , ! Π, L, G ℓ , ! ℓ q, T , ?(p, S ℓ↓ℓ ′ ), ?(Π, 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
) 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 : 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) 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.

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):

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 ℓ : -(respectively Γ, a ℓ : L, G ℓ ′ and Γ, X : S ℓ T ) only if
x ℓ ′′ (respectively a ℓ ′′ and X) does not belong to the domain of Γ, that is, we don't want Γ to contain the same variable or service name with two different security levels.

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 Γ:

Γ ⊢ tr✉❡ ℓ , ❢❛•s❡ ℓ : ❜♦♦• ℓ Γ, u : S ℓ ⊢ u : S ℓ ⌊NAME⌋
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.

Rule ⌊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⌋.

Γ ⊢ ℓ P ⊲ ∆ ℓ ′ ≤ ℓ ⌊SUBS⌋ Γ ⊢ ℓ ′ P ⊲ ∆ ∆ ❡♥❞ only ⌊INACT⌋ Γ ⊢ ⊤ 0 ⊲ ∆ Γ ⊢ ℓ P ⊲ ∆ Γ ⊢ ℓ Q ⊲ ∆ ′ ⌊CONC⌋ Γ ⊢ ℓ P | Q ⊲ ∆, ∆ ′ Γ ⊢ e : ❜♦♦• ℓ Γ ⊢ ℓ P ⊲ ∆ Γ ⊢ ℓ Q ⊲ ∆ ⌊IF⌋ Γ ⊢ ℓ ✐❢ e t❤❡♥ P ❡•s❡ Q ⊲ ∆ Γ, a ℓ : L, G ℓ ⊢ ℓ ′ P ⊲ ∆ ⌊NRES⌋ Γ ⊢ ℓ ′ (ν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 Γ ⊢ ℓ P ⊲ ∆, α : G ↾ p ⌊MACC⌋ Γ, u : L, G ℓ ⊢ ℓ u[p](α).P ⊲ ∆ Γ ⊢ e : S ℓ Γ ⊢ ℓ ′′ P ⊲ ∆, c : T ℓ ′′ ≤ ℓ ′ ≤ ℓ 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 )
Table 8: Typing rules for processes.

RR n°7368

⌊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 as the tested expression. So the level of the conditional is the level of the tested expression, which cannot be modified, while process P and Q could also have higher levels.

⌊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.

⌊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, tr✉❡ ⊤ .0 | a ⊤ [2](α 2 ).α 2 ?(1, x ⊤ ).✐❢ x ⊤ t❤❡♥ b⊤ [2] ❡•s❡ 0 | b ⊤ [1](β 1 ).c ⊥ [1](γ 1 ).γ 1 ! 2, tr✉❡ ⊥ .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. 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 both the process B and the session b between S and 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 ∈ ∆ and τ 1 ∈ {S ℓ 1 ↓ℓ 1 , L 1 , G 1 ℓ , ? ℓ (p 1 , T 1 )} and τ 2 ∈ {S ℓ 2 ↓ℓ ′ 2 , L 2 , G 2 ℓ ′ , ? ℓ ′ (p 2 , T 2 )}. If τ 1 precedes τ 2 in T , 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 :! ⊥ 1, T ; ? ⊥ (1, T ′ ); & ⊥ (1, {♦❦ : ❡♥❞,❦♦ : ❡♥❞})} where T =?(1, ◆✉♠❜❡r ⊤↓⊥ ); ⊕ ⊥ 1, {♦❦ :! 1, ❙tr✐♥❣ ⊥↓⊥ ; ❡♥❞,❦♦ : ❡♥❞} T ′ = ⊕ ⊥ 1, {♦❦ :! 1, ❙tr✐♥❣ ⊥↓⊥ ; ❡♥❞,❦♦ : ❡♥❞} RR n°7368

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 ! ℓ Π, T express the communication to all p ∈ Π of a value of type S ℓ declassified to level ℓ ′ , of a service of type L, G ℓ and of a channel of type T with ℓ = M(T ), respectively. 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 (with Typing judgments for queues have the shape

♮ ∈ {!, ! ℓ , ⊕ ℓ } and Z ∈ {T, S ℓ↓ℓ ′ , L, G ℓ , λ }). Γ ⊢ s : h ⊲ Θ ⌊QSEL⌋ Γ ⊢ s : h • (p, Π, λ ℓ ′ ) ⊲ Θ; {s[p] : ⊕ ℓ ′ Π, λ } Γ ⊢ s : h ⊲ Θ Θ ≈ Θ ′ ⌊QCONG⌋ Γ ⊢ s : h ⊲ Θ ′
Γ ⊢ s : h ⊲ Θ ⌊QSINIT⌋ Γ ⊢ / 0 / 0 ⊲ / 0 Γ ⊢ Σ H ⊲ Θ Γ ⊢ s : h ⊲ Θ ′ ⌊QSUNION⌋ Γ ⊢ Σ,s H ∪ {s : h} ⊲ Θ, Θ ′ Table 11: Typing rules for Q-sets.
where Θ is a queue environment associating message types with channels:

Θ ::= / 0 | Θ, 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. The composition ";" of queue environments is defined by:

Θ; Θ ′ = {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 ′ ∈ Θ ′ }
Rule ⌊QCONG⌋ allows a queue to be typed with equivalent queue environments.

Example: we can derive ⊢ s : (2, {1, 3}, ♦❦ ⊤ ) ⊲ {s [2] : ⊕ ⊤ {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.

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}, ❙tr✐♥❣ ⊤ ; ?(3, ◆✉♠❜❡r ⊥ ); ❡♥❞
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.2 The configuration type of a channel s[p] in a configuration environment

< ∆ ⋄ Θ > (notation < ∆ ⋄ Θ > (s[p]) ) is defined by: < ∆ ⋄ Θ > (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] ∈ dom(Θ) and s[p] : T ∈ ∆, ❡♥❞ otherwise.
Configuration types can be projected on a participant q. Definition 7.3 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. (⊕ ℓ Π, {λ 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.T ) ↾ q = µt.(T ↾ q) 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.4 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 RR n°7368 Γ ⊢ ℓ 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 ⊲ < ∆ ⋄ Θ >
Table 12: Typing rules for configurations.

The above definitions are needed to state coherence of 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.5 A configuration environment < ∆ ⋄ Θ > is coherent if s[p] ∈ dom(∆) ∪ dom(Θ) and s[q] ∈ dom(∆) ∪ dom(Θ) imply < ∆ ⋄ Θ > (s[p]) ↾ q ⊲⊳ < ∆ ⋄ Θ > (s[q]) ↾ p
Typing rules assure that configurations are always typed with coherent environments. 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 and Θ \ s are defined as follows:

• ∆ \ s = {s ′ [p] : T | s ′ [p] ∈ Dom(∆) & s ′ = s} • Θ \ s = {s ′ [p] : T| s ′ [p] ∈ Dom(Θ) & s ′ = s} Proposition 4 If Γ ⊢ Σ C ⊲ < ∆ ⋄ Θ >, then < ∆ ⋄ Θ > is coherent.
Proof. All rules assure that the configuration environments in the conclusions are coherent. Rules ⌊CINIT⌋ and ⌊CPAR⌋ explicitly check this condition. For rule ⌊GSRES⌋, note that the coherence of < ∆ \ s ⋄ Θ \ s > follows easily from the coherence of < ∆ ⋄ Θ >. Let us look back again at the C, S, B example of Section 4.1. Recall the following definitions:

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}) P B = s b [1]! ⊥ 2, s a [2] .✐❢ valid(cc ⊥ ) t❤❡♥ s b [1] ⊕ ⊥ 2, ok .0 ❡•s❡ s b [1] ⊕ ⊥ 2, ko .0
Then we can type the configuration

< P C | s b [2]? ⊥ ((1, η)).P S | s a [2]? ⊤ (1, cc ⊥ ).P B , {s a : (1, 2, ❈r❡❞✐t❈❛r❞ ⊤↓⊥ ), s b : ε} >
by the configuration environment: < {s a [1] : T a,1 , s a [2] : T a,2 , s b [1] : T b,1 , s b [2] : T b,2 } ⋄ {s a [1]

:! 2, ◆✉♠❜❡r ⊤↓⊥ } > RR n°7368
where:

T a,1 = & ⊥ (2, {♦❦ :?(2, ❙tr✐♥❣ ⊥↓⊥ ); ❡♥❞,❦♦ : ❡♥❞}) T a,2 =?(1, ◆✉♠❜❡r ⊤↓⊥ ); ⊕ ⊥ 1, {♦❦ :! 1, ❙tr✐♥❣ ⊥↓⊥ ; ❡♥❞,❦♦ : ❡♥❞} T b,1 =! ⊥ 1, ⊕ ⊥ 1, {♦❦ :! 1, ❙tr✐♥❣ ⊥↓⊥ ; ❡♥❞,❦♦ : ❡♥❞} ; ⊕ ⊥ (2, {♦❦ : ❡♥❞,❦♦ : ❡♥❞}) T b,2 =? ⊥ (1, ⊕ ⊥ 1, {♦❦ :! 1, ❙tr✐♥❣ ⊥↓⊥ ; ❡♥❞,❦♦ : ❡♥❞} ); & ⊥ (1, {♦❦ : ❡♥❞,❦♦ : ❡♥❞}) 7.

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 < ∆ ⋄ Θ > ⇒ < ∆ ′ ⋄ Θ ′ >. Definition 7.6 (Reduction of configuration environments) Let ⇒ be the reflexive and transitive relation on configuration environments generated by:

1. < {s[p] : ! Π, S ℓ↓ℓ ′ ; T } ⋄ Θ > ⇒ < {s[p] : T } ⋄ Θ; {s[p] : ! Π, S ℓ↓ℓ ′ } > 2. < {s[p] : ! Π, L, G ℓ ; T } ⋄ Θ > ⇒ < {s[p] : T } ⋄ Θ; {s[p] : ! Π, L, G ℓ } > 3. < {s[p] : ! ℓ q, T ; T ′ } ⋄ Θ > ⇒ < {s[p] : T ′ } ⋄ Θ; {s[p] : ! ℓ q, T } > 4. < {s[p] : ⊕ ℓ Π, {λ i : T i } i∈I } ⋄ Θ > ⇒ < {s[p] : T j } ⋄ Θ; {s[p] : ⊕ ℓ (Π, λ j )} > 5.
< {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[q] : T ′ } ⋄ Θ > 8. < {s[q] : & ℓ (p, {λ i : T i } i∈I )} ⋄ {s[p] : ⊕ ℓ (q, λ j )}; Θ > ⇒ < {s[q] : T j } ⋄ Θ > 9. < ∆, ∆ ′′ ⋄ Θ > ⇒ < ∆ ′ , ∆ ′′ ⋄ Θ ′ > if < ∆ ⋄ Θ > ⇒ < ∆ ′ ⋄ Θ ′ >
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. 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.

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.

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. By induction on the definition of ⇒ (Definition 7.6).

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) 11.

1. If Γ ⊢ ℓ 0 ⊲ ∆, then ∆ ❡♥❞ only. 2. If Γ ⊢ ℓ P | Q ⊲ ∆, then ∆ = ∆ 1 , ∆ 2 and Γ ⊢ ℓ P ⊲ ∆ 1 and Γ ⊢ ℓ Q ⊲ ∆ 2 . 3. If Γ ⊢ ℓ ✐❢ e t❤❡♥ P ❡•s❡ 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 ⊲ ∆.
If Γ ⊢ ℓ c! ℓ ′ q, c ′ .P ⊲ ∆, then ∆ = ∆ ′ , c : ! ℓ ′ q, T ′ ; T, c ′ : δ ; T ′ Γ ⊢ ℓ P ⊲ ∆ ′ , c : T and ℓ ≤ ℓ ′ .
12. If Γ ⊢ ℓ ′ c? ℓ ((p, α)).P ⊲ ∆, then ∆ = ∆ ′ , c :?(p, T ′ ); T and Γ ⊢ ℓ ′ P ⊲ ∆ ′ , c : T, α : T ′ and ℓ = ℓ ′ .

13. If Γ ⊢ ℓ ′ c ⊕ ℓ Π, λ j .P ⊲ ∆, then ∆ = ∆ ′ , c : ⊕ ℓ Π, {λ i : T i } i∈I and j ∈ I and Γ ⊢ ℓ ′ P ⊲ ∆ ′ , c : T j and ℓ = ℓ ′ .

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 ℓ = ℓ ′ .
Lemma 7 (Inversion Lemma for Queues and Q-sets)

1. If Γ ⊢ s : ε ⊲Θ, then Θ = / 0. 2. If Γ ⊢ s : h • (p, Π, v ℓ↓ℓ ′ ) ⊲ Θ, then Θ = Θ ′ ; {s[p] : ! Π, S ℓ↓ℓ ′ } and Γ ⊢ s : h ⊲ Θ ′ and Γ ⊢ v ℓ : S ℓ . 3. If Γ ⊢ s : h • (p, Π, a ℓ ) ⊲ Θ, then Θ = Θ ′ ; {s[p] : ! Π, L, G ℓ }, Γ ⊢ s : h ⊲ Θ ′ and Γ ⊢ a : L, G ℓ . 4. If Γ ⊢ s : h • (p, q, s ′ [p ′ ]) ⊲ Θ, then Θ = Θ ′ ; s ′ [p ′ ] : T ; {s[p] : ! q, T } and Γ ⊢ s : h ⊲ Θ ′ . 5. If Γ ⊢ s : h • (p, Π, λ ℓ ) ⊲ Θ; {s[p] : ⊕ ℓ Π, λ }, then Θ = Θ ′ ; {s[p] : ⊕ ℓ Π, λ } and Γ ⊢ s : h ⊲ Θ ′ . 6. If Γ ⊢ Σ / 0 ⊲ Θ, then Σ = Θ = / 0. 7. 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. 2. If Γ ⊢ Σ C 1 C 2 ⊲ < ∆ ⋄ Θ >, then Σ = Σ 1 ∪ Σ 2 and ∆ = ∆ 1 , ∆ 2 and Θ = Θ 1 , Θ 2 and Γ ⊢ Σ 1 C 1 ⊲ < ∆ 1 ⋄ Θ 1 > and Γ ⊢ Σ 2 C 2 ⊲ < ∆ 2 ⋄ Θ 2 > and Σ 1 ∩ Σ 2 = / 0 and < ∆ ⋄ Θ > is coherent. 3. If Γ ⊢ Σ (νs)C ⊲ < ∆ ⋄ Θ >, then Σ = Σ ′ \s and ∆ = ∆ ′ \ s and Θ = Θ ′ \ s and Γ ⊢ Σ ′ C ⊲ < ∆ ′ ⋄ Θ ′ >. 4. If Γ ⊢ Σ (νa ℓ )C ⊲ < ∆ ⋄ Θ >, then Γ, a ℓ : L, G ℓ ⊢ Σ C ⊲ < ∆ ⋄ Θ >.
The next lemma characterises the types due to messages occurring as heads of queues.

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

Lemma 9 1. If Γ ⊢ s : (p, Π, v ℓ↓ℓ ′ ) • h ⊲ Θ, then Θ = {s[p] : ! Π, S ℓ↓ℓ ′ }; Θ ′ and Γ ⊢ s : h ⊲ Θ ′ and Γ ⊢ v ℓ : S ℓ . 2. If Γ ⊢ s : (p, Π, a ℓ ) • h ⊲ Θ, then Θ = {s[p] : ! Π, L, G ℓ }; Θ ′ and Γ ⊢ s : h ⊲ Θ ′ and Γ ⊢ a ℓ : L, G ℓ . 3. If Γ ⊢ s : (p, q, s ′ [p ′ ]) • h ⊲ Θ, then Θ = {s[p] : ! q, T }; Θ ′ and Γ ⊢ s : h ⊲ Θ ′ and s ′ [p ′ ] : T ∈ Θ. 4. If Γ ⊢ s : (p, Π, λ ) • h ⊲ Θ, then Θ = {s[p] : ⊕ ℓ Π, λ }; Θ ′ and Γ ⊢ s : h ⊲ Θ ′ .
Theorem 10 (Type Preservation under Equivalence)

If Γ ⊢ Σ C ⊲ < ∆ ⋄ Θ > and C ≡ C ′ , then Γ ⊢ Σ C ′ ⊲ < ∆ ⋄ Θ >.
Proof. By induction on the definition of ≡.

Lemma 11 (Substitution Lemma)

1. If Γ ⊢ v ℓ : S ℓ and Γ, x ℓ ′ : S ℓ ′ ⊢ ℓ ′′ P ⊲ ∆ and ℓ ′′ ≤ ℓ ′ ≤ ℓ, then Γ ⊢ ℓ ′′ P{v ℓ ′ /x ℓ ′ } ⊲ ∆. 2. If Γ ⊢ a ℓ : L, G ℓ and Γ, x ℓ : L, G ℓ ⊢ ℓ ′′ P ⊲ ∆ and ℓ ′′ ≤ ℓ, then Γ ⊢ ℓ ′′ P{a ℓ /x ℓ } ⊲ ∆. 3. If Γ ⊢ ℓ P ⊲ ∆, α : T , then Γ ⊢ ℓ P{s[p]/α} ⊲ ∆, s[p] : T .

RR n°7368

Proof. By standard induction on P.

Theorem 12 (Subject Reduction) Suppose Γ ⊢ Σ C ⊲ < ∆ ⋄ Θ > and C -→ * C ′ . Then Γ ⊢ Σ C ′ ⊲ < ∆ ′ ⋄ Θ ′ > with < ∆ ⋄ Θ > ⇒ < ∆ ′ ⋄ Θ ′ >.
Proof. We prove the simpler statement (of which Theorem 12 is an immediate corollary):

If Γ ⊢ Σ C ⊲ < ∆⋄Θ > and C -→ C ′ , then Γ ⊢ Σ C ′ ⊲ < ∆ ′ ⋄Θ ′ > with < ∆ ⋄ Θ > ⇒ < ∆ ′ ⋄ Θ ′ >.
By induction on the derivation of C -→ C ′ , with a case analysis on the final rule. We only consider some paradigmatic cases.

[Link]

a ℓ [1](α 1 ).P 1 | ... | a ℓ [n](α n ).P n | āℓ [n] -→ (νs) < P 1 {s[1]/α 1 } | ... | P n {s[n]/α n } , s : ε > By hypothesis we have Γ ⊢ Σ < a ℓ [1](α 1 ).P 1 | ... | a ℓ [n](α n ).P n | āℓ [n] , / 0 > ⊲ < ∆ ⋄ Θ >
which implies by Lemma 8(1)

Γ ⊢ ℓ ′ a ℓ [1](α 1 ).P 1 | ... | a ℓ [n](α n ).P n | āℓ [n] ⊲ ∆ (1)
Γ ⊢ Σ / 0 ⊲ Θ (2)
From (2) by Lemma 7(6) we get Σ = Θ = / 0.

From (1) by Lemma 6(2) we get

∆ = n i=1 ∆ i ∪ ∆ ′ and Γ ⊢ ℓ ′ a ℓ [i](α i ).P i ⊲ ∆ i (1 ≤ i ≤ n) (3) Γ ⊢ ℓ ′ āℓ [n] ⊲ ∆ ′ (4)
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 rule ⌊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) RR n°7368
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

< ∆ ⋄ Θ > ⇒ < ∆ ⋄ Θ >. [Send] < s[p]! ℓ ′ Π, e .P , s : h >-→< P , s : h • (p, Π, v ℓ↓ℓ ′ ) > (e ↓ v ℓ )
By hypothesis we have

Γ ⊢ Σ < s[p]! ℓ ′ Π, e .P , s : h > ⊲ < ∆ ⋄ Θ > which implies by Lemma 8(1) Γ ⊢ ℓ ′′ s[p]! ℓ ′ Π, e .P ⊲ ∆ (8)
Γ ⊢ Σ s : h ⊲ Θ (9)
From ( 8) by Lemma 6(9) we get 1. either ∆ = ∆ ′ , s[p] : ! Π, S ℓ 0 ↓ℓ ′ ; T and ℓ ′′ ≤ ℓ ′ ≤ ℓ 0 and Γ ⊢ e : S ℓ 0 (10)

Γ ⊢ ℓ ′′ P ⊲ ∆ ′ , s[p] : T (11)
From [START_REF] Dezani-Ciancaglini | Sessions and Session Types: an Overview[END_REF] 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( 6) and ( 7) 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 ( 11) and ( 14) we derive

Γ ⊢ {s} < P , s : h • (p, Π, v ℓ↓ℓ ′ ) > ⊲ < ∆ ′ , s[p] : T ⋄ Θ; {s[p] : ! Π, S ℓ↓ℓ ′ } >
This concludes the proof, since

< ∆ ′ , {s[p] : ! Π, S ℓ↓ℓ ′ ; T } ⋄ Θ > ⇒ < ∆ ′ , s[p] : T ⋄ Θ; {s[p] : ! Π, S ℓ↓ℓ ′ } > RR n°7368 2. or ∆ = ∆ ′ , c : ! Π, L, G ℓ 0 ; T and ℓ ′′ ≤ ℓ ′ = ℓ 0 and Γ ⊢ e : L, G ℓ 0 (15) Γ ⊢ ℓ ′′ P ⊲ ∆ ′ , c : T (16)
From ( 15) by subject reduction on expressions we have:

Γ ⊢ v ℓ : L, G ℓ 0 ( 17
)
which implies ℓ = ℓ 0 by our assumption on the typing of values. From ( 9) by Lemma 7( 6) and ( 7) 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 ( 11) and ( 19) 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)
From ( 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( 6) and [START_REF] Boudol | Access Control and Declassification[END_REF] we get Σ = {s} and

Γ ⊢ s : (p, q, v ℓ↓ℓ ′ ) • h ⊲ Θ which implies by Lemma 9(1) Γ ⊢ s : h ⊲ Θ ′ and : RR n°7368 (a) either Θ = {s[p] : ! Π, S ℓ↓ℓ ′ }; Θ ′ and Γ ⊢ v ℓ : S ℓ 0 ( 23
) (b) or Θ = {s[p] : ! Π, L 0 , G ℓ 0 }; Θ ′ and Γ ⊢ v ℓ : L 0 , G ℓ 0 ( 24
)
The coherence of < ∆ ⋄ Θ > gives S = S 0 , and therefore from ( 22) and ( 23) by Lemma 11(1) 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

Γ ⊢ {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 ⋄ Θ ′ > 2
Γ ⊢ ℓ ′ 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 ⋄ Θ ′ > RR n°7368

Soundness for Access Control

To prove that our type system ensures access control it is convenient to distinguish two classes of operational rules: computational rules, which apply to a redex and correspond to an actual computation step (these are the first nine rules in Table 5), and contextual rules, which allow a term to be reduced within a static context (these are the last three rules in Table 5) [START_REF] Pierce | Types and Programming Languages[END_REF]. 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:

J(T ) = J(T ) if T = T; T or T = T ⊥ if T = T Lemma 15 Let C 0 be an initial configuration, and suppose Γ ⊢ / 0 C 0 ⊲ < / 0 ⋄ / 0 > for some standard environment Γ such that a ℓ : L, G ℓ ∈ Γ. If C 0 -→ * (νs)C and s is an a-generated queue of C, then, assuming Γ ⊢ {s} C ⊲ < ∆ ⋄ Θ >, it holds that J(< ∆ ⋄ Θ > (s[p])) ≤ J(G ↾ p) for each participant p ∈ dom(L).
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 <

∆ ⋄ Θ > (s[p]) = G ↾ p.
Otherwise let C n-1 = (νs)C ′ . By Theorem 12 and Lemma 8(3), we have Γ ⊢ {s} C ′ ⊲ < ∆ ′ ⋄ Θ ′ > for some ∆ ′ , Θ ′ . Then, by induction, J(< ∆ ′ ⋄ Θ ′ > (s[p])) ≤ J(G ↾ p). 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]. If the last rule is one of the output rules [Send], [Deleg] or [Sel], then < ∆⋄Θ > is obtained from < ∆ ′ ⋄Θ ′ > by shifting an element of ∆ ′ to Θ ′ , and thus J(< ∆ ⋄ Θ >) = J(< ∆ ′ ⋄ Θ ′ >). If the last rule applied is one of the input rules [Rcv], [Srec] or [Branch], then an input type is erased from ∆ ′ and a message type is erased from Θ ′ , hence J(< ∆ ⋄ Θ >) ≤ J(< ∆ ′ ⋄ Θ ′ >) and we may conclude.

Theorem 16 (Access Control) Let C 0 be an initial configuration, and suppose that Γ ⊢ / 0 C 0 ⊲ < / 0 ⋄ / 0 > for some standard environment Γ such that a ℓ : L, G ℓ ∈ Γ. If C 0 -→ * (νs)C, 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 ℓ↓ℓ ′ , 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.2) we have then ℓ ≤ J(< ∆ ⋄ Θ > (s[q])) and by Lemma 15 we get J(< ∆ ⋄ Θ > (s[q])) ≤ J(G ↾ q), where G is the global type associated with the service a. Then we may conclude, since the well-formedness of safety global types implies J(G ↾ q) ≤ L(q).

Soundness for Noninterference

We start by showing the confinement lemma, which says that a process of level ℓ can only add or remove messages of level greater than or equal to ℓ in the queues. Note that, for any level ℓ ∈ S , the complement L = {ℓ ′ | ℓ ≤ ℓ ′ } of the upward-closure of ℓ is a downward-closed set containing all levels lower than or incomparable with ℓ.

Lemma 17 (Confinement)

Let Γ ⊢ ℓ P ⊲ ∆ and L = {ℓ ′ | ℓ ≤ ℓ ′ }. Then, for any Q-set H such that P, H is typable: P, H -→ * (ν r) P ′ , H ′ implies H = L H ′ .

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. We consider the most interesting base cases, leaving out the inductive cases which are easy.

• [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 , ℓ 2 , P ′′ such that ℓ ≤ ℓ 2 ≤ ℓ 1 and P = s[q]? ℓ 1 (p, x ℓ 2 ).P ′′ . Then P ′ = P ′′ {v ℓ 2 /x ℓ 2 } and the reduction is: < s[q]? ℓ 1 (p, x ℓ 2 ).P ′′ , s : (p, q, v ℓ 1 ↓ℓ 2 ) • h >-→< P ′′ {v ℓ 2 /x ℓ 2 } , s : h > As in the previous case, ℓ ≤ ℓ 2 implies ℓ 2 / ∈ L . Hence s : (p, q, v ℓ 1 ↓ℓ 2 )•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:

< 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.

RR n°7368 9 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 does not prevent deadlocks due to inverse session calls. We plan to study a strengthening of interaction typing that would rule out also this kind of deadlock.

The form of declassification considered in this work is admittedly quite simple. However, it already illustrates the connection between declassification and access control, since a declassified value may only be received by a participant whose level is greater than or equal to the original level of the value. This means that declassification is constrained by the access control policy, as in [START_REF] Boudol | Access Control and Declassification[END_REF]. We plan to extend declassification also to data which are not received from another participant, by allowing declassification of a tested expression, as in this variant of the B process of our example in Section 2: B ′ = . . . ✐❢ {cc ⊤ = secret ⊤ } ⊤↓⊥ t❤❡♥ β 1 ⊕ ⊥ 2, ok .0 ❡•s❡ β 1 ⊕ ⊥ 2, ko .0 Again, this declassification would be controlled by requiring B ′ to have level ⊤.

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 to require saturation of Q-sets, since an empty Q-set would no longer be L -equal to a Q-set which contains an empty queue where messages of levels belonging to L can be put. However, notice that this would require adding security levels on queues, since the empty queue that is created when initiating a session corresponding to a high service should not be observable. This is why we chose a simpler (and weaker) form of observation here.

Note finally that, since our syntax is annotated with security levels, it would be possible to equip our calculus with a monitored semantics as in [START_REF] Boudol | Secure Information Flow as a Safety Property[END_REF]. The induced notion of safety would be less restrictive than typability since it would allow, for instance, a high conditional with a low branch provided this branch is never taken.

2. S δ S → B : T 3 .

 3 C → S : ◆✉♠❜❡r ⊤↓⊥ 4. S δ B → S : T ′ 5. B → S : {♦❦ : ❡♥❞,❦♦ : ❡♥❞} 6. S → C : {♦❦ : S → C : ❙tr✐♥❣ ⊥ ; ❡♥❞,❦♦ : ❡♥❞}

7 . 8 .

 78 If Γ ⊢ ℓ ū[n] ⊲ ∆, then Γ = Γ ′ , u : L, G ℓ and dom(L)={1, . . . , n} and ∆ = / 0. 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 ℓ = ℓ ′′ .

  . or ∆ = ∆ ′ , c :?(p, L, G ℓ ); T and ℓ = ℓ ′ and Γ, x ℓ : L, G ℓ ⊢ ℓ ′′ P ⊲ ∆ ′ , c : T (27) From (21) by Lemma 7(6) and (7) we get Σ = {s} and Γ ⊢ s : (p, q, v ℓ↓ℓ ′ ) • h ⊲ Θ which implies by Lemma 9(1) implies Γ ⊢ s : h ⊲ Θ ′ and either Θ = {s[p] : ! Π, S ℓ↓ℓ ′ }; Θ ′ and (23) or Θ = {s[p] : ! Π, L 0 , G ℓ 0 }; Θ ′ and (24). The coherence of < ∆ ⋄ Θ > gives L 0 = L and G 0 = G, and therefore from (27) and (23) by Lemma 11(2) we have

Table 2 :

 2 Global types of the C, S, B example.

Table 10 :

 10 Typing rules for single queues.

RR n°7368

⌊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 : T j j ∈ I ℓ ≤ i∈I

• ♮ Π, Z ; ♮ ′ Π ′ , Z ; T ≈ ♮ ′ Π ′ , Z ; ♮ Π, Z ; T if Π ∩ Π ′ = / 0 • ♮ Π, Z ; 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 }

Notice that in the definition of J(T ) we cannot omit ℓ in the cases of selection and branching, because we could have M(T ) ≤ J(T ). For example M(µt.t) = ⊤ and J(µt.t) = ⊥.

Acknowledgments We would like to thank Nobuko Yoshida for her encouragement to engage in this work, and the anonymous referees of [8] for helpful feedback.

Properties of T-reachable configurations

The definition of coherence (Definition 7.5) 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)

A configuration C is T-reachable if there is a typable initial configuration C 0 such that C 0 -→ * C.

Lemma 13 If (ν s)C is a T-reachable configuration and C does not contain session restrictions, then Γ ⊢ { s} C ⊲ < ∆⋄Θ > for some Γ, ∆, Θ and the configuration environment < ∆ ⋄ Θ > is complete.

Proof. The proof is by induction on the length n of the reduction sequence C 0 -→ * (ν s)C, and then by induction on the inference of the last transition. The basic case C 0 = (ν s)C is trivial.

Suppose that C 0 -→ * (ν s′ )C n-1 -→ (ν s)C. By Theorem 12 and Lemma 8(3) we get Γ ⊢ { s′ } C n-1 ⊲ < ∆ n-1 ⋄ Θ n-1 > for some Γ, ∆ n-1 , Θ n-1 . 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]. If the last rule is one of the output rules

then if an input type for s[p] involving q, for instance ?(q, S ℓ↓ℓ ′ ), is erased from ∆ n-1 , a matching message type ! p, S ℓ↓ℓ ′ for s[q] is erased at the same time from Θ n-1 , and thus we may conclude using induction.

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

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 .

• [Label] In this case, since Γ ⊢ ℓ P ⊲ ∆ is deduced by the typing rule ⌊SEL⌋, we have P = s[p] ⊕ ℓ Π, λ .P ′ and the reduction is:

Again, since ℓ / ∈ L , we may conclude that s : h = L s : h • (p, Π, λ ℓ ).

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.

On the set of typable processes, we call syntactic L -highness the complement of non L -boundedness, which amounts to typability with a level not belonging to L . A closely related property is that of semantic L -highness, the property of processes that do not manipulate any messages of level in L during their execution. Formally:

The set of semantically high processes with respect to L , denoted H L s❡♠ , is the largest set such that P ∈ H L s❡♠ implies:

Note that a semantically L -high process is not necessarily syntactically L -high. For instance a conditional whose condition is always true and whose first branch is of level ⊤ will be semantically L -high for all downward-closed L ⊂ S (proper inclusion) even if its second branch could emit some message of level ⊥. On the other hand syntactic L -highness implies semantic L -highness, as stated next.

Lemma 18 (Syntactic L -highness implies semantic L -highness) Let Γ ⊢ ℓ P ⊲ ∆ for some ℓ ∈ L . Then P ∈ H L s❡♠ . Proof. If Γ ⊢ ℓ P ⊲ ∆ for some ℓ ∈ L then, by the Confinement lemma (Lemma 17), P may only add or remove Q-set messages of level ℓ ′ such that ℓ ≤ ℓ ′ . This means that the Q-set remains L -equal to itself during the whole execution.

Lemma 19 (Security of semantically L -high processes)

Let P ∈ H L s❡♠ . Then P ≃ L P.

Proof. We show that the relation

Then we may choose the empty move as the matching move for (ν r) P 2 , H 2 , given that

We next define the bisimulation relation that will be used in the proof of soundness.

RR n°7368

Definition 8.5 (Bisimulation for soundness proof) Given a downward-closed set of security levels L ⊆ S , the relation R L Γ on processes is defined inductively as follows:

2 and one of the following holds:

p , and ∀p, ∀ s fresh, Q

(1)

p {s[p]/α p };

for every j ∈ 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.

j follows from one of the previous cases (including the case of semantically high processes).

Theorem 20 (Noninterference) If P is typable, then P ≃ L P for all down-closed L .

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 definition (Clause 1). We proceed by induction on the definition of R L Γ . Suppose that Γ ⊢ ℓ 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

We distinguish two cases: i) Both P i are not L -bounded in Γ;

ii) Both P i are L -bounded in Γ;

Suppose that the P i 's are not L -bounded. Then by Lemma 18 we have P i ∈ H L s❡♠ , for i = 1, 2, and thus the move < P 1 , H 1 >-→ (ν r) < P ′ 1 , H ′ 1 > can be matched by the empty move of < P 2 , H 2 >, where H ′ 1 = L H 1 = L H 2 , and P ′ 1 ∈ H L s❡♠ implies P ′ 1 R L Γ P 2 by Clause i) of Definition 8.5. Suppose now that the P i 's are L -bounded. We consider some interesting cases.

p , then we can only reduce by applying rule [Link], so we get

, and the matching move will be

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

• 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

, by Clauses 12 and 1 of Definition 8.5 we get

and we may conclude using Clause 12.

In the second case we can apply the induction hypothesis to

• If

j follows from one of the previous cases (including the case of semantically high processes), then we have a reduction:

and

and thus we may conclude using 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.

RR n°7368

A 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

Semantics: some reductions [2]? ⊥ ((1, η)).P S | s a [2]? ⊤ (1, cc ⊥ ).P B , {s a : (1, 2, ❈r❡❞✐t❈❛r❞ ⊤↓⊥ ), s b : ε} >)

where the continuation processes P C , P S , P B are defined by:

Typing of processes

The following process P is a fragment of the component S:

Then we can derive:

where

Typing of configurations

We can type the configuration

by the configuration environment:

< {s a [1] : T a,1 , s a [2] : T a,2 , s b [1] : T b,1 , s b [2] : T b,2 } ⋄ {s a [1] :! 2, ◆✉♠❜❡r ⊤↓⊥ } > where: