{'fraction_non_alphanumeric': 0.044997534381677716, 'fraction_numerical': 0.003876499917812723, 'mean_word_length': 4.312545481007131, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 5, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Verifying the Interplay of Authorization Policies and Workflow in Service-Oriented Architectures (Full version)

A widespread design approach in distributed applications based on the service-oriented paradigm, such as web-services, consists of clearly separating the enforcement of authorization policies and the workflow of the applications, so that the interplay between the policy level and the workflow level is abstracted away. While such an approach is attractive because it is quite simple and permits one to reason about crucial properties of the policies under consideration, it does not provide the right level of abstraction to specify and reason about the way the workflow may interfere with the policies, and vice versa. For example, the creation of a certificate as a side effect of a workflow operation may enable a policy rule to fire and grant access to a certain resource; without executing the operation, the policy rule should remain inactive. Similarly, policy queries may be used as guards for workflow transitions. In this paper, we present a two-level formal verification framework to overcome these problems and formally reason about the interplay of authorization policies and workflow in service-oriented architectures. This allows us to define and investigate some verification problems for SO applications and give sufficient conditions for their decidability.


I. INTRODUCTION
A widespread design approach in distributed applications based on the Service-Oriented paradigm (SO), such as webservices, consists of clearly separating the Workflow (WF) from the Policy Management (PM). The former orchestrates complex processing of data performed by the various principals using a set of resources made available in the application, while the latter aims to regulate access decisions to the shared resources, based on policy statements made by the involved principals. This separation of concerns is beneficial in several respects for the design, maintenance, and verification of the resulting applications such as reusing policies across applications.
One of the key problems in obtaining a correct design of SO applications is to be able to foresee all the-sometimes subtle-ways in which their WF and PM levels interact. To understand the difficulty underlying this endevor, let us first consider the WF level. In this respect, SO applications can be seen as distributed systems whose transitions can be interleaved in many possible ways. This already creates a first difficult problem: to understand the behaviors of an SO application and then to establish if it meets certain properties. An additional burden, typical to SO applications, is the presence of the PM level, which is supposed to constrain the allowed behaviors of the application so as to meet certain crucial security requirements. Declarative policy languages (such as Datalog and other languages built on top of it, like Binder [13], SecPal [6] and DKAL [16]), usually based on a (fragment of) first-order logic, are used to design the PM level of SO applications in a more flexible, reusable, and verificationfriendly way. The high flexibility and expressiveness of such languages may grant access to a resource to someone who, in the intention of the policy designer, is not allowed to do so.
To further complicate the situation, there are the subtle ways in which the WF and the PM levels may interact so as to give rise to behaviors that are unintended and may breach some crucial security requirements of an SO application. As a concrete example of this point, consider a system for virtual Program Committee meetings. A policy governing access to the reviews of a paper may be the following: a reviewer assigned to a paper is required to submit his own review before being able to read those of the others. So, in order to resolve an access request to the reviews of a paper, the system should be able not only to know the identities and the roles of the various members of the Program Committee but also to maintain and consult the information about which reviewers have already submitted their reviews. Indeed, information of the first kind must be derived from the WF level.
Given all the difficulties to obtain correct designs for SO applications, formal methods have been advocated to help in this task. Unfortunately, most (see, e.g., [14], [23]) of the specification and verification techniques (with some notable exceptions, e.g., [20]) have concentrated on one level at a time and abstracted away the possible interplays between the WF and the PM level. The first contribution of this paper is a framework capable of formalizing both the WF and the PM level as well as their interface so as to enable a more precise analysis of the possible behaviors of SO applications. In particular, we use a temporal extension of first-order logic, similarly to what has been proposed in [17] for the specification and verification of reactive systems. The motivations for this choice are three-fold. First, workflows can be easily specified by using first-order formulae to describe sets of states and transitions of SO applications. Second, a simple extension of this well-known framework allows us to easily specify policy-relevant facts and statements. Third, we hope to adapt and reuse to the case of SO applications the cornucopia of specification and verification techniques developed for reactive systems. As a first step in this direction, the second contribution of this paper is to define and investigate some verification problems for SO applications and give sufficient conditions for their decidability. In particular, we show how executability and some security properties (which can be expressed as invariants) can be automatically verified within the proposed framework.
We proceed as follows. In Section II, we summarize the key points of a restricted combination of first-order and temporal logic, which provides a formal basis for our approach. In Section III, we present our formal two-level specification framework for SO applications, which we apply, in Section IV, on a number of interesting verification problems for SO applications. In Section V, we discuss related and future work, and draw conclusions. Due to lack of space, proofs are given in the appendix, together with the detailed formalization of a case study that illustrates our framework at work, and with a number of useful pragmatical observations.

II. A RESTRICTED COMBINATION OF FIRST-ORDER LOGIC AND TEMPORAL LOGIC
As a formal basis for our approach we use a standard [17] minimal extension of Linear Time Logic (LTL) with a manysorted version of First-Order Logic with equality (FOL=). We recall now some useful definitions and properties of FOL= where, for brevity, we do not explicitly consider sorts although all notions can be easily adapted to the many-sorted version. We assume the usual first-order syntactic notions of signature, term, literal, formula, quantifier-free formula, substitution and grounding substitution, sort and so on, and call sentence a formula that does not contain free variables. Also the semantic notions of structure, satisfiability, validity, and logical consequence are the standard ones.
Let Σ be a FOL= signature. An expression is a term, an atom, a literal, or a formula. A Σ(x)-expression is an expression built out of the symbols in Σ where at most the variables in the sequence x of variables may occur free, and we write E(x) to emphasize that E is a Σ(x)-expression. Similarly, for a finite sequence r of predicate symbols in Σ, we write φ(r) to denote a Σ-formula where at most the predicate symbols in r may occur. We juxtapose sequences to denote their concatenation, e.g. xy, and abuse notation and write ∅ to denote the empty sequence besides the empty set. If σ is a substitution and t is a (finite) sequence of expressions, then tσ is the sequence of expressions obtained from t by applying the substitution σ to each element of t.
Following [17], we use a tuple x of variables, called WF state variables, to represent the values of application variables at a given instant of time, and use a FOL formula ϕ(x) to represent sets of states. WF state variables take values in the domain of a first-order structure, which formalizes the data structures, the values of the control locations, and those of the auxiliary variables of the WF of a certain SO application. Formally, let Σ be a signature (containing, e.g., the operators of certain data structures or the names of some control locations) and M be a Σ-structure; M, v |= ϕ(x) means that the state formula ϕ(x) is true in M for the valuation v mapping the variables in x to elements of the domain of M. As shown in [17], this is enough for the specification of virtually any reactive system and hence also for the WF level. However, the state of SO applications should also support the PM level whose relevant part is represented by tables where certain facts are recorded (e.g., "is-reviewer-of" for the example in the introduction). Following the relational model of databases, we formalize tables as predicates and we add to the WF state variables a set p of fresh predicate symbols (i.e. p ∩ Σ = ∅), called PM state variables. Any Σ-formula ϕ(x, p) is an SO state formula. For a Σ-structure M = (I, D), a valuation v mapping the WF state variables in x to elements of the domain D, and a relational valuation b mapping the PM state variables in p (such that p ∩ Σ = ∅) to the powerset of D, we write Let Σ be a signature and M be a Σ-structure. We formalize an SO application by a tuple (x, p, ι, Tr ), called an SO transition system, where x are the WF state variables, p are the PM state variables, ι is a Σ(x, p)-formula, and Tr is a finite set of Σ(x, p, x , p )-formulae, called transitions, which relate a set of SO states (identified by the "values" of x, p) to that of a set of SO "next" states (identified by the "values" of x , p ). 1 If p = ∅ and x = ∅, then our notion of SO transition system reduces to that of transition system in [17]; in the rest of this paper, we assume that p = ∅.
A run of an SO transition system (x, p, ι, Tr ) is an in- ) map state variables and predicates in x, p (respectively, x , p ).
To specify properties of SO transition systems, we use an extension of Linear Time Logic. Formally, let x, p be SO state variables and Σ be a signature; the set LTL(Σ, x, p) of LTL (state-based) formulae for Σ and x, p is inductively defined as follows: state formulae are in LTL(Σ, x, p) and if ϕ is a state formula then ϕ is in LTL(Σ, x, p). 2 Note that we prohibit alternation of FOL quantifiers and temporal operators: this makes the logic less expressive but it helps to derive decidability results for the satisfiability problem, which is a necessary condition to develop (semi-)automatic verification methods for SO applications.
Let M be a Σ-structure. A model of an LTL(Σ, x, p)formula is an infinite sequence v 0 , b 0 , ..., v i , b i , ... of SO states such that each v i , b i map all the SO state variables in x, p, for i ≥ 0. We then say that an LTL(Σ, x, p)-formula ϕ(x, p) is true in a model v 0 , b 0 , ..., v i , b i , ..., and write Let S = (x, p, ι, Tr ) be an SO transition system, M be a Σ-structure, and ϕ(x, p) be an LTL(Σ, x, p)-formula. Then,

