Jovanka Pantović

Ivan Prokić

Hugo Torres Vieira

A Calculus for Modeling Floating Authorizations

Controlling resource usage in distributed systems is a challenging task given the dynamics involved in access granting. Consider, e.g., the setting of floating licenses where access can be granted if the request originates in a licensed domain and if the number of active users is within the license limits. Access granting in such scenarios is given in terms of floating authorizations, addressed in this paper as first class entities of a process calculus model, encompassing the notions of domain, accounting and delegation. We present the operational semantics of the model in two equivalent alternative ways, each informing on the specific nature of authorizations. We also introduce a typing discipline to single out systems that never get stuck due to lacking authorizations, addressing configurations where authorization assignment is not statically prescribed in the system specification.

Introduction

Despite the continuous increase of computational resources, their usage will always nevertheless be subject to accessibility and availability. Regardless whether such resources are of hardware or software in nature, they might have finite or virtually infinite capabilities. Physical examples, that can be mapped to finite capabilities directly, include devices such as printers or cell phones, and components of a computing system such as memory or processors. Virtual examples, such as a shared memory cell or a web service, can be more easily seen as having infinite potential but often their availability is also finitely constrained. In general, ensuring proper resource usage is a crucial yet non trivial task, given the highly dynamic nature of access requests and the flexibility necessary to handle such requests, while ensuring secure and efficient system operation.

For security purposes it is crucial to control that access is granted only to authorized users, but also to enforce that access granting is subject to availability. Concrete examples include a wireless access point that has a given access policy and a limited capacity on the number of connected devices, and a software application that is licensed to be used by an institution in a bounded way. Both examples address limited capabilities that are accessible in a shared way to authorized users. We thus identify a notion of floating authorization, adopting the terminology from the licensing realm, where access to resources can be granted to any authorized user in a given domain up to the point the capacity is reached. We also identify a notion of implicit granting since users may be granted access directly when using the resource (e.g., running the licensed software).

Considering the licensing setting, we find further examples that inform on the dynamic nature of authorizations. For example, a user deploys a software application on the cloud and provides the license himself (cf. Bring Your Own License [START_REF] Ferris | Offering additional license terms during conversion of standard software licenses for use in cloud computing environments[END_REF]), potentially losing access to run the application locally given the capacity constraints. We identify here a notion of authorization delegation, where the intention to yield or obtain an authorization is explicit. We therefore distill the following dimensions in a floating authorizations model: domain so as to specify where access may be (implicitly) granted; accounting so as to capture capacity; and delegation so as to model (explicit) authorization granting.

In this paper, we present a model that encompasses these dimensions, developed focusing on a process calculus tailored for communication centered systems. In our model the only resources considered are communication channels, so our exploration on authorization control is carried out considering authorizations refer to channels and their usage (for communication) is controlled. Our development builds on the π-calculus [START_REF] Sangiorgi | The Pi-Calculus -a theory of mobile processes[END_REF], which provides the basis to model communicating systems including name passing, and on a model for authorizations [START_REF] Ghilezan | Dynamic role authorization in multiparty conversations[END_REF], from where we adopt the language constructs for authorization domain scope and delegation. We adapt here the interpretation for authorization domains so as to encompass accounting, which thus allows us to model floating authorizations. To the best of our knowledge, ours is the first process calculus model that addresses floating resources (in our case authorizations) as first class entities. Naturally, this does not mean our language cannot be represented in more canonical models, only that we are unaware of existing approaches that offer abstractions that support reasoning on floating resources in a dedicated way.

After presenting the model, we show a typing discipline that ensures systems never incur in authorization errors, i.e., systems that are blocked due to lacking authorizations. Our type analysis addresses systems for which the authorization assignment is not statically given in the system specification, in particular when authorizations for (some) received names are already held by the receiving parties, a notion we call contextual authorizations. We first discuss some examples that informally introduce our model.

Model Preview

We present our language by resorting to the licensing setting for the sake of a more intuitive reading. First of all, to model authorization domains we consider a scoping construct, and we write (license)University to represent that the University domain holds one license. This means that one use of license within University is authorized. In particular, if University comprises two students that are simultaneously active, which we dub Alice and Bob, we may write (license)(Alice | Bob) in which case either Alice or Bob can be granted the license that is floating, but not both of them.

The idea is to support a notion of accounting, so when one of the students uses the license the scope is confined accordingly. For example, if Bob uses the license and evolves to LicensedBob then the system evolves to Alice | (license)LincensedBob where the change in the scope denotes that license is not available to Alice anymore. The evolution of the system is such that the authorization is directly confined to Bob, who is using it, so as to model implicit granting. At this point Alice cannot implicitly grab the authorization and gets stuck if she tries to use license. Hence, name license may be shared between Alice and Bob, so the (change of) scoping does not mean the name is privately held by LicensedBob, just the authorization. Now consider that Bob and Carol want to explicitly exchange an authorization, which can be carried out by a delegation mechanism supported by two communication primitives. We write auth license .UnlicensedBob to represent the explicit delegation of one authorization for license via communication channel auth, after which activating configuration UnlicensedBob. Instead, by auth(license).LicensedCarol we represent the dual primitive that allows to receive one authorization for license via channel auth after which activating configuration LicensedCarol . So by (license)(auth)auth license .UnlicensedBob | (auth)auth(license).LicensedCarol we represent a system where the authorization for license can be transferred leading to

(auth)UnlicensedBob | (auth)(license)LicensedCarol
where the scope of the authorization for license changes accordingly. The underlying communication is carried out by a synchronization on channel auth, for which we remark the respective authorizations (auth) are present. In fact, in our model channels are the only resources and their usage is subject to the authorization granting mechanism.

Our model supports a form of fairness and does not allow a "greedy" usage of resources. For example, in the configuration (license)(Alice | (license)LincensedBob) the user LincensedBob can only be granted the closest (license) first, not interfering with Alice, but can be also granted the top-level license if he needs both licenses.

