Ivan Gazeau

Tom Chothia

Dominic Duggan

‡ Stevens

Types for Location and Data Security in Cloud Environments

Cloud service providers are often trusted to be genuine, the damage caused by being discovered to be attacking their own customers outweighs any benefits such attacks could reap. On the other hand, it is expected that some cloud service users may be actively malicious. In such an open system, each location may run code which has been developed independently of other locations (and which may be secret). In this paper, we present a typed language which ensures that the access restrictions put on data on a particular device will be observed by all other devices running typed code. Untyped, compromised devices can still interact with typed devices without being able to violate the policies, except in the case when a policy directly places trust in untyped locations. Importantly, our type system does not need a middleware layer or all users to register with a preexisting PKI, and it allows for devices to dynamically create new identities. The confidentiality property guaranteed by the language is defined for any kind of intruder: we consider labeled bisimilarity i.e. an attacker cannot distinguish two scenarios that differ by the change of a protected value. This shows our main result that, for a device that runs well typed code and only places trust in other well typed devices, programming errors cannot cause a data leakage.

Introduction

Organisations commonly trust their cloud providers not to be actively malicious but may still need to verify that the cloud service does not make mistakes and does store their data at particular locations. For example, data protection laws prevent the storage of certain forms of data outside the European Union. In order to ensure compliance, a company policy may require that data from a user's device not be synchronized with a cloud storage provider, unless that provider can certify that the data will not be stored in data centers outside the EU. Such checks against inappropriate storage of data can be costly and time consuming, sometimes leading to organisations not allowing their employees to use cloud services, even though a particular cloud service may be known to be compliant with data handling policies.

This paper presents a language-based approach to dealing with these kinds of scenarios, of ensuring that data can be shared with cloud services while ensuring compliance with policies on data storage. The approach is based on a type system that explicitly models trust between cloud typed), and potentially malicious. These devices are able to use any third-party cloud services, including services used by honest devices. A secure data-sharing system should remain robust to such an intruder. Our security guarantee is that if data is protected with rights that only includes honest principals (i.e., that do not include any principal which is associated to an attacker device), then an attacker cannot learn any information about that data. In this work, we are focused on confidentiality of the data, and do not consider integrity (that data has not been tampered with by attackers). There is a notion of integrity in the sense of trust management underlying our approach: Honest principals identify themselves by their public keys, and these keys are to state access restrictions on data, to specify when a device is allowed to "act for" a principal, and to validate that communication channels are with honest parties trusted to be type-checked and therefore conformant with data-sharing policies. This is reflected in several aspects of the communication API, including the establishment of communication channels, generating new principals and transmitting those principals between devices.

A practical difficulty with expressing security guarantees in this setting is that, as principals can be created dynamically, it is not possible to statically check if a variable has a higher or lower security level than some other variable. Consider the following example:

Example 1 Assume three devices: an honest cloud service with a certified principal p, and two (mobile) devices, an honest device A and a malicious device B. The server code consists of receiving two principal values p 1 and p 2 from the network before it creates two memory locations x 1 and x 2 where x 1 has rights {p, p 1 } while x 2 has right {p, p 2 }. A secure location is defined one which cannot be accessed by the attacker. If we assume that devices A and B send their principal values (public keys) to the server, then depending on which key is received first, either x 1 or x 2 will be considered secure (only accessible by the honest principal and the cloud provider), while the other is explicitly accessible by the attacker. As usual with information flow control type systems, we propagate these access restrictions through the handling of data by the cloud provider and the devices, ensuring that data protected by the right {p, p i }, where p i is the representative for the honest principal.

Therefore, our security property is a posteriori: once the system has created a memory cell corresponding to some variable, if the rights associated to this variable at creation time did not include a principal controlled by the attacker, then there will never be any leak about the contents of this memory cell to the attacker. We argue that such a property is suitable for cloud services to increase users' confidence that their data will not be leaked by the service due to a programming error. Indeed, our system allows us to certify that once some principal creates data, only explicitly authorised principals can obtain information about that data, by statically checking the code that processes that data. Verifying the identity of the principals allowed to access the data, and deciding where to place trust among the principals in a distributed system, is an important consideration. However it properly remains the responsibility of the application written in our language, and a concern which is independent of this type system. Our approach serves to guarantee proper handling of data among honest principals, once an appropriate trust management system has established who is honest.

Our typed language is intended to be a low level language, without high-level notions such as objects and closures. It includes consider references, multi-threading and a realistic application programming interface (API) for distributed communication. Communications can either be through a secure channel mechanism, implementable using a secure transport layer such as TLS for example, or through public connections, in which case any device can connect. The language includes primitives for asymmetric key encryption, since we represent by public keys. "Possessing" a secret key, in the sense that the private key of a public-private key is stored in its memory, allows a device to "act for" the principal that key represents. Our approach is similar in philosophy to the Simple Public Key Infrastructure (SPKI), where principals and public keys are considered as synonymous, rather than linking principals to a separate notion of public key representatives. However, we do not include notions such as delegation that are the central consideration of SPKI, since we explicitly avoid the consideration of trust management, leaving that to applications written using the API that we provide. This also differentiates our approach from frameworks such as JIF and Fabric, that include delegation of authority to principals based on an assumed trust management infrastructure.

Nevertheless, there is a notion at least tangentially relegated to delegation of trust in our framework: In order to allow a device to act for more than one principal, our semantics allows a principal to be created on one device and communicated to another device, where it is registered on the receiver device as one of the principals upon whose behalf that device can access data. For example, a client of a cloud service provider may generate a proxy principal representing that client on the cloud service, and then upload that principal to the cloud service in order to access data that the client is storing on the cloud service. This ability to share principals across devices is controlled by restrictions established when proxy principals are generated: Such a proxy (client) principal can only be registered on a device that acts for (cloud service) principals that are identified at the point of generation of the proxy.

The security analysis of the type system uses standard techniques from the applied-pi calculus [START_REF] Abadi | Mobile values, new names, and secure communication[END_REF]. This allows us to prove our correctness property as a non-interference property based on process equivalence, i.e., two systems differing by one value are indistinguishable by any party that is not allowed to access this value. The standard pi-calculus includes message-passing with structured values, but does not include an explicit notion of memory (although it can obviously be modeled using processes as references). Since our language combines message-passing communication and localized stateful memory, we use the stateful applied pi-calculus [START_REF] Arapinis | Stateful Applied Pi Calculus[END_REF] as the starting point for our security analysis. This calculus does not explicitly model location (i.e., the distinction between two processes on the same device and two processes on two distinct devices). Since this distinction is critical for our security analysis, we add this notion in our calculus. Nevertheless the proof techniques that we employ are heavily based on those developed for the stateful applied pi-calculus.

The security analysis that we perform expresses that data are secure if keys received from other devices are not associated to an attacker. To formalise this conditional statement, we need more techniques than in a standard protocol where data are either secret or public, but their status does not depend on the execution. In our verification in subsection 5.3, we introduce an extended syntax that marks which keys, variables and channels are secure in the current trace. We then prove that when a new memory location is created with a secure key according to this marking, then the attacker cannot distinguish between two scenarios: one where the system reduces normally, and another one where the memory location is sometimes altered to another value. This is the basis for our noninterference property for the security guarantee provided by this approach.

In the next section we discuss related work. In Section 3 we present our language, type system and semantics. In Section 4 we present an extended example and in Section 5 present our result and outline the proof, then we conclude in Section 6. Appendix A provides addtional type rules for the language considered in this paper. Appendix B considers proofs of correctness omitted from Section 5. Appendix C considers addtional operational semantics rules for the "open" semantics that enables us to reason about interactions with untyped attackers.

Related Work

Implicit flow Implicit information flow properties involve the ability for an attacker to distinguish between two executions. Previous work that has provided type systems to control implicit information flow [START_REF] Vaughan | A cryptographic decentralized label model[END_REF][START_REF] Askarov | Cryptographically-masked flows[END_REF] considered high and low data, and this could be extended to a bigger lattice but not to the creation of new principals, as the security of a variable is defined statically. Zheng and Myers presented an information flow type system that includes dynamic checks on rights [START_REF] Zheng | Dynamic security labels and noninterference (extended abstract)[END_REF] which can be used, for instance, when opening a file. The Jif Project [START_REF] Myers | Protecting privacy using the decentralized label model[END_REF] adds security types to a subset of Java, leading to a powerful and expressive language. Unlike our work, this other work does not address how to enforce principal identities and type information to be correctly communicated to other locations.

Security properties on distributed system Work on type security for distributed systems can be distinguished according to the kind of security they aim to provide. Muller and Chong present a type system that includes a concept of place [START_REF] Muller | Towards a practical secure concurrent language[END_REF] and their type system ensures that covert channels between "places" cannot leak information. Vaughan et al. look at types that can be used to provide evidence based audit [START_REF] Jia | AURA: a programming language for authorization and audit[END_REF][START_REF] Vaughan | Evidence-based audit[END_REF]. Fournet et al. look at adding annotations with a security logic to enforce policies [START_REF] Fournet | Cryptographically sound implementations for typed information-flow security[END_REF]. Liu and Myers [START_REF] Liu | Defining and enforcing referential security[END_REF] look at a type system which ensures referential integrity in a distributed setting. This work uses a fix lattice of policy levels, which does not change at runtime. The Fabric language [START_REF] Liu | Fabric: A platform for secure distributed computation and storage[END_REF] provides decentralised, type-enforced security guarantees using a powerful middleware layer for PKI, and Morgenstern et al. [START_REF] Morgenstern | Security-typed programming within dependently typed programming[END_REF] extend Agda with security types. In contrast, our work allows programs to generate new principals at run-time and provides a security property that tracks implicit information flow, without requiring the support of a purpose built middleware layer or global PKI. Due to the fact that the attackers in our model can access services in the same way as honest principals, this security property is an adaptation of the bisimulation property which is a strong property introduced in the (s)pi-calculus by [START_REF] Abadi | Mobile values, new names, and secure communication[END_REF]. Bisimilation can be checked for processes by tools like Proverif [START_REF] Blanchet | An Efficient Cryptographic Protocol Verifier Based on Prolog Rules[END_REF] but these kind of tools do not scale up to large systems. Bengtson et al. [4] present a security type system which allows creation of dynamic principals in presence of an untyped attacker. However, this type system provides only assertion-based security properties of cryptographic protocols. These are weaker than non-interference properties as they are expressed on one process instead of comparing two processes. [START_REF] Chothia | Type-based distributed access control[END_REF] considers a framework in which principals can be created at run time (without a global PKI) they prove type soundness rather than a non-interference result. Finally, the DSTAR program [START_REF] Zeldovich | Securing distributed systems with information flow control[END_REF] achieves these two goals but is focused on network information and relies on local systems to actually analyse implicit flow, which leads to a more coarse system.

Managements of new principals

Safety despite compromised principals Past work [START_REF] Chothia | Type-based distributed access control vs. untyped attackers[END_REF] has looked at un-typed attackers in a security type system, however this work only considers a static number of principals, fixed at run time. Fournet, Gordan and Maffeis [START_REF] Fournet | A type discipline for authorization in distributed systems[END_REF] develop a security type system for a version of the applied picalculus extended with locations and annotation. Their type system can enforce complex policies on these annotations, and they show that these policies hold as long as they do not depend on principals that have been compromised. Unlike our work they assume that the principals are all known to each other and there is a direct mapping from each location to a single principal that controls it. Our work allows principals to be dynamically created, shared between locations and for locations to control multiple principal identities. We argue that this model is a better fit to cloud systems in which users can dynamically create many identities and use them with many services.

3 Language: Semantics and Type System

Syntax

The syntax of our language is given in Figures The list c records which channel names correspond to establish channels (globally bound). Channel also appear in connect and accept commands in the devices, and these are added to c once the channel is opened. When there are no established channels, we omit the ν{}. prefix. Note that to guarantee freshness of keys and nonce used in encryption, we might also provide global binders k and n in addition to c. However this guarantee is straightforward to provide, using "freshness" predicates, so for readability reasons we omit explicit binders for generated keys and nonces.

A device consists of a memory M and a command C. Memories associate variable names with values, key names with keys and principal names with principals.

Given a nonce k from some assumed set of key nonces, we define (k + , k -) as the public pri- -are two constructors. A principal pv is a tuple prin(k -, k + , LR) which contains a key pair (k -, k + ), together with a (possibly empty) set of public key values LR. When a device has pv in its memory, it is allowed to act for pv. Devices that can act as a principal pv 0 , whose public key k 0 + is one of the public keys in LR, are allowed to add pv to their memory.

Each variable x in N v represents a reference to a value i.e. variables are mutable. At declaration time, a reference is associated with some rights R, which cannot be revoked or changed. Making all variables mutable is convenient for our security analysis: it allows us to define non interference as the property that a parallel process that alters the value of a high-level variable cannot be detected by an attacker. If variables were not mutable we would have to consider a much more complex security property and proof. In addition, to avoid to consider scope of variables, we assume that a command never declares twice the same name for variables, channels, keys and principals.