III. A FORMAL TWO-LEVEL SPECIFICATION FRAMEWORK
FOR SO APPLICATIONS Recall that one of the main goals of this paper is to provide a natural specification framework for SO applications whose architecture is organized in two levels. Indeed, it is possible to model a large class of SO applications by using the notion of SO transition system introduced in the previous section. However, a good framework should provide an adequate support to restrict the design space for a two-level SO application and allow the designer to easily specify the WF level, the PM level, and their interface in isolation according to a divide-and-conquer strategy. In our framework, this consists of identifying suitable first-order structures formalizing both the data structures at the WF level and the tables at the PM level. Unfortunately, working with first-order structures for specification is quite difficult since there is no obvious way to mechanically represent and reason about them. Fortunately, first-order theories are sets of FOL= sentences that can be used as reasonably precise approximations of first-order structures and for which there is automated reasoning support. Hence, we decided to use theories to describe the WF, the PM levels, and their interface, as illustrated in Fig. 1: if T WF and T PM are the theories formalizing the WF and the PM levels, respectively, then their intersection T sub = T WF ∩T PM , called the substrate theory, formalizes their interface.
Intuitively, the theory T sub ensures that the WF and PM levels "agree" on certain notions. For example, T sub univocally identifies the principals involved in the SO application and possibly (an abstraction of) the structure of the resources that the SO application can access or make available. As we will see, the use of theories allows us to easily import declarative policy specifications expressed in logical languages based on (extensions of) Datalog in our framework.
A similar approach can also be used to restrict the formulae characterizing transitions. Intuitively, the transitions that can be specified by formulae in the identified class are such that the updates on the values of both the WF and the PM state variables are functional (if we regard relations as first-order objects). Since the identities of the principals involved in the SO application being specified play a crucial role in enabling or disabling the possibility to execute a certain transition, the Before being able to formalize these intuitions, we recall the concept of FOL= theory and some standard related notions.

A. First-order theories for SO applications
A Σ-theory T is a set of first-order Σ-sentences, called the axioms of T . A Σ-structure M is a model of the Σ-theory T iff all the sentences in T are true in M. A Σ-theory T is consistent if it admits at least one model. The T -satisfiability problem for a quantifier-free Σ-formula ϕ(x, p) (such that p ∩ Σ = ∅) consists of checking whether there exists a model M of T and mappings v and b such that M, v, b |= ϕ(x, p). By transformation in disjunctive normal form (i.e. as disjunctions of conjunctions of literals), the T -satisfiability problem for quantifier-free formulae can be reduced to the T -satisfiability problem for (quantifier-free) conjunctions of literals.
For specifying SO applications, we usually need to introduce a finite set of unique identifiers to name the various principals. Formally, this can be done by using a theory of the following kind. An enumerated data-type theory EDT (C, S) is axiomatized by the sentences  for S a sort symbol in the given signature (omitted for simplicity) and C = {c 1 , ..., c n }, c i of sort S for i = 1, . . . , n and n ≥ 1. It is easy to see that the EDT (C, S)-satisfiability problem is decidable. Enumerated data-type theories will be sub-theories of the theory formalizing the interface between the WF and PM levels.
For the WF level, we can reuse all the theories available in the literature formalizing data structures and the decision procedures for their satisfiability problem (see, e.g., [21] for an overview). Enumerated data-type theories are also useful for the WF level as they can formalize the (finitely many) control locations of an application. We now give a concrete example of a theory capable of formalizing a simple message passing network that is relevant for SO applications (see Appendix B for a more detailed case study).
Example 1 (Message passing): A net can be seen abstractly as a set of messages: sending a message amounts to adding the message to the set while receiving a message consists of checking if it is a member of the net; hence, messages are never deleted, only added to the set representing the net. This view is simple but still allows one to model interesting facts such as the reception of messages in any order (since a set does not require an ordering on its elements) or duplication of messages (as a message is never removed from the net).
To model the simple fragment of set theory necessary to formalize this idea in FOL, we use a theory MsgPass[Msg], parametrized over the sort Msg of messages which contains SetOfMsg as the sort for sets of messages, the constant mty of sort SetOfMsg denoting the empty set, the binary function symbol ins of sort Msg × SetOfMsg → SetOfMsg denoting the operation of adding a message to a set of messages, and the binary predicate symbol mem of sort Msg × SetOfMsg for checking if a message is in a set of messages. The axioms of MsgPass[Msg] are the following three sentences: where E, E are variables of sort Msg and S is a variable of sort SetOfMsg. It is easy to describe the states of a variable net: just introduce a logical variable net and use suitable formulae from the theory MsgPass [Msg]. For example, the formula ∃m 1 , m 2 : Msg, net : SetOfMsg. m 1 = m 2 ∧ net = ins(m 1 , ins(m 2 , net )) constrains net to contain at least two messages (plus possibly others). Note that the only free variable in the formulae describing sets of states is net.
The MsgPass[Msg]-satisfiability problem is decidable [1]. For the PM level, we recall the class of Bernays-Schönfikel-Ramsey (BSR) sentences [9], which has been used, among other applications, to model relational databases. A BSRtheory is a set of sentences of the form ∃x ∀y. ϕ(x, y), where x and y are tuples of variables and ϕ is a quantifierfree formula containing only predicate and constant symbols (or, equivalently, no function symbols of arity greater than or equal to 1). The decidability of the satisfiability problem for any BSR-theory is a well-known decidability result [9].
The following sub-class of BSR-theories can be used to specify policies as shown in, e.g., [18]. A Datalog-theory is a BSR-theory whose sentences are of the form where p, q i , for i = 1, ..., n, are predicate symbols, and x, y are disjoint tuples of variables such that the length of x is equal to the arity of p. Usually, sentences of the form (1) are written as ∀x, y. p(x) ← q 1 (x, y) ∧ · · · ∧ q n (x, y) , where ← can be read as the reverse of the implication connective (sometimes also the universal quantifiers will be dropped). Formulae written in this way are called rules in the literature, while their hypotheses and p(x) are called the body and the head of the rule, respectively. We conclude by recalling some notions that are relevant for the combination of theories that provide us with the formal tools to separately specify the WF and PM levels of an SO application and then modularly combine them. Let T 1 and T 2 be two theories; we say that they share the theory T 0 = T 1 ∩ T 2 if T 0 = ∅ and their combination T 1 ∪ T 2 is non-disjoint. Otherwise (i.e. when T 0 = ∅), we say that the combination T 1 ∪T 2 is disjoint. For verification, it is important to combine decision procedures for each theory T 1 and T 2 so as to obtain a decision procedure for their combination. This is crucial to derive decidability results for verification problems of SO applications as we will reduce them to satisfiability problems in the combination of the theories formalizing the WF and the PM levels. A class of theories that will be relevant in this task (see Lemma 2 below) is the following. A theory T is stably infinite if a T -satisfiable quantifier-free formula is satisfiable in a model of T whose domain has infinite cardinality. Examples of stably infinite theories are MsgPass[Msg] of Example 1, any BSR theory (see, e.g., [22]), and many theories formalizing data structures, such as arrays or sets. Enumerated data-type theories are not stably infinite as they admit only models whose domains have finite cardinality.