We remark that no name passing is involved in the authorization delegation mechanism and that name license is known to both ends in the first place. Instead, name passing is supported by dedicated primitives, namely (comm)comm!license.Alice | (comm)comm?x .Dylan represents a system where the name license can be passed via a synchronization on channel comm, leading to the activation of Alice and Dylan where, in the latter, the placeholder x is instantiated by license. Notice that the synchronization can take place since the authorizations to use channel comm are given, one for each endpoint.

Name passing allows to model systems where access to channels changes dynamically (since the communicated names refer to channels) but, as hinted in the previous examples, knowing a name does not mean being authorized to use it. So, for instance, (comm)comm?x .x !reply.0 specifies a reception in (authorized) comm where the received name is then used to output reply, leading to an inactive state (denoted by 0). Receiving license in channel comm leads to (comm)license!reply.0 where the authorization for comm is still present but no authorization for license is acquired as a result of the communication. Hence the output specified using license is not authorized and cannot take place. We remark that an authorization for reply is not required, hence communicating a name does not entail usage for the purpose of authorizations. By separating name passing and authorization delegation we are then able to model systems where unauthorized intermediaries (e.g., brokers) may be involved in forwarding names between authorized parties without ever being authorized to use such names. For example (comm)comm?x .(forward )forward !x .0. which requires no further authorizations. Configuration (comm)comm?x .(auth)auth(x ).LicensedDylan shows a possible pattern for authorizing received names where, after the reception on comm, an authorization reception for the received name (using placeholder x) via auth is specified, upon which the authorization to use the received name is acquired. Another possibility for enabling authorizations for received names is to use the authorization scoping, e.g., (comm)comm?x .(x )LicensedDylan where the authorization (x) is instantiated by the received name. This example hints on the fact that the authorization scoping is a powerful mechanism that may therefore be reserved in some circumstances to the Trusted Computing Base, resorting to authorization delegation elsewhere.

To introduce the last constructs of our language, consider the system !(license)license?x.(x)license x .0 | (νfresh)(license)license!fresh.license(fresh).0

where a licensing server is specified on the left hand side, used in the specification given on the right hand side. By (νfresh)Domain we represent the creation of a new name which is private to Domain, so the specification on the right hand side can be read as first create a name, then send it via channel license, after which receive the authorization to use the fresh name via channel license and then terminate (the received authorization is not actually used in this simple example). On the left hand side, we find a replicated (i.e., repeatably available) reception on channel license, after which an authorization scope for the received name is specified that may then be delegated away. We now present our type analysis returning to the university scenario. Consider (exam)(minitest)(alice)alice?x.x!task .0 where there are available authorizations for exam and for minitest, and where alice is waiting to receive the channel on which she will send task . Assuming that she can only receive exam or minitest the authorizations specified are sufficient. Which authorization will actually be used depends on the received name, so the authorization is implicitly taken when the received channel is used. However, if a name viva is sent then the provided authorizations do not suffice.

In order to capture the fact that the above configuration is authorization safe, provided it is inserted in a context that matches the assumptions described previously, our type analysis records the names that can be safely communicated. For instance, we may say that only names exam and minitest can be communicated in channel alice. Also, consider that exam and minitest can only receive values that are not subject to authorization control. We then denote by {alice}({exam, minitest}(∅)) the type of channel alice in such circumstances, i.e., that it is not subject to replacement (we will return to this point), and that it can be used to communicate exam and minitest that in turn cannot be used for communication (typed with ∅), reading from left to right. Using this information, we can ensure that the specification given for alice above is safe, since all names that will possibly be used in communications are contextually authorized.

To analyze the use of the input variable x we then take into account that it can be instantiated by either exam or minitest (which cannot be used for channel communication) so the type of x is {exam, minitest}(∅). Hence the need to talk about possible replacements of a name, allowing us to uniformly address names that are bound in inputs. Our types, denoted γ(T ), are then built out of two parts, one addressing possible replacements of the name identity itself (γ), and the other informing on the (type of the) names that may be exchanged in the channel (T ). The typing assumption alice : {alice}({exam, minitest}(∅)) informs on the possible contexts where the Table 1. Syntax of processes. system above can be safely used. For instance, it is safe to compose with the system (alice)alice!minitest where minitest is sent to alice, since the name to be sent belongs to the names expected on alice. Instead, consider configuration

(exam)(minitest)((alice)alice?x.x!task .0 | (bob)bob?x.x!task .0)
which is also safe and addressed by our typing analysis considering typing assumptions alice : {alice}({exam}(∅)) and bob : {bob}({minitest}(∅)). Notice that which authorization is needed by each student is not statically specified in the system, which is safe when both exam and minitest are sent given the authorization scopes can be confined accordingly. Clearly, the typing specification already yields a specific association.

The typing analysis shown in Section 3 addresses such configurations where authorizations for received names may be provided by the context. In Section 2 we present the operational semantics of our language considering two equivalent alternatives that inform on the specific nature of authorizations in our model. We refer to the supporting document [START_REF] Pantovic | A calculus for modeling floating authorizations[END_REF] for additional material, namely proofs of the results reported here.

A Model of Floating Authorizations

In this section, we present our process model, an extension of the π-calculus [START_REF] Sangiorgi | The Pi-Calculus -a theory of mobile processes[END_REF] with specialized constructs regarding authorizations adopted from a model for authorizations [START_REF] Ghilezan | Dynamic role authorization in multiparty conversations[END_REF]. The syntax of the language is given in Table 1, assuming a countable set of names N , ranged over by a, b, c, . . . , x, y, z, . . . We briefly present the constructs adopted from the π-calculus. An inactive process is represented by 0. By P | P we represent two processes simultaneously active, that may interact via synchronization in channels. The name restriction construct (νa)P specifies the creation of a channel name a that is known only to the process P. The output prefixed process a!b.P sends the name b on channel a and proceeds as P, and the input prefixed process a?x.P receives a name on channel a and replaces name x in P with the received name.

The remaining constructs involve authorization specifications. Term (a)P is the authorization scoping, representing that process P has one authorization to use channel a. In contrast with name restriction, name a is not private to P . Term a b .P represents the process that delegates one authorization for name b along name a and proceeds as P. Term a(b).P represents the dual, i.e., a process which receives one authorization for name b along name a and proceeds as (b)P. Term !(a)a?x.P allows to specify infinite behavior: the process receives the name along (authorized) name a and substitutes x in P with the received name, which is activated in parallel with the original process. We adopt a simple form of infinite processes, but we remark that a general replication construct can be encoded following standard lines using replicated input, as discussed later.