Types (Figure 2) for these variables consists of a pure-type S which indicates the base type for the value of the variable (e.g. integer, public key, cipher, etc.) and a label (or right) R which indicates the principals who are allowed to access to the variable. A label can be either ⊥ i.e. the variable is public or a set which contains public key names: k ∈ N k and pub(p) where p ∈ N p .

Key names are declared by a command let k = x in C. This command copies the value of the reference x into k which represents a public key (not a reference to a public key). The type system (deref T) ensures that x in this command is an unrestricted public key: x : PubKey ⊥ .

Channel types are declared when they are established, we have two kinds of channel: public and secure channels. Their types have syntax Chan(S R 1 ) R 2 where S R 1 is the type of values that are past over the channel and R 2 expresses which principals are allowed to know the existence of c and when communication on this channel takes place.

Semantics

The semantics of the system is defined as a small-step semantics for commands and as a big-step semantics for expressions. Devices run concurrently with synchronized communication between them. Inside each device, all parallel threads run concurrently and communicate through the shared memory of the device (since memory is mutable). The main reduction rules are presented in Figure 5 for commands and in Figure 6 for main expressions. When a command that declares a new variable is reduced, the name is replaced by a fresh name that represents a pointer to the location in the memory where the value has been stored. The evaluation of expressions has the form M (e) = v: the evaluation of e with memory M returns the value v. We note that this is different from some other calculi, in which variables are not references, and are replaced with a value when declared. Our correctness statement below depends on the use of references and, since we have a memory mechanism, we prefer to store the key names and principal names in memory and instead of applying a substitution, the names are evaluated when a command reduces (cf the (rights RS) rules). Principals are generated using the newPrin p RS ; C command, where RS are the keys to use to protect the principal (and therefore cannot ⊥). The rule for this command (newPrin S) generates a fresh key pair (k + , k -) and stores the principal prin(k + , k -, LR) at a new location p in the memory, where M (RS) = LR. To bootstrap the creation of these principals, they can be declared with RS = {}; such principal identities can only be used on a single device, they cannot be sent over channels. Additionally some devices may start off with the public keys of some trusted parties, i.e., the same assumption as TLS. This too lends itself well to cloud systems, in which web browsers come with a number of trusted certificates.

C ::= if (e 1 = e 2 ) then C 1 else C 2 | new x : S R = e; C | x := e; C | x[e 1 ] := e 2 ; C | let k = x in C | C 1 | C 2 | skip | ! C | connect c : Chan(S ⊥ ) ⊥ ; C | accept c : Chan(S ⊥ ) ⊥ ; C | connect c : Chan(S R ) R to
Communication between devices uses Java like channels: a channel is first established then it can be used to input and output values. The channel establishment is done by substituting the channel names in both devices by a unique fresh channel name added to c (we assume that initial channel names and active channel names range over distinct sub-domains of N c to avoid collision). Note that channels do not name the sending and receiving device as these may be spoofed by an attacker, however, to get a more tuneable system, it would be a simple extension to add a port number which would restrict possible connections. For secure channels (open priv S), in a similar way to TLS with client certificates, both devices must provide the public key k + of who they want e ::= x, y, . . . to connect to. They must also provide the principal (which includes a private key) to identify themselves to the other party. To set up a secure channel, the client and the server also have to ensure that they are considering the same rights for the channel. For that they have to exchange the value of their channel right M (Chan(S R 1 ) R 2 ) and make sure that it corresponds to the distant right value M (Chan(S R 1 ) R 2 ). Indeed, even if type-checking is static inside a device, type-checking has to be dynamic between distinct devices since programs are type-checked on each device and not globally.

Example 2 (Principal set up) Assume that a cloud service C has a public key c + , which is known to Alice and Bob, and that Alice wants to share some private data with Bob using this cloud service. Alice can do this using the code shown in Figure 7. Alice starts by generating a key pair (a -, a + ). As neither Alice nor Bob have certificates, Bob just sends his key publicly to Alice over a public channel. Alice receives it, and creates a new variable to be shared with Bob and the cloud service. She then opens a secure channel with the cloud that is typed to allow data of type {a + , b + , c + }, the ⊥ right on this channel indicates that, while the data on the channel must be kept confidential, the knowledge that some value has been sent is not. This fragment of code does not authenticate Bob, this could be done using another protocol, or offline, but we will show that if the device that sent her this key, and the cloud server, both run well typed code, then she is guaranteed that the secret will only be shared by the device sending the key, the cloud server and herself. She knows that no leak can come from, for instance, bad code design on the cloud device.

The enc RS (e) expression, governed by the (enc E) rule, encrypts the evaluation of e for each of the public keys k i + named in RS, i.e., anyone that has a single private key corresponding to any k i + can decrypt it, the set of all k i + is also included in the encryption. We use randomised encryption to avoid leakage that would occur otherwise when the same value is encrypted twice, and we model this by including a fresh nonce in the encryption. The decrypt p e as x : S RS then C 1 else C 2 command reduces successfully (dec true S) when e evaluates to a ciphertext enc RS,n (v) that can be opened by the secret key of p and that the LR, which is packed into the encryption, is a subset of the evaluation of RS.

The release(p) expression reduces by encrypting the principal p for each of the set of public keys representing the principals that can access it. It is the only way to produce a value which contains a secret key and therefore to send private keys through a channel. The register command behaves as decrypt except that it deals with encrypted principals instead of encrypted values.

All other semantics rules are standard except that instead of returning run-time error (division by 0, illegal offset index etc.) expression returns a special value NaV. This feature is critical to fresh(k + , k -) fresh(p )

M (RS) = LR νc.D | M C | newPrin p RS ; C → νc.D | M ∪ {p → prin(k + , k -, LR)} C | C{p /p} (newPrin S) M (e) = v fresh(y) νc.D | M C | new x : S R = e; C → νc.D | M ∪ {y → v} C | C{y/x} (new S) M (e) = v 2 νc.D | M ∪ {x → v 1 } C | x := e; C → νc.D | M ∪ {x → v 2 } C | C (assign S) fresh(k ) M (e) = k + νc.D | M C | let k = e in C → νc.D | M ∪ {k → k + } C | C{k /k} (deref S) M (p) = prin(k + , k -, LR 2 ) M (e) = enc LR,n (v) k + ∈ LR M (RS) ⊆ LR fresh(y) νc.D | M C | decrypt p e as x : S RS then C 1 else C 2 → νc.D | M ∪ {y → v} C | C 1 {y/x} (dec true S) fresh(c) νc.D | M 1 C | connect c 1 : Chan(S ⊥ ) ⊥ ; C 1 | M 2 C | accept c 2 : Chan(S ⊥ ) ⊥ ; C 2 → νc.c.D | M 1 C | C 1 {c/c 1 } | M 2 C | C 2 {c/c 2 } (open public S) fresh(c) M 1 (p s ) = prin(k 1 -, k 1 + , LR s ) M 2 (p c ) = prin(k 2 -, k 2 + , LR c ) M 1 (R 1 ) = M 2 (R 2 ) M 1 (R 1 ) = M 2 (R 2 ) M 1 (k c ) = k 2 + M 2 (k s ) = k 1 + νc.D | M 1 C | accept c 1 : Chan(S R 1 ) R 2 from k c as p s ; C 1 | M 2 C | connect c 2 : Chan(S R 1 ) R 2 to k s as p c ; C 2 → νc.c.D | M 1 C | C 1 {c/c 1 } | M 2 C | C 2 {c/c 2 } (open priv S) M 1 (e) = v fresh(y) νc.D | M 1 C | output c e ; C 1 | M 2 C | input c(x); C 2 → νc.D | M 1 C | C 1 | M 2 ∪ {y → v} C | C 2 {y/x} (i/o S) M (e) = enc LR 1 ,n (prin(k + 1 , k - 1 , LR 1 )) M (p 2 ) = prin(k + 2 , k - 2 , LR 2 ) k + 2 ∈ LR 1 fresh(p 3 ) νc.D | M C | register p 2 e as p 1 then C 1 else C 2 → νc.D | M ∪ {p 3 → prin(k + 1 , k - 1 , LR 1 )} C | C 1 {p 3 /p 1 } (register true S) M (e) = enc LR 1 ,n (prin(k + 1 , k - 1 , LR 1 )) M (p 2 ) = prin(k + 2 , k - 2 , LR 2 ) k + 2 ∈ LR 1 νc.D | M C | register p 2 e as p 1 then C 1 else C 2 → νc.D | M C | C 2 (register false S)
Figure 5: Main command rules

M (p) = prin(k + , k -, LR) LR = {} fresh(n) M (release(p)) = enc LR,n (prin(k + , k -, LR)) (release E) fresh(n) M (e) = v M (RS) = LR M (enc RS (e)) = enc LR,n (v) (enc E) M (e 1 ) = v 1 M (e 2 ) = v 2 v 1 ∈ Z v 2 ∈ Z M (e 1 + e 2 ) = v 1 + v 2 (+ E) M (e 1 ) = v 1 M (e 2 ) = v 2 v 1 / ∈ Z ∨ v 2 / ∈ Z M (e 1 + e 2 ) = NaV (error + E) ∀i, 1 ≤ i ≤ n, p i → prin(k i + , k i -, LR i ) ∈ M ∀i, n + 1 ≤ i ≤ n + m, k i → k i + ∈ M M ({pub(p 1 ), . . . , pub(p n ), k n+1 , . . . , k n+m }) = {k 1 + , . . . , k n+m + } (rights RS)
Figure 6: Main semantic rules for expressions and rights guarantee the security of our system. Indeed, we allow a device to evaluate expressions with secure variables and then to do an output on a public channel. This scenario is safe only if we can ensure that no expression will block any thread. Note that the attacker can also send values with some type through a channel of another type, consequently run time type errors can also occur.

k c → c + newPrin A {} ; accept c : Chan(PubKey ⊥ ) ⊥ ; input c(x b ); let k b = x b in new secret : Int {kc,pub(A),k b } = 42; connect upload : Chan(Int {kc,pub(A),k b } ) ⊥ to k c as pub(A); output upload secret ;
Finally, the command synchronised{C} executes a command C with no communication or interleaving of other processes. This is useful to avoid race conditions.

Types

The type judgment for expressions takes the form Γ p ; Γ k ; Γ e : S R and the type judgment for commands takes the form pc; Γ p ; Γ k ; Γ c ; Γ C where Γ is a mapping from variable names to types S R , Γ c from channel names to channel type Chan(S R 1 ) R 2 , Γ p is a set of principal names, Γ k is a set of public key names, and where pc is a right of form R called the program-counter. The program counter allows to analyse programs for indirect secure information flow [START_REF] Denning | Certification of programs for secure information flow[END_REF]. Figure 8 defines the main type rules for commands and Figure 9 defines the rules for expressions and rights.

In many typing judgments, we use a condition

R 1 ⊆ R 2 that states that R 1 is more confidential than R 2 . The predicate R 1 ⊆ R 2 holds either when R 2 = ⊥ or when R 1 is a syntactical subset of R 2 (no aliasing). For instance, we have {k 2 , pub(p)} ⊆ {k 1 , pub(p), k 2 } and {k 1 , k 2 } {k 2 } even if k 1 and k 2 map to the same key in memory. We also use R 1 ∩ R 2 to define the syntactic intersection of the sets R 1 and R 2 (which is R 2 if R 1 = ⊥).
Types rules for new principals and variables The typing rule for principal declaration (newPrin T) only allows the program counter to be bottom. This restriction avoids the situation in which a variable with a right including this principal might be less confidential than the principal itself.

The new variable declaration (new T) checks that the rights R 1 to access the new variable x are more restrictive than (a subset of) the rights R 2 of the expression being assigned and of the program counter pc. We also ensure that one of the principal in R 1 belongs to Γ p . The type rule for assignment (assign T) ensures that high security values cannot be assigned to lower security variables.

While the semantics for new principals (newPrin S) stores the rights set LR dynamically (as LR is only used when the principal is sent to another device), the semantics for managing variables (new S) does not consider them: their confidentiality is entirely provided by the type system.

Example 3 We consider the following piece of code in which two new principals are declared, and both Alice and Bob may know the value of y, but only Alice may know the value of x:

{} newPrin Alice {} ; newPrin Bob {} ; new x : Int {pub(Alice)} = 5; new y : Int {pub(Alice),pub(Bob)} = 7; x := y; if (x = 1) then y := 1;
Here the assignment of y to x should be allowed because x is protected by rights more confidential than y. However, in the last line, the value of y (which Bob can read) leaks some information about