B. Two-level SO transition systems
We are now ready to define an instance of the framework of Section II to formally specify SO applications designed according to the two-level architectures considered in this paper. This framework relies on the following assumptions.
Framework assumption 1: As depicted in Fig. 1, we assume that the WF and PM levels are formalized by a Σ WFtheory T WF and a (Σ PM ∪p)-theory T PM , which share a Σ subtheory T sub , called the substrate. Formally, Σ sub ⊆ Σ WF and Σ sub ⊆ Σ PM , and T sub ⊆ T WF and T sub ⊆ T PM .
The shared theory T sub plays the role of interface between the two levels. A minimal requirement on the interface is to provide some knowledge about the identities of the principals involved in the SO application. This is formalized as follows.
Framework assumption 2: Σ sub contains the sort symbol Id .
This last assumption is crucial for many aspects of SO applications related to PM, such as integrity (of messages or certificates), authenticity (of certificates), and proof-ofcompliance (of credentials).
Using the notion of combination of theories introduced at the end of Section III-A, we are now able to define the concept of background theory for an SO application that is obtained by modularly combining the theories formalizing the WF and the PM levels. Let T sub , T WF , and T PM be consistent theories satisfying Framework assumptions 1 and 2. The background Σ SOA -theory T SOA is the union of the theories T WF and T PM , i.e. Σ SOA := Σ WF ∪ Σ PM and T SOA := T WF ∪ T PM . Note that, by Robinson consistency theorem (see, e.g., [12]), T SOA is consistent since both T WF and T PM are assumed to be so. We will sometimes refer to T WF as the WF background theory and to T PM as the PM background theory.
We introduce a particular class of SO transition systems (defined in Section II) by using background theories obtained by combining theories for the WF and PM levels satisfying the two framework assumptions above. A technical problem in doing this is the following. SO transition systems (in particular their states and runs) are defined with respect to a certain first-order structure. Instead, we want to use theories that, in general, identify classes of first-order structures and not just one particular structure. However, since the verification problems for SO applications considered below will be reduced to satisfiability problems, the following notion tells us thatunder suitable conditions-we can use theories in place of , for some valuation v mapping the variables in x to elements of the domain of M, is equivalent to the T -satisfiability of ϕ(x), for any quantifier-free formula ϕ(x). For example, it is possible to see that enumerated data-type theories are adequate for any of their models (as they are all isomorphic) or that the theory MsgPass[Msg] is adequate to the structure containing finite sets of messages.
As notation, let us write ∀z.
. . , ι n (respectively, ϕ = ϕ 1 , . . . , ϕ n ), z j ⊆ z, and the length of z j is equal to the arity of p j . Definition 1 (Two-level SO transition system): Let T sub , T WF , and T PM be consistent theories satisfying Framework assumptions 1 and 2 and M be a Σ SOA -structure. A two-level SO transition system (with background theory T SOA adequate for M) is an SO transition system (x, p, ι, Tr ) such that (a) p ∩ Σ SOA = ∅; (b) ι is a state Σ SOA -formula of the form: where i is a finite sequence of variables of sort Id , ι W F is a quantifier-free Σ W F (i, x)-formula, and ι P M is a quantifierfree Σ P M (z, i, p)-formula; and (c) Tr is a finite state of transition formula of the form called guarded assignment transition, where i is a tuple of variables of sort Id ; d, z are sets of variables of a sort dependent on the WF and PM levels of the application; G is a quantifier-free formula, called the guard of the transition; f is a tuple of Σ WF (x, i)-terms, called the WF updates of the transition, whose sorts are pairwise equal to those of the state variables in x; and ϕ is a tuple of quantifier-free Σ PM (i, p, z)formulae, called the PM updates of the transition. If x = ∅ (recall that we have assumed that p = ∅ for SO transition systems, cf. Section II), then we say that the SO application is (purely) relational. Intuitively, the form (2) for the initial state formula is inspired by the observation that usually the principals at the beginning of the computation have some common (or no) knowledge about the facts that are relevant to the PM level. Note that f and ϕ may not contain the state variables in x and the state predicates in p , i.e. updates are not recursive.
Below, for simplicity, we will no more mention the Σ SOAstructure M and implicitly assume that T SOA is adequate for M. To help intuition, we illustrate the notion of two-level SO transition system by means of a simple example (extracted from the case study in the appendix).
Example 2: Consider a situation where the clerks of an office may send messages over a network. The messages may contain, among many other things, certificates about their identities, roles, or capability to access certain resources in the organization they belong to. Certificates about the identities and roles are issued by a trusted certification authority while those about the access to a certain resource are issued by heads (who are clerks with this special right). In order to comply with the policies of accessing resources, each clerk maintains a table about his/her identity, role, and access capability as well as about other clerks. We describe a two-level SO transition system to formalize this situation.
First of all, we specify the WF background theory: where Ed and Helen are two clerks, RegOffCA is the trusted certification authority, Res is a shared resource (e.g., a repository), employee and head are the possible roles of clerks, and MsgPass[Msg] is the theory for message passing introduced in Example 1. In particular, Msg is a theory to describe the structure of messages as follows: a message contains a field identifying the sender, a field identifying the receiver, and a field carrying their contents. Formally, this is done by introducing two new sort symbols Body and the ternary function msg of sort Id × Body × Id → Msg. Finally, Cert is a theory to provide functionalities to analyze the body of messages and extract some relevant information: the predicate cert of role of sort Body × Id × Role is capable of recognizing that the body of a message contains a certificate that its second argument is the identifier of a clerk whose role is that of its third argument. For example, if cert Ed empl is a constant of sort Body representing the certificate that the employee Ed has the role employee, then the message sent by RegOffCA to Helen containing the certificate cert Ed empl is encoded by the following term: msg(RegOffCA, cert Ed empl, Helen) and we will also have that, e.g., cert of role(cert Ed empl, Ed, employee) holds. The state of the two-level SO transition system specifying the situation above should contain a WF state variable net of sort SetOfMsg (containing the set of messages exchanged during a run of the transition system) and a PM state variable hasrole of arity Id × Id × Role (storing the join of the tables of each clerk about their roles). The initial state of the system should specify that no message has been exchanged over the net and that no role is known to the various clerks. This can be formalized by a state formula as follows: where i 1 , i 2 , z 1 , z 2 are variables of sort Id , c is a variable of sort Body, and d is a variable of sort Role which is a formula of the form (2) by taking i = ∅, z = {z 1 , z 2 , r}, net ∈ x, and hasrole ∈ p.
As an example of interplay between the WF and PM levels, Fig. 2 shows the guarded assignment transition of the form (3) that formalizes what happens when a message containing a certificate about the role of an employee (say, Ed) is sent to another employee (say, Helen) by the certification authority (RegOffCA). Note that the content of the state variable net is left unchanged by the transition, whose only effect is to update the access table (represented by the predicate hasrole) with the entry corresponding to the content of the received (role) certificate. For example, upon reception of the message containing the certificate cert Ed empl, the following fact hasrole (Helen, Ed, employee) must hold in the next state, while for all the other triples, hasrole has the same Boolean value of hasrole.
So far, we have specified the WF level of the SO application. As anticipated above, we can define T PM to contain T sub and a finite set of Datalog rules that declaratively formalize the access policy statements of the SO application. Since this way of formalizing policies has been well studied in the literature (see, e.g., [13]), as a simple example, we only give the following Datalog rule where the variable i is of sort Id and can access ∈ Σ PM . It says that the clerk i can access the shared resource Res if the latter knows (by retrieving the right entry in the table represented by hasrole) that i has the role of head.
Appendix C-A contains a generalization of the example above inspired by an industrial application.
IV. SOME VERIFICATION PROBLEMS FOR SO APPLICATIONS Let A = (x, p, ι, T r) be a two-level SO transition system with background theory T SOA for an SO application; for brevity, we will sometimes refer to A simply as SO application. We define and investigate some verification problems for SO applications and give sufficient conditions for their decidability. In appendices C-B and C-C, we then discuss pragmatical aspects of how to implement the decision procedures.