In (νx)P, a?x.P and !(a)a?x.P the name x is binding with scope P. As usual, we use fn(P ) and bn(P ) to denote the sets of free and bound names in P, respectively. In (a)P occurrence of the name a is free and occurrences of names a and b in processes a b .P and a(b).P are also free. We remark that in our model authorization scope extrusion is not applicable since a free name is specified, unlike name restriction, and constructs to send and receive authorizations only affect the scope of authorizations. For the rest of presentation we use the following abbreviations: α a stands for a!b, a?x, a b or a(b) (including when b = a) and (νã) stands for (νa 1 ) . . . (νa n ).

Action Semantics

As in the π-calculus, the essence of the behavior of processes can be seen as communication. Specific to our model is that two processes ready to synchronize on a channel must be authorized to use the channel. For example, consider that (a)a!b.P | (a)a?x.Q can evolve to (a)P | (a)Q{b/x}, since both sending and receiving actions are authorized, while (a)a!b.P | a?x.Q lacks the proper authorization on the receiving end, hence the synchronization cannot occur. Another specific aspect of our language is authorization delegation. For example, in (a)(b)a b .P | (a)a(b).Q both actions along name a are authorized and the delegating process has the authorization on b, hence the delegation can take place, leading to (a)P | (a)(b)Q where the authorization scope for b changes. If actions along name a are not authorized or the process delegating lacks the authorization for b, then the synchronization is not possible. We formally define the behavior of processes by means of a labeled transition system and afterwards by means of a reduction semantics, which are shown equivalent but inform in somewhat different ways on the specific nature of authorizations in our model. The labeled transition system (LTS) relies on observable actions, ranged over by α, defined as follows:

α ::= (a) i a!b | (a) i a?b | (a) i (b) j a b | (a) i a(b) | (νb)(a) i a!b | τ ω
where ω is of the form (a) i+j (b) k and i, j, k ∈ {0, 1} and it may be the case that a = b. We may recognize the communication action prefixes together with annotations that capture carried/lacking authorizations and bound names. Intuitively, a communication action tagged with (a) 0 represents the action lacks an authorization on a, while (a) 1 represents the action is carrying an authorization on a. In the case for authorization delegation two such annotations are present, one for each name involved. As in πcalculus, (νb) denotes that the name in the object of the output is bound. In the case of internal steps, the ω identifies the lacking authorizations, and we use τ to abbreviate τ (a) 0 (b) 0 where no authorizations are lacking. By n(α), fn(α) and bn(α) we denote the set of all, free and bound names of α.

The transition relation is the least relation included in P × A × P, where P is the set of all processes and A is the set of all actions, that satisfies the rules in Table 2, which we now briefly describe. The rules (L-OUT), (L-IN), (L-OUT-A), (L-IN-A) capture the actions that correspond to the communication prefixes. In each rule the continuation

α -→ Q bn(α) ∩ fn(R) = ∅ P | R α -→ Q | R (L-RES) P α -→ Q a / ∈ n(α) (νa)P α -→ (νa)Q (L-OPEN) P (a) i a!b ----→ Q a = b (νb)P (νb)(a) i a!b -------→ Q (L-SCOPE-INT) P τ ω(a) ---→ Q (a)P τω --→ Q (L-SCOPE-EXT) P σa --→ Q (a)P (a)σa ---→ Q (L-SCOPE) P α -→ Q τ ω(a) = α = σa (a)P α -→ (a)Q (L-COMM) P (a) i a!b ----→ P Q (a) j a?b -----→ Q ω = (a) 2-i-j P | Q τω --→ P | Q (L-CLOSE) P (νa)(b) i b!a -------→ P Q (b) j b?a ----→ Q ω = (b) 2-i-j a / ∈ f n(Q) P | Q τω --→ (νa)(P | Q ) (L-AUTH) P (b) k (a) i a b --------→ P Q (a) j a(b) -----→ Q ω = (a) 2-i-j (b) 1-k P | Q τω --→ P | Q Table 2. LTS rules.
is activated under the scope of the proper authorizations so as to realize confinement. The labels are not decorated with any authorizations, representing that the actions are not carrying any authorizations, omitting (a) 0 annotations. In contrast, replicated input is authorized by construction, which is why in (L-IN-REP) the label is decorated with the authorization. Rule (L-PAR) lifts the actions of one of the branches (the symmetric rule is omitted) while avoiding unintended name capture; rule (L-RES) says that actions of P are also actions of (νa)P, provided that the restricted name is not specified in the action; and (L-OPEN) captures the bound output case, opening the scope of the restricted name a, thus allowing for scope extrusion, all three rules adopted from the π-calculus.

Rule (L-SCOPE-INT) shows the case of a synchronization that lacks an authorization on a, so in the conclusion the action exhibited no longer lacks the respective authorization and leads to a state where the authorization scope is no longer present. We use similar lines as (L-SCOPE-INT) as it also refers to lacking authorizations, specifically for the case of an (external) action that is not carrying a necessary authorization. We use σ a to denote both an action that specifies a as communication subject (cf. α a ) and is annotated with (a) 0 (including bound output), and of the form (b) i b a where i ∈ {0, 1} (which includes (a) 1 a a ). By (a)σ a we denote the respective annotation exponent increase. Rule (L-SCOPE) captures the case of an action that is not lacking an authorization on a, in which case the action crosses seamlessly the authorization scope for a.