Γ p ; Γ k RS pc = ⊥ pc; Γ p ∪ {p}; Γ k ; Γ c ; Γ C pc; Γ p ; Γ k ; Γ c ; Γ newPrin p RS ; C (newPrin T) Γ p ; Γ k R 1 Γ p ; Γ k ; Γ e : S R 2 R 1 ⊆ pc ∩ R 2 ∃p ∈ Γ p .pub(p) ∈ R 1 pc; Γ p ; Γ k ; Γ c ; Γ ∪ {x : S R 1 } C pc; Γ p ; Γ k ; Γ c ; Γ new x : S R 1 = e; C (new T) Γ p ; Γ k RS Γ p ; Γ k ; Γ e : S R RS ⊆ R Γ p ; Γ k ; Γ enc RS (e) : Enc{S} ⊥ (enc T) p ∈ Γ p Γ p ; Γ k ; Γ release(p) : PrivKeyEnc ⊥ (release T) ∀i, 1 ≤ i ≤ n, p i ∈ Γ p ∀i, 1 ≤ i ≤ m, k i ∈ Γ k Γ p ; Γ k {pub(p 1 ), . . . , pub(p n ), k 1 , . . . , k m } (rights T)
Figure 9: Types rules for non standard expressions and rights the value of x (which Bob should not be able to read). Therefore, this is an unsafe command and it cannot be typed.

Types rules for encryption

The type rule for encrypting values (enc T) verifies that the encrypted value is less confidential than the set of keys used for encryption, it then types the ciphertext as a public value, i.e., encryption removes the type restrictions on a value while ensuring that the encryption provides at least as much protection. We note that if the encrypting key depends on non-public data, then the program counter would not be public, which would ensured that the ciphertext was not stored in a public variable. Hence the use of restricted keys will not leak information.

The corresponding decryption rule (dec T) verifies that the principal p used to decrypt the cipher is valid (p ∈ Γ p ) and is consistent with the rights of the decrypted value. As the knowledge of which keys has been used to encrypt is protected with the rights R 2 of the cipher, the success of the decryption also depends on R 2 . Therefore, the program counter has to be at least as high as R 2 when typing the continuation. Finally, as with an assignment, the rule enforces that the created variable does not have a type that is more confidential than the program counter.

Types rules for public channels Typing rules for public channels ensures that these are only of type public and, when they are used, the program counter is ⊥.

Example 4

The following system illustrates the use of public channels and encryption:

{Alice → prin(k + a , k - a , {}), bobP ub → k + b }} new x : Int {Alice,bobP ub} = 7; connect c : Chan(Enc{Int} ⊥ ) ⊥ ; output c enc {pub(Alice),bobP ub} (x) ; input c(e);
decrypt Alice e as xInc : Int {pub(Alice),bobP ub} then

x := xInc; | {Bob → prin(k + b , k - b , {}), aliceP ub → k + a } ! accept c : Chan(Enc{Int} ⊥ ) ⊥ ; input c(z);
decrypt Bob z as w : Int {pub(Bob),aliceP ub} then output c enc {pub(Bob),aliceP ub} (w + 1) ;

Alice and Bob start off knowing each other's public keys, and Bob provides a service to add one to any number sent by Alice. The variable x is restricted so that only Alice and Bob can know the value. Encrypting this value removes these type protections, so that it can be sent across the public channel c. On Bob's device decrypting with Bob's private key replaces these type protections.

Types rules for secure channels For secure channels (client and server side), the rule (connect 2 T) enforces that the principal who is creating the channel and the principal being connected to, both have the right to access the data passed over the channel, hence {pub(p), k} ⊆ R 1 . In order to ensure that the possible side effects caused by using the channel are not more restrictive than the data passed over the channel we need that R 1 ⊆ R 2 . The R 2 ⊆ pc condition stops side channel leakage to the device receiving the connection at the time the channel is opened. Finally, the program counter is set to R 2 once connected: this ensures both devices have the same program counter. Without this we would have implicit leakage, for instance, one device with a public program counter could wait for a message from a device with a non public program counter, then outputs something on a insecure channel. As the sending of the message may depend on a value protected by the program counter, this would result in a leakage.

We make the strong assumption that the existence of a connection attempt can only be detected by someone with the correct private key to match the public key used to set up the connection. If we assumed a stronger attacker, who could observe all connection attempts, we will need the condition that pc = ⊥ at least for the client.

The output rule (output T) has two main restrictions: one which verifies that the device still has the program counter agreed with the corresponding device, and R 1 ⊆ R 3 i.e., the type on the channel is no less restrictive than the type of data sent. This is because when this data is received it will be treated as data of type R 1 .

For channel creation the restriction on the channel must be at least as restrictive as the program counter. For input and output we must additionally check that the program counter has not become more restrictive, hence requiring that the channel restriction and the program counter are equal, i.e., testing the value of a high level piece of data and then sending data over a lower level channel is forbidden. Both programs aim at sending x to Bob, which is a secret shared by Alice and Bob. In the first case, the sending of x depends on its value: therefore the communication should can only be on a channel with rights Chan(Int {pub(Alice),bob} ) {pub(Alice),bob} . In the other example, even if the value of x is updated due to a parallel thread that has a non public program counter, the sending of x is unconditional.

Note that the language does not have "{if condition then C }; C structure as this construct would not be safe: if C waits infinitely for a connection then C is not executed. However, a delay command could be added to help the second program to output x after x has been updated.

Type rules for release and register

The release command is similar to the encryption command except that the rights with which the principal is encrypted are provided by the principal value. Therefore, there is no static check to perform in (release T). The registration rule (register T), for the same reason has less checks than (dec T). However, it does enforce that pc = ⊥, without which we could get non public rights; revealing a such a none public right would then be an information leak. Removing this restriction, and allowing non public rights, would be possible in a more complex type system but we decide not to do so to keep the type system more understandable.

Example: A Secure Cloud Server

As an extended example we consider a cloud server that provides a data storage service. The motivation of our work is to make it possible to type an open cloud service, without the need for a global PKI neither the need to verify that its users run typed programs, so ensuring that it provides security guarantees to all of its users. The server process in Figure 10 defines an open service which users can connect to and register to store data. This data can be shared with another principal, hence the server takes a pair of public keys, representing the principals, when registering.