A. Executability of SO applications
Symbolic execution is a form of execution where many possible behaviors of a system are considered simultaneously. This is achieved by using symbolic variables to represent many possible states and executions. For each possible valuation of these variables, there is a concrete system state that is being indirectly simulated. This technique is particularly useful for the design of SO applications when usually several scenarios are identified as typical execution paths that the application should support. Given the high degree of non-determinism and the subtle interplay between the WF and the PM levels, it is often far from being obvious that the SO application just designed allows one or many of the chosen scenarios. A valuable contribution of the proposed framework is that symbolic execution of SO applications can be done by using existing techniques for automated deduction.
In any scenario, there is only a known and finite number of principals. So, for the verification of the executability of two-level SO transition systems, we can assume that: Verification assumption 1: T sub ⊇ EDT (c, Id ). Since there are only finitely many principals, universal quantifiers in initial state formulae do not add to expressiveness as ∀i. ι(i, x, p) is logically T SOA -equivalent to a quantifier-free formula of the form σ ι(iσ, x, p), where σ ranges over all possible grounding substitutions mapping the variables in i to the constants in c. Thus, we can further assume that: Verification assumption 2: Initial state formulae as well as any other state formula used to describe a state of a scenario are quantifier-free.
The key notion for symbolic execution in our framework is the following. Let ϕ(p, x) and ψ(p, x) two quantifier-free state Σ SOA -formulae; and let τ (p, x, p , x ) ∈ Tr be a transition formula of the form (3). We write {ϕ} τ {ψ} (in analogy with Hoare triples) to abbreviate the following formula: whose validity modulo T SOA implies that the transition τ leads A from a state satisfying ϕ to one satisfying ψ. Definition 2: Let A = (x, p, ι, T r) be a two-level SO transition system with background theory T SOA , let τ 1 , ..., τ n be a sequence of transition formulae such that τ i ∈ T r, and let ϕ 0 , ..., ϕ n be a sequence of quantifier-free state formulae. The (symbolic) execution problem consists of checking whether τ i leads A from a state satisfying ϕ i to a state satisfying ϕ i+1 , or, equivalently, to checking Property 1: Let ϕ and ψ be two quantifier-free state formulae and τ be a transition. Then, it is possible to effectively compute a quantifier-free formula φ that is logically equivalent to the negation of {ϕ} τ {ψ} and such that That is, for quantifier-free ϕ and ψ, the negation of {ϕ} τ {ψ} "is" still quantifier-free (e.g., the negation of {ι} GetRoleCertEmpl {ϕ 1 } in the case study in Appendix B).
If we are able to check the T SOA -satisfiability of quantifierfree formulae, then we are also able to solve the symbolic execution problem for the two-level SO transition system with T SOA as background theory. We now identify sufficient conditions on the component theories of T SOA (i.e. T sub , T WF , and T PM ) for the decidability of the T SOA -satisfiability problem.
Lemma 1: Let T sub be an enumerated data-type theory, and T WF ⊇ T sub and T PM ⊇ T sub be consistent theories with decidable satisfiability problems. The T SOA -satisfiability problem is decidable for T SOA = T WF ∪ T PM .
Pragmatical aspects of how to implement the decision procedures are discussed in Appendix C-B, extending the observations on the pragmatics of modeling WF and PM of SO applications of Appendix C-A.
We are now in the position to state the main result of this section, which follows from the properties and lemmas above.
Theorem 1: Let T sub be an enumerated data-type theory, and T WF ⊇ T sub and T PM ⊇ T sub be consistent theories with decidable satisfiability problems. Then, the symbolic execution problem for two-level SO transition systems with background theory T SOA = T WF ∪ T PM is decidable.
Note that the use of an enumerated data-type theory as T sub does not imply that only two-level SO transition systems with finite state space can be verified by our method. In fact, both T WF and T PM can have models with infinite cardinalities (this is the case, for example, of the theory MsgPass). So, symbolic execution is decidable even if the state space of the two-level SO transition systems is infinite provided that there exist decision procedures for the theories characterizing the WF and the PM levels and it is possible to find a common sub-theory, used for synchronization by the two levels, whose models are finite.

B. Invariant verification of SO applications
Recall that we fixed a two-level SO transition system A = (x, p, ι, T r) with background theory T SOA . We now consider the problem of verifying that A satisfies a certain security property φ, in symbols A |= φ. Since many interesting security properties can be expressed as invariance properties (e.g., for the verification of security protocols or web services), which are a sub-class of safety properties, we assume below that φ is a state formula of the form ∀i : Id . ϕ(i, x, p).
Two remarks are in order. First, we are considering a subclass of invariance properties since, in general, ϕ can be a past-formula (see, e.g., [17]). Second, we cannot assume that a finite and known number of principals is fixed so that (5) is equivalent to a quantifier-free formula and thus the verification techniques in Section IV-A still apply. Rather, we want to verify that for a fixed but unknown number of principals, A satisfies the invariance property φ, i.e. we want to solve a parameterized invariance verification problem. For this reason, in the rest of this section, we assume that: Verification assumption 3: T sub is the theory of an equivalence relation.
In this way, we are able to distinguish between the identifiers of the various principals. Now, in order to show that formulae of the form (5) are invariant of A, we can use the well-known INV rule of Manna and Pnueli [17]: The intuition underlying the correctness of the rule is the following. Assume there exists a formula ψ of the form (5) identifying a set of states that includes both the set of initial states (I 1 ) and the set of states characterized by ϕ (I 2 ), and, furthermore is an invariant of A (I 2 ), i.e. each transition of τ i in Tr leads from a state satisfying ψ to a state satisfying again ψ. Then, also ϕ is an invariant of A.
Using the INV rule, assuming that the invariant ψ has been guessed, it is possible to reduce the problem of verifying that a certain property is an invariant of the application, to several T SOA -satisfiability problems. In fact, reasoning by contradiction we have that (I 1 ) and (I 2 ) hold iff the quantifierfree formulae are T SOA -unsatisfiable, respectively, where the variables in i are regarded as (Skolem) constants. Similarly, for a given τ , (I 3 ) holds iff the (universally) quantified formula is T SOA -unsatisfiable, where x, x and i are regarded again as (Skolem) constants, for each τ ∈ Tr .
Property 2: Let ψ 0 (x, p) := ∀i. ψ(i, x, p) be a state formula and τ (x, p, x , p ) be a transition formula. Then, it is possible to effectively compute a formula of the form To be able to check that A |= ϕ, we need to solve the T SOA -satisfiability problem of (universally) quantified formulae. We now identify sufficient conditions on the background theory T SOA for this problem to be decidable.
Lemma 2: Let Σ sub contain only (countably many) constant symbols (i.e. T sub is the theory of an equivalence relation), T WF ⊇ T sub be a consistent and stably-infinite theory with decidable satisfiability problem such that the signature of no function symbol in Σ WF is of the kind S 1 × · · · S n → Id (for S i ∈ Σ WF and i = 1, ..., n) and T PM ⊇ T sub be a consistent BSR theory. Then, the T SOA -satisfiability problem is decidable for formulae of the form ∀i : Id . ϕ(i, x, p), where T SOA = T WF ∪ T PM and x, p are (finite) sequences of variables and predicate symbols (such that p ∩ Σ SOA = ∅), respectively.
As we have already said, there are many theories formalizing data structures (such as MsgPass) relevant for modeling the WF of SO applications, which are stably infinite. Also, it is frequently the case that the data structures formalized by these theories use identifiers to create new pieces of information (typical examples are the certificates of the identities or the roles of principals) but do not create new identifiers. In this way, the requirement that functions in T WF do not create identifiers (syntactically, this is expressed by forbidding that the return type of the functions is not Id ) is frequently satisfied. We point out that this requirement is a sufficient condition to avoid the creation of new identifiers and it may be weakened. However, we leave the study of more general sufficient conditions to future work.
As before, pragmatical aspects of invariant verification of SO applications are discussed in Appendix C-C, extending appendices C-A and C-B.
We conclude this section with the main technical result, which follows from the above properties and lemma.
Theorem 2: Let Σ sub contain only (countably many) constant symbols (i.e. T sub is the theory of an equivalence relation), T WF ⊇ T sub be a consistent and stably-infinite theory with decidable satisfiability problem such that the signature of no function symbol in Σ WF is of the kind S 1 × · · · S n → Id (for S i ∈ Σ WF and i = 1, ..., n), and T PM ⊇ T sub be a consistent BSR theory. Let A = (x, p, ι, Tr ) be a two-level SO transition system with background theory T SOA = T WF ∪ T PM , and ∀i. ϕ(i, x, p) be a state formula. It is decidable to check whether A |= ∀i. ϕ(i, x, p), provided there exists a state formula ∀i. ψ(i, x, p) such that (a) T SOA |= ∀i.ι(i) → ψ(i), (b) T SOA |= ∀i.ψ(i) → ϕ(i), and (c) T SOA |= {ψ} τ {ψ} for each τ ∈ Tr .
Indeed, the usefulness of the theorem depends on the availability of the formula ∀i. ψ(i), which is called an inductive invariant since it is preserved under the application of the transitions of the two-level SO transition system. Since the problem of finding such a formula when p = ∅ is undecidable (see, e.g., [17]), it is also undecidable in our case. However, several heuristics have been proposed; see, e.g., [11] for a recent proposal and pointers to the literature. An interesting line of future work is to adapt these techniques to find invariants of SO applications. Note that it is possible to dispense with the computation of the auxiliary invariant whenever ∀i. ϕ(i) is already inductive; in which case, conditions (a) and (b) of the theorem are trivially satisfied and we are only required to discharge proof obligation (c).