P | Q ≡ Q | P (SC-PAR-ASSOC) (P | Q) | R ≡ P | (Q | R) (SC-RES-INACT) (νa)0 ≡ 0 (SC-RES-SWAP) (νa)(
The synchronization of parallel processes is expressed by the last three rules, omitting the symmetric cases. In rule (L-COMM) one process is able to send and other to receive a name b along name a so the synchronization may take place. If the sending and receiving actions are not carrying the appropriate authorizations, then the transition label τ ω specifies the lacking authorizations (the needed two minus the existing ones). In rule (L-CLOSE) one process is able to send a bound name a and the other to receive it, along name b, so the synchronization may occur leading to a configuration where the restriction scope is specified (avoiding unintended name capture) so as to finalize the scope extrusion. The authorization delegation is expressed by rule (L-AUTH), where an extra annotation for ω is considered given the required authorization for the delegated authorization. Carried authorization annotations, considered here up to permutation, thus identify, in a compositional way, the requirements for a synchronization to occur.

Reduction Semantics

Reduction is defined as a binary relation between processes, denoted →, so P → Q specifies that process P evolves to process Q in one computational step. In order to identify processes which differ syntactically but have the same behavior, we introduce the structural congruence relation ≡, which is the least congruence relation between processes satisfying the rules given in Table 3. Most rules are standard considering structural congruence in the π-calculus. In addition we adopt rules introduced previously [START_REF] Ghilezan | Dynamic role authorization in multiparty conversations[END_REF] that address authorization scopes, including (SC-AUTH-INACT) that allows to discard unused authorizations.

Regarding authorization scoping, we remark there is no rule which relates authorization scoping and parallel composition. Adopting a rule of the sort (a

)(P | Q) ≡ C[•] ::= • | P | C[•] | (a)C[•] C[•1, •2] ::= C[•1] | C[•2] | P | C[•1, •2] | (a)C[•1, •2]
Table 4. Contexts with one and two holes. 4 following standard lines. We use • 1 and • 2 notation to avoid ambiguity, i.e., when

(C-END) drift( • ; ∅; d) = • (C-REM) drift(C[•]; ã; d, c) = C [•] drift((c)C[•]; ã, c ; d) = C [•] (C-SKIP) drift(C[•]; ã; d) = C [•] c ∈ d drift((c)C[•]; ã; d) = (c)C [•] (C-PAR) drift(C[•]; ã; d) = C [•] drift(C[•] | R; ã; d) = C [•] | R (C2-SPL) drift(C1[•1]; ã; d) = C 1 [•] drift(C2[•2]; b; ẽ) = C 2 [•] drift(C1[•1] | C2[•2]; ã; b; d; ẽ) = C 1 [•1] | C 2 [•2] (C2-REM-L) drift(C[•1, •2]; ã; b; d, c; ẽ) = C [•1, •2] drift((c)C[•1, •2]; ã, c ; b; d; ẽ) = C [•1, •2] (C2-REM-R) drift(C[•1, •2]; ã; b; d; ẽ, c) = C [•1, •2] drift((c)C[•1, •2]; ã; b, c ; d; ẽ) = C [•1, •2] (C2-SKIP) drift(C[•1, •2]; ã; b; d; ẽ) = C [•1, •2] c ∈ d, ẽ drift((c)C[•1, •2]; ã; b; d; ẽ) = (c)C [•1, •2] (C2-PAR) drift(C[•1, •2]; ã; b; d; ẽ) = C [•1, •2] drift(C[•1, •2] | R; ã; b; d; ẽ) = C [•1, •2] | R
C[• 1 , • 2 ] = C [• 1 ] | C [• 2 ] then C[P, Q] = C [P ] | C [Q].
Note that in Table 4 there is no case for name restriction construct (νa), which allows to identify specific names and avoid unintended name capture. Remaining cases specify holes can occur in parallel composition and underneath the authorization scope, the only other contexts underneath which processes are deemed active. We omit the symmetric cases for parallel composition since contexts will be used up to structural congruence.

Operator drift plays a double role: on the one hand it is defined only when the hole/holes is/are under the scope of the appropriate number of authorizations in the context; on the other hand, when defined, it yields a context obtained from the original one by removing specific authorizations (so as to capture confinement). In our model, the specific authorizations that are removed for the sake of confinement are the ones nearest to the occurrence of the hole. Operator drift is defined inductively on the structure of contexts by the rules shown in Table 5, both for contexts with one hole (rules prefixed with C-) and for contexts with two holes (rules prefixed with C2-). For the one hole case, drift(C[•]; ã; d) takes a context and lists of names ã and d, in which the same name can appear more than once. The first list carries the names of authorizations that are to be removed and the second carries the names of authorizations that have already been removed. Similarly, drift(C[• 1 , • 2 ]; ã; b; d; ẽ) takes a context with two holes, two lists of names ã and b representing the names of authorizations which are to be removed and two list of names d and ẽ representing names of authorizations already removed. Lists ã and d refer to the • 1 hole while b and ẽ refer to the • 2 hole.

We briefly comment on the rules shown in Table 5, reading from conclusion to premises. The rule where the authorization is removed from the context (C-REM) specifies that the name is passed from the "to be removed" list to the "has been removed" list, where we use ã, c to refer to the list that contains ã and c and likewise for d, c. In the rule where the authorization is preserved in the context (C-SKIP), we check if the name is not in the second list, hence only authorizations that were not already removed proceeding towards the hole can be preserved. This ensures the removed authorizations are the ones nearest to the hole. The rule for parallel composition (C-PAR) is straightforward and the base rule (C-END) is defined only if the first list is empty. This implies that the operator is defined only when all authorizations from the first list are actually removed from the context up to the point the hole is reached. Note that when defining the operator for some context C[•] and some list of names ã that are to be removed from the context, no authorizations have been removed and the respective list d is empty. Rule (C2-SPL) describes the case for two contexts with one hole each, in which case the respective operator is used to obtain the resulting context, considering the name lists ã and d for the context on the left hand side and b and ẽ for the context on the right hand side. The remaining rules follow exactly the same lines of the ones for contexts with one hole, where authorization removal addresses left and right hole in a dedicated way. For example,

drift((b)(a)(a)( • 1 | • 2 ); a, b; a; ∅; ∅) = • 1 | • 2 drift((b)(a)( • 1 | (a) • 2 ); a, b; a; ∅; ∅) = • 1 | • 2 drift((a)(b) • 1 | (a) • 2 ; a, b; a; ∅; ∅) = • 1 | • 2 drift((b)( • 1 | (a)(a) • 2 ); a, b; a; ∅; ∅) is undefined.
The derivation for the case of two holes relies on the derivations for the cases of one hole and is possible only if the axioms for empty contexts hold. Thus, the operator is undefined if the proper authorizations are lacking. As before, lists d and ẽ are

(R-COMM) drift(C[•1, •2]; a; a) = C [•1, •2] C[a!b.P, a?x.Q] → C [(a)P, (a)Q{b/x}] (R-AUTH) drift(C[•1, •2]; a, b; a) = C [•1, •2] C[a b .P, a(b).Q] → C [(a)P, (a)(b)Q)] (R-STRU) P ≡ P → Q ≡ Q P → Q (R-NEWC) P → Q (νa)P → (νa)Q Table 6. Reduction rules.
used only internally by the operator and we abbreviate