To keep the example simple this server accepts up to 3 accounts and denies further registrations. The data for each accounts is stored in the data variable defined in the RegisterU sers process; the restriction set used to type this variable specifies that only the server and the two clients named at registration can have knowledge of this data. Additionally, the server keeps track of how often each account is used (in the usage array) and runs a process to monitor the usage (the CheckU sage Server ≡ new usage : Array{Int} ⊥ = {0, 0, 0}; new blocked : Array{Int} ⊥ = {0, 0, 0}; new nextID :

Int ⊥ = 0; RegisterU sers | CheckU sage RegisterU sers ≡ ! accept newUsers : Chan(Array{PubKey} ⊥ ) ⊥ ; input newU sers(client1Client2); let client1 = client1Client2[0] in let client2 = client1Client2[1] in synchronized { new accountID : Int ⊥ = nextID; nextID = nextID + 1; } if (accountID ≤ 2) then{ new data : Int {pub(Server),client1,client2} = 0; ServeClient(client1, client2, client1) | ServeClient(client1, client2, client2) } CheckU sage ≡! synchronized{ new total : Int ⊥ = usage[0] + usage[1] + usage[2] + 3; { if (usage[0] > total/2) then blocked[0] := 1 else blocked[0] := 0; | if (usage[1] > total/2) then blocked[1] := 1 else blocked[1] := 0; | if (usage[2] > total/2) then blocked[2] := 1 else blocked[2] := 0; } ServeClient(c1, c2, c3) ≡ ! accept upload : Chan(Int {Server,c1,c2} ) ⊥ from c3 as Server; if (blocked[accountID] = 0) then{ input upload(z); usage[accountID] = usage[accountID] + 1; data = z; } | ! accept dowload : Chan(Int {Server,c1,c2} ) ⊥ from c3 as Server; if (blocked[accountID] = 0) then{ usage[accountID] = usage[accountID]
≡ {srvKey → k + s } Sender M D ≡ {srvKey → k + s } M obile RD ≡ {srvKey → k + s } Receiver Srv ≡ {Server → prin(k + s , k - s , {})} Server System ≡ SD | M D | RD | RD | Srv Figure 12:
The server context with 4 devices: a sender with its mobile device and two concurrent receivers process). If any account is found to have made more than 50% of the total number of requests (plus 3), it is temporarily blocked (by setting the corresponding index in the blocked array to 1). The usage data and blocked status are public data. This is an example of an open cloud service which writes to public variables after processing private data. Our type system ensures that there is no leakage between the two.

An example configuration is given in Figure 12, with the definitions of the processes provided in Figure 11: this configuration consists of four devices SD, M D and two identical RD devices. We assume that, in the physical world, SD and M D are the laptop and respectively the mobile of Alice while the two other devices RD are owned by Bob and Charlie. In the system definition, Alice's and Bob's devices start off knowing the servers public key, but the server has no knowledge of Alice's and Bob's principals. The mobile device M D first creates a new principal identity and shares the public key to SD. Note that RD could also send its private key to SD at this point which is not the expected behavior. To avoid honest users to establish unwanted connection, a port number mechanism should be added to the connections rules. Once SD receives the principal's public key from M D, SD creates a new principal identity to use with the cloud service which is known by the mobile's principal identity. This allows SD to release and to send the new principal Alice to M D which registers it. Therefore both SD and M D can use the service with the same account. Finally Bob's device RD and SD exchange their public keys, and SD sends to M D the public key received from RD then SD registers for a shared account between pub(Alice) and bobKey on the server. Finally, SD or M D can upload a sharedSecret value to the server. Meanwhile M D is able to recover the last uploaded value (0 if it downloads before an upload occurs).

The security type on the variable sharedSecret means that its value can only have an effect on other variables with the same or a more restrictive type. Importantly, our correctness result limits knowledge of these values to just the Alice, Bob and Server devices, no matter what well-typed code are run in these devices. On the other hand, checking the authenticity of the Bob key (with a mechanism such as PGP, or out-of-band checks) is Alice's responsibility.

These are exactly the guarantees that a user, or a organisation, would want before using the cloud service. While many people trust their cloud services, and organisations enter into complex legal agreements, leaks can still occur due to programming errors. Type checking the code, as we outline in this paper can show that it is safe from such programming errors, and help provide the users with the guarantees they need to use the system.

Security analysis

We now prove that the type system preserves confidentiality of data: when a variable is declared with rights R then the only devices that can observe anything when the variable's value changes are the devices that are allowed to know one of the keys in R.

The proof uses techniques from the applied pi-calculus, rephrased for our formalism. Our basic result uses a notion of bisimulation formulated for reasoning about information flow in nondeterministic programs [START_REF] Sabelfeld | Probabilistic noninterference for multi-threaded programs[END_REF]. Intuitively, two programs are bisimilar (for "low" observers) if each one can "imitate" the low actions of the other, and at each step the memories are equivalent at low locations. Note that memory can change arbitrarily at each step, reflecting the ability of concurrent attacker threads to modify memory at any time.

The applied pi-calculus extends the well-known pi-calculus, a process calculus where communication channels may be sent between processes, with binding of variables to non-channel values. In our approach, "memory" is this set of bindings of variables to values in the applied pi-calculus. Also, our bisimilarity is a labelled bisimilarity since we consider communications on channels as observable events. Our correctness result shows that a high (insider) attacker cannot leak information to low observers by communication on high channels or by modifying high locations in memory.

We explain our proof over the following five subsections. In the following subsection we annotate devices with an identifier, so that we can keep track of particular devices as a process reduces, and we define when a particular device is entitled to read data protected with a particular set of rights. In Subsection 5.2 we define our untyped attacker and outline an labelled, open semantics which defines how an "honest" (typed) process can interact with an untyped attacker process. We also prove that this open semantics is correct with respect to the semantics presented above.

To give us the machinery we need to prove our main results, in Subsection 5.3 we annotate our processes with the rights that apply to all variables. We show that a well annotated, well typed process reduces to a well annotated, well typed process, this results shows that a well typed system does not leak data, but it does not account for untyped attackers. To do this we introduce a labelled bisimulation in Subsection 5.4. This bisimulation relation defines the attackers view of a process, and their ability to distinguish systems. Finally, in Subsection 5.5, we prove that, for our open semantics, a well annotated, well typed process is bisimular to another process that is the same as the first, except that the value of a high level variable is changed. This means that no information can leak about the value of that variable for any possible attacker behaviour, so proving our main correctness results.

From rights to allowed devices

As a preliminary step, we need to formally define which devices are and are not granted permissions by a particular set of rights. To do this we need a way to refer to particular devices while they make reductions, so as a notational convention, we place identifiers on devices, that are preserved through reductions. By convention an identifier will be an index on each device, so for example

D 1 | D 2 → D 1 | D 2 expresses that D i and D i represent the same physical device in different states.
In Definition 1, Definition 2 and Definition 3 below, we formally define an association between the public keys in a rights set and devices, but first we motivate these definitions with an example:

Example 6 Consider the the system SD A | SD B | M D M | M D N | RD X | RD Y | Srv S
where SD, M D, RD and Srv are defined in Figure 11 and Figure 12 (i.e. there are two clones of each devices of the system from Section 4, except for the server). Consider the variable data : Int {pub(Server ),client1 ,client2 } of the RegisterUser command on Device S (the server). There are three reasons for a device to be allowed to access shared data, depending on which reduction occurs in the system.

First, the devices that created the keys client1 and client2 are allowed access to this data. This pair of keys is passed to the server at the start of its loop. Depending on which device (A or B) made the connection to the server channel newUsers, client1 allows either Device A or Device B (as client1 ). Assume that it is Device A. Similarly client2 represents Device X or Y depending on which device connected to channel c during the Sender command of Device A. Assume it is Device X.

Next, since the public key client1 has been created by the command newPrin Alice {mobile} in Device A, the device which corresponds to the public key mobile is also allowed to access data. We assume that it is Device M .

Thirdly, the public key pub(Server ) has not been generated by any device. However it was in the initial memory of Device S, therefore this device is also allowed to access the shared data by the right granted by this key.

Our security property grants that no other device than Device S, A, X and M can get information about the value of data. On the other hand, if an untyped attacker provides its own key to Device A, through channel c, then no security guarantee can be provided about data. Indeed, such a case means that the rights explicitly allows the attacker's device to access the data as any other regular device.

Before we formalise what are the allowed devices, we make reasonable assumption about the initial process. For instance, when the process starts, we assume that devices have not already established any channel between them. We also consider that they have an empty memory except for some public keys and principals (and we do not allow duplicate principals). Finally, we consider that all devices are well-typed except one (Device 0) which is the untyped attacker.

We first define a well-formed and well-typed condition on processes:

Definition 1 A valid initial process P = νc. M 0 C 0 0 | M 1 C 1 1 | . . . | M n
C n n is a process where:

1. There is no active channel already established between the processes: c = {}.

2. The bound values in memory are either principals or public keys: For all 0 ≤ i ≤ n, x → w ∈ M i implies there exists k + , w = prin(k + , k -, {}) or w = k + .

3. Each principal exists only on one device: For all 0 ≤ i, j ≤ n, i = j, prin(k

+ , k -, {}) ∈ M i implies prin(k + , k -, {}) / ∈ M j .
4. The memory of every device is well-typed with contexts corresponding to its memory and pc = ⊥: for all 1 ≤ i ≤ n, w.l.o.g. assume that Before defining the set of allowed devices, we define an auxiliary function that maintains which devices are allowed to access shared data, and which public keys need to be associated to devices. This auxiliary metafunction maps backward from a set of rights LR that confers access, to all possible devices that may have provided the keys that gave them those rights. This is the set of allowed devices Entitled(LR) T where T is a process trace, defined below. Any device that is not in this set is not allowed by LR; we will consider such devices as attacker devices in our threat model. Definition 2 Given a reduction P → P where devices identifiers are in {0, . . . , n}, given a subset of identifiers I ⊆ {1, . . . , n} and a set of public keys LR, we define the backward function B P →P (I, LR) in the following way.

M i = {p 1 → prin(k 1 + , k 1 -, {}), . . . , p m → prin(k m + , k m -, {}), pk 1 → k 1 + , . . . pk p → k p + },
• If P → P is the reduction (newPrin S) on a device D i , i = 0 that creates a new principal prin(k + , k -, LR ) and that k + ∈ LR then

B P →P (I, LR) = I ∪ {i}, LR ∪ LR \ {k + } .
• Otherwise B P →P (I, LR) = (I, LR).

Definition 3 Let P 0 = M 0 C 0 0 | M 1 C 1 1 | . . . | M n C n n a valid initial process.
Let a sequence of reductions T = P 0 → P 1 . . . → P n and let LR a set of public keys, we consider

(I 0 , LR 0 ) = B P 0 →P 1 • . . . • B P n-1 →Pn (∅, LR). Let I = {i | ∃k + ∈ LR 0 , i ∈ {1, . . . , n}, prin(k + , k -, {}) ∈ M i }.
We define the set of allowed devices identifiers Entitled(LR) T as Entitled(LR)

T = I 0 ∪ I . Consider the set {k + | k + ∈ LR 0 ∧ i ∈ I , prin(k + , k -, {}) ∈ M i }.
We say that Entitled(LR) T is safe if this set is empty.

In other words, Entitled(LR) T is safe when all keys involved by LR have been either created by devices of Entitled(LR) T or owned by them at the beginning. This implies, since valid initial processes don't have duplicated keys, that the untyped attacker whose index cannot be in Entitled(LR) T have not generated any of these keys.

Definition of the attacker and of the open process semantics

An attacker is a device A = M C where M is a standard memory and C is a command which is not typed and which contains additional expressions to do realistic operations that an attacker can perform like extracting k -, k + and LR from prin(k + , k -, LR), decrypting a ciphertext with only a secret key, or releasing a principal with arbitrary rights (enc LR,n (prin(k + , k -, LR )) with LR = LR ).However, the attacker is not able to create principals with a public key that does not correspond to the private key because we assume that the validity of any pairs is checked when received by an honest device. We denote such an extended expression using E.

To reason about any attacker, we introduce open processes in a similar way as in the applied picalculus [START_REF] Abadi | Mobile values, new names, and secure communication[END_REF]. An open process has the syntax K |= νc. D 1 | . . . | D n where D 1 , . . . , D n are well-typed devices (the indexes 1, . . . n are the tags of the devices: we do not change them through reductions), where c are the channels which have been established between devices D 1 , . . . , D n (not with the attacker) and where K is a memory representing the values that the attacker already received. We refer to D 1 , . . . , D n as the honest devices. We also refer to K as the attacker knowledge. This plays the same role as frames in the applied pi-calculus, and also plays a similar role as computer memory in the bisimulation that we use for reasoning about noninterference for nondeterministic programs. We denote K(E) the evaluation of E with the memory K (to be defined the variables of E should exists in K).

Our type system ensures that an attacker is never able to learn any of the secret keys belonging to "honest" devices, as represented by the notion of reference rights defined below. The following predicate overapproximates what an attacker can learn about a value, based on the "knowledge" represented by its memory K and on the assumption that it knows all keys which are not in LR (which aims at being the reference rights). Definition 4 Given a set of keys LR and a value v, we define the predicate K LR v as there exists an extended expression E such that K(E) = v, where this extended expression contains all standard functions and attacker functions, as well as an oracle function which provides the secret key of any public key which is not in LR.

Open processes have two forms of reductions: internal reductions, which are the same as the reductions for closed processes, and labeled reductions which are reductions involving the attacker. Labels on these latter reductions represent the knowledge that an attacker can use to distinguish between two traces, effectively the "low" information that is leaked from the system.

There are two forms of labelled reductions, both of which take the form P l -→ P . In the first form, input reductions P in((c)att,E)

-------→ P , the attacker provides data, and in the second form, output reductions P out((c)att,x)

-------→ P , the attacker receives data from an honest device. There are also two further forms of input reductions: those for establishing channels and those which send data. The reduction that establishes a secure channel takes the form:

K |=νc.D | M accept c : Chan(S R 1 ) R 2 from k as P ; C i in((c)att,(Chan(S R 1 ) R 2 ,E,E )) -------------------→ K |= νc.D | M C{(c) att /c} i
where (c) att is any attacker channel name, K(E) should be the private key corresponding to M (k) and K(E ) should be the public key of M (p). The reduction to establish a public channel is similar but simpler. There is no need for checks on E or E .

Note that, unlike standard connection establishment where a fresh channel name is added to νc, here the name of the established channel is provided by the attacker and is not added in c, which is out of the scope of the attacker. However the attacker has to provide channel names in a separate subdomain which prevents it from using an existing honest channel name. The names which are the attacker's channel names are written (c) att . To summarize, a channel name of form (c) att represents a channel which is established between a device and the attacker, a channel c ∈ c is a channel between two devices (not accessible from the attacker) and a channel name c / ∈ c and not in the attacker's channel domain is just a program variable representing a future channel. Finally, we consider an implicit injection c → (c) att from c to attacker's channels.

For input reductions that sends data on an established attacker channel, E is an expression of the extended syntax admitting lower level operations that are available to attackers but not to honest devices, as explained above. There is just one rule for output reduction, saying that an attacker can learn from a value output on an attacker channel:

fresh(x) M 1 (e) = v K |= νc.D | M 1 C | output (c) att e ; C i out((c)att,x) -------→ K ∪ (x → v) |= νc.D | M 1 C | C i
→ {} |= SD A | MD M in((c)att,ct) -------→ {} |= SD A | MD M out((c)att,x) -------→ (x → k + ) |= SD A | MD M
where ct = Chan(PubKey ⊥ ) ⊥ and Device M has memory Mobile → prin(k + , k -, {}) (a renaming of the local variable Mobile on the device), after the first internal reduction where the principal is created.

After the first reduction where MD M creates its principal, the attacker establish the connection with Device M : as M is expecting a connection of type ct, the attacker have to provide ct and one of its channel name (c) att . Next, Device M outputs the value of pub(M obile) on (c) att which is then stored on the attacker's memory.

The following defines a subprocess of the "honest" devices of a system P , where some (other) devices of that system may be attacker devices. This subprocess of honest devices will be those defined by Entitled(LR) T . In other words, all devices which are not allowed by some key in LR are assumed to be controlled by the attacker. In the following, we will denote by P l 1 ,...,ln ====⇒ P a sequence of reductions P → * P 1 l 1 -→ P 1 → * P 2 . . . P n ln -→ P n → * P . We also denote by P l ? -→ P a reduction which is either P → P or P l -→ P for some label l and by P l ? -→ ? P either P l ?

-→ P or P = P . The following proposition states that if there is an execution of a system that includes communication with attacker devices, where all communication is local in this closed system, then we can consider subsystem of this, omitting the attacker devices, where communications with attacker devices are modelled by labelled reductions of the form described above. So the attacker devices become part of the context that the devices in the subsystem interact with through a labelled transition system. Such a subsystem may also exclude some of the "honest" devices in the original system, and in that case we treat those excluded devices as attacker devices in the context (since labels on the reductions only model communication with attackers).

Proposition 1 Let P = νc.A | D 1 | . . . | D n
where all D i are well-typed and A is an untyped device. If P → * νc .P , then for all subset S of {1, . . . , n}, there exist l 1 , . . . , l m and K (the attacker knowledge at the end of the execution) such that

K |= P S l 1 ,...,lm = === =⇒ K |= P S
where K is a memory which is the union of the memories of A and all D i with i / ∈ S (variable names are renamed whenever there is a name conflict).

For instance, the system SD A | MS M | SD 0 , where SD 0 is part of the attacker, can perform three internal reductions between MS M and SD 0 where MS M sends its public key to SD 0 . In Example 7, we provided the three reductions of the system ({} |= SD A | MS M | SD 0 ) {A,M } .

Extended syntax with extra annotations

In this section, we add extra annotations to processes to perform a specific analysis about a given right LR = {pk 1 , . . . , pk n }. Since the keys in LR do not necessary exist in the initial process, we first annotate open processes with a reference right R r with the intention that this right will eventually grow to the right LR as keys are generated and added to this right during execution. Given a reference right R r , we define any rights whose all keys are in R r to be high (by opposition to low ). The set R r starts with keys that exists in the initial process.

An annotated process has the syntax K; R r |= P for attacker knowledge K, reference right R r and process P . The exact form of the annotations is explained below. The reference right R r only changes during a reduction of a command newPrin p RS . In this case, there is a choice of whether or not to include the generated public key in R r .

Definition 6 A sequence of reductions is called standard if each time a (newPrin S) reduction adds a key to R r :

K; R r |= νc. M newPrin p RS ; C | P → K; R r ∪ {k + } |= νc. M ∪ p → prin(k + , k -, LR) C | P we have LR ⊆ R r .
The next proposition ensures the existence of a standard annotation such that the rights we want to consider at the end are high and that the attacker does know any key in the set R r of the initial process. We will state in Proposition 3 that this implies that the attacker never knows the keys in R r during the whole reduction.

Proposition 2 Let P be a valid initial process such that P → * P and let LR a set of keys defined in P . If D H = Entitled(LR) P → * P is safe then there exists a standard annotation for the reduction provided by Proposition 1:

K 0 ; R r0 |= P D H l 1 ,...,ln ====⇒ K; R r |= P D H where R r0 and R r are such that ∀k + ∈ R r0 , K 0 Rr 0 k -and LR ⊆ R r .
When a variable or a channel is created with some rights, the reduction rules of the operational semantics remove all information about those rights. Therefore we add annotations to devices to remember if the defined right was high or low, according to R r . Recall that a right is high if it contains a key in the reference right R r . We use as a metavariable for an annotation H or L.

1. A memory location x → v ∈ M which is created by a command new x : S R = e; C, where R evaluates in M to a high right according to R r , is annotated as a high location: x H → v. Otherwise x is annotated as a low location: x L → v. By convention K contains only low locations.

2. A new channel name c, which is created by a command that establishes a channel c :

Chan(S R 1 ) R 2 , is annotated as c 1 2 where 1 resp. 2 is H if the evaluation of R 1 (resp. R 2 )
is high, and is annotated as L otherwise.

A value which is the result of an expression (besides an encryption expression) where one

variable refers to a high location is annotated as a high value (v) H . Otherwise, it is annotated as a low value (v) L . When a value (v) is encrypted, it becomes (enc RS,n ((v) )) L i.e., the initial tag is associated to the subterm.

4. A device M C 1 | . . . | C n is annotated as M (C 1 ) ( 1 ) | . . . | (C n ) ( n) i .
There is one tag i ∈ {L, H} for each sub-command C i which can be reduced. The annotation of each thread (C i ) ( i ) records whether the existence of this thread was due to a high value or a high right. When i = H, we say that the thread is high, otherwise the thread is low. For instance, the annotated device

a H → (1) H (if (a = 0) then C 1 else C 2 ) (L) 1 reduces to a H → 1 (C 2 ) (H) 1
because a is a high location. The other case where a thread can be set to high is in the establishment of a secure channel that is annotated with c H (H) . These annotations allow us to define technical invariants that are preserved during reduction. In the following technical definition, we formalize the idea that there exist a typing judgment for devices (Case (1) below) which is consistent with the annotations:

1. Variables (Case ( 2)) and channels (Case (3)) should have a type which corresponds to their annotation 2. The type system tracks a notion of security level for the control flow, and this level pc must be consistent with the thread annotation (Case ( 4)).

3. In addition, we express that the devices are not in a corrupted configuration, in the sense that secure channels are not being used to communicate with the attacker (Case ( 5)), nor are they used in a low thread (Case ( 6)).

4. Finally, ciphers for values (Case ( 7)) and principals (Case (8)) should not have high contents protected by low keys.

Definition 7 A tuple consisting of a reference right R r , a memory M and a thread (C) ( ) is wellannotated written " R r M (C) ( ) : well-annotated" if there exists pc, Γ p , Γ k , Γ c and Γ such that 1. pc; Γ p ; Γ k ; Γ c ; Γ C 2. For all locations x in M , we have

• either x L → (v) L in M for some value v and x ∈ Γ p ∪ Γ k • or Γ p ; Γ k ; Γ x : S R and -if R r ⊇ M (R), x H → (v) H in M , -if R r M (R), x L → (v) L in M for some value v.
3. For all channels c in the thread such that Γ c c :

Chan(S R 1 ) R 2 , the annotation of c is c 2 ( 1 )
where 2 = H iff. R r ⊇ R 2 , 1 = H iff. R r ⊇ M (R 1 ).
4. R r ⊇ pc if and only if = H.

For all (c) att , we have

Γ c (c) att : Chan(S R 1 ) R 2 with R r M (R 2 ) and R r M (R 1 ). 6. if is L, then there is no c H (H) in C.
7. For all values v stored in memory, if a sub-term of v matches enc LR,n ((t) H ) then R r ⊇ LR.

8. For all values v in memory, if a sub-term of v matches enc LR ,n (prin(k, LR, )) then LR = LR or R r ⊇ LR.

When, for a device

D = M (C 1 ) ( 1 ) | . . . | (C n ) ( n) i and a set R r , we have R r M (C i ) ( i ) :
well-annotated for i ∈ {1, . . . , n}, then we use the notation R r D : well-annotated.

Finally, we get the following subject-reduction result:

Proposition 3 Let K; R r |= νc.D 1 | . . . | D n
an open process such that for all k + ∈ R r we have

K Rr k -and for all 1 ≤ i ≤ n we have R r D i : well-annotated. If K; R r |= νc.D 1 | . . . | D n l ? -→ K ; R r |= νc .D 1 | . . . | D n then for all 1 ≤ i ≤ n we have R r D i : well-annotated. Moreover if the reduction is standard, we have K Rr k -for all k + ∈ R r .
Finally, valid initial processes which only require each device to be well-typed are well-annotated.

Proposition 4 Given a valid initial process

P = K |= M 1 C 1 1 | . . . | M n C n n , We have R r M i (C i ) (L) : well-annotated for 1 ≤ i ≤ n for any R r .

Labelled bisimilarity

The invariants expressed above are about a single process. To ensure that the attacker cannot track implicit flows, we need to compare the execution of two processes in parallel. In this section, we define a relation between processes which implies an adapted version of the bisimilarity property of the applied pi-calculus [START_REF] Abadi | Mobile values, new names, and secure communication[END_REF].

The two processes that we compare are the actual process and another one where the value of one of the high variables of the memory of some device has been changed to another one. So first, we define what is a process where a variable is modified arbitrarily. Definition 8 Given a device D = M ∪ {x → v } C , and a value v, we define D x=v to be the device that updates the variable x to be v by assignment, M ∪{x → v } C | x := v; . Extending this from devices to processes, given a process P which contains D with index i, we define P i:x=v to be the same process except that D has been replaced by D x=v .

In contrast to systems where the attacker can only observe public values in memory after reduction, here we model that the attacker can observe communications on channels that have been established with other devices. In the following examples, we stress how an attacker can distinguish between two processes even without knowing actual confidential values in the memory of those devices.

Example 8

We consider the device D(X, Y ), where the description is parametrized by two metavariables: X is a value stored in memory and Y is a value that is encrypted and sent on an attacker channel. The device has a memory M (X) = {x → X, k → k 0 + }, and the full description of the device is M (X) if x = 0 then output (c) att enc k (Y ) A .

The process D(0, Y ) can be distinguished from the process D(1, Y ). In the first case, we have:

{} |= D(0, Y ) out((c)att,m) --------→ {m → enc k (Y )} |= M (X) skip A
On the other hand, there is no reduction with only the label out((c) att , m) and internal reductions starting from {} |= D(1, Y ). This distinction models the fact that if the attacker receives data on (c) att , it learns that X = 0.

The processes D(0, 2) and D(0, 3) can also be distinguished even if both {k → k 0 -} |= D(0, 2) and {k → k 0 -} |= D(0, 3) can reduce with a label out((c) att , m). Indeed, after reduction the attacker's knowledge is

K = {k → k 0 -, m → enc k 0 + ,n (Y )} where Y is 2 (resp.
3): By performing the decryption of m with an untyped decryption, the attacker can compare the result to 2, and K(decr k (m)) = 2 is only true in the first case.

Finally, the processes {} |= D(0, 2) and {} |= D(0, 3) are not distinguishable. In both cases:

• there is no test to distinguish between the two attacker's knowledge, and

• the labelled reductions are the same i.e out((c) att , m)

With these examples in mind, we introduce static equivalence, an adaptation of the one used in the applied pi-calculus, which expresses that it is not possible to test some equality which would work with one memory but not with the other.

Definition 9

We say that two memories M 1 and M 2 are statically equivalent (≈ s ) if they have exactly the same variable names and for all extended expressions E where its variables x 1 , . . . ,

x n ∈ M 1 , we have M 1 (E) = M 2 (E).
Finally, we define an adaptation of the labelled bisimilarity. This recursive definition generalizes the conclusion of the example: the two memories should be statically equivalent, and a transition in one process can be mimicked in the other process, where the reduced processes should also be bisimilar.

Definition 10 Labeled bisimilarity (≈ l ) is the largest symmetric relation R on open processes such that (K A |= P A ) R (K B |= P B ) implies: 1. K A ≈ s K B ; 2. if (K A |= P A ) → (K A |= P A ), then (K B |= P B ) → * (K B |= P B ) and (K A |= P A ) R (K B |= P B ) for some K B |= P B ; 3. if (K A |= P A ) l - → (K A |= P A ), then (K B |= (K B |= P B ) l = =⇒ (K B |= P B ) and (K A |= P A ) R (K B |= P B ) for some K B |= P B .
The labelled bisimilarity is a strong equivalence property, and its we use it to state the security property that an attacker is unable to distinguish between two processes in the same class [START_REF] Arapinis | Stateful Applied Pi Calculus[END_REF]. However this definition does not help to actually compute the processes in the same class. Therefore we define a stronger relation that can be defined from our annotated semantics.

First, we define an obfuscation function obf(LR, w) which takes a set of public key LR and a value or a principal w and returns an obfuscated value (its syntax is like the syntax of value except that there is an additional option and that a principal value is also an option).

Definition 11 Let LR a set of public key, w a principal p or a value v. We define obf(LR, w) depending on the structure of w.

obf(LR, enc LR ,n (w )) = enc LR ,n (obf(LR, w )) if LR LR enc LR ,n ( ) if LR ⊇ LR obf(LR, {v 1 , . . . , v n }) ={obf(LR, v 1 ), . . . , obf(LR, v n )} otherwise obf(LR, w) =w.
where w is a value or a principal and n a nonce.

The set LR aims at containing a set of keys whose private keys will never be known by the attacker. In our previous example, we have obf(k 0 + , enc k 0 + ,n (Y )) = enc k 0 + ,n ( ): if k 0 -is never known by the attacker, the attacker will never be able to know anything about Y . Note that the random seed n used for the cipher is not hidden. Indeed, the attacker is able to distinguish between a cipher that is sent twice and two values which are encrypted then sent: in the first case the two message are strictly identical.

We now define an equivalence on memories: given a reference right R r , a set of safe keys, then we say that two memories are equivalent if they differ only by the high values which aims at never been sent to the attacker and by the obfuscated terms of the low values.

Definition 12 (equivalent memories) Equivalent memory is a relation on memories such that

M 1 R Rr M 2 if for each low location x L → v A in M 1 (resp. M 2 ), there exists x L → v B in M 2 (resp. M 1 ) such that obf(R r , v A ) = obf(R r , v B ) and each location p → pv in M 1 (resp. M 2 ) exists in M 2 (resp. M 1 ).
Next, we define an equivalence relation between two well-annotated processes: two processes are equivalent if they have the same commands up to some additional high threads and have equivalent memories: Definition 13 Two annotated processes P A and P B are annotated-equivalent (P A R P B ) when there exists an alpha-renaming (capture-avoiding renaming of bound variables) of P B such that

P A is K A ; R r |= νc. M A 1 C A (1,1) | . . . | C A (1,m 1 ) 1 | . . . | M A n C A (n,1) | . . . | C A (n,mn) n , P B is K B ; R r |= νc . M B 1 C B (1,1) | . . . | C B (1,m 1 ) 1 | . . . | M B n C B (n,1) | . . . | C B (n,mn) n ,
and we have K A R Rr K B , for all k + ∈ R r , we have K A Rr k -and furthermore for all (i, j), first M A i R Rr M B i , next, the annotation on each thread C X (i,j) (where X stands for A or B) is either H or L such that either:

• R r M X i (C X (i,j) ) (H) : well-annotated • R r M X i (C X (i,j) ) (L)
: well-annotated and C A (i,j) = C B (i,j) (the commands are syntactically identical up to renaming of bound variables).

Finally, we prove that this relation actually implies bisimilarity.

Proposition 5 Let P A be (K A ; R r |= νc.Q A ) and P B be (K B ; R r |= νc .Q B )
, where both are wellannotated processes such that P A R P B , Furthermore assume that for all k + ∈ R r we have K A Rr k -. Then the processes are annotated equivalent, P A ≈ l P B (with the annotations removed).

Main theorems

Our first security property grants confidentiality for each created variable in the following way. When a variable x is created with a protection R, this implicitly defines a set of devices which are allowed to access x. If the untyped attacker is not in this set, then any collaboration of the attacker with the denied-access devices can not learn any information about the value stored by the variable: they cannot detect an arbitrary modification of the variable.

Theorem 1 Let P = A | D 1 | . . . | D n
be a valid initial process. We consider a reduction P → * P with ∈D H M i . As P is a valid initial process, we get that P D H is also a valid initial process (the verification of all conditions to be a valid initial process is immediate). Since D H is safe, we consider R r0 , R r and the standard annotated semantics from Proposition 2:

P = νc.A | D 1 | . . . | D n such that for some 1 ≤ i ≤ n, D i is M new x : S R = E; C | C . Let LR = M (R)
K 0 ; R r0 |= P D H l 1 ,...,ln ====⇒ K; R r |= P D H where LR ⊆ R r and ∀k + ∈ R r0 , K 0 Rr 0 k -. (1)
From Proposition 4, the annotation of the initial process is well-annotated. From Proposition 3 on this annotation, we get for all i ∈ D H : R r D i : well-annotated and, due to (1), for all k + ∈ R r we have K Rr k -. Since LR ⊆ R r , and given the (assign T) rule, we also have

R r M ∪ {x H → v } (x := v) (H) : well-annotated.
Therefore, we satisfy all conditions of Definition 13:

(K; R r |= P ) R (K; R r |= P i:x=v ).
Finally, we conclude with Proposition 5.

Example 9

From the example of Section 4, let consider the variable sharedSecret : Int {serverKey,Alice,Bob} of the device SD. The Theorem 1 states that only devices from Entitled({serverKey, Alice, Bob}) System→System can distinguish between sharedSecret = 42 or sharedSecret = 43. Whatever are the reductions, these devices contains for sure Srv since its key is known from the beginning and SD since it creates Alice. The only threat is that the channel otherPrin has not been established with MD or that c has not been established with the device RD of Bob. These threats could be removed by an additional authentication protocol or the use of a private channel (for instance if the connection between SD and MD is a direct wired connection). This means that not knowing which code is run on Srv and RD is not a threat as long as Srv and RD guarantee that their codes are well-typed.

Finally, we state a standard security property in the simpler case where there is no untyped attacker. Given a process P , if, at some point, we change the value that a variable is bound to in memory, where that variable has been typed with right R, then new reductions will not alter values in memory locations that have been typed strictly less confidential than R (i.e., those variables have rights that contain public keys not contained in R).

Theorem 2 Let P be a valid initial process. We consider a reduction P → P with

P = D 1 | . . . |D n such that for some i, D i is M new x : S R = E; C | C .
Let v be any value of type S. Let P = D 1 | . . . |D n such that P → * P then there exists Q such that P x=v → * Q where for all memory location y that have been created in any device with rights R l with R R l , we have obf(R, v P ) = obf(R, v Q ) where v P is the value of y in P and v Q the value of y in Q .

Implementation:

We have implemented an interpreter for this language in Ocaml2 . The program strictly follows the extended semantics, it has commands to add a new device; to do an internal reduction on the selected thread(s) of the selected device(s); to perform an attacker communication, and to type-check each device of the system according to the annotations. To define a device which starts with keys in memory, two additional commands are provided which are allowed only as a preamble: load principal p from i; and load x : PubKey from i; where i is a number; an identical i on two devices represents a shared key. This implementation demonstrates that the syntax is well-defined and effective, and allows us to test the invariance of the properties with demonstrative examples. The example of Section 4 has been tested using this implementation: we are able to reduce the process such that Bob gets the secret from Alice and we can verify that each step correctly type-checks.

Conclusion

We have presented a security type system that provides location based correctness results as well as a more traditional non-interference result. The key novelty of our system is to allow principal identities to be created and shared across devices in a controlled way, without the need for a global PKI or middleware layer. Hence, our correctness result states that well-typed devices can control which other devices may acquire their data, even in the presents of untyped attackers. We have illustrated our system with an example of an open cloud server that accepts new users. This server does perform some monitoring of its users but our type system proves that it does not monitor the value of their data. We argued that our framework is particularly appropriate to cloud systems where organizations will want guarantees about where their data will be stored as well as the secrecy of their data.

A Additional Language Rules

Reduction is defined modulo the standard equivalence rules, which may be applied in any context, e.g.

D 1 | D 2 ≡ D 2 | D 1 D 1 | (D 2 | D 2 ) ≡ (D 1 | D 2 ) | D 2 M 1 C 1 | C 2 ≡ M 1 C 2 | C 1 M 1 C 1 | (C 2 | C 3 ) ≡ M 1 (C 1 | C 2 ) | C 2
The rules not mentioned in Figure 6 can be found in Figure 15 and the types rules not mentioned in Figure 8 and Figure 9 can be found in Figure 13 and Figure 13.

B Proofs of correctness

Here we provide the proof of all propositions of Section 5.

B.1 From rights to allowed devices

No proposition in this section. where K is a memory which is the union of the memories of A and all D i with i / ∈ S (variable names are renamed whenever there is a name conflict).

B.2 Definition of the attacker and of the open process semantics

Proof. By induction on the number of reduction steps. We assume that the result is true for n -1 reductions i.e we have P | A → * P | A which is mimicked by

K |= P S l 1 ,...,lm ----→ K |= P a S
and we prove that if P | A → P | A then we can also have

K |= P a S l? -→ K |= P a S .
1. If the last reduction involves devices which are part of S, then this same reduction can be done on P a S . ------→ K |= νc.P 1 {(c) att /c} is possible since v has been produced from values into memory not in S and the attacker can derive all these values. 4. If the last reduction is a channel establishment between a device from S and a one not from S, the proof is similar. Note that the new channel name is annotated with (c) att instead of c. -----→ K ∪ v |= νc.P 1 exists and we still have for all v in memory of a device of P which identifier is not in S, K ∪ v v .

Γ p ; Γ k ; Γ e 1 : Int R 1 Γ p ; Γ k ; Γ e 2 : S R 2 Γ p ; Γ k ; Γ x : Array{S} R 3 γ R 3 ⊆ pc ∩ R 1 ∩ R 2 pc; Γ p ; Γ k ; Γ c ; Γ C pc; Γ p ; Γ k ; Γ c ; Γ x[e 1 ] := e 2 ; C (assign array T) pc = ⊥ pc; Γ p ; Γ k ; Γ c ∪ {c :Chan(S ⊥ ) ⊥ }; Γ C pc; Γ p ; Γ k ; Γ c ; Γ accept c : Chan(S ⊥ ) ⊥ ; C (accept 1 T) p ∈ Γ p k ∈ Γ k {pub(p), k} ⊆ R 1 ⊆ R 2 ⊆ pc R 2 ; Γ p ; Γ k ; Γ c ∪ {c : Chan(S R 1 ) R 2 }; Γ C pc; Γ p ; Γ k ; Γ c ; Γ accept c : Chan(S R 1 ) R 2 from k as p; C (accept 2

B.3 Extended syntax with extra annotations

Proposition 2 Let P be a valid initial process such that P → * P and let LR a set of keys defined in P . If D H = Entitled(LR) P → * P is safe then there exists a standard annotation for the reduction provided by Proposition 1: K 0 ; R r0 |= P D H l 1 ,...,ln ====⇒ K; R r |= P D H where R r0 and R r are such that ∀k + ∈ R r0 , K 0 Rr 0 k -and LR ⊆ R r .

Proof. We assume that P is the n-th reduction of P . We denote by P m , P after m reductions. Let (I i , LR i ) = B P →P 1 (I i+1 , LR i+1 ) for 0 ≤ i < n and (I n , LR n ) = (∅, LR).

We now prove by induction on the number of reduction steps that the annotation K 0 ; R r0 |=

P D H l 1 ,...,lm = === =⇒ K m ; R rm |= P m D H such that R rm = 0≤k≤m
LR i is standard. Note that as the set is safe, we have ∀k + ∈ R r0 , K 0 Rr 0 k -. Moreover we also LR ⊆ R rn by definition.

LR m ⊆ R rm where LR m contains all the keys of LR which have already been created.

The only reduction we need to consider are the one which might not be standard i.e. when a reduction which creates a new principal pv = prin(k + , k -, {k 1 , . . . , k n }) where k is in 0≤k≤m LR i . However, by design of the B function, we have {k 1 , . . . , k n } ∈ R rm-1 : the reduction is standard.

E ::= m 1 a variable of K | encr E 2 (E 1 ) encrypt E 1 with rights E 2 | decr E 1 (E 2 ) decrypt E 1 with
, . . . E n } tuple | E 1 [E 2 ] element of a tuple | E 1 ⊕ E 2
where ⊕ is +, -, ×, . . . | i an integer

M (E 1 ) = v M (E 2 ) = {k 1 + , . . . , k n + } fresh(n) M (encr E 2 (E 1 )) = enc {k 1 + ,...,kn + },n (v) (attacker encryption) M (E 1 ) = enc {k 1 + ,...,kn + },n (v) M (E 2 ) = k i -i ∈ {1, . . . , n} M (decr E 2 (E 1 )) = v (attacker decryption) M (E 1 ) = prin(k + , k -, r) M (E 2 ) = r M (alter(E 1 , E 2 )) = prin(k + , k -, r) (attacker alter) M (E) = i ∈ N M (freshprin(E)) = prin(k i + , k i -, {}) (attacker fresh)
Figure 16: extended expressions of the attacker and some of their reduction rules.

In the following auxiliary lemma, we state that low expressions reduces to low values while high expressions reduces to high values.

Lemma 1 Let e and M be such that the sub-expressions e i : R i of e are such that M (e i ) = (v i ) i with x i = H iff. R r ⊇ R i . Let (v) such that M (e) = (v) . We have: e : S R with R r ⊇ R iff = H.

Proof. If R r ⊇ R, we consider all constructors:

1. e = a + b. If e : S R with R r ⊇ R, due to the typing rule a or b has type Int R with R r ⊇ R , by the induction hypothesis, one of them reduced to a high value and the reduction rule states that the result has to be high. If e : S R with R r R due to the typing rule both a and b has type R r R , by hypothesis both of them reduce to a low value, the reduction rule states that the result will not be low.

2. e = x[e ]. If e : S R with R r ⊇ R, due to the typing rule element T x or e has type with label R r ⊇ R , by the induction hypothesis, one of them reduced to a high value and the reduction rule states that the result has to be high. If e : S R with R r R, due to the typing rule both

x and e has type R r R , by hypothesis both of them reduce to a low value, the reduction rule states that the result will be low.

3. e = enc R (e 1 ). According to enc T, we have e : S ⊥ and reduces to a low value (since the new root is low).

4. e = release(P ), according to release T, e : secKey ⊥ and reduces to a low value.

5. e = pub(P ), according to pubKey T, e : k pub ⊥ and reduces a low value.

Lemma 2 Let R r , C, M, y such that R r y (C) (M ) : well-annotated for some Γ and where C is a command with an expression e such that Γ p ; Γ k ; Γ e : S R . We have that R r ⊇ R iff. M (e) = (v) H for some value v.

Proof. By induction on the structure of e. If e is a variable, we conclude from Item 2 of Definition 7. For the inductive case, we use Lemma 1 to conclude.

≤ i ≤ n we have R r D i : well-annotated. If K; R r |= νc.D 1 | . . . | D n l ? -→ K ; R r |= νc .D 1 | . . . | D n then for all 1 ≤ i ≤ n we have R r D i : well-annotated. Moreover if the reduction is standard, we have K Rr k -for all k + ∈ R r .
Proof. W.l.o.g. we consider that the reduction is done on D 1 (eventually D 1 and D 2 if it is a communication between two device). We write

D 1 = M 1 (C 1 ) (x) | . . . | (C n ) (xn) and D 1 = M 1 (C 1 ) (x ) | . . . | (C n ) (xn) . Let Γ p i , Γ ki , Γ i and pc i such that R r M i (C i ) (x i )
: well-annotated. We prove all the conditions of well-annotated separately.

1. C i is well-typed for some pc i , Γ i By hypothesis, we know that C i is well-typed for some Γ p i , Γ ki , pc i , Γ i . If C i := C | C then the two new threads after reduction are well-typed with Γ p i , Γ ki , Γ i and pc i due to (para T). If C i :=!C then the two new threads are also well-typed due to (bang T). Otherwise, the form of C i is c; C i (up to name renaming) or cond(c) then C a else C b where C a or C b is an renaming of C i . All the corresponding type rules enforces that C i is well-typed only if C i is well-typed.

2. For all location x in M , we have

• either x L → (v) L in M for some value v and x ∈ Γ p ∪ Γ k • or Γ p ; Γ k ; Γ x : S R and -if R r ⊇ M (R), x H → (v) H in M , -if R r M (R), x L → (v) L in M for some value v.
First, we consider the annotation of variables. Once a memory location is created, there is no reduction rule to change its type (low or high), R r never becomes more confidential (R r increases only with new fresh keys) and all types rules enforce that the reduced command C can be typed with a context which preserves rights for all variables. For these reasons, if the property holds when a variable is created, it holds forever. During creation, by design of the annotated rules, the location is created as high or low only depending on if R r ⊇ R for regular variable and is always low when the location contains a principal or a key. For inputs, since the input command does not specify the type, we look at the annotation of the channel, which is itself defined from the condition R r ⊇ R 1 in the annotated semantic rules about channel creation (high open priv), (low thread/high value open priv), (low open priv) for channel opening with the attacker, from the fact that K Rr k -for all k + ∈ R r we know that the channel has a type for values less confidential than R r .

For the annotation of values, we need to check that no high values are stored into low memory (the annotation always produces high values from high memory). The reductions which set new values to low memory locations are the following: (low assign), (low new), (deref S), (low dec true), (low i/o) and (att. input). For the first rules ((low assign), (low new) ), the stored value is the evaluation of an expression E. Since the type rules associated to these commands enforces E to be of a type R such that R r ⊇ R, according to Lemma 2, E reduces to a low term. The argument is the same for (deref S).

For the internal communication (low i/o), the argument is the same except that the type judgment of E is on the other device. For the input from the attacker att. input, the rule set that attacker's inputs are low.

For rule (low dec true) where one layer of encryption is removed, we have to ensure that the decrypted value is low. The typing rule requires that R r R 1 and R 2 ⊇ R 1 which implies R r R 2 . From Item 7, we conclude.

The rule (high thread/low var dec true) can never be applied. Indeed, if the cipher is high, from Lemma 2, the cipher has a high type, then the typing rule enforce the program counter to be high which means the thread has to be high.

R r ⊇ pc if and only if y = H.

First note that all types rules of commands requires that their continuation can be typed with the same program counter. The interesting cases are when the type rules requires the continuation to be typed with a more restrictive program counter and, for the other direction of the equivalence, when the reduction rules reduces a low thread into a high thread.

• Conditional is typed with (if T): the program counter pc of the continuation if set to R r ⊇ pc when at least one of the expressions is more confidential than R r (we assume that initially R r pc). According to Lemma 2, one of the expression reduces to a high value. In this case, the reductions rules (high if true) and (high if false) sets the thread to high. Reciprocally, if the thread is set to high, on of the value is high and according to Lemma 2 the type of the continuation is R r ⊇ pc .

• Secure channel opening is typed with (connect 2 T) and (accept 2 T). Both type rules requires the continuation to have a program counter pc set such that R r ⊇ pc iff R r ⊇ R 2 where R 2 is the right to see the channel. The reduction rule (high open priv) can be applied only when R 2 and R 2 , the rights to see the channel of both threads are equal and sets both threads to high exactly with the same condition.

• Decryption is typed with (dec T), the program counter pc of the continuation if set to R r ⊇ pc when the expression to decrypt has rights R with R r ⊇ R. This coincides with the reductions rules (high dec true), (high thread/low var dec true),(high dec false) where the thread becomes high iff the decrypted value is high (due to Lemma 2).

3. For all c in the thread such that Γ c :

Chan(S R 1 ) R 2 , the annotation of c is c z (z ) where z = H iff. R r ⊇ R 2 , z = H iff. R r ⊇ R 1 .
The annotation on channel is definitively fixed once it is created. 5 For all (c) att , we have Γ (c) att :

Chan(S R 1 ) R 2 with R r R 2 and R r R 1 .
The interesting case is the creation of a new channel with the attacker. This can be done through rules (att. open server) and (att. open priv client). By hypothesis, the attacker does not know any key in R r so it can only provides a secret key k -not in R r . Due to (connect 2 T) or (accept 2 T), R 1 and R 2 should contains k + . Therefore neither R 1 or R 2 is a subset of R r , which means R r R 2 and R r ⊇ R 1 as γ is required to be empty.

6 If y is L, then there is no c H (H) in C. This is true before reduction. Since establishing a new channel c H (H) set the thread to high, the property is also true after reduction.

7 For all x in memory, if a sub-term of x is enc RS,n ((t) H ) then R r ⊇ RS.

The encryption typing rule for

E = enc R (E 1 ), (dec T), requires that E 1 : R 1 is such that R 1 ⊇ R. From Lemma 2, we have M (E 1 ) = (v) H implies R r ⊇ R 1 and therefore R r ⊇ R which allows to conclude. 8 For all x in memory, if a sub-term of x matches enc LR ,n (prin(k, LR, )) then LR = LR or k + / ∈ R r .
Encapsulated principals can only be produced with a release(P ) expression or by an input of the attacker. In the first key, the release reduction (release E) always encrypts the principal prin(k + , k -, LR) with the keys of LR in the other case since by hypothesis we have K Rr k - we also have K Rr prin(k, r,) for any r so the attacker cannot output this value.

• Case where the reduction rule applied to P A is (att. output) on a thread (output e (c) att ; C A ) (z) , with label out((c A ) att , x). According to Item 5 of Definition 13 the channel is of type Chan(S R 1 ) R 2 with R r R 1 and R r R 2 . According to (output T), we have R 2 pc and so R r pc. According to Item 4 of Definition 7 the thread is low (z = L). Therefore there exists an identical thread in P B where the same label reduction is possible. Moreover, according to (output T), we have e : R 1 with R r R 1 so according to Lemma 2, M A (e) = (v A ) L for some v A . According to Lemma 5, we have obf

(R r , v B ) = obf(R r , v A ), hence K A R K B .
• Case where the reduction rule applied to P A is (att. input) on a thread (input (c) att (x); C A ) (z) with label in((c A ) att , f ). According to Item 5 of Definition 13 the channel is of type Chan

(S R 1 ) R 2 with R r R 1 and R r R 2 .
According to (input T), we have R 2 pc and so R r pc. According to Item 4 of Definition 7 the thread is low (z = L). So there is an identical thread in P B (which reduces with the same label). According to Lemma 3 we have obf(R r , K A (f )) = obf(R r , K A (f )). Therefore, the new memories M A and M B are equivalent.

When the reduction is made on a thread where R r M (C) (L) : well-annotated In that case, we use the fact for any thread (C A ) (L) on some device with memory M A on which the reduction happens, there exists a thread (C B ) (L) on the other process with memory M B such that

C A C B and M A R Rr M B .
We prove all the requirements sequentially: first, we prove that R r reduces to the same R r in both process. Secondly, we prove the commands reduce to equivalent commands. Thirdly, we prove the equivalence of the new memories.

1. We have R r A = R r B The one reduction that changes R r is (high newPrin). When reference rights change in a reduction due to (high newPrin), the thread is low due to the typing rule so the reduction can also occurs in process B. We conclude by renaming the new key variables of both processes to the same name.

2. Reductions rules for C B is the same as for C A : C A = C B (or both new threads are high)

There are two cases for "if", and two cases for "dec"

• The rule C A → C A is (high if true) or (high if false). In these cases, according to Lemma 2, the evaluated expressions was high. So it is also true for C B therefore the conditional expression of C B also evaluates to a high value according to Lemma 2. On the other hand, the new thread C A is H so whatever C B reduces to the then or the else branch, the condition about commands of Definition 13 is satisfied.

• The rule C A → C A is (low if true) or (low if false). This means the expression evaluates to a low value. In addition, the evaluation returns an integer which implies the expression can only contains +, integers and variables. This implies that the results is only dependent on low values: since low values in C A and C B are the same both reduce according to the same rule.

• The rule is (low dec false), (low dec true) or (low thread/high var dec true). Since the value to decrypt is low, the value in A and B differ only on high sub-terms which means that the encryption key is the same, so both processes take the same branch.

• The rule is (high dec false) or (high dec true): whatever (low dec false) or (low dec true) is taken the thread become high on A and B.

3. New values in memories are such that M A R Rr M B . First of all, because the rights are the same in C A and C B and premisses on the rules depends only on rights, the high or low rule is applied for both command.

• Rules that store values into high memory locations (high new), (high assign), (low thread/high var dec true), (high dec true): they affect high locations so condition M A R Rr M B holds whatever is the stored value.

• Rules that store values into low memory locations: (low new), (low assign), (low dec true), (deref S) according to Item 2 of Definition 7, these values are not high so, according to Lemma 5, we have obf(R r , v A ) = obf(R r , v B ).

• Rule (low register): K A is in a low memory location so K A = K B and so the new principals are identical.

• Creates a principal (high newPrin) and (low newPrin): the new value contains fresh values and rights that are identical in A and B.

When the reduction is done on a thread C where R r M (C) (H) : well-annotated 1. Internal reductions does not change the equivalence class of the process (so the other process can simulate it with no reduction). Indeed, first, there is no reduction that reduces a high thread to a low thread: the reduced command C does not impact the equivalence class of the process. Secondly, the reductions that create or change memories location are: (high new), (high dec true) and (high assign). In each case, the type rules states that pc ⊇ R where R is the right of the memory. Due to Item 4 of Definition 7, we have that pc is high. Hence R is high too, so the rule either creates or change a memory location with flag H.

When the reduction is made between two threads C 1 and C 2 where C 1 is high.

• If both C 1 and C 2 are high. The only possible reduction are (high i/o) and (high open priv).

In case of (high open priv), from Item 6, we have R r ⊇ pc. The types rules (connect 2 T) and (accept 2 T) enforces that R 1 and R 2 are high. Due to Item 3, the channel is annotated with c H (H) . In case of (high i/o), the type rules (input T) enforces that all received values are stored into high memory. Since high threads and high memory locations are free to differ between the two processes, the equivalence is preserved after reduction.

• If C 2 is low. Any annotation variant of the rule (i/o S) is not possible when one thread is low and the other is high. Indeed, according to Item 3 of Definition 7, there is no c H H channel on the low thread. On the other high thread, a c L L or c H L channel has a low type according to Item 3 of Definition 7, so according to (output T) and (input T) they cannot be used one this thread. So only establishing connection is possible with rule (high open priv) where the client is on the low thread C 2 and the server is on the high thread C 1 . Due to the reduction rule (high open priv), C 2 is a high thread and C 1 is high too so the equivalence is preserved in both processes.

When the reduction is made on two threads which are low.

For all communication opening rules, rights in both process are identical since the public keys of the rights set are public. So both processes thread reduces either to a high thread or a low thread. Hence the two reduced processes remains in the same equivalent class.

For the input/output reduction rule (low i/o), according to Item 6 of Definition 7, the channel type can only be c L L or c H L since the threads are low. On the output thread, high values are sent only on c H L channels. According to Item 3, on the input side c H L has type Chan(S R ) R with R r ⊇ R. According to (input T), the value is stored in a high memory location so even if the values differ between P A and P B memories are still equivalent. On the other hand, if the values v A and v B sent on the channels are not high then they have to be equivalence: obf(R r , v A ) = obf(R r , v B ).

Proposition 5 Let P A be (K A ; R r |= νc.Q A ) and P B be (K B ; R r |= νc .Q B ), where both are wellannotated processes such that P A R P B , Furthermore assume that for all k + ∈ R r we have K A Rr k -. Then the processes are annotated equivalent, P A ≈ l P B (with the annotations removed).

Proof. The first item is a direct consequence of Lemma 4 The two last items are a consequence of Proposition 6 with the fact that when the annotation is standard, according to Proposition 3, we have that ∀k + ∈ R r , K i Rr k -is preserved by the reduction, so the proposition can be generalized to any number of reduction steps.

B.5 Main theorems

Theorem 2 Let P be a valid initial process. We consider a reduction P → P with P = D 1 | . . . |D n such that for some i, D i is M new x : S R = E; C | C . Let v be any value of type S. Let P = D 1 | . . . |D n such that P → * P then there exists Q such that P x=v → * Q where for all memory location y that have been created in any device with rights R l with R R l , we have obf(R, v P ) = obf(R, v Q ) where v P is the value of y in P and v Q the value of y in Q .

Proof. Since there is no untyped attacker, we can use non-standard annotations. We consider the one such that at the beginning R r contains all the keys of R which are present in some memory, and which add a key in R r if and only if this key is in R. From Proposition 6 on this annotated process, we get the existence of Q such that Q≈ P which imply that for all memory M i in P and M i in Q, we have M i R R M i . By definition of R R , we conclude.

C Annotated rules

We define ↑ (x, y) to be L except if x = y = H.

M (e 1 ) = (v) t M (e 2 ) = (v ) t v = v ↑ (t, t ) = L K; R r |= M (if (e 1 = e 2 ) then C 1 else C 2 ) (z) A → K; R r |= M (C 2 ) (H) A (high if false)

PFigure 1 :

 1 Figure 1: The syntax of devices, values, principals and rights where k -/k + is a secret/public key pair.

SFigure 2 :

 2 Figure 2: The types syntax

Figure 3 :

 3 Figure 3: The syntax of the commands.

Figure 4 :

 4 Figure 4: The syntax of the expressions

Figure 7 :

 7 Figure 7: Alice sharing data with Bob using a cloud service. N.B. this code does not authenticate Bob.

Figure 11 :

 11 Figure 11: Definitions of Sender, Receiver and Mobile Processes

Example 7

 7 We consider the system consisting of MD | SD from Figure 12 running in parallel with an untyped attacker A. The corresponding open process is initially {} |= SD A | MD M . Assume that Device M (MD M ) reduces with the attacker instead of SD A , we have:

Definition 5

 5 Given a process P = νc. D 1 | . . . | D n and {I 1 , . . . , I m } ⊆ {1, . . . , n}, let c the names of channels between devices of {I 1 , . . . , I m } we define the subprocess of devices P {I 1 ,...,Im} = νc .D I 1 | . . . | D Im where D i is D i where each channel name c ∈ c \ c have been replaced by an attacker-channel name (c) att .

  be the set of keys corresponding to R, let D H = Entitled(LR) P →P and let K be the unions of memories of the devices of P whose indexes are not in D H and of device A . If D H is safe (as stated in Definition 3), then (K |= P D H ) ≈ l (K |= P i:x=v D H ). Proof. According to Proposition 1, we have K 0 |= P D H l 1 ,...,ln ====⇒ * K |= P D H where K 0 = i /

Proposition 1

 1 Let P = νc.A | D 1 | . . . | D n where all D i are well-typed and A is an untyped device. If P → * νc .P , then for all subset S of {1, . . . , n}, there exist l 1 , . . . , l m and K (the attacker knowledge at the end of the execution) such that K |= P S l 1 ,...,lm = === =⇒ K |= P S

T)Figure 13 :Figure 14 :

 1314 Figure 13: Other type rules for commands

5 .

 5 If the last reduction νc.c.P | A → P 1 | A 1 is (i/o S) from S to outside S transferring v on c then the labeled reduction K |= νc.P out(c,v)

Proposition 3

 3 Let K; R r |= νc.D 1 | . . . | D n an open process such that for all k + ∈ R r we have K Rr k -and for all 1

  The channel establishment rules (high open priv), (low thread/high value open priv), (low thread/high value open priv) and (low open priv) all enforce this property in their premisses. Public channels have type ⊥ and are annotated with c - L .

M

  (e) = (v) t fresh(y) R r ⊆ M (R) K; R r |= M (new x : S R = e; C) (z) A → K; R r |= M ∪ x H → (v) H (C{y/x}) (z) A (high new) M (e) = (v) t R r M (R) fresh(y) K; R r |= M (new x : S R = e; C) (z) A → K; R r |= M ∪ x L → (v) t (C) (z) A (low new) (M ∪ x L → (v) t )(e) = (v ) t K; R r |= M ∪ x L → v (x := e; C) (z) A → K; R r |= M, x L → (v ) t (C) (z) A (low assign) (M ∪ x H → (v) H )(e) = (v ) t K; R r |= M ∪ x H → (v) H (x := e; C) (z) A → K; R r |= M ∪ x H → (v ) H (C) (z) A (high assign) M (e 1 ) = (v) L M (e 2 ) = (v) L K; R r |= M (if (e 1 = e 2 ) then C 1 else C 2 ) (z) A → K; R r |= M (C 1 ) (z) A (low if true) M (e 1 ) = (v) L M (e 2 ) = (v ) L v = v K; R r |= M (if (e 1 = e 2 ) then C 1 else C 2 ) (z) A → K; R r |= M (C 2 ) (z) A (low if false) M (e 1 ) = (v) t M (e 2 ) = (v ) t ↑ (t, t ) = H K; R r |= M (if (e 1 = e 2 ) then C 1 else C 2 ) (z) A → K; R r |= M (C 1 ) (H) A (high if true)

  RS ; C | decrypt p e as x : S RS then C 1 else C 2 | register p 1 e as p 2 then C 1 else C 2

	k as p; C
	| accept c : Chan(S R ) R from k as p; C
	| output c e ; C
	| input c(x); C
	| synchronized{G}; C 2
	| newPrin p

  Example 5 The different roles of R 1 and R 2 is illustrated in these two programs. new x : Int {pub(Alice),bob} = 7; accept c : Chan(Int {pub(Alice),bob} ) {pub(Alice),bob} from bob as Alice;

	if (x > 10){
	x := x + 1;
	output c x ; }
	new x : Int {pub(Alice),bob} = 7;
	accept c : Chan(Int {pub(Alice),bob} ) ⊥ from bob as Alice;
	{if (x > 10){
	x := x + 1; }}
	| output c x ;

  the secret key E 2 | alter(E 1 , E 2 ) the principal E 1 where its rights are now E 2 | freshprin(E) the E-th principal generated by the attacker

	| pub(E)	the public key of a principal E
	| sec(E)	the secret key of a principal E
	| rights(E)	the rights of a principal E
	| {E 1

Although middleware for e-commerce (such as CORBA) was popular in the 1990s, that approach was discredited by experience, while SOAP-based approaches have been largely superseded by REST-based Web services, that deliberately eschew the notion of a middleware at least for Internet communication..

Γ p ; Γ k ; Γ x : S R 1 Γ p ; Γ k ; Γ e : S R 2 R 1 ⊆ pc ∩ R 2 pc; Γ p ; Γ k ; Γ c ; Γ C pc; Γ p ; Γ k ; Γ x := e; C (assign T) pc = ⊥ Γ p ; Γ k ; Γ x : PubKey ⊥ pc; Γ p ; Γ k ∪ {k}; Γ c ; Γ C pc; Γ p ; Γ k ; Γ c ; Γ let k = x in C (deref T) Γ p ; Γ k ; Γ e 1 : S R 1 Γ p ; Γ k ; Γ e 2 : S R 2 pc ∩ R 1 ∩ R 2 ; Γ p ; Γ k ; Γ c ; Γ C 1 pc ∩ R 1 ∩ R 2 ; Γ p ; Γ k ; Γ c ; Γ C 2 pc; Γ p ; Γ k ; Γ c ; Γ if (e 1 = e 2 ) then C 1 else C 2 (if T) Γ p ; Γ k RS 1 pub(p) ∈ RS 1 p ∈ Γ p Γ p ; Γ k ; Γ e : Enc{S} R 2 RS 1 ⊆ (R 2 ∩ pc) pc ∩ R 2 ; Γ p ; Γ k ; Γ c ; Γ ∪ {x : S RS 1 } C 1 pc ∩ R 2 ; Γ p ; Γ k ; Γ c ; Γ C 2 pc; Γ p ; Γ k ; Γ c ; Γ decrypt p e as x : S RS 1 then C 1 else C 2 (dec T) pc = ⊥ pc; Γ p ; Γ k ; Γ c ∪ {c :Chan(S ⊥ ) ⊥ }; Γ C pc; Γ p ; Γ k ; Γ c ; Γ connect c : Chan(S ⊥ ) ⊥ ; C (connect 1 T) Γ p ; Γ k R 1 Γ p ; Γ k R 2 p ∈ Γ p k ∈ Γ k {pub(p), k} ⊆ R 1 ⊆ R 2 ⊆ pc R 2 ; Γ p ; Γ k ; Γ c ∪ {c : Chan(S R 1 ) R 2 }; Γ C pc; Γ p ; Γ k ; Γ c ; Γ connect c : Chan(S R 1 ) R 2 to k as p; C (connect 2 T) Γ p ; Γ k ; Γ e : S R 3 c : Chan(S R 1 ) R 2 ∈ Γ c pc = R 2 R 1 ⊆ R 3 pc; Γ p ; Γ k ; Γ c ; Γ C pc; Γ p ; Γ k ; Γ c ; Γ output c e ; C (output T) c : Chan(S R 1 ) R 2 ∈ Γ c R 2 = pc pc; Γ p ; Γ k ; Γ c ; Γ ∪ {x : S R 1 } C pc; Γ p ; Γ k ; Γ c ; Γ input c(x); C (input T) p 2 ∈ Γ p Γ p ; Γ k ; Γ e : PrivKeyEnc ⊥ pc; Γ p ∪ {p 1 }; Γ k ; Γ c ; Γ C 1 pc; Γ p ; Γ k ; Γ c ; Γ C 2 pc = ⊥pc; Γ p ; Γ k ; Γ c ; Γ register p 2 e as p 1 then C 1 else C 2 (register T) Figure 8: Typing rules for main commands

https://github.com/gazeaui/secure-type-for-cloud

If the last reduction involves devices which are not part of S then no reduction has to be done in the open semantics.

v : T ∈ Γ Γ p ; Γ k ; Γ v : T (var T) Γ p ; Γ k ; Γ i : Int ⊥ (int T) P ∈ Γ p Γ p ; Γ k ; Γ pub(P ) : PubKey ⊥ (pubKey T) Γ p ; Γ k ; Γ e 1 : Int R 1 Γ p ; Γ k ; Γ e 2 : Int R 2 Γ p ; Γ k ; Γ e 1 + e 2 : Int R 1 ∩R 2 (Sum T) Γ p ; Γ k ; Γ v 1 : S R . . . Γ p ; Γ k ; Γ v n : S R Γ p ; Γ k ; Γ {v 1 , . . . v n } : Array{S} R (array T) Γ p ; Γ k ; Γ x : Array{S} R 1 Γ p ; Γ k ; Γ e : Int R 2 Γ p ; Γ k ; Γ x[e] : S R 1 ∩R 2 (element T) Γ p ; Γ k ⊥ (public T) pc; Γ p ; Γ k ; Γ c ; Γ C 1 pc; Γ p ; Γ k ; Γ c ; Γ C 2 pc; Γ p ; Γ k ; Γ c ; Γ C 1 | C 2 (paraT) pc; Γ p ; Γ k ; Γ c ; Γ skip (skip T) pc; Γ p ; Γ k ; Γ c ; Γ C pc; Γ p ; Γ k ; Γ c ; Γ ! C (bang T)

Acknowledgement

We would like to thank Alley Stoughton for her help with this work; her insightful comments and useful advice greatly improved this paper.

Finally, we prove that when the annotation is standard, we have K Rr k -for all k + ∈ R r . The result is immediate for reductions which do not change K or R r .

The set K increases only with the reduction (att. output). The values which contains secret keys of R r are of type PrivKeyEnc (or a combination of tuples and encryptions of this type). According to item 8, any prin(k + , k -, R) is encrypted with R. Moreover, by definition of standard annotation, all keys prin(k i + , k i -, R i ) in R r are such that all keys of R i are also in R r . Since K Rr k, the attacker cannot decrypt the key.

The reduction which modify R r is (high newPrin), but the new key is fresh so the attacker cannot derive new facts from the fact that K Rr v is syntactically more powerful than K Rr v.

Proposition 4 Given a valid initial process

Proof. Condition item 6 of well-annotated is true since pc = ⊥ and the tread is L. Since M i and Γ only contains principals and public keys, the other conditions which concerns other kind of values and variables are immediately true.

B.4 Labelled bisimilarity

Lemma 3 When two memories M 1 and M 2 only contains low locations, M 1 k -and M 2 k - for all k such that k + ∈ R r and M 1 R Rr M 2 implies that, for all extended attacker expression f (Figure 16),

Proof. By induction on the structure of f . This is true if f is a variable or an integer. We assume that obf(R r , M 1 (f i )) = obf(R r , M 2 (f i )) for all sub-expressions f i of f . For freshprin(i), i has to evaluate has an integer. Since the function freshprin(i) returns the i-th principal of a determined sequence of principals, the expression returns the same key in both memory. For encr r (f ), since the extended expression r has to evaluate to a right it evaluate to the same right for both memories, so the result is either obfuscated with both memories or none of them. For decr s (f ), the result is immediate if f evaluates to a cipher which is not obfuscated. Otherwise, f is a cipher encrypted with rights r , R r ⊇ r , by hypothesis, we have that s cannot corresponds to any key in r therefore the decryption fails (result NaV) in both memories.

Lemma 4 When two memories M 1 and M 2 only contain low locations,

Proof. Let f and g be two extended expressions which evaluates to the same value

However the obfuscation function does not obfuscate the nonce of ciphers. And the attacker power does not allow the attacker to generate a cipher with a nonce which is not fresh (this is due to the fact that nonce cannot be extracted from ciphers from which the key is unknown). Therefore each nonce is uniquely associated to a unique value. As nonces are equals the obfuscated values are equals too.

Lemma 5 Given a command context C, a set of public keys R r , two memories M and M , an expression E and

Proof. By induction on the structure of E.

2. If E is e 1 + e 2 with M (E) = (v) L , due to rule (low sum) and (high sum) v is low implies that none of its sub-expressions is high, we conclude by induction.

3. For E = x[n], the principle is the same. [START_REF] Bengtson | Refinement types for secure implementations[END_REF]. For E = x{E 1 , . . . , E n }, the principle is also the same.

5

.

6. For expressions which involves principals (pub(p) and release(p)) we conclude as principals are not stored in high location.

Proposition 6 Let K 1 ; R r |= P 1 and K 2 ; R r |= P 2 be two well-annotated processes such that ∀k

) and P 1 R P 2 , we have:

-→ P 2 and P 1 R P 2 for some P 2 .

2. if P 1 → P 1 , then P 2 → ? P 2 and P 1 R P 2 for some P 2 , Proof. To avoid conflict of indexes, we consider P A and P B instead of P 1 and P 2 .

When the reduction is a labeled reduction with the attacker

• Case where the reduction rule applied to P A is (att. open public) on a thread (connect (c A ) att :

. From (connect 1 T), we know that R r ⊇ pc. From Item 4 of Definition 7, we know that this reduction is possible only when x = L. Hence there exists the same thread in P B . The reduction on the corresponding thread of P B leads to C A through the same label in(c, S) up to the name of (c B ) att , but they are equal up to alpha-renaming of the channel name. Hence we have the condition on commands of Definition 13. Finally the memory is unchanged and the attacker does not learn any value any both process: the condition about memories of Definition 13 and memory equivalence of the attackers hold.

• Case where the reduction rule applied to P A is (att. open server), on a thread (connect (c A ) att :

, with label in((c A ) att , k s -, k c + , S, r, r ) be the values in the label of the reduction. Since k s + / ∈ R r (according to our hypothesis), due to (att. open server), k / ∈ R r and due to the type rule (accept 2 T), we have R r R 1 and R r R 2 . According to Item 4 of Definition 7, the thread is low (x = L). So an identical thread exists in P B , and since the label enforces S, R 1 and R 2 to be the sames, it reduces to C A up to the renaming of the channel name. Finally, K A , K B , M A and M B remain the sames.

• The case where the reduction rule applied to P A is (att. open priv client) is similar.

(low dec true)

(high thread/low var dec true)

(low thread/high var dec true)

(high dec true)