V. RELATED WORK AND CONCLUSIONS
We have presented a two-level formal framework that allows us to specify and verify the interplay of authorization policies and workflow in SO applications and architectures. In the previous sections, we already discussed relevant related works and also pointed out different research lines along which we are currently extending the techniques and results presented here. In particular, as we remarked, formal methods are being increasingly applied extensively to support the correct design of SO applications. These works range from extending the workflow with access control aspects (e.g., [7], [19]) to, vice versa, embedding the workflow within the access control system (e.g., [6], [14], [16], [23]), thus mainly focusing on one level at a time and abstracting away most or all of the possible interplay between the WF and PM levels. Other works (e.g. [2], [4], [5], [20]) have in contrast proposed approaches that attempt to model and analyze the interplay. We believe that our framework is abstract enough to encompass such approaches and we are currently investigating how they can be recast in our framework. In particular, we plan to use our framework to model Petri nets and access control policies as in [2] so as to perform deductive-based model checking of security-sensitive business processes, and also to formally analyze properties of RBAC by adapting the framework of [4], [5]. Finally, we also plan to extend the framework as we presented it in this paper, e.g. with interfaces more refined than the T sub we considered here, so as to be able to perform modular reasoning in the assume-guarantee style.
APPENDIX A PROOFS Proof of Property 1: We reason by contradiction and reduce validity to satisfiability. The validity (modulo T SOA ) of formulae of the form (4) is equivalent to the T SOAunsatisfiability of the negation of (4), i.e.
∃x, x . ϕ(p, x) ∧ τ (p, x, p , x ) ∧ ¬ψ(p , x ), which, in turn, is equivalent to the T SOA -unsatisfiability of After some simple logical manipulations, the problem reduces to checking the T SOA -unsatisfiability of the following quantifier-free formula where x, x are considered as Skolem constants (or, equivalently, as implicitly existentially quantified variables). Now, to simplify our argument and make it easier to grasp, we use a little bit of higher-order logic and regard ∀z. p (z) ↔ φ(p, z, i) as p = λz. φ(p, z, i). In this way, it is obvious that, after two simple substitutions, the last formula above becomes which is easily seen to be equisatisfiable to the previous one (intuitively, it is always possible to find an assignment for the variables in x when the last formula is satisfiable: just take the values of f (x, i); a similar observation holds for the predicate symbols in p ). Now, we are left with the problem of checking whether the last formula is quantifier-free. To see this, recall that ψ is quantifier-free and this implies that every occurrence of a predicate symbol in p is applied to a tuple of ground terms. Hence, the effect of substituting p with λz. φ(p, z, i) is a tuple of quantifier-free formulae because of β-reduction. Let ψ(φ(p, i), f (x, i))) be the result of exhaustively performing such β-reductions; then, the formula is quantifier-free. This concludes the proof.
Proof of Lemma 1: We apply one of the results on nondisjoint combination of theories in [15], namely the following: if (i) T sub is a universal theory contained in both T WF and T PM , (ii) T sub admits a model completion T * sub , (iii) every model of T WF and T PM embeds into a model of T WF ∪ T * sub and of T WF ∪ T * sub , respectively, and (iv) T sub is effectively locally finite, then the (T WF ∪ T PM )-satisfiability problem is decidable (by an extension of the Nelson-Oppen combination schema). Let us check each of the conditions (i)-(iv): (i) This is satisfied by assumption.
(ii) By a well-known result in model-theory (see, e.g., [12]), a theory T admitting elimination of quantifiers also admits a model completion T * and furthermore T = T * . It is not difficult to check that T sub admits elimination of quantifiers (it is sufficient to note that ∃x. ϕ(x) is T sub -equivalent to ci ϕ(x/c i ) for ϕ a quantifier-free formula and c i 's the constants denoting the elements of the domain of the enumerated data type). Hence, T sub admits a model completion and T * sub = T sub . (iii) Since T * sub = T sub and, by assumption, T WF ⊇ T sub and T PM ⊇ T sub , we have that T WF ∪ T * sub = T WF ∪ T sub = T WF and, similarly, T PM ∪ T * sub = T PM ∪ T sub = T PM . This implies that every model of T WF (respectively, T PM ) is also a model of T WF ∪ T * sub (respectively, T WF ∪ T * sub ), which implies that every model of T WF (respectively, T PM ) can be embedded into a model of T WF ∪ T * sub (respectively, T WF ∪ T * sub ), just take identity as the embedding. 3 (iv) Indeed, the signature of an enumerated data-type theory is finite and consists of a finite set of constants, say {c 1 , ..., c n } for some n ≥ 1. The constants c 1 , ..., c n are the representatives since, for every term t, T sub |= t = c i for some i. 4 Proof of Property 2: Reason by refutation and expand the definition of the negation of {ψ 0 }τ {ψ 0 }, so as to obtain the following formula: This, in turn, is equivalent to Then, by recalling the definition of τ and performing the obvious substitutions (in a way similar to what we have done in the proof of Property 1 above), we obtain: ∃x, x , j, k, d.
which, by exhaustively applying β-reduction and considering existentially quantified variables as Skolem constants, is equivalent to where τ and ψ are the result of β-reducing the corresponding formulae. It is not difficult to see that the last formula is a conjunction of a universally quantified formula ∀i. ψ(i, p, x) 3 An embedding µ between two Σ-structures M = (M, I) and N = (N, J) is a mapping from M to N such that M |= α iff N |= α, for every Σ M -atom α. (In other words, an embedding between M and N is an isomorphism of M onto a sub-structure of N .) We say that M is embeddable in N if there exists an embedding between M and N . 4 A Σ-theory T is locally finite if Σ is finite and, for every set of constants a, there are finitely many ground terms t 1 , ..., t ka , called representatives, such that for every ground Σ a -term u, we have T |= u = t i for some i. If the representatives are effectively computable from a and t i is computable from u, then T is effectively locally finite. with a quantifier-free formula τ (p, x, φ(p, z, k), f (x, k)) ∧ ¬ψ(j, φ(p, z, k), f (x, k)) and that it cannot be simplified further or, in other words, that the universal quantifier on i cannot be removed. This concludes the proof.
Proof of Lemma 2: We claim that the quantifier-free formula σ ϕ(iσ, x, p) is T SOA -equisatisfiable to the universally quantified formula above, where σ ranges over all possible ground substitutions mapping the variables in i to a finite subset of constant symbols in Σ sub . If the T SOA -satisfiability problem is decidable (for quantifier-free) formulae, then the proof is complete. To this end, we use the same combination result in [15] as that for Lemma 1, i.e. if (i) T sub is a universal theory contained in both T WF and T PM , (ii) T sub admits a model completion T * sub , (iii) every model of T WF and T PM embeds into a model of T WF ∪ T * sub and of T WF ∪ T * sub , respectively, and (iv) T sub is effectively locally finite, then the (T WF ∪T PM )-satisfiability problem is decidable (by an extension of the Nelson-Oppen combination schema). Let us check each of the conditions (i)-(iv): (i) T sub is the theory of an equivalence relation, which can be axiomatized by a finite set of universal sentences corresponding to reflexivity, symmetry, and transitivity. Hence, T sub is universal. (ii) It is well-known that the model-completion T * sub of the theory of an equivalence relation is the theory of an infinite set (see, e.g., [15]). (iii) It is possible to show that this is equivalent to stably infiniteness (again, see [15]) which is an assumption for T WF while it can be easily shown that any BSR theory is stably infinite (see, e.g., [22]), hence T PM is also so. (iv) T sub is the theory of an equivalence relation with finitely many equivalence classes. So, although there are infinitely (more precisely, countably many) constant symbols of sort Id , there exists a finite subset C = {c 1 , ..., c n } such that for any other constant symbol d of sort Id , we have T sub |= d = c i for some i ∈ {1, ..., n}. This means that T sub is an effectively locally finite theory. Thus, we conclude that the T SOA -satisfiability problem for quantifier-free formulae is decidable.
To conclude the proof, we are left with the problem of proving the claim above. To this end, first of all, recall that T sub is effectively locally finite. Then, observe that T PM is a BSR theory and hence Σ PM has no function symbol of arity greater than 0. Furthermore, recall that, by assumption, all function symbols of arity greater than 0 in Σ WF are such that their return type is not Id . Thus, we have that T PM |= d = c i and T WF |= d = c i , for every constant symbol of sort Id in Σ sub and some c i ∈ C. This is so because the reduct to Σ sub of every Σ PM -model of T PM and Σ WF -model of T WF is a model of T sub . So, if the quantifier-free formula σ ϕ(iσ, x, p) is T SOA -unsatisfiable, where σ is a ground substitution mapping the variables in i to the computable finite subset C of the constants in Σ sub of sort Id , then the universally quantified formula ∀i : Id . ϕ(i, x, p), is also unsatisfiable. For the converse, it is sufficient to recall that T sub is a universal theory and that universal theories are closed under sub-structures, i.e. any sub-structure of a model of the theory is also a model. This implies that if the quantifierfree formula above is T SOA -satisfiable, then the universally quantified-formula is also so.

APPENDIX B A CASE STUDY: CAR REGISTRATION OFFICE
The techniques and results that we give in this paper are general and independent of particular concrete applications, but, to illustrate them concretely, it is useful to consider an example from industrial practice: we consider a simplified version of the car registration office case study described in [3], which can be intuitively summarized as follows.
A citizen, called Charlie, submits a request to register his new car to an employee, called Ed, of the local car registration office CRO. 5 Charlie's message contains all the documents to support his request and it is suitably signed. Upon reception of the request, Ed has appropriate support for checking the signature of the document and comparing it with the identity of the sender of the request: if the signature and the identity of the requester do not match, then the request is immediately refused and the sender is acknowledged of this fact; otherwise, Ed starts to consider the content of the request for the car registration. If, according to some criteria (that are abstracted away in the specification), the request is not suitably supported by the documents, then the request is refused and, again, the sender is acknowledged of this fact; otherwise, the request is accepted, the sender is acknowledged of acceptance and the request is marked as accepted, signed by Ed, and finally sent to the central repository CRep to be archived.
This process is completely transparent to Charlie and, in order to be successfully completed, Ed should have the right to store documents in the CRep. This right can only be granted by the head of the CRO, a (special) employee called Helen. Upon reception of the request by Ed to store a processed request in its internal database, the CRep checks whether Ed has been granted the right to do so. If this is the case, the CRep stores the document; otherwise, it refuses to comply.
Roles are assigned to employees (of the CRO) by circulating appropriate certificates; such as, e.g., "Ed is an employee" or "Helen is the head of the CRO." These certificates are emitted by a certification authority RegOffCA, that is recognized by the employees of the CRO and the CRep. Permission to store documents in the CRep are also distributed to employees by creating appropriate certificates; however, these certificates are created by the head of the CRO (not by the certification authority).
The CRep, before storing a processed request in its internal database, checks whether the employee has the right to do so. For this to be successfully executed, the following policy should be enforced: • an employee of the car registration office can store documents in the CRep, if the head of the car registration office permits it, and the following trust relationships should have been preliminarily established: • the RegOffCA is trusted by all employees, by the head of the car registration office, and the CRep for what concerns role certificates; and • the head of the car registration office is trusted by the CRep for action (e.g., storing documents) certificates.
Finally, to be able to successfully execute the scenario with Charlie and Ed described above, the following certificates should be available in the system: • Ed is an employee of the car registration office (by a certificate emitted by RegOffCA), • Helen is the head of the car registration office (by a certificate emitted by RegOffCA), and • Helen permits Ed to store documents in the CRep (by a certificate emitted by Helen).

Formalization
Since only the exchange of messages drives the workflow of the system and the most interesting part of the case study concerns its policies, we adopt the MsgPass[Msg] theory described in Example 1. In the body of a message, documents (such as car registration requests or processed requests) can be embedded (embeddoc). Since both citizens and employees should be able to sign documents and the latter should also be able to check signatures, appropriate primitives are provided to generate signatures (sign), attaching them to documents (augdocwithsign), and checking that the signature attached to a document belongs to a certain principal (matchuser). An employee has also the primitive to attach a decision (accept or refuse) to a document containing a citizen request (augdocwithact). Finally, as role certificates should be distributed over the network, we provide an appropriate primitive (rolecert) to create these documents. (Role certificates are handled at the policy level only; see below for more details.) Now, we identify the theories involved: , the theory described in the Example 1 above, a set of Horn rules defined below. 6 As we have said above, the workflow of the system is almost state-less. There are however two exceptions. One is the database of the central repository which is modeled by the unary predicate dbdoc to which documents may only be added (and never deleted). The other is the unary predicate isok that allows us to abstract away the criteria according to which a citizen request is accepted or refused. This completes the description of the (static part of the) workflow. We now describe the policy level of the system. We adapted the DKAL [16] approach to specifying policies in our framework. To this end, DKAL provides predicates (knows and knows 0 ) to represent the knowledge of the various agents and predicates (saysTo and saysTo 0 ) for the communication between agents.
It is important to observe the differences between the communication at the workflow and the policy levels of the system. The former (modeled via the MsgPass[Msg] theory) is state-full and thus modeled by an appropriate set of transitions (see below). The latter (modeled via saysTo or saysTo 0 ) is state-less and thus modeled by suitable Horn clauses. Finally, DKAL proposes two functions (tdOn or tdOn 0 ) to track trust relationships between agents concerning certain facts. All this is formally captured in the following set of Horn clauses.
First, we provide an (incomplete) characterization of the DKAL-like predicates expressing knowledge and communication for policies (this is adapted from [16], to which the interested reader is pointed to for details).
Knowledge 0∞ : Internal knowledge is knowledge. knows(P, AnyT hing) ← knows0(P, AnyT hing) Say2know 0∞ : An agent knows whatever is said to him and he/she also knows whether the piece of knowledge being communicated is based on the internal knowledge of the speaker (say2know 0 ) or not (say2know ∞ ). knows0(P, said0(Q, AnyT hing)) ← saysTo 0 (Q, AnyT hing, P ) knows(P, said(Q, AnyT hing)) ← saysTo(Q, AnyT hing, P ) T rustedknowledge 0∞ : An agent P knows a piece of information AnyT hing whenever an agent P knows that another agent Q said the piece of information AnyT hing and also that P knows that the agent Q is trusted on saying the piece of information AnyT hing.
knows(P, AnyT hing) ←knows(P, tdOn0(Q, AnyT hing)) ∧ knows(P, said0(Q, AnyT hing)) knows(P, AnyT hing) ←knows(P, tdOn(Q, AnyT hing)) ∧ knows(P, said(Q, AnyT hing)) 6 The class of Horn rules is an extension of that of Datalog rules whereby function symbols of arity greater than 0 are allowed. Then, we consider the policies of each agent. The first three Horn clauses specify the communication of (role and action) certificates at the policy level. (Note that while the knowledge of an action certificate for Ed is explicitly given in the initial state above, the knowledge of the role certificates for Ed and Helen will be lifted from the existence of the corresponding messages in the network by appropriate transitions.) The last three Horn clauses are the formal counterparts of the trust relationships described above.
(Simple) employee saysTo(Empl,said0(RegOffCA, Cert), ) ← (Cert1) knows(Empl, said0(RegOffCA, Cert)) saysTo(Empl,said0(Head, Cert), ) ← (Cert2) knows(Empl, said0(Head, Cert)) In the Horn rules above, and also in some of the following ones, we use a Prolog-like notation where the symbol is employed as an abbreviation for a universally quantified variable that occurs only once in the rule. knows(CentrRep, tdOn0(Head, storedocCRep(Empl))) ← knows(CentrRep, said0(RegOffCA, isRegOffHead(Head))) ∧ knows(CentrRep, said0(RegOffCA, isRegOffEmpl(Empl))) (CentrRepTrustAnyoneViaHead) Finally, in Fig. 3, we give the transitions modeling the dynamics of the system. The first two transitions (GetRoleCertEmpl , GetRoleCertHead ), are part of the interface between the workflow and the policy levels of the system as they allow employees to convert the content of role certificates received from the network to (internal) knowledge, which is relevant for the application of policies (compare the right-hand sides of these rules with the hypotheses of the Horn clauses Cert1 and Cert2). The following two transitions specify the processing of a citizen request by an employee (Accept), and how the central repository handles the request of an employee to store a document in its internal database (Storedoc). This is (the remaining) part of the interface between the workflow and the policy level: the guard knows(CentrRep, storedocCRep(Empl)) is a query that is possibly solved by the Horn clauses above.

Executability
It is relatively easy to check that the scenario described above involving Ed and Helen can be executed by a suitable sequence of transitions and solving appropriate queries against the policies of the system. For instance, let us, for the sake of brevity, only analyze the first step, which requires the application of the transition GetRoleCertEmpl to lead the two-level SO transition system from the initial state to a state where the PM knowledge about the identity of Ed has been acquired. The initial state ι is characterized by the following formula, net = ins(msg(Charlie, embeddoc(augdocwithsign(req, sign(Charlie, req))), Ed), ins(msg(RegOffCA, embeddoc(augdocwithsign(ρE, sign(RegOffCA, ρE))), Ed), ins(msg(RegOffCA, embeddoc(augdocwithsign(ρH , sign(RegOffCA, ρH ))), Ed), mty))) ∧ p 1 ,p 2 ∈C,r∈R ¬hasrole(p1, p2, r) saying that principals knows nothing about their respective roles and the net contains three messages: one is the car registration request of Charlie and the other two are the role certificates of Ed (who is an employee) and Helen (who is the head of the car registration office), where ρ E and ρ H abbreviate the terms rolecert(Ed, employee) and rolecert(Helen, head), respectively, C = {RegOffCA, CRep, Ed, Charlie, Helen}, and R = {employee, head}.
The transition GetRoleCertEmpl is formalized as in Fig. 3. The set of states to which the transition GetRoleCertEmpl should lead the two-level SO transition system must be so as to satisfy the following formula ϕ 1 : saying that Ed has acquired the knowledge about its role at the PM level of the SO application. It is not difficult to show the T SOA -validity of {ι} GetRoleCertEmpl {ϕ 1 }. In fact, the transition is enabled since the following formula (obtained by instantiating both i 1 and i 2 with the constant Ed and substituting the state variable net with the term at the right of the first equality in ι): mem(msg(RegOffCA, embeddoc (augdocwithsign(ρE, sign(RegOffCA, ρE))), Ed)), ins(msg(Charlie, embeddoc(augdocwithsign(req, sign(Charlie, req))), Ed), ins(msg(RegOffCA, embeddoc(augdocwithsign(ρE, sign(RegOffCA, ρE))), Ed), ins(msg(RegOffCA, embeddoc(augdocwithsign(ρH , sign(RegOffCA, ρH ))), Ed), mty)))) is T SOA -satisfiable. We are left with the problem of showing the T SOA -unsatisfiability of the formula: ¬knows(Ed, isRegOffEmpl(Ed)) obtained by negating ϕ 1 . This can be easily done by observing that hasrole(Ed, Ed, employee) holds in the state where the transition GetRoleCertEmpl has lead the two-level SO transition system as the result of executing the PM update. Then, by instantiating the following Horn rule (in T PM ): with i 1 and i 2 substituted with Ed, it is possible to immediately detect unsatisfiability. In this way, we have proved the T SOA -unsatisfiability of the formula ¬({ι} GetRoleCertEmpl {ϕ 1 }) or, equivalently, the T SOAvalidity of {ι} GetRoleCertEmpl {ϕ 1 }.