drift(C[• 1 , • 2 ]; ã; b; ∅; ∅) with drift(C[• 1 , • 2 ]; ã; b).
We may now present the reduction rules, shown in Table 6. Rule (R-COMM) states that two processes can synchronize on name a, passing name b from emitter to receiver, only if both processes are under the scope of, at least one per each process, authorizations for name a. The yielded process considers the context where the two authorizations have been removed by the drift operator, and specifies the confined authorizations for a which scope only over the continuations of the communication prefixes P and Q. Analogously to (R-COMM), rule (R-AUTH) states that two process can exchange authorization (b) on a name a only if the first process is under the scope of authorization b and if both processes are authorized to perform an action on name a. As before, the yielded process considers the context where the authorizations have been removed by the drift operator. The authorization for b is removed for the delegating process and confined to the receiving process so as to model the exchange. Finally, the rule (R-STRU) closes reduction under structural congruence, and rule (R-NEWC) closes reduction under the restriction construct (νa). Note there are no rules that close reduction under parallel composition and authorization scoping, as these constructs are already addressed by the contexts in (R-COMM) and (R-AUTH). There is also no rule dedicated to replicated input since, thanks to structural congruence rule (SC-REP), a single copy of replicated process may be distinguished and take a part in a synchronization captured by (R-COMM).