Invariant properties
We consider the following interesting property about documents stored in the central repository: Integrity: any processed request preq stored in the central repository must be consistent, i.e., it should be double signed (by the citizen cit submitting the request req and by the employee empl handling it) and stamped with the seal of acceptance. Such a property can be written as the following safety formula in the extended version of LTL introduced above: 0 B B @ ∀preq.dbdoc(preq) ⇒ ∃cit, req, empl , preq 1 , preq 2 . 0 @ preq 1 = augdocwithsign(req, sign(user , req)) ∧ preq 2 = augdocwithdec(preq 1 , accept) ∧ preq = augdocwithsign(preq 2 , sign(empl , preq 2 )) Showing that the SO application ensures integrity is nontrivial, as the central repository treats documents as blackboxes and trusts employees to check signatures and correctly prepare processed requests. Furthermore, it trusts the head of GetRoleCertEmpl : where, µ is a term symbol of type Body that contains a sub-term of interest that represent a role certificate. GetRoleCertHead : Fig. 3. Transition formulae the central repository to judge the capability of employees to perform this job correctly. Ultimately, the central repository also trusts the certification authority to emit role certificates for both employees and the head of the car registration office. Besides these difficulties, the state formula inside the "alwaysin-the-future" operator is not of the kind supported by the decidability result of Lemma 2 because of the existential quantifier. As a consequence, more ingenuity is required by the specifier. We are currently working to derive a hand proof of this property.

A. Pragmatics of modeling WF and PM of SO applications
We extend the technical results of Section III with some observations on the pragmatics of modeling WF and PM of SO applications. In fact, pragmatically, the theories T WF and T PM are obtained by extending the substrate theory T sub as follows. For the WF theory, consider a finite set Ax(W F ) of universal Σ WF -sentences where Σ WF ⊇ Σ sub ; then The process of adding finitely many axioms to an available theory can be iterated several times to obtain the final WF theory. As an example, recall the theories Msg and MsgPass[Msg] of Examples 1 and 2. For the PM theory, along the lines of several other works in the PM literature (e.g., [18]), regard a logic program P (P M ) (formalizing policy statements) as a set of universal Horn Σ PM -clauses where Σ PM := Σ sub ∪ R for R a (finite) set of predicate symbols such that Σ sub ∩ R = ∅; 7 then Usually, the state predicates in P (PM ) are intensional, i.e. occur in the head of the rules of P (P M ). This is a sufficient condition to ensure that no transition may add a fact to the theory T PM that gives rise to an inconsistency.
In the (constraint) logic programming literature, T sub is usually introduced as a certain first-order structure (e.g., the integers). This is not compatible with the notion of theory adopted here (and in most logic textbooks) as we work with sets of sentences (axioms) rather than structures. However, given a structure M, it is possible to find a theory T admitting M as a model. So, if we are able to verify that T |= ϕ, we also know that M |= ϕ (while the converse, in general, may not hold). As a consequence, if we are able to reduce a certain verification problem for an SO application to showing that a formula follows from the background theory of the application and we succeed in doing this, we are entitled to conclude that the verification problem has a positive answer for any structure satisfying the axioms of the background theory. Indeed, we may obtain false negatives, as there may exist formulae that are true in a particular model of a theory T that are not logical consequences of T . An advantage of adopting this notion of theory is the possibility of re-using and adapting existing automated reasoning techniques (see below).