As mentioned previously, we may encode a general form of replication, that we may write as !P , as where both a copy of P and the original process are active. Notice that since a ∈ fn(P ) the process ((a)(P | a!a.0) does not require any further authorizations on a. Synchronizations in our model are tightly coupled with the notion of authorization, in the sense that in the absence of the proper authorizations the synchronizations cannot take place. We characterize such undesired configurations, referred to as error processes, by identifying the redexes singled-out in the reduction semantics which are stuck due to the lack of the necessary authorizations. This is the case when the premise of the reduction rules does not hold, hence when the drift operator is not defined.

Definition 1 (Error). Process P is an error if

P ≡ (νc)C[α a .Q, α a .R] and 1. α a = a!b, α a = a?x and drift(C[• 1 , • 2 ]; a; a) is undefined, or 2. α a = a b , α a = a(b) and drift(C[• 1 , • 2 ]; a, b; a) is undefined.
Notice that the definition is aligned with that of reduction, where structural congruence is used to identify a configuration that directly matches one of the redexes given for reduction, but where the respective application of drift is undefined.

We may show that (fully authorized) τ transitions match reductions.

Theorem 1 (Harmony). P → Q if and only if

P τ -→≡ Q.
Both presentations of the semantics inform on the particular nature of authorizations in our model. On the one hand, the labeled transition system is more explicit in what concerns authorization manipulation; on the other hand, the reduction semantics identifies the pairs of processes that may synchronize, and is therefore useful to identify communication errors in a direct way and more amenable to use in the proofs of our typing results.

Type System

In this section, we present a type discipline that allows to statically identify safe processes, hence that do not exhibit unauthorized actions (cf. Definition 1). As mentioned before, our typing analysis addresses configurations where authorizations can be granted contextually. Before presenting the type language, we introduce auxiliary notions that cope with name generation, namely symbol annotations and well-formedness.

Since the process model includes name restrictions and types contain name identities, we require a symbolic handling of bound names when they are included in type specifications. Without loss of generality, we refine the process model for the purpose of the type analysis adding an explicit symbolic representation of name restrictions. In this way, we avoid a more involved handling of bound names in typing environments.

Formally, we introduce a countable set of symbols S ranged over by r, s, t, . . . , disjoint with the set of names N , and symbol κ not in N ∪S. Also, in order to introduce a unique association of restricted names and symbols, we refine the syntax of the name creation construct (νa)P in two possible ways, namely (νa : r)P and (νa : κ)P, decorated with symbol from S or with symbol κ, respectively. We use sym(P ) to denote a set of all symbols from S in process P. Names associated with symbols from S may be provided contextual authorizations, while names associated with symbol κ may not.

For the purpose of this section we adopt the reduction semantics, adapted here considering refined definitions of structural congruence and reduction. In particular for structural congruence, we omit axiom (SC-RES-INACT) (νa)0 ≡ 0 and we decorate name restriction accordingly in rules (SC-RES-SWAP), (SC-RES-EXTR) and (SC-SCOPE-AUTH)e.g., P | (νa : r)Q ≡ (νa : r)(P | Q) and P | (νa : κ)Q ≡ (νa : κ)(P | Q) keeping the condition a / ∈ fn(P ). We remark that the omission of (SC-RES-INACT) is used in process models where name restriction is decorated with typing information (cf. [START_REF] Acciai | Spatial and behavioral types in the pi-calculus[END_REF]).

The annotations with symbols from S allow to yield a unique identification of the respective restricted names. The well-formed processes we are interested in have unique

(T-STOP) ∆ ρ 0 (T-PAR) ∆ ρ 1 P1 ∆ ρ 2 P2 sym(P1) ∩ sym(P2) = ∅ ∆ ρ 1 ρ 2 P1 | P2 (T-AUTH) ∆ ρ {a} P ∆ ρ (a)P (T-NEW) ∆, a : {a}(T ) ρ P ∆ = ∆{r/a} r / ∈ sym(P ) a / ∈ ρ, names(T ) ∆ ρ (νa : r)P (T-NEW-REP) ∆, a : κ(T ) ρ P a / ∈ ρ, names(T, ∆) ∆ ρ (νa : κ)P (T-OUT) ∆ ρ P ∆(a) = γ(γ (T )) ∆(b) = γ (T ) γ ⊆ γ a / ∈ ρ ⇒ γ ⊆ ρ ∆ ρ a!b.P (T-IN) ∆, x : T ρ P ∆(a) = γ(T ) x / ∈ ρ, names(∆) a / ∈ ρ ⇒ γ ⊆ ρ ∆ ρ a?x.P (T-REP-IN) ∆, x : T {a} P ∆(a) = γ(T ) x / ∈ ρ, names(∆) sym(P ) = ∅ ∆ ρ !(a)a?x.P (T-DELEG) ∆ ρ P ∆(a) = γ(T ) a / ∈ ρ ⇒ γ ⊆ ρ ∆ ρ {b} a b .P (T-RECEP) ∆ ρ {b} P ∆(a) = γ(T ) a / ∈ ρ ⇒ γ ⊆ ρ ∆ ρ a(b).P Table 7. Typing rules.
occurrences of symbols from S and no occurrences of symbols from S in the body of replicated inputs. We may show that well-formedness is preserved under (adapted) structural congruence and reduction, and that typable processes are well-formed.

We may now introduce the type language, which syntax is given by γ ::= ϕ | κ and T ::= γ(T ) | ∅. Types inform on safe instantiations of names that are subject to contextual authorizations, when γ is a set of names from N and of symbols from S (denoted ϕ), and when names are not subject to contextual authorizations (κ). In γ(T ) type T characterizes the names that can be communicated in the channel, and type ∅ represents names that cannot be used for communication. A typing environment ∆ is a set of typing assumptions of the form a : T . We denote by names(T ) the set of names that occur in T and by names(∆) the set of names that occur in all entries of ∆.

The type system is defined by the rules given in Table 7. A typing judgment ∆ ρ P states that P uses channels as prescribed by ∆ and that P can only be placed in contexts that provide the authorizations given in ρ, which is a multiset of names (from N , including their multiplicities). The use of a multiset can be motivated by considering process a!b.0 | a?x.0 that can be typed as a : {a}({b}(∅)) ρ a!b.0 | a?x.0 where necessarily ρ contains {a, a} specifying that the process can only be placed in contexts that offer two authorizations on name a (one is required per communicating prefix).

We briefly discuss the typing rules. Rule (T-STOP) says that the inactive process is typable using any ∆ and ρ. Rule (T-PAR) states that if processes P 1 and P 2 are typed under the same environment ∆, then P 1 | P 2 is typed under ∆ as well. Also if P 1 and P 2 own enough authorizations when contexts provide authorizations ρ 1 and ρ 2 , respectively, then P 1 | P 2 will have enough authorizations when the context provides the sum of authorizations from ρ 1 and ρ 2 . By ρ 1 ρ 2 we represent the addition operation for multisets which sums the frequencies of the elements. The condition sym(P 1 ) ∩ sym(P 2 ) = ∅ is necessary to ensure well-formedness. Rule (T-AUTH) says that (a)P and P are typed under the same environment ∆, due to the fact that scoping is a nonbinding construct. If P owns enough authorizations when the context provides ρ {a}, then (a)P can be safely placed in a context that provides ρ.

Rule (T-NEW

) states that if P is typable under an environment that contains an entry for a, then (νa : r)P is typed under the environment removing the entry for a and where each occurrence of name a in ∆ is substituted by the symbol r. By ∆{r/a} we denote the environment obtained by replacing occurrences of a by r in every assumption in ∆, hence in every type, excluding when a has an entry in ∆. Condition r / ∈ sym(P ) is necessary to ensure well-formedness and a / ∈ ρ, names(T ) says that the context cannot provide authorization for name a and ensures consistency of the typing assumption.

The symbolic representation of a bound name in the typing environment enables us to avoid the case when a restricted (unforgeable) name could be sent to a process that expects to provide a contextual authorization for the received name. For example consider process (a)(d)a?x.x!c.0 | (νb : r)(a)a!b.0 where a contextual authorization for d is specified, a configuration excluded by our type analysis since the assumption for the type of channel a carries a symbol (e.g., a : {a}({r}(∅))) for which no contextual authorizations can be provided. Notice that the typing of the process in the scope of the restriction uniformly handles the name, which leaves open the possibility of considering contextual authorizations for the name within the scope of the restriction.

In rule (T-NEW-REP) the difference with respect to rule (T-NEW) is that no substitution is performed, since the environment must already refer to symbol κ in whatever pertains to the restricted name. For example to type process (νb : κ)(a)a!b.0 the type of a must be γ(κ(T )), for some γ and T , where κ identifies the names communicated in a are never subject to contextual authorizations. Rule (T-OUT) considers that P is typed under an environment where types of names a and b are such that all possible replacements for name b (specified in γ ) are safe to be communicated along name a (which is formalized by γ ⊆ γ , where γ is given in the type of a), and also that T (the carried type of b) matches the specification given for a. In such case, the process a!b.P is typed under the same environment. There are two possibilities to ensure name a is authorized, namely the context may provide directly the authorization for name a or it may provide authorizations for all replacements of name a, formalized as a / ∈ ρ ⇒ γ ⊆ ρ. Notice this latter option is crucial to address contextual authorizations and that in such case γ does not contain symbols, since ρ by definition does not. Rule (T-IN) follows similar principles. Rule (T-REP-IN) considers the continuation is typed with an assumption for the input bound name x and that the expected context provides authorizations only for name a. In such a case, the replicated input is typable considering the environment obtained by removing the entry for x, which must match the carried type of a, provided that x / ∈ ρ, names(∆) since it is bound to this process. Also, the fact that process P does not contain any symbol from S is necessary to ensure the unique association of symbols and names when copies of the replicated process are activated (see the discussion on example (4) at the end of this Section). In that case, process !(a)a?x.P can be placed in any context that conforms with ∆ and provides (any) ρ.

Rules (T-DELEG) and (T-RECEP) consider the typing environment is the same in premises and conclusion. The handling of the subject of the communication (a) is similar to, e.g., rule (T-OUT) and the way in which the authorization is addressed in rule (T-RECEP) follows the lines of rule (T-AUTH). In rule (T-DELEG), the authorization for b is added to the ones expected from the context. Notice that in such way no contextual authorizations can be provided for delegation, but the generalization is direct.

For the sake of presenting the results, we say process P is well-typed if ∆ ∅ P and ∆ only contains assumptions of the form a : {a}(T ) or a : κ(T ). At top level the typing assumptions address the free names of the process, which are not subject to instantiation. Free names are either characterized by a : {a}(T ) which says that a is the (final) instantiation, or by a : κ(T ) which says that a cannot be granted contextual authorizations. For example, process (a)a!b.0 | (a)(b)a?x.x!c.0 is typable under the assumption that name b has type {b}({c}(∅)), while it is not typable under the assumption κ({c}(∅)). The fact that no authorizations are provided by the context (ρ = ∅) means that the process P is self-sufficient in terms of authorizations.

We may now present our results, starting by mentioning some fundamental properties. We may show that typing derivations enjoy standard properties (Weakening and Strengthening) and that typing is preserved under structural congruence (Subject Congruence). As usual, to prove typing is preserved under reduction we may also show an auxiliary result that addresses name substitution (cf. Lemma 3.1 [START_REF] Pantovic | A calculus for modeling floating authorizations[END_REF]). Noticeably, even though subtyping is not present, the result uses an inclusion principle that already hints on substitutability. Our first main result says that typing is preserved under reduction.

Theorem 2 (Subject Reduction). If P is well-typed, ∆ ∅ P and P → Q then ∆ ∅ Q.

Not surprisingly, since errors involve redexes, the proof of Theorem 2 is intertwined with the proof of the error absence property, given in our second main result which captures the soundness of our typing analysis.

Proposition 1 (Type Soundness). If P is well-typed then P is not an error.

As usual, the combination of Theorem 2 and Proposition 1 yields type safety, stating that any configuration reachable from a well-typed one is not an error. Hence type safety ensures that well-typed processes will never incur in a configuration where the necessary authorizations to carry out the communications are lacking.

We extend the example shown in the Introduction to illustrate the typing rules:

(alice)alice!exam.0 | (exam)(minitest)(alice)alice?x.x!task .0

Considering assumption alice : {alice}({exam, minitest}(∅)), and assuming that the type of exam is {exam}(∅), by rule (T-OUT) we conclude that it is safe to send name exam along alice, since the (only) instantiation of exam is contained in the carried type of alice. Now let us place process (1) in a context restricting exam:

(νexam : r)((alice)alice!exam.0 | (exam)(minitest)(alice)alice?x.x!task .0) (2)
To type this process, the assumption for alice specifies type {alice}({r, minitest}(∅)), representing that in alice a restricted name can be communicated. Hence, the process shown in (2) cannot be composed with others that rely on contextual authorizations for names exchanged in alice, and can only be composed with processes like (alice)alice?x.(x)x!task or that use authorization delegation. Now consider process:

!(license)license?x.(νexam : r)((x)x!exam.0 | (x)(exam)x?y.y!task .0) (3)
that models a server that receives a name and afterwards is capable of both receiving (on the lhs) and sending (a fresh name, on the rhs) along the received name. Our typing analysis excludes this process since it specifies a symbol (r) in the body of a replicated input. In fact, the process may incur in an error, as receiving alice twice leads to:

(νexam 1 : r)((alice)alice!exam

where two copies of the replicated process are active in parallel, and where two different restricted names can be sent on alice, hence the error is reached when the contextual authorization does not match the received name (e.g., (exam 2 )(alice)exam 1 !task .0). In order to address name generation within replicated input, we use distinguished symbol κ that types channels that are never subject to contextual authorizations, even within the restriction scope. Hence replacing the r annotation by κ in the process shown in (3) does not yield it typable, since a contextual authorization is expected for name exam and may lead to an error like before. However, process: !(license)license?x.(νexam : κ)(alice)alice!exam.0

is typable, hence may be composed with contexts compliant with alice : {alice}(κ(T )), i.e., that do not rely on contextual authorizations for names received on alice.

Concluding remarks

In the literature, we find a plethora of techniques that address resource usage control, ranging from locks that guarantee mutual exclusion in critical code blocks to communication protocols (e.g., token ring). Several typing disciplines have been developed to ensure proper resource usage, such as [START_REF] Das | Work analysis with resource-aware session types[END_REF][START_REF] Gorla | Dynamic management of capabilities in a network aware coordination language[END_REF][START_REF] Swamy | Enforcing stateful authorization and information flow policies in fine[END_REF], where capabilities are specified in the type language, not as a first class entity in the model. Therefore in such approaches it is not possible to separate resource and capability like we do. We distinguish an approach that considers accounting [START_REF] Das | Work analysis with resource-aware session types[END_REF], in the sense that the types specify the number of messages that may be exchanged, therefore related to the accounting presented here.

We also find proposals of models that include capabilities as first class entities, addressing usage of channels and of resources as communication objects, such as [START_REF] Bodei | Checking global usage of resources handled with local policies[END_REF][START_REF] Giunti | Hide and new in the pi-calculus[END_REF][START_REF] Kobayashi | Resource usage analysis for the p-calculus[END_REF][START_REF] Vivas | Dynamic channel screening in the higher order pi-calculus[END_REF]. More specifically, constructs for restricting (hiding and filtering) the behaviors allowed on channels [START_REF] Giunti | Hide and new in the pi-calculus[END_REF][START_REF] Vivas | Dynamic channel screening in the higher order pi-calculus[END_REF], usage specification in a (binding) name scope construct [START_REF] Kobayashi | Resource usage analysis for the p-calculus[END_REF], and authorization scopes for resources based on given access policies [START_REF] Bodei | Checking global usage of resources handled with local policies[END_REF]. We distinguish our approach from [START_REF] Giunti | Hide and new in the pi-calculus[END_REF][START_REF] Vivas | Dynamic channel screening in the higher order pi-calculus[END_REF] since the proposed constructs are static and are not able to capture our notion of a floating resource capability. As for [START_REF] Kobayashi | Resource usage analysis for the p-calculus[END_REF], the usage specification directly embedded in the model resembles a type and is given in a binding scoping construct, which contrasts with our non-binding authorization scoping. Also in [START_REF] Bodei | Checking global usage of resources handled with local policies[END_REF] the provided detailed usage policies are associated to the authorization scopes for resources. In both [START_REF] Bodei | Checking global usage of resources handled with local policies[END_REF][START_REF] Kobayashi | Resource usage analysis for the p-calculus[END_REF] the models seem less adequate to capture our notion of floating authorizations as access is granted explicitly and controlled via the usage/policy specification, and for instance our notion of confinement does not seem to be directly representable.

We have presented a model of floating authorizations, a notion we believe is unexplored in the existing literature. We based our development on previous work [START_REF] Ghilezan | Dynamic role authorization in multiparty conversations[END_REF] where a certain form of inconsistency when handling the authorization granting in delegation was identified, while in this work granting is handled consistently thanks to the interpretation of accounting. We remark that adding choice to this work can be carried out in expected lines. More interesting would be to consider non-consumptive authorizations, that return to their original scope after (complete) use. We also presented a typing analysis that addresses contextual authorizations, which we also believe is unexplored in the literature in the form we present it here. Our typing rules induce a decidable typechecking procedure, since rules are syntax directed, provided as usual that a (carried) type annotation is added to name restrictions. Albeit the work presented here is clearly of a theoretical nature, we hope the principles developed here may be conveyed to, e.g., the licensing domain where we have identified related patents [START_REF] Armstrong | Management of a concurrent use license in a logically-partitioned computer[END_REF][START_REF] Baratti | License management system[END_REF][START_REF] Ferris | Offering additional license terms during conversion of standard software licenses for use in cloud computing environments[END_REF] for the purpose of certifying license usage.

A notion of substitutability naturally arises in our typing analysis and we leave to future work a detailed investigation of a subtyping relation that captures such notion. We believe our approach can be extended by considering some form of usage specifications like the ones mentioned above [START_REF] Bodei | Checking global usage of resources handled with local policies[END_REF][START_REF] Kobayashi | Resource usage analysis for the p-calculus[END_REF], by associating to each authorization scoping more precise capabilities in the form of behavioral types [START_REF] Hüttel | Foundations of session types and behavioural contracts[END_REF]. This would also allow us to generalize our approach addressing certain forms of infinite behavior, namely considering recursion together with linearity constraints that ensure race freedom. It would also be interesting to resort to refinement types [START_REF] Freeman | Refinement types for ML[END_REF] to carry out our typing analysis, given that our types can be seen to some extent as refinements on the domain of names.

P

  ::= 0 (Inaction) P | P (Parallel) (νa)P (Restriction) a!b.P (Output) a?x.P (Input) (a)P (Authorization) a b .P (Send authorization) a(b).P (Receive authorization) !(a)a?x.P (Replicated input)

  (L-OUT) a!b.P a!b --→ (a)P (L-IN) a?x.P a?b --→ (a)P {b/x} (L-OUT-A) a b .P a b --→ (a)P (L-IN-A) a(b).P a(b) --→ (a)(b)P (L-IN-REP) !(a)a?x.P (a)a?b ----→ (a)P {b/x} | !(a)a?x.P (L-PAR) P

  ω(a) to abbreviate (a) 2 (b) k , (a) 1 (b) k , and (b) i+j (a) 1 , for a given b (including the case b = a), in which case ω is obtained by the respective exponent decrement. We remark that in contrast to the extrusion of a restricted name via bound output, where the scope floats up to the point a synchronization (rule (L-CLOSE) explained below), authorization scopes actually float down to the level of communication prefixes (cf. rules (L-OUT), (L-IN), (L-OUT-A), (L-IN-A)), so as to capture confinement. Rule (L-SCOPE-EXT) follows (SC-PAR-INACT) P | 0 ≡ P (SC-PAR-COMM)

Table 3 .

 3 νb)P ≡ (νb)(νa)P (SC-REP) !(a)a?x.P ≡ !(a)a?x.P | (a)a?x.P (SC-RES-EXTR) P | (νa)Q ≡ (νa)(P | Q) (a / ∈ fn(P )) (SC-ALPHA) P ≡α Q =⇒ P ≡ Q (SC-AUTH-SWAP) (a)(b)P ≡ (b)(a)P (SC-AUTH-INACT) (a)0 ≡ 0 (SC-SCOPE-AUTH) (a)(νb)P ≡ (νb)(a)P if a = b Structural congruence.

  (a)P | (a)Q would represent introducing/discarding one authorization, thus interfering with authorization accounting. We distinguish (a)(P | Q) where the authorization is shared between P and Q and (a)P | (a)Q where two authorizations are specified, one for each process. Another approach could be a rule of the sort (a)(P | Q) ≡ P | (a)Q, which also may affect the computational power of a process. For example, processes a!b.0 | (a)0 and (a)(a!b.0 | 0) are clearly not to be deemed equal. Structural congruence is therefore not expressive enough to isolate two authorized processes willing to synchronize. To define the reduction relation we introduce an auxiliary notion of static contexts with one and two holes and operation drift that allows to single out configurations where communication can occur. Intuitively, reduction is possible if two processes have active prefixes ready for synchronization and each holds the proper authorization.Static contexts are defined in Table

  For example, drift((a) • ; a; ∅) = • drift((a)((a) • | R); a; ∅) = (a)( • | R) drift( • ; a; ∅) is undefined drift((a)(b) • ; a, b; ∅) = • drift((a) • ; a, b; ∅) is undefined drift((a) • | (b)0; a, b; ∅) is undefined.

  (νa)((a)a!a.0 | !(a)a?x.(P | a!a.0)) where a ∈ fn(P ), since in two steps it reduces to P | (νa)((a)(P | a!a.0) | !(a)a?x.(P | a!a.0)).

  1 .0 | (exam 1 )(alice)alice?y.y!task .0) | (νexam 2 : r)((alice)alice!exam 2 .0 | (exam 2 )(alice)alice?y.y!task .0).

Table 5 .

 5 drift rules.

Acknowledgments We thank anonymous reviewers for useful remarks and suggestions. This work has been partially supported by the Ministry of Education and Science of the Republic of Serbia, project ON174026, and EU COST Action IC1405 (Reversible Computation).