B. Pragmatics of executability of SO applications
Recall our remark on how the theories T WF and T PM are formed by augmenting the theory T sub with a finite set of universal axioms (see end of Section III), i.e.
T WF := {ψ is a sentence | Ax(W F ) |= ψ} ∪ T sub and T PM := {ψ is a Horn clause | P (P M ) |= ψ} ∪ T sub , where Ax(W F ) is a (finite) set of universal sentences and P (P M ) is a (finite) set of Horn clauses. It is not difficult to argue that both the T WF -and T PM -satisfiability problems are decidable. The decidability of the former can be derived by the decidability of the MsgPass-satisfiability problem (shown in [1]), the decidability of the satisfiability problem of any enumerated data-type theory (since it admits elimination of quantifiers), and the combination results in [8]. It is possible to use available SMT solvers (such as Yices, Z3, or MathSAT) to obtain a decision procedure for the T WF -satisfiability problem (almost) off-the-shelf; maybe using characteristic functions for sets and then using arrays of Booleans to formally represent such functions, see, e.g., [11]. The decidability of the T PMsatisfiability is an immediate consequence of the (well-known) decidability of the satisfiability problem for BSR theories. Since T sub is an enumerated data-type theory, the hypotheses of Lemma 1 are satisfied and we are entitled to conclude the decidability of the T SOA -satisfiability problem. Again, it is possible to use available SMT solvers, such as Z3, to have direct support for the class of BSR theories and hence to implement a decision procedure for the T PM -satisfiability problem.
We are then left with the problem of modularly reusing the decision procedures for the satisfiability problem in the component theories to obtain a decision procedure for the T SOAsatisfiability problem. When T sub is an enumerated data-type theory, as it is the case of Lemma 1, it is possible to use the non-deterministic version of the combination algorithm in [15] to implement a decision procedure for the T SOA -satisfiability problem. To understand this, let us briefly summarize an adaptation of the non-deterministic combination schema of [15]. To this end, let w.l.o.g. Γ be a conjunction of Σ SOA -literals. 8 First of all, we transform Γ into an equisatisfiable conjunction Γ WF ∧ Γ PM by naming sub-terms by means of additional constants a: this process is usually called purification and it can be implemented in polynomial time. As there are only finitely many constants c 1 , ..., c n in the enumerated data-type theory T sub , we non-deterministically guess an arrangement ∆, i.e. a conjunction of literals such that, for each a ∈ a, either a = c i or a = c i , for each c i is in Σ sub . Then, we check whether both Γ WF ∪ ∆ is T WF -satisfiable and Γ PM ∪ ∆ is T PM -satisfiable. If, for some arrangement, both tests are successful, then we conclude the T SOA -satisfiability φ (cf. Atoms at line 2) but also of all possible equalities between the constants in a and the constants in c (cf. IE at line 2). In this way, we are guaranteed to consider all possible arrangements as defined by the non-deterministic algorithm sketched above. Then, we check-separately-the T i -satisfiability of the conjunction of Σ i -literals Γ i ∧ ∆ sub (cf. lines 5 and 6): the T i -sat procedure besides returning sat or unsat also returns a conjunction π i (called the conflict set) of Σ i -literals, all of which also occur in Γ i ∧ ∆ sub , which is T i -unsatisfiable (for i ∈ {W F , P M }). If both satisfiability checks are positive, then we return the satisfiability of the input quantifier-free formula (cf. line 7). Otherwise, i.e. if at least one of the satisfiability checks returned unsat, the negation of π i , called a conflict clause, is added to φ (cf. line 8 or 9) so as to reduce the number of Boolean assignments that are to be considered in the main loop. This is one of the key ingredients (among many others, see, e.g., [21], for more details) of the success of current state-of-the-art SMT solvers and it avoids the burden of transforming quantifier-free formulae to disjunctive normal form, although the problem indeed is NP-hard.
The correctness of the algorithm in Fig. 4 is an immediate corollary of Lemma 1 above.
Property 3: Let T sub be an enumerated data-type theory, and T WF ⊇ T sub and T PM ⊇ T sub be consistent theories with T WF -sat and T PM -sat as decision procedures for their corresponding satisfiability problems. Then, the function T SOA -sat (depicted in Fig. 4) is a decision procedure for the T SOA -satisfiability problem.

C. Pragmatics of invariant verification of SO applications
Here the basis to implement an algorithm for the T SOAsatisfiability check of quantifier-free formulae is almost the same as the function depicted in Fig. 4. The main difference is in the definition of arrangement. In fact, we say that ∆ sub is an arrangement for the theory T sub of an equivalence relation over the set a of finite constants of sort Id if, for every pair (d, d ) for d, d ∈ a, either c = c ∈ ∆ sub or c = c ∈ ∆ sub . To implement this definition of arrangement, it is sufficient to replace line 2 of the function in Fig. 4 with the following one:
Let T SOA -qfsat be the new function so obtained; its correctness is a corollary of Lemma 2 above. Furthermore, following the proof of Lemma 2, it is sufficient to generate finitely many instances of a universally quantified formula of the form ∀i : Id . ϕ(i, x, p) to obtain a decision procedure for such a class of formulae. Indeed, the challenge here is to efficiently integrate the function T SOA -qfsat and an instantiation strategy for the universally quantified variables in i. This requires some heuristics to filter out instances that are unlikely to contribute to detecting the unsatisfiability of the formula. To understand why heuristics are needed, consider that the number of the possible ground substitutions σ is n k where n is the length of a and k is the length of i. Another key ingredient to scale up is to invoke T SOA -qfsat incrementally so as to add one by one the instances of ϕ. Since tuning these heuristics and making them work smoothly together require extensive experimental evaluation, we leave the details for future work.