Loïc Hélouët
email: loic.helouet@inria.fr

John Mullins
email: john.mullins@polymtl.ca

Hervé Marchand
email: herve.marchand@inria.fr

Concurrent secrets with quantified suspicion

A system satisfies opacity if its secret behaviors cannot be detected by any user of the system. Opacity of distributed systems was originally set as a boolean predicate before being quantified as measures in a probabilistic setting. This paper considers a different quantitative approach that measures the efforts that a malicious user has to make to detect a secret. This effort is measured as a distance w.r.t a regular profile specifying a normal behavior. This leads to several notions of quantitative opacity. When attackers are passive that is, when they just observe the system, quantitative opacity is brought back to a language inclusion problem, and is PSPACEcomplete. When attackers are active, that is, interact with the system in order to detect secret behaviors within a finite depth observation, quantitative opacity turns to be a two-player finitestate quantitative game of partial observation. A winning strategy for an attacker is a sequence of interactions with the system leading to a secret detection without exceeding some profile deviation measure threshold. In this active setting, the complexity of opacity is EXPTIME-complete.

I. INTRODUCTION

Opacity of a system is a property stating that occurrences of runs from a subset S of runs of the system (the secret) can not be detected by malicious users. Opacity [START_REF] Bryans | Opacity generalised to transition systems[END_REF], [START_REF] Badouel | Concurrent secrets[END_REF] can be used to model several security requirements like anonymity and non-interference [START_REF] Goguen | Security policies and security models[END_REF]. In the basic version of non-interference, actions of the system are divided into high (classified) actions and low (public) ones, and a system is non-interferent iff one can not infer from observation of low operations that highlevel actions were performed meaning that occurrence of high actions cannot affect "what an user can see or do". This implicitly means that users have, in addition to their standard behavior, observation capacities.

Non-interference is characterized as an equivalence between the system as it is observed by a low-level user and a ideally secure version of it where high-level actions and hence any information flow, are forbidden. This generic definition can be instantiated in many ways, by considering different modeling formalisms (automata, Petri nets, process algebra,...), and equivalences (language equivalence, bisimulation(s),...) representing the discriminating power of an attacker. (see [START_REF] Sabelfeld | Language-based information-flow security[END_REF] for a survey).

Opacity generalizes non-interference. The secrets to hide in a system are sets of runs that should remain indistinguishable from other behaviors. A system is considered as opaque if, as observed, one can not deduce that the current execution belongs to the secret. In the standard setting, violation of opacity is a passive process: attackers only rely on their partial observation of runs of the system. Checking whether a system is opaque is a PSPACE-complete problem [START_REF] Cassez | Synthesis of opaque systems with static and dynamic masks[END_REF].

As such, opacity does not take in account information that can be gained by active attackers. Indeed, a system may face an attacker having the capability not only to observe the system but also to interact with him in order to eventually disambiguate observation and detect a secret. A second aspect usually ignored is the quantification of opacity : the more executions leaking information are costly for the attacker, the more secure is the system. In this paper we address both aspects. A first result of this paper is to consider active opacity, that is opacity in a setting where attackers of a system perform actions in order to collect information on secrets of the system. Performing actions in our setting means playing standard operations allowed by the system, but also using observation capacities to infer whether a sensible run is being performed. Checking opacity in an active context is a partial information reachability game, and is shown EXPTIME-complete.

We then address opacity in a quantitative framework, characterizing the efforts needed for an attacker to gain hidden information with a cost function. Within this setting, a system remains opaque if the cost needed to obtain information exceeds a certain threshold. This cost is measured as a distance of the attacker's behavior with respect to a regular profile, modeling that deviations are caught by anomaly detection mechanisms. We use several types of distances, and show that quantitative and passive opacity remains PSPACE-complete, while quantitative and active opacity remains EXPTIMEcomplete.

Opacity with passive attackers has been addressed in a quantitative setting by [START_REF] Bérard | Quantifying opacity[END_REF]. They show several measures for opacity. Given a predicate φ characterizing secret runs, a first measure quantifies opacity as the probability of a set of runs which observation suffice to claim the run satisfies φ. A second measure considers observation classes (sets of runs with the same observation), and defines the restrictive probabilistic opacity measure as an harmonic mean (weighted by the probability of observations) of probability that φ is false in a given observation class. Our setting differs from the setting of [START_REF] Bérard | Quantifying opacity[END_REF] is the sense that we do not measure secrecy as the probability to leak information to a passive attacker, but rather quantify the minimal efforts required by an active attacker to obtain information.

The paper is organized as follows: Section II introduces our model for distributed systems, and the definition of opacity. Section III recalls the standard notion of opacity usually found in the literature and its PSPACE-completeness, shows how to model active attackers with strategies, and proves that active opacity can be solved as a partial information game over an exponential size arena, and is EXPTIME-complete. Section IV introduces quantification in opacity questions, by measuring the distance between the expected behavior of an agent and its current behavior, and solves the opacity question with respect to a bound on this distance. Section V enhances this setting by discounting distances, first by defining a suspicion level that depends on evolution of the number of errors within a bounded window, and then, by averaging the number of anomalies along runs. The first window-based approach does not change the complexity classes of passive/active opacity, but deciding opacity for averaged measures is still an open problem.

II. MODEL

Let Σ be an alphabet, and let Σ ⊆ Σ. A word of Σ * is a sequence of letters w = σ 1 . . . σ n . We denote by w -1 the mirror of w, i.e., w -1 = σ n . . . σ 1 .The projection of w on Σ ⊆ Σ is defined by the morphism π Σ : Σ * → Σ * defined as π Σ ( ) = , π Σ (a.w) = a.π Σ (w) if a ∈ Σ and π Σ (a.w) = π Σ (w) otherwise. The inverse projection of w is the set of words which projection is w, and is defined as π -1 Σ (w) = {w ∈ Σ * | π Σ (w ) = w}. For a pair of words w, w defined over alphabets Σ and Σ , the shuffle of w and w is denoted by w||w and is defined as the set of words w||w = {w | π Σ (w ) = w ∧ π Σ (w ) = w }. The shuffle of two languages L 1 , L 2 is the set of words obtained as a shuffle of a words of L 1 with a word of L 2 .

Definition 1: A concurrent system S = (A, U ) is composed of:

• A finite automaton A = (Σ, Q, -→, q 0 , F ) • A finite set of agents U = u 1 , . . . u n , where each u i is a tuple u i = (A i , P i , S i , Σ i o ), where A i , P i , S i are automata and Σ i o an observation alphabet. Agents behave according to their own logic, depicted by a finite automaton A i = (Σ i , Q i , -→ i , q i 0 , F i ) over an action alphabet Σ i . We consider that agents moves synchronize with the system when performing their actions. This allows modeling situations such as entering critical sections. We consider that in A and in every A i , all states are accepting. This way, every sequence of steps of S that conforms to transition relations is a behavior of S. An agent u i observes a subset of actions, defined as an observation alphabet Σ i o ⊆ Σ 1 . Every agent u i possesses a secret, defined as a regular language L(S i ) recognized by automaton

S i = (Σ, Q S i , -→ S i , q S 0,i , F S i ).
All states of secret automata are not accepting, i.e. some behaviors of an agent u i are secret, some are not. We equip every agent u i with a profile P i = (Σ, Q P i , δ P i , s P 0,i , F P i ), that specifies its "normal" behavior. The profile of an agent is 1 A particular case is Σ i o = Σ i , meaning that agent u i observes only what it is allowed to do. prefix-closed. Hence, F P i = Q P i , and if w.a belongs to profile L(P i ) then w is also in user u i 's profile. In profiles, we mainly want to consider actions of a particular agent. However, for convenience, we define profiles over alphabet Σ, and build them in such a way that L(

P i ) = L(P i ) (Σ \ Σ i ) * .
We assume that the secret S i of an user u i can contain words from Σ * , and not only words in Σ * i . This is justified by the fact that an user may want to hide some behavior that are sensible only if they occur after other agents actions (u 1 plays b immediately after a was played by another agent). For consistency, we furthermore assume that Σ i ⊆ Σ i o , i.e., an user observes at least its own actions. Two users may have common actions (i.e., Σ i ∩ Σ j = ∅), which allows synchronizations among agents. We denote by Σ U = ∪ i∈U Σ i the possible actions of all users. Note that Σ U ⊆ Σ as the system may have its own internal actions.

Intuitively, in a concurrent system, A describes the actions that are feasible with respect to the current global state of the system (available resources, locks, access rights,...). The overall behavior of the system is a synchronized product of agents behaviors, intersected with L(A). Hence, within a concurrent system, agents perform moves that are allowed by their current state if they are feasible in the system. If two or more agents can perform a transition via the same action a, then all agents that can execute a move conjointly to the next state in their local automaton. More formally, a configuration of a concurrent system is a tuple C = (q, q 1 , . . . , q |U | ), where q ∈ Q is a state of A and each q i ∈ Q i is a local state of user u i . The first component of a configuration C is denoted state(C). We consider that the system starts in an initial configuration C 0 = (q 0 , q 1 0 , . . . , q |U | 0 ). A move from a configuration C = (q, q 1 , . . . , q |U | ) to a configuration C = (q , q 1 , . . . , q |U | ) via action a is allowed

• if a ∈ Σ U and (q, a, q ) ∈-→, or • if a ∈ Σ U , (q, a, q ) ∈-→, there exists at least one agent u i such that (q i , a, q i ) ∈-→ i , and for every q j such that some transition labeled by a is firable from q j , (q j , a, q j ) ∈-→ j . The local state of agents that cannot execute a remains unchanged, i.e., if agent u k is such that a ∈ Σ k and (q j , a, q j ) ∈-→ j , then

q k = q k . A run of S = (A, U ) is a sequence of moves ρ = C 0 a1 -→ C 1 . . . C k . Given a run ρ = C 0 a1 -→ C 1 . . . a k -→ C k , we denote by l(ρ) = a 1 • • • a k its corresponding word.
The set of run of S is denoted by Runs(S), while the language L(S) = l(Runs(S)) is the set of words labeling runs of S. We denote by Conf (S) the configurations reached by S starting from C 0 . The size |S| of S is the size of its set of configurations. Given an automaton A, P i , or S i , we denote by δ(q, A, a) (resp δ(q, P i , a), δ(q, S i , a)) the states that are successors of q by a transition labeled by a, i.e. δ(q, A, a) = {q | q a -→ q }. This relation extends to sets of states the obvious way, and to words, i.e. δ(q, A, w.a) = δ(δ(q, A, w), A, a) with δ(q, A, ) = {q}. Last, for a given sub-alphabet Σ ⊆ Σ and a letter a ∈ Σ , we define by ∆ Σ (q, A, a) the set of states that are reachable from q in A by sequences of moves which observation is a. More formally, ∆ Σ (q, A, a) = {q | ∃w ∈ (Σ \ Σ ) * , q ∈ δ(q, A, w.a)}.

III. OPACITY FOR CONCURRENT SYSTEMS

The standard Boolean notion of opacity introduced by [START_REF] Bryans | Opacity generalised to transition systems[END_REF], [START_REF] Badouel | Concurrent secrets[END_REF] says that the secret of u i in a concurrent system S is opaque to u j if, every secret run of u i is equivalent with respect to u j 's observation to a non-secret run. In other words, u j cannot say with certainty that the currently executed run belongs to L(S i ).

Implicitly, opacity assumes that the specification of the system is known by all participants. In the setting of concurrent system with several agents and secrets, concurrent opacity can then be defined as follows:

Definition 2 (Concurrent Opacity):

A concurrent system S is opaque w.r.t. U (noted U -Opaque) if ∀i = j, ∀w ∈ L(S i ) ∩ L(S), π -1 Σ j o (π Σ j o (w)) ∩ L(S) L(S i )
Clearly, U -opacity is violated if one can find a pair of users u i , u j and a run labeled by a word w ∈ L(S i )∩L(S) such that π -1

Σ j o (π Σ j o (w)) ∩ L(S) ⊆ L(S i ),
i.e. after playing w, there in no ambiguity for u j on the fact that w is a run contained in u i s secret. Unsurprisingly, checking opacity can be brought back to a language inclusion question, and is hence PSPACE-complete. This property was already shown in [START_REF] Cassez | Synthesis of opaque systems with static and dynamic masks[END_REF] with a slightly different model (with a single agent j which behavior is Σ * j and a secret defined as a sub-language of the system A).

Theorem 3 ( [START_REF] Cassez | Synthesis of opaque systems with static and dynamic masks[END_REF]): Deciding whether S is U -opaque is PSPACE-complete.

Proof:[sketch] The proof of PSPACE-completeness consists in first showing that one can find a witness run in polynomial space. One can chose a pair of users u i , u j in logarithmic space with respect to the number of users, and then find a run after which u j can estimate without error that u i is in a secret state. Then, an exploration has to maintain u j 's estimation of possible configuration of status of u i 's secret with |Conf (S)| * |S i | bits. It is also useless to consider runs of length greater than 2 |Conf (S)| * |Si| . So finding a witness is in NPSPACE and using Savitch's lemma [START_REF] Walter | Relationships between nondeterministic and deterministic tape complexities[END_REF] and closure of PSPACE by complementation, opacity is in PSPACE. Hardness comes from a reduction from universality question for regular languages. We refer interested readers to appendix for a complete proof.

The standard notion of opacity considers accidental leakage of secret information to an honest user u j that is passive, i.e. that does not behave in order to obtain this information. One can also consider an active setting, where a particular agent u j behaves in order to obtain information on a secret S i . In this setting, one can see opacity as a partial information reachability game, where player u j tries to reach a state in which his estimation of S i s states in contained in F S i . Following the definition of non-interference by Goguen & Messeguer [START_REF] Goguen | Security policies and security models[END_REF], we also equip our agents with observation capacities. These capacities can be used to know the current status of resources of the system, but not to get directly information on other agents states. We define a set of atomic propositions Γ, and assign observable propositions to each state of A via a map O : Q → 2 Γ . We next equip users with additional actions that consist in asking for the truth value of a particular proposition γ ∈ Γ. For each γ ∈ Γ, we define action a γ that consists in checking the truth value of proposition γ, and define Σ Γ = {a γ | γ ∈ Γ}. We denote by a γ (q) the truth value of proposition γ in state q, i.e., a γ (q) = tt if γ ∈ O(q) and ff otherwise. Given a set of states X = {q 1 , . . . q k }, the refinement of X with assertion γ = v where v ∈ {tt, ff } is the set X \γ=v = {q i ∈ X | a γ (q i ) = v}. Refinement easily extends to a set of configurations CX ⊆ Conf (S) with

CX \γ=v = {C ∈ CX | a γ (state(C)) = v}.
We allow observation from any configuration for every user, hence a behavior of a concurrent system with active attackers shuffles behaviors from L(S), observation actions from Σ * Γ and the obtained answers. To simplify notations, we assume that a query and its answer are consecutive transitions. The set of queries of a particular agent u j will be denoted by Σ Γ j . Adding the capacity to observe states of a system forces to consider runs of S containing queries followed by their answers instead of simply runs over Σ * .

We will denote by S Γ the system S executed in an active environment Formally, a run of S Γ in an active setting is a sequence

ρ = C 0 e1 -→ S Γ C 1 . . . e k -→ S Γ C k where C 0 , . . . , C k are usual configurations, each e i is a letter from Σ ∪ Σ Γ ∪ {tt, ff }, such that • if e k ∈ Σ Γ then C k+1 ∈ δ(C k , S, e k ).
• if e k = a γ ∈ Σ Γ , then e k+1 = a γ (q k-1 )2 , and C k-1 = C k+1 . Intuitively, testing the value of a proposition does not change the current state of the system. Furthermore, playing action a γ from C k-1 leaves the system in the same configuration, but remembering that an agent just made the query a γ . We will write C k = C k-1 (a γ ) to denote this situation. The semantics of S Γ can be easily obtained from that of S. It can be defined as a new labeled transition system LT S Γ (S) = (Conf (S Γ ), -→ S Γ , C 0 ) over alphabet Σ ∪ Σ Γ ∪ {tt, ff } recognizing runs of S Γ . If LT S(S) = (Conf (S), -→) is an LTS defining runs of S, then LT S(S Γ ) can be built by adding a loop of the form

C k aγ -→ S Γ C k (a γ ) aγ (q k ) -→ S Γ C k from each configuration C k in Conf (S).
We denote by Runs(S Γ ) the set of runs of system S in an active setting with observation actions Σ Γ . As usual, ρ is a secret run of agent u i iff l(ρ) is recognized by automaton S i . The observation of a run ρ by user u j is a word l j (ρ) obtained by projection of l(ρ) on Σ j ∪ Σ Γ j ∪ {tt, ff }. Hence, an observation of user j is a word l j (ρ) = α 1 . . . α k where α m+1 ∈ {tt, ff } if α m ∈ Σ Γ j (α m is a query followed by the corresponding answer).

Let w ∈ (Σ j .(Σ Γ j .{tt, ff }) * ) * . We denote by l -1 j (w) the set of runs of S Γ which observation by u j is w. A malicious agent can only rely on his observation of S to take the decisions that will provide him information on other users secret. Possible actions to achieve this goals are captured by the notion of strategy.

Definition 4: A strategy for an user u j is a map µ j from Runs(S Γ ) to Σ j ∪ Σ Γ j ∪ { }. We assume that strategies are observation based, that is if l j (ρ) = l j (ρ ), then µ j (ρ) = µ j (ρ ).

A run ρ = C 0 e1 -→ C 1 . . . C k conforms to strategy µ j iff, ∀i, µ j (l(C 0 -→ . . . C i )) = implies e i+1 = µ j (l(C 0 -→ . . . C i )) or e i+1 ∈ Σ j ∪ Σ Γ j .
Intuitively, a strategy indicates to player u j the next move to choose (either an action or an observation or nothing. Even if a particular action is advised, another player can play before u j does. We will denote by Runs(S, µ j ) the runs of S that conform to µ j . Let µ j be a strategy of u j and ρ ∈ Runs(S Γ ) be a run ending in a configuration C = (q, q 1 , . . . q |U | ), we now define the set of all possible configurations in which S can be after observation l j (ρ) under strategy µ j . It is inductively defined as follows:

• ∆ µj (X, S Γ , ) = X for every set of configurations X • ∆µ j (X, S Γ , w.e) =                ∆ Σ j o (∆µ j (X, S Γ , w), S Γ , e) if e ∈ Σj ∆µ j (X, S Γ , w) if e = aγ ∈ Σ Γ j ,
∆µ j (X, S Γ , w) \γ(q) if e ∈ {tt, ff } and w = w .aγ for some γ ∈ Γ Now, ∆ µj ({C 0 }, S Γ , w) is the estimation of the possible set of reachable configurations that u j can build after observing w. We can also define a set of plausible runs leading to observation w ∈ (Σ j o ) * by u j . A run is plausible after w if its observation by u j is w, and at every step of the run ending in some configuration C k a test performed by u j refine u j s estimation to a set of configuration that contain C k . More formally, the set of plausible runs after w under strategy µ j is P l j (w) = {ρ ∈ Runs(S, µ j ) | l j (ρ) = w ∧ ρ is a run from C 0 to a configuration C ∈ ∆ µj ({C 0 }, S Γ , w)}.

We now redefine the notion of opacity in an active context. A strategy µ j of u j to learn S i is not efficient if despite the use of µ j , there is still a way to hide S i for an arbitrary long time.

In what follows, we assume that there is only one attacker of the system.

Definition 5 (Opacity with active observation strategy): A secret S i is opaque for any observation strategy to user u j in a system S iff µ j and a bound K ∈ N, such that ∀ρ ∈ Runs(S, µ j ), ρ has a prefix ρ 1 of size ≤ K, l(P l(ρ 1 )) ⊆ L(S i ). A system S is opaque for any observation strategy iff ∀i = j, secret S i is opaque for any observation strategy of u j .

Let us comment differences between passive (def. 2) and active opacity (def. 5). A system that is not U-opaque may leak information while a system that not opaque with active observation strategy cannot avoid leaking information if u j implements an adequate strategy. U-opaque systems are not necessarily opaque with strategies, as active tests give additional information that can disambiguate state estimation. However, if a system is U-opaque, then strategies that do not use disambiguation capacities do not leak secrets. Note also that a non-U-opaque system may leak information in more runs under an adequate strategy. Conversely, a non-opaque system can be opaque in an active setting, as the system can delay leakage of information for an arbitrary long time. Based on the definition of active opacity, we can state the following result:

Theorem 6: Given a system S = (A, U ) with n agents and a set secrets S 1 , . . . S n , observation alphabets Σ 1 o , . . . Σ n o and observation capacities Σ Γ 1 , . . . , Σ Γ n , deciding whether S is opaque with active observation strategies is EXPTIMEcomplete.

Proof:[sketch] An active attacker u j can claim that the system is executing a run ρ that is secret for u i iff it can claim with certainty that ρ is recognized by S i . This can be achieved by maintaining an estimation of the system's current configuration, together with an estimation of S i 's possible states. We build an arena with nodes of the form n = (b, C, s, ES) contains a player's name b (0 or 1): intuitively, 0 nodes are nodes where all agents but u j can play, and 1 nodes are nodes where only agent u j plays. Nodes also contain the current configuration C of S, the current state s of S i , an estimation ES of possible configurations of the system with secret's current state by

u j , ES j = {(C 1 , s 1 ), ...(C k , s k )}.
The attacker starts with an initial estimation ES 0 = {(C 0 , q S 0,i )}. Then, at each occurrence of an observable move, the state estimation is updated as follows : given a letter a ∈ Σ j o , for every pair (C k , s k ), we compute the set of pairs (C k , s k ) such that there exists a runs from C k to C k , that is labeled by a word w that is accepted from s k and leads to s k in S i and such that l j (w) = a. The new estimation is the union of all pairs computed this way.

Moves in this arena represent actions of player u j (from nodes where b = 1 and actions from the rest of the system (see appendix for details). Obviously, this arena is of exponential size w.r.t. the size of configurations of S.

A node n = (b, C, s, ES) is not secret if s ∈ F S i , and secret otherwise. A node is ambiguous if there exists (C p , s p ) and

(C m , s m ) in ES such that s p ∈ F S i is secret and s m ∈ F S i . If the restriction of ES to it second components is contained in F S i , n leaks secret S i .
The set of winning nodes in the arena is the set of nodes that leak S i . Player u j can take decisions only from its state estimation, and wins the game if it can reach a node in the winning set. This game is hence a partial information reachability game. Usually, solving such games requires computing an exponentially larger arena containing players beliefs, and then apply polynomial procedures for a perfect information reachability game. Here, as nodes already contain beliefs, there is no exponential blowup, and checking active opacity is hence in EXPTIME.

For the hardness part, we use a reduction from the problem of language emptiness for alternating automata to an active opacity problem. (see appendix for details)

Moving from opacity to active opacity changes the complexity class from P SP ACE-complete to EXP T IM E-complete. This is due to the game-like nature of active opacity. However, using observation capacities does not influence complexity: even if an agent u j has no capacity, the arena built to verify opacity of S i w.r.t. u j is of exponential size, and the reduction from alternating automata used to prove hardness does not assume that observation capacities are used.

IV. OPACITY WITH THRESHOLD DISTANCES TO PROFILES

So far, we have considered passive opacity, i.e. whether a secret can be leaked during normal use of a system, and active opacity, i.e. whether an attacker can force secret leakage with an appropriate strategy and with the use of capacities. In this setting, the behavior of agents is not constrained by any security mechanism. This means that attackers can perform illegal actions with respect to their profile without being discovered, as long as they are feasible in the system.

We extend this setting to systems where agents behaviors are monitored by anomaly detection mechanisms, that can raise alarms when an user's behavior seems abnormal. Very often, abnormal behaviors are defined as difference between observed actions and a model of normality, that can be a discrete event model, a stochastic model,.... These models or profiles can be imposed a priori or learnt from former executions. This allows for the definition of profiled opacity, i.e. whether users that behave according to predetermined profile can learn a secret, and active profiled opacity, i.e. a setting where attackers can perform additional actions to refine their knowledge of the system's sate and force secret leakage in a finite amount of time without leaving their normal profile.

One can assume that the behavior of an honest user u j is a distributed system is predictable, and specified by his profile P j . The definitions of opacity (def. 2) and active opacity (def. 5) do not consider these profiles, i.e. agents are allowed to perform legally any action allowed by the system to obtain information. In our opinion, there is a need for a distinction between what is feasible in a system, and what is considered as normal. For instance, changing access rights of one of his file by an agent should always be legal, but changing access rights too many times within a few seconds should be considered as an anomaly. In what follows, we will assume that honest users behave according to their predetermined regular profile, and that deviating from this profile could be an active attempt to break the system's security. Yet, even if an user is honest, he might still have possibilities to obtain information about other user's secret. This situation is captured by the following definition of opacity wrt a profile. Definition 7:

A system S = (A, U ) is opaque w.r.t. profiles P 1 , . . . P n if ∀i = j, ∀w ∈ L(S i ) ∩ L(S), w ∈ L(P j ) ⇒ π -1 Σ j o (π Σ j o (w)) ∩ L(S) L(S i
) Intuitively, a system is opaque w.r.t profiles of its users if it does not leak information when users stay within their profiles. If this is not the case, i.e. when w ∈ L(P j ), then one can assume that an anomaly detection mechanism that compares users action with their profiles can raise an alarm. Definition 7 can be rewritten as ∀i = j, ∀w ∈ L(S i ) ∩ L(P j ) ∩ L(S), π -1

Σ j o (π Σ j o (w)) ∩ L(S)
L(S i ) Hence, P SP ACEcompleteness of opacity in Theorem 3 extends to opacity with profiles: it suffices to find witness runs in L(S)∩L(S i )∩L(P j ).

Corollary 8: Deciding whether a system S is opaque w.r.t. a set of profiles P 1 , . . . P n is PSPACE complete.

If a system is U-opaque, then it is opaque w.r.t its agents profiles. Using profiles does not change the nature nor complexity of opacity question. Indeed, opacity w.r.t. a profile mainly consists in considering regular behaviors in L(P j ) instead of L(A j ). In the rest of the paper, we will however use profiles to measure how much users deviate from their expected behavior and quantify opacity accordingly.

One can similarly define a notion of active opacity w.r.t. profiles, by imposing that choices performed by an attacker are actions that does not force him to leave his profile. This can again be encoded as a game. This slight adaptation of definition 5 does not change the complexity class of the opacity question (as it suffices to remember in each node of the arena a state of the profile of the attacker). Hence active opacity with profiles is still a partial information reachability game, and is also EXPTIME-complete. Passive opacity (profiled or not) holds iff certain inclusion properties are satisfied by the modeled system, and active opacity holds if an active attacker has no strategy to win a partial information reachability game. Now, providing an answer to these opacity questions returns a simple boolean information on information leakage. It is interesting to quantify the notions of profiled and active opacity for several reasons. First of all, profiles can be seen as approximations of standard behaviors: deviation w.r.t. a standard profile can be due to errors in the approximation, that should not penalize honest users. Second, leaving a profile should not always be considered as an alarming situation: if profiles are learned behaviors of users, one can expect that from time to time, with very low frequency, the observed behavior of a user differs from what was expected. An alarm should not be raised as soon as an unexpected event occurs. Hence, considering that users shall behave exactly as depicted in their profile is a too strict requirement. A sensible usage of profiles is rather to impose that users stay close to their prescribed profile. The first step to extend profiled and active opacity to a quantitative setting is hence to define what "close" means.

Definition 9: Let u, v be two words of Σ * . An edit operation applied to word u consists in inserting a letter a ∈ Σ in u at some position i, deleting a letter a from u at position i, or substituting a letter a for another letter b in u at position i.

Let OP s(Σ) denote the set of edit operations on Σ, and ω(.) be a cost function assigning a weight to each operation in OP s(Σ). The edit distance d(u, v) between u and v is the minimal sum of costs of operations needed to transform u in v. Several edit distances exist, the most known ones are

• the Hamming distance ham((u, v)), that assumes that OP s(Σ) contains only substitutions, and counts the number of substitutions needed to obtain u from v (u, v are supposed of equal lengths).

• the Levenshtein distance lev((u, v)) is defined as the distance obtained when ω(.) assigns a unit to every operation (insertion, substitution, deletion). One can notice that lev((u, v)) is equal to lev((v, u)), and that max(|u|, |v|) ≥ lev((u, v)) ≥ ||u| -|v||. For a particular distance d(.) among words, the distance between a word u ∈ Σ * and a language R ⊆ Σ * is denoted d(u, R) and is defined as

d(u, R) = min{d(u, v) | v ∈ R}.
We can now quantify opacity. An expected secure setting is that no secret is leaked when users have behaviors that are within or close enough from their expected profile. In other words, when the observed behavior of agents u 1 , . . . u k resemble the behavior of their profiles P 1 , . . . , P k , no leakage should occur. Resemblance of u i 's behavior in a run ρ labeled by w can be defined as the property d(w, L(P i ))) ≤ K for some chosen notion of distance d(.) and some threshold K fixed by the system designers. In what follows, we will use the Hamming and Levenshtein distances as a proximity measures w.r.t. profiles. However, we believe that this notion of opacity can be extended to many other distances. We are now ready to propose a quantified notion of opacity.

Definition 10 (threshold profiled opacity): A system S is opaque wrt profiles P 1 , . . . P n with tolerance K for a distance

d iff ∀i = j, ∀w ∈ L(S i ) ∩ L(S), d(w, L(P j )) ≤ K ⇒ π -1 Σ j o (π Σ j o (w)) ∩ L(S) L(S i
) Threshold profiled opacity is again a passive opacity. In some sense, it provides a measure of how much anomaly detection mechanisms comparing users behaviors with their profiles are able to detect passive leakage. Consider the following situation: the system S is opaque w.r.t. profiles P 1 , . . . P n with threshold K + 1 but not with threshold K. Then it means there exists a run of the system with K + 1 anomalies of some user u j w.r.t. profile P j , but no run with K anomalies. If anomaly detection mechanisms are set to forbid execution of runs with more than K anomalies, then the system remains opaque.

We can also extend the active opacity with thresholds. Let us denote by Strat K j the set of strategies that forbid actions leaving a profile P j if the behavior of the concerned user u j is already at distance K from P j (the distance can refer to any distance, e.g., Hamming or Levenshtein).

Definition 11 (active profiled Opacity): A system S is opaque w.r.t. profiles P 1 , . . . P n with tolerance K iff ∀i = j, µ j ∈ Strat K j such that it is unavoidable for u j to reach a correct state estimation X ⊆ F S i in all runs of Runs(S, µ j ). Informally, definition 10 says that a system is opaque if no attacker u j of the system have a strategy that leaks a secret S i and costs less than K units to reach this leakage. Again, we can propose a game version for this problem, where attacker u j is not only passive, but also has to play his best actions in order to learn u i 's secret.

A player u j can attack u i 's secret iff it has a strategy µ j to force a word w ∈ L(S i ) that conforms to µ j , such that d(w, L(P j )) ≤ K and π -1

Σ j o (π Σ j o (w)) ∩ L(S) ⊆ L(S i
). This can be seen as a partial information game between u j and the rest of the system, where the exact sate of each agent is partially known to others. The system wins if it can stay forever is states where u j 's estimates does not allow to know that the secret automaton S i is in one of its accepting states. The arena is built in such a way that u j stops playing differently from its profile as soon as it reaches penalty K. This is again a partial information rechability game and that is decidable on finite arenas [START_REF] Chatterjee | The complexity of partial-observation parity games[END_REF]. Fortunately, we can show (in lemma 12 below) that the information to add to nodes with respect to the games designed for active opacity (in theorem 6) is finite.

Lemma 12: For a given automaton G, one can compute an automaton G K that recognizes words at distance at most K of L(G), where the distance is either the Hamming or Levenshtein distance.

Proof: Let us first consider the Hamming distance. For an automaton

G R = (Q R , -→ R , q 0 R , F R ), we can design an automaton G K ham = (Q K , -→ K , q K 0 , F K )
that recognizes words at a distance at most K from the reference language L(G). We have

Q K = Q R × {0..K}, F K = Q × {0.
.K}, and q K 0 = (q 0 , 0). Last, we give the transition function: we have ((q, i), a, (q , i)) ∈-→ K iff (q, a, q ) ∈-→ R , and ((q, i), a, (q , i + 1)) ∈-→ K if (q, a, q ) ∈-→ R and i+1 ≤ K, and there exists b = a such that (q, b, q ) ∈-→ R . This way, G K ham recognizes sequences of letters that end on a state (q f , i) such that q f is an accepting state of G R , and i ≤ K. One can easily show that for any accepting path in G K ham ending on state (q f , i) recognizing word w, there exists a path in G R of identical length recognizing a word w that is at hamming distance at most K of w. Similarly, let us consider any accepting path

ρ = q 0 R a1 -→ R q 1 . . . an -→ R q f of G R . Then, every path of the form ρ k = (q 0 R , 0) . . . ai1 -→ K (q i1 , 1) . . . (q ik-1 , k -1) a ik -→ K (q ik , k) . . . an -→ K (q f ,
i) such that i ≤ K and for every

(q ij-1 , j -1) aij -→ K (q ij ,
j), a ij is not allowed in sate q ij is a path that recognizes a word at distance i of a word in R and is also a word of G K R . One can show by induction on the length of paths that the set of all paths recognizing words at distance at most k can be obtained by random insertion of at most k such letter changes in each path of G R . The size of

G K ham is exactly |G R | × K.
Let us now consider the Levenshtein distance. Similarly to the Hamming distance, we can compute an automaton G K Lev that recognizes words at distance at most K from L(G). Namely, G K Lev = (Q lev , -→ lev , q 0,Lev , F lev ) where Q lev = Q×{0..K}, q 0,lev = (q 0 , 0), F lev = F ×{0..K}. Last the transition relation is defined as ((q, i), a, (q , i)) ∈-→ lev if (q, a, q ) ∈-→, ((q, i), a, (q, i + 1)) ∈-→ lev if q , (q, a, q ) ∈-→ (this transition simulates insertion of letter a in a word), ((q, i), a, (q , i + 1)) ∈-→ lev if ∃(q, b, q ) ∈-→ with b = a (this transition simulates substitution of a character), ((q, i), , (q , i + 1)) ∈-→ lev if ∃(q, a, q ) ∈-→ (this last move simulates deletion of a character from a word in L(G).

One can notice that this automaton contains transition, but after and -closure, one obtains an automaton without epsilon that recognizes all words at distance at most K from L(G). The proof of correctness of the construction follows the same lines as for the Hamming distance, with the particularity that one can randomly insert transitions in paths, by playing letters that are not accepted from a state, leaving the system in the same state, and simply increasing the number of differences. Notice that if a word w is recognized by G K Lev with a path ending in a state (q, i) ∈ F Lev , this does not mean that the Levenshtein distance from L(G) is i, as w can be recognized by another path ending in a state (q , j) ∈ F Lev with j < i.

s 0 s 1 s 2 a b a, c a s 0 , 0 s 0 , 1 s 0 , 2 s 0 , 3 s 1 , 0 s 1 , 1 s 1 , 2 s 1 , 3 s 2 , 0 s 2 , 1 s 2 , 2 s
One can notice that the automata built in the proof of lemma 12 are of size in O(K.|G|), even after -closure. Figure 1 represents an automaton G that recognizes the prefix closure of a.a * .b.(a + c) * , and the automaton G 3

Ham . Theorem 13: Deciding threshold opacity for the Hamming and Levenshtein distance is PSPACE complete. Proof: First of all, one can remark that, for a distance d(.), a system S is not opaque if there exists a pair of users u i , u j and a word w in L(S) ∩ L(S i ) such that d(w, L(P j )) ≤ K, and π -1

Σ j o (π Σ j o (w)) ∩ L(S) ⊆ L(S i ).
As already explained in the proof of theorem 3, w belongs to L(S i ) if a state q w reached by S i after reading w belongs to F S i . Still referring to the proof of Theorem 3, one can maintain online when reading letters of w the set reach j (w) of possible configurations and states of S i that are reached by a run which observation is the same as π Σ j o (w). One can also notice that lev(w, L(P j )) ≤ K iff w recognized by P K j,lev , the automaton that accepts words at Levenshtein distance at most K from a word in P j . Again, checking online whether w is recognized by P K j,Lev consists in maintaining a set of states that can be reached by P K j,Lev when reading w. We can denote by reach K j,Lev (w) this set of states. When no letter is read yet, reach K j,Lev ( ) = {q K 0 }, and if lev(w, L(P j )) > K, we have reach K j,Lev (w) = ∅, meaning that the sequence of actions played by user u j have left the profile. We can maintain similarly a set of states reach K j,Ham (w) for the Hamming distance. In what follows, we will simply use reach K j (w) to denote a state estimation using Levenstein of Hamming distance.

Hence, non-opacity can be rephrased as existence of a run, labeled by a word w such that reach j (w) ⊆ F S i and reach K j (w) = ∅. The contents of reach j (w) and reach K j (w) after reading a word w can be recalled with a vector of

h = |S| + |P K j | bits.
Following the same arguments as in Theorem 3, it is also useless to consider runs of size greater than 2 h . One can hence non-deterministically explore the whole set of states reached by reach j (w) and reach K j (w) during any run of S by remembering h bits and a counter which value is smaller of equal to 2 h , and can hence be encoded with at most h bits. So, finding a witness for non-opacity is in NP-SPACE, and by Savitch's theorem and closure by complementation of PSPACE, opacity with a threshold K is in PSPACE.

For the hardness part, it suffices to remark that profiled opacity is exactly threshold profiled opacity with K = 0.

Theorem 14: Deciding active profiled opacity for the Hamming and Levenshtein distance is EXPTIME-complete. Proof:[sketch] Let us first consider the Hamming distance. One can build an arena for a pair of agents u i , u j as for the proof of theorem 6. This arena is made of nodes of the form (b, C, s, spjk, ES, d) that contain: a bit b indicating if it is u j turn to play and choose the next move, C the current configuration of S , s the current state of S i , the estimation of ES of possible pairs (C, s) of current configuration and current state of the secret by player u j , and spjk a set of states of the automaton P K j,ham that recognizes words that are at Hamming distance at most K from P j . In addition to this information, a node contains the distance d of currently played sequence w.r.t. profile P j . This distance can be easily computed: if all states of P K j,ham memorized in spjk are pairs of state and distance, i.e., spkj = {(q 1 , i 1 ), (q 2 , i 2 ), . . . , (q k , i k )} then d = min{i 1 , . . . , i k }. User u j (the attacker) has partial knowledge of the current state of the system (i.e. a configuration of S and of the state of S i ), perfect knowledge of d. User j wins if it can reach a node in which his estimation of the current state of secret S i is contained in F S i (a non-ambiguous and secret node), without exceeding threshold K. The rest of the system wins if it can prevent player u j to reach a non-ambiguous and secret node of the arena. We distinguish a particular node ⊥ reached as soon as the distance w.r.t. profile P j is greater than K. We consider this node as ambiguous, and every action from it gets back to ⊥. Hence, after reaching ⊥, player u j has no chance to learn S i anymore. The moves from a node to another are the same as in the proof for theorem 6, with additional moves from any node of the form n = (1, q, s, spjk, ES, d) to ⊥ using action a is the cost of using a from n exceeds K.

We add an equivalence relation ∼, such that n = (b, q, s, spjk, ES, d) ∼ n = (b , q , s , spjk , ES , d ) iff b = b , spjk = spjk , d = d , and ES = ES . Obviously, u j has a strategy to violate u i 's secret without exceeding distance K w.r.t. its profile P j iff there is a strategy to reach W in = {(b, q, s, spjk, ES, d) | ES ⊆ S F i } for player u j with partial information that does not differentiate states in the equivalence classes of ∼. This is a partial information reachability game over an arena of size in O(2.|Conf (S)|.|S i |.2 |Conf (S)|.|Si|.K.|Pj | ), that is exponential in the size of S and of the secret S i and profile P j . This setting is a partial information reachability game over an arena of exponential size. As in the Boolean setting, the nodes of the arena already contain a representation of the beliefs that are usually computed to solve such games, and hence transforming this partial information reachability game into a perfect information game does not yield an exponential blowup. Hence, solving this reachability game is in EXPTIME.

The hardness part is straightforward: the emptiness problem for alternating automaton used for the proof of theorem 6 can be recast in a profiled and quantified setting by setting each profile P i to an automaton that recognizes (Σ Γ i ) * (i.e., users have the right to do anything they want as far as they always remain at distance 0 from their profile).

V. DISCOUNTING ANOMALIES

Threshold opacity is a first step to improve the standard Boolean setting. However, this form of opacity supposes that anomaly detection mechanisms memorize all suspicious moves of users and never revises their opinion that a move was unusual. This approach can be too restrictive. In what follows, we propose several solutions to discount anomalies. We first start by counting the number of substitutions in a bounded suffix with respect to the profile of an attacker. A suspicion score is computed depending on the number of differences within the suffix. This suspicion score increases if the number of errors in the considered suffix is above a maximal threshold, and it is decreased as soon as this number of differences falls below a minimal threshold. As in former sections, this allows for the definition of passive and active notions of opacity, that are respectively PSPACE-complete and EXPTIME-complete. We then consider the mean number of discrepancies w.r.t. the profile as a discounted Hamming distance.

A. A Regular discounted suspicion measure

Let u ∈ Σ K .Σ * and let v ∈ Σ * . We denote by d K (u, v) the distance between the last K letters of word u and any suffix of v, i.e.

d K (u, v) = min{d(u [|u|-K,|u|] , v ) | v is a suffix of v}. Given a regular language R we define d K (u, R) = min{d K (u, v) | v ∈ R}
Lemma 15: Let R be a regular language. For a fixed K ∈ N, and for every k ∈ [0..K], one can compute an automaton C k that recognizes words which suffixes of length K are at Hamming distance k from a suffix of a word of R.

We now define a cost model, that penalizes users that get too far from their profile, and decreases this penalty when getting back closer to a normal behavior. For a profile P j and fixed values α, β ≤ K we define a suspicion function Ω j for words in Σ * inductively:

Ω j (w) = 0 if |w| ≤ K Ω j (a.w.b) = Ω j (a.w) + 1 if d K (w.b, P j ) ≥ β max(Ω j (a.w) -1, 0) if d K (w.b, P j ) ≤ α
As an example, let us take as profile P j the automaton G of One can easily define a notion of passive opacity with respect to a suspicion threshold T . Again, verifying this property supposes finding a witness run of the system that leaks information without exceeding suspicion threshold, which can be done in PSPACE (assuming that T is smaller than 2 |Conf | ). As for profiled opacity, we can define Strat T the set of strategies of an user that never exceed suspicion level T . This immediately gives us the following definitions and results.

Definition 16: Let K ∈ N be a suffix size, α, β ≤ K and T ∈ N be a suspicion threshold. S is opaque with suspicion threshold

T iff ∀i = j, ∀w ∈ L(S i ) ∩ L(S), Ω j (w) < T implies π -1 Σ j o (π Σ j o (w)) ∩ L(S) L(S i ) .
Theorem 17: Opacity with suspicion threshold for the Hamming distance is PSPACE-complete.

Definition 18: Let K ∈ N be a suffix size, α, β ≤ K and T ∈ N. S is actively opaque with suspicion threshold T iff ∀i = j there exists no strategy µ j ∈ Start T such that it is unavoidable for u j to reach a correct state estimation X ⊆ F S i in all runs of Runs(S, µ j ).

Theorem 19: Active opacity with suspicion threshold for the Hamming distance is EXPTIME-complete. Proof: We build an arena that contains nodes of the form n = (b, C, ES, EC 0 , . . . EC k , sus). C is the actual current configuration of S Γ , ES is the set of pairs (C, s) of configuration and secret sates in which S Γ could be according to the actions observed by u j and according to the belief refinements actions performed by u j . Sets EC 1 . . . EC k remembers sets of states of cost automata C 0 , . . . C K . Each EC i memorizes the states in which C i could be after reading the current word. If EC i contains a final state, then the K last letters of the sequence of actions executed so far contain exactly i differences. Note that only one of these sets can contain an accepting state. Suspicion sus is a suspicion score between 0 and T . When reading a new letter, denoting by p the number of discrepancies of the K last letters wrt profiles, one can update the suspicion score using the definition of C j above, depending on whether

p ∈ [0, α], p ∈ [α, β] or p ∈ [β, K].
The winning condition in this game is the set

W in = {(b, C, ES, EC 0 , . . . EC k , sus) | ES ⊆ Conf (S) × F S i }. We partition the set of nodes into V 0 = {(b, C, ES, EC 0 , . . . EC k , sus) | b = 0} and V 1 = {(b, C, ES, EC 0 , . . . EC k , sus) | b = 1}
. We de-fine moves from (b, C, ES, EC 0 , . . . EC k , sus) to (1b, C, ES, EC 0 , . . . EC k , sus) symbolizing the fact that it is user u j 's turn to perform an action. There is a move from n = (b, C, ES, EC 0 , . . . EC k , sus) to n = (b , C , ES, EC 0 , . . . EC k , sus ) if there is a transition (C, a, C ) in S Γ performed by an user u i = u j , and a is not observable by u j . There is a move from n = (b, C, ES, EC 0 , . . . EC k , sus) to n = (b , C , ES , EC 0 , . . . EC k , sus) if there is a transition (C, a, C ) in S Γ performed by an user u i = u j and a is observable by u j . We have ES = ∆ Σ j o (ES, S Γ , a). Suspicion and discrepancies observation (sets EC i ) remain unchanged as this move does not represent an action played by u j .

There is a move from n = (b, C, ES, EC 0 , . . . EC k , sus)

to n = (1 -b, C , ES , EC 0 , . . . EC k , sus) if b = 1
and there is a transition (q, a, q ) in S Γ performed by user u j from the current configuration. Set ES is updated as before ES = ∆ Σ j o (ES, S Γ , a) and sets EC i are updated according to transition relation δ suf i of automaton C i , i.e. EC i = δ suf i (E i , a). Similarly, sus is the new suspicion value obtained after reading a. Last, there is a move from n = (b, C, ES, EC 0 , . . . EC k , sus) to n = (b, C, ES , EC 0 , . . . EC k , sus), if there is a sequence of moves (C, a, C(a γ )).(C(a γ ), a γ(q) , C) in S Γ , ES = ES /a γ(q) , and EC i 's and sus are computed as in the former case.

As for the proofs of theorems 6 and 14, opacity can be brought back to a reachability game of partial information, and no exponential blowup occurs to solve it. For the hardness, there is a reduction from active profiled opacity. Indeed, active profiled opacity can be expressed as a suspicion threshold opacity, by setting α = β = K = 0, to disallow attackers to leave their profile.

B. Discounted Opacity : an open problem

A frequent interpretation of discounting is that weights or penalties attached to a decision should decrease progressively over time, or according to the length of runs. This is captured by averaging contribution of individual moves.

Definition 20: The discounted Hamming distance between a word u and a language R is the value d(u, R) = ham(u,R) |u| This distance measures the average number of substitutions in a word u with respect to the closest word in R. The next quantitative definition considers a system as opaque if an active attacker can not obtain a secret while maintaining a mean number of differences w.r.t. its expected behavior below a certain threshold. Let λ ∈ Q be a positive rational value. We denote by Strat λ (R) the set of strategies that does not allow an action a after a run ρ labeled by a sequence of actions w if d(w.a, R) > λ.

Definition 21 (Discounted active Opacity): A system S is opaque wrt profiles P 1 , . . . P n with discounted tolerance λ iff ∀i = j, µ j ∈ Strat λ (P j ), strategy of agent u j such that it is unavoidable for u j to reach a correct state estimation X ⊆ F i S in all runs of Runs(S, µ j ).

A system is opaque in a discounted active setting iff one can find a strategy for u j to reach a state estimation that reveals the secret S i while maintaining a discounted distance wrt P j smaller than λ. At first sight, this setting resembles discounted games with partial information, already considered in [START_REF] Zwick | The complexity of mean payoff games[END_REF]. It was shown that finding optimal strategies for such mean payoff games is in N P ∩ co-N P . The general setting for mean payoff games is that average costs are values of nodes in an arena, i.e. the minimal average reward along infinite runs that one can achieve with a strategy starting from that node. As a consequence, values of nodes are mainly values on connected components of an arena, and costs of moves leading from a component to another have no impact. In out setting, the game is not a value minimization over infinite run, but rather a co-reachability game, in which at any moment in a run, one shall not exceed a mean number of unexpected moves.

For a fixed pair of users u i , u j , we can design an arena with nodes of the usual form n = (b, C, ES, l, su) in which b indicates whether it is u j 's turn to play, C is the current configuration of the system, ES the estimation of the current configuration and of the current state of secret S i reached, l is the number of moves played so far, and su the number of moves that differ from what was expected in P j . As before, the winning states for u j are the states where all couples in state estimation refer to an accepting state of S i . In this arena, player u j looses if it can never reach a winning node, or if it plays an illegal move from a node n = (b, C, ES, l, su) such that su+1 l+1 > λ. One can immediately notice that defined this way, our arena is not finite anymore.

Consider the arena used in theorem 6, i.e. composed of nodes of the form n = (b, C, ES) that only build estimations of the attacker. Obviously, when ignoring mean number of discrepancies, one can decide whether the winning set of nodes is reachable from the initial node under some strategy in polynomial time (wrt the size of the arena). The decision algorithm builds an attractor for the winning set (see for instance [START_REF] Grädel | Automata Logics, and Infinite Games : A Guide to Current Research[END_REF] for details), but can also be used to find short paths under an adequate strategy to reach W in (without considering mean number of discrepancies). If one of these paths keeps the mean number of discrepancies lower or equal to λ at each step, then obviously, this is a witness for non-opacity. However, if no such path exists, there might still be a way to play longer runs that decrease the mean number of discrepancies before moving to a position that requires less steps to reach the winning set.

We can show an additional sufficient condition : Let ρ = n 0 .n 1 . . . n w be a path of the arena in theorem 6 (without length nor mean number of discrepancies recall) from n 0 to a winning node n w . Let d i denote the number of discrepancies with respect to profile P j at step i. Let n i be a node of ρ such that di i ≤ λ and di+1 i+1 > λ. We say that u j can enforce a decreasing loop β = n j .n j+1 . . . n j at node n j if β is a cycle that u j can enforce with an appropriate strategy, and if the mean number of discrepancies is smaller in ρ β = n 0 . . . n j .β than in n 0 . . . n j , and the mean cost of any prefix of β is smaller that λ. A consequence is that the mean cost M β of cycle β is smaller than λ. We then have a sufficient condition:

Proposition 22: Let ρ be a winning path in an arena built to check active opacity for users u i , u j such that di i > λ for some i ≤ |ρ|. If there exists a node n b in ρ such that d k k ≤ λ for every k ≤ b and u j can enforce a decreasing loop at n b , then u j has a strategy to learn S i without exceeding mean number of discrepancies λ. Similarly, if B is large enough, playing any prefix of n b+1 . . . n w to reach the winning set does not increase enough the mean number of discrepancies to exceed λ. A lower bound for B such that λ is never exceeded in n 0 . . . n b .β B .n b+1 . . . n w can be easily computed. Hence, if one can find a path in a simple arena withouts mean discrepancy counts, and a decreasing loop in this path, then u j has a strategy to learn S i without exceeding threshold λ.

VI. CONCLUSION

We have shown several ways to quantify opacity with passive and active attackers. In all cases, checking passive opacity can be brought back to a language inclusion question, and is hence PSPACE-complete. In active settings, opacity violation is brought back to existence of strategies in reachability games over arenas which nodes represent beliefs of agents, and is EXPTIME-complete.

Suspicion can be discounted or not. Non-discounted suspicions simply counts the number of anomalies w.r.t. a profile, and raises an alarm when a maximal number K of anomalies is exceeded. We have shown that when anomalies are substitutions, deletions and insertions of actions, words with less than K anomalies w.r.t. the considered profile (words at Hamming or Levenshtein distance ≤ K) are recognized by automata of linear size. This allows to define active and passive profiled opacity, with the same PSPACE/EXPTIME-complete complexities. A crux in the proofs is that words at distance lower than K of a profile are recognized by automata. A natural extension of this work is to see how regular characterization generalizes to other distances.

Discounting the number of anomalies is a key issue to avoid constantly raising false alarms. t is reasonable to consider that the contribution to suspicion raised by each anomaly should decrease over time. The first solution proposed in this paper computes a suspicion score depending on the number of discrepancies found during the last actions of an agent. When differences are only substitutions, one can use finite automata to maintain online the number of differences. This allows to enhance the arenas used in the active profiled setting without changing the complexity class of the problem (checking regular discounted suspicion remains EXPTIME-complete). Again, we would like to see if other distances (eg the Levenstein distance) and suspicion scores can be regular, which would allow for the defiition of new opacity measures.

Discounted suspicion weights discrepancies between the expected and actual behavior of an agent according to run length. This suspicion measure can be seen as a quantitative game, where the objective is to reach a state leaking information without exceeding an average distance of λ ∈ Q. In our setting, the mean payoff has to be compared to a threshold at every step. This constraint can be recast as a reachability property for timed automata with one stopwatch and linear diagonal constraints on clock values. We do not know yet if this question is decidable but we provide a sufficient condition for discounted opacity violation.

In the models we proposed, discounting is performed according to runs length. However, it seems natural to consider discrepancies that have occurred during the last ∆ seconds, rather than This requires in particular considering timed systems and they timed runs. It is not sure that adding timing to our setting preserves decidability, as opacity definitions rely a lot on languages inclusion, which are usually undecidable for timed automata [START_REF] Alur | A theory of timed automata[END_REF]. If time is only used to measure durations elapsed between actions of an attacker, then we might be able to recast the quantitative opacity questions in a decidable timed setting, using decidability results for timed automata with one clock [START_REF] Ouaknine | On the language inclusion problem for timed automata: Closing a decidability gap[END_REF] or event-clock timed automata.

APPENDIX PROOF OF THEOREM 3

Proof: Let us first prove that U -opacity is in PSPACE. A system is not opaque if one can find a pair of users u i , u j , and a run w of S such that w ∈ L(S i ) and π -1

Σ j o (π Σ j o (w)) ∩ L(S) ⊆ L(S i ).
One can non-deterministically choose a pair of users u i , u j in space logarithmic in n, and check that i = j in logarithmic space. To decide whether a run of S belongs to S i , it is sufficient to know the set of states reached by S i after recognizing w. A word w belongs to L(S i ) is the state q w reached by S i after reading w belongs to F S i . Now, observe that an user u j does not have access to w, but can only observe π Σ j o (w), and may hence believe that the run actually played is any run with identical observation, i.e. any run of π -1

Σ j o (π Σ j o (w)) ∩ L(S).
Let ρ be a run of S, one can build online the set of states reach j (w) that are reached by a run which observation is the same as π Σ j o (w). We have

reach j ( ) = {q ∈ Q S i | ∃w, q S 0,i w -→ q ∧ π Σ j o (w) = } and reach j (w.a) = {q ∈ Q S i | ∃q ∈ reach j (w), ∃w , q w -→ q ∧ π Σ j o (w ) = a}.
Obviously, a word w witnesses a secret leakage from S i to u j if reach j (w) ⊆ F S i . To play a run of S, it is hence sufficient to remember a configuration of S and a subset of states of S i . Let q ρ denote the pair (q, X) reached after playing run ρ.

Now we can show that witness runs with at most K 1 = |Conf |.2 |Si| letters observable by u j suffice. Let us assume that there exists a witness ρ of size ≥ K 1 . Then, ρ can be partitioned into ρ = ρ 1 .ρ 2 .ρ 3 such that q ρ1 = q ρ1.ρ2 . Hence, ρ 1 .ρ 3 is also a run that witness a leakage of secret S i to u j , but of smaller size.

Hence one can find a witness of secret leakage by a nondeterministic exploration of size at most |Conf |.2 |Si| . To find such run, one only needs to remember a configuration of S (which can be done with log(|S|) bits, all states of reach j (ρ) for the current run ρ followed in S, which can be done with |S i | bits of information, and an integer of size at most K 1 , which requires log |S|.|S i | bits. Finding a witness can hence be done in NPSPACE, and by Savitch's lemma it is in PSPACE. As PSPACE is closed by complement, deciding opacity of a system is in PSPACE.

Let us now consider the hardness part. We will reduce the non-universality of any regular language to an opacity problem. As universality is in PSPACE, non-universality is also in PSPACE. The language of an automaton B defined over an alphabet Σ is not universal iff L(B) = Σ * , or equivalently if Σ * L(B). For any automaton B, one can design a system S B with two users u 1 , u 2 such that S 1 = B, L(S 2 ) = a.Σ * for some letter a, A accepts all actions, i.e. is such that L

(A) = Σ * , Σ 2 o = Σ 1 o = ∅.
Clearly, for every run of S, u 1 observes , and hence leakage can not occur from u 2 to u 1 (one cannot know whether a letter and in particular a was played). So the considered system is opaque iff ∀w ∈ L(S 1 ) ∩ L(S), π -1

Σ 2 o (π Σ 2 o (w)) L(S 1
). However, as Σ 2 o = ∅, for every w, π -1

Σ 2 o (π Σ 2 o (w)) = Σ * .
That is, the system is opaque iff Σ * L(B).

PROOF OF THEOREM 6

Proof: An active attacker u j can claim that the system is executing a run ρ that is secret for u i iff it can claim with certainty that ρ is recognized by S i . This can be achieved by maintaining an estimation of the system's current configuration, together with an estimation of S i 's possible states. We build an arena with nodes N 0 ∪ N 1 . Each node of the form n = (b, C, s, ES) contains :

• a player's name b (0 or 1). Intuitively, 0 nodes are nodes where all agents but u j can play, and 1 nodes are nodes where only agent u j plays.

G ⊆ N 0 ∪ N 1 × N 0 ∪ N 1 . • (n, n ) ∈ δ G if n and n differ only w.r.t. their player's name • (n, n ) ∈ δ G if n = (0, C, s, ES) , n = (1, C , s , ES )
and there exists σ

∈ (Σ \ Σ j ) ∩ Σ j o such that C σ =⇒ C , s σ =⇒ S i
) -→ S i . • (n, n ) ∈ δ G n = (1, C, s, ES), n = (1, C, s, ES ) if
there exists γ ∈ Σ Γ j such that ES is the refinement of ES by a γ (state(C)). We assume that checking the status of a proposition does not affect the secrets of other users. We says that a node n = (b, C, s, ES) is not secret if s ∈ F S i , and say that n is secret otherwise. We say that a node is ambiguous if there exists (C p , s p ) and (C m , s m ) in ES such that s p is secret and s m is not. If the restriction of ES to it second components is contained in F S i , we says that n leaks secret S i .

We equip the arena with an equivalence relation ∼⊆

N 0 × N 0 ∪ N 1 × N 1 , such that n = (b, C, s, ES) ∼ n = (b , C , s , ES ) iff b = b = 1 and ES = ES .
Intuitively, n ≡ n if and only if they are nodes of agent u j , and u j cannot distinguish n from n using the knowledge it has on executions leading to n and to n .

Clearly, secret S i is not opaque to agent u j in S iff there exists a strategy to make a leaking node accessible. This can be encoded as a partial information reachability game G = (N 0 N 1 , δ G , ≡, W in), where W in is the set of all leaking nodes. In these games, the strategy must be the same for every node in the same class of ≡ (i.e. where u j has the same state estimation). Usually, partial information games are solved at he cost of an exponential blowup, but we can show that in our case, complexity is better. First, let us compute the maximal size of the arena. A node is of the form n = (b, C, s, ES), hence the size of the arena |G| is in O(2.|Conf |.| § i |.2 |Conf |.|Si| ) (and it can be built in time O(|Conf |.|G|). Partial information reachability games are known to be EXPTIME-complete [START_REF] Reif | Universal games of incomplete information[END_REF]. Note here that only one player is blind, but this does not change the overall complexity, as recalled by [START_REF] Chatterjee | The complexity of partial-observation parity games[END_REF]. However, solving games of partial information consists in computing a "belief" arena G B that explicitly represent players beliefs (a partial information on a state is transformed into a full knowledge of a belief), and then solve the complete information game on arena G B . This usually yields an exponential blowup. In our case, this blowup is not needed, and the belief that would be computed to solve a partial information game simply duplicates the state estimation that already appears in the partial information arena. Hence, deciding opacity with active observation strategies can be done with |U | 2 opacity tests (one for each pair of users) of exponential complexity, in only in EXPTIME.

Let us now prove the hardness of opacity with active attackers. We reduce the problem of emptiness of alternating automata to an opacity question. An alternating automaton is a tuple

A alt = (Q, Σ, δ, s 0 , F ) where Q contains two distinct subsets of states Q ∀ , Q ∃ . Q ∀ is a set of universal states, Q ∃ is a set of existential states, Σ is an alphabet, δ ⊆ (Q ∀ ∪Q ∃ )×Σ×(Q ∀ ∪Q ∃
) is a transition relation, s is the initial state and F is a set of accepting states. A run of A alt over a word w ∈ Σ * is an acyclic graph G A alt ,w = (N, -→) where nodes in N are elements of Q × {1 . . . |w|}. Edges in the graph connect nodes from a level i to a level i+1. The root of the graph is (s, 1). Every node of the from (q, i) such that q ∈ Q ∃ has a single successor (q , i+1) such that q ∈ δ(q, w i ) where w i is the i th letter of w. For every node of the from (q, i) such that q ∈ Q ∀ , and for every q such that q ∈ δ(q, w i ), ((q, i), (q , i + 1)) is an edge. A run is complete is all its node with index in 1..|w| -1 have a successor. It is accepting if all path of the graph end in a node in F × {|w|}. Notice that due to non-deterministic choice of a successor for existential states, there can be several runs of A alt for a word w. The emptiness problem asks whether there exists a word w ∈ Σ * that has an accepting run. We will consider, without loss of generality that alternating automata are complete, i.e. all letters are accepted from any state. If there is no transition of the form (q, a, q ) from a sate q, one can nevertheless create a transition to an non-accepting absorbing state while preserving the language recognized by the alternating automaton.

Let us now show that the emptiness problem for alternating automata can be recast in an active opacity question. We will design three automata A, A 1 , A 2 . The automata A 1 and A 2 are agents. Agent 1 performs actions from universal sates and agent 2 chooses the next letter to recognize and performs actions from existential states. The automaton A serves as a communication medium between agents, indicates to A 2 the next letter to recognize, and synchronizes agents 1 and 2 when switching the current state of the alternating automaton from an existential state to an universal state or conversely.

We define A

= (Q s , -→ s , Σ s ) with Σ s = {(end, 2 A); (end, A 1)} ∪ Σ × {2 A, A 1} × (Q ∃ ∪ U ) × {1 A, A 2, 2 A, A 2}.
To help readers, the general shape of automaton A is given in Figure 3.

States of A are of the form U , (U, σ), W , dU , dq i , wq i for every state in Q, and Eq i for every existential state q i ∈ Q ∃ . The initial state of A is state U if s 0 is an universal state, or s 0 if s 0 is existential. State U has |Σ| outgoing transitions of the form (U, < σ, 2 A >, (U, σ), indicating that the next letter to recognize is σ. It also has a transition of the form (U, < end, 2 A >, end 1 ) indicating that A 2 has decided to test whether A 1 is in a secret state (i.e. simulates an accepting state of A alt ). There is a single transition (end 1 , < end, A 2 >, end 2 ) from state end 1 , and a single transition (end 2 , < Ackend, A 1 >, end 3 ) indicating to A 2 that A 1 has acknowledged end of word recognition.

There is a transition ((U, σ), < σ, A → 1 >, (W, σ)) for any state (U, σ), indicating to A 1 that the next letter to recognize from its current universal state is σ. In state W , A is waiting for an universal move from A 1 . Then from W , A can receive the information that A 1 has moved to an universal state, which is symbolized by a pair of transitions (W, < σ, U, 1 A >, dU )) and (dU, < again, A 2 >, U ).

There is a transition (W, < σ, q i , 1 → A >, dq i ) for every existential state q i ∈ Q ∃ , followed by a transition (dq i , < σ, q i , A 2 >, Eq i ), indicating to A 2 that the system has moved to recognition of a letter from an existential state q i .

There is a transition (Eq i , < σ, 2 A >, (Eq i , σ)) from every state Eq i with q i ∈ Q ∃ and every σ ∈ Σ to indicate that the next letter to recognize is σ. Then, there is a transition ((Eq i , σ), < σ, q j , 2 A >, (W q j , σ)) for every existential move (q i , σ, q j ) ∈ δ. From every state (W q j , σ), there is a transition of the form ((W q j , σ), < σ, q j , A → 1 >, (dq j , σ)) to inform A 1 of A 2 's move. Then, from (Dq j , σ) if q j ∈ Q ∃ , there is a transition of the form ((Dq j , σ), < again, A 1 >, Eq j ) and if q j ∈ Q ∀ , a transition of the form ((dq j , σ), < again, A 1 >, U ), indicating to A 1 that the simulation of the current transition recognizing a letter is complete, and from which state the rest of the simulation will resume.

Let us now detail the construction of A 2 . A description of all its transition is given in Figure 4. This automaton has one universal state U , a state W , states of the form (U, σ), a pair of states Eq i and W q i and a state (Eq i , σ) for every σ ∈ Σ and every q i ∈ Q ∃ . Last, A 1 has two states End 1 and End 2 .

There is a transition (U, < σ, 2 A >, (U, σ)) from U for every σ ∈ Σ, symbolizing the choice of letter σ as the next letter to recognize when the system simulates an universal state. Note that A 2 needs not know which universal state is currently simulated. Then, there is also a transition ((U, σ), again, U ) returning to U symbolizing the end of a transition of the alternating w q j again σ, A 1, q j d qi d q i σ, 1 A, q i σ, 1 A, q i E qi E qi , σ σ, A 2, q i σ, 2 A W qj , σ σ, q j , 2 A (q j ∈ Q ∃ ) σ, q j , 2 A (q j ∈ Q ∀ )

d qj σ, q j , A 1
E qj End, 2 A
End, 2 A again Fig. 3: Automaton A in the proof of theorem 6.

automata that returns to an universal state (hence owned by A 2 ). From every state (U, σ) there is a transition ((U, σ), again, U ) and a transition ((U, σ), < σ, q i , A → 2 >, Eq i ) for every existential state q i that has an universal predecessor q with (q, σ, q i ) ∈ δ. From a state Eq i and for every σ ∈ Σ, there is a transition (Eq i , < σ, 2 A >, (Eq i , σ)) symbolizing the choice to recognize σ as the next letter. Then, from every state (Eq i , σ) for every transition of the form (q i , σ, q j ) ∈ δ where q j is existential, there is a transition ((Eq i , σ), < σ, q j , 2 → A >, W q j ).

For every transition of the form (q i , σ, q j ) ∈ δ where q j is universal, there is a transition ((Eq i , σ), < σ, q j , 2 → A >, W ). Last, transitions ((W q j , σ), again, Eq j ) and (W, again, U ) complete simulation of recognition of the current letter. Last, A 2 has a transition (U, < end, 2 A >, End 1 ), a transition (Eq i , < end, 2 A >, End 1 ) for every existential state q i ∈ Q ∃ and a transition (end 1 , ackend, End 2 ), symbolizing the decision to end recognition of a word.

Let us detail the construction of A 1 . The general shape of this automaton is described in Figure 5. This automaton has two states of the form U q i , (U q i , σ) per universal state and for each σ ∈ Σ. Similarly A 1 has a state Eq i , (Eq i , σ) per existential state and for each σ ∈ Σ. From state U q i there is a transition (U q i , < σ, A → 1 >, (U q i , σ)) to acknowledge the decision to recognize σ.

From state (U q i , σ) there exists two types of transitions. For every universal state q j such that (q i , σ, q j ) ∈ δ, Eq i , σ σ, 2 A σ, 2 A σ, q j , 2 A (q j ∈ Q ∀ ) Eq j End, 2 A End, 2 A W q j again σ, q j , 2 A (q j ∈ Q ∃ ) Fig. 4: Automaton A 2 in the proof of theorem 6, simulating existential moves .

there is a transition ((U q i , σ), < σ, U, 1 A >, U q j ), symbolizing a move to universal state q j . For every existential state q j such that (q i , σ, q j ) ∈ δ, there is a transition ((U q i , σ), < σ, q j , 1 A >, Eq j ).

Similarly, from a state Eq i , there exists a transition (Eq i , < σ, A 1 >, (Eq i , σ)) indicating to A 1 the letter chosen by A 2 . From state (Eq i , σ), there is a transition ((Eq i , σ), < σ, q j , A → 1 >, Eq j ) for every existential state q j such that (q i , σ, q j ) ∈ δ. There is also a transition ((Eq i , σ), < σ, U, 1 A >, U q j ) for every universal state q j such that (q i , σ, q j ) ∈ δ. Notice that the universal state reached is not detailed when A 1 sends the confirmation of a move to A.

The remaining transitions are transitions of the form (Eq i , < End, A 1 >, S) and (U q i , < End, A 1 >, Sec) for every accepting state q i ∈ F . We also create transitions of the form Eq i , < End, A 1 >, Sec and U q i , < End, A 1 >, Sec for states that are not accepting. Reaching Sec indicates the failure to recognize a word chosen by A 1 along a path in which universal moves were played by A 1 and existential moves by A 2 .

We define a agent u 1 s secret S 1 as the automaton that recognizes all words that allow A 1 to reach sate Sec. Now, we can prove that if a word w is accepted by A alt then the strategy in which A 2 chooses letter w i at its i t h passage through a letter choice state (U or Eq i ), existential transitions appearing in the accepting run of A alt , and then transition < end, 2 A > at the i + 1 th choice, is a strategy to force U q i U q i , σ U q j Eq j σ, 1 A σ, U, 1 A σ, q j , 1 A Eq i Eq j σ, A 1, q j (q j ∈ Q ∃ ) Eq i U q j σ, A 1, q j (q j ∈ Q ∀ ) Eq i Sec End, A 1 (q i ∈ F ) Eq i Sec End, A 1 (q i ∈ F ) U q i Sec End, A 1 (q i ∈ F ) U q i Sec End, A 1 (q i ∈ F ) Fig. 5: Automaton A 1 in the proof of theorem 6, simulating Universal moves .

A 1 to reach the secret state. Conversely, one can associate to every run of A, A 1 , A 2 , a word w that is read, and a path in some run that is used to recognize w. If A 2 has a strategy to force A 1 secret leakage, then all path following this strategy lead to a winning configuration. As a consequence, there is a choice of existential moves such that all states simulated along a run of the alternating automaton with these existential moves end in accepting state. Hence, L(A alt ) is empty iff the system composed of A, A 1 , A 2 is opaque. Now, the system built to simulate A alt is of polynomial size in |A alt |, so there is a polynomial size reduction from the emptiness problem for alternating automata to the active opacity question, and active opacity is EXPTIME-complete. PROOF OF LEMMA 15 Proof: One can first recall that for the Hamming and Levenshtein distances, we have d(u, v) = d(u -1 , v -1 ), where u -1 is the mirror of u. Similarly, we have d K (u, R) = d(u -1

[1,K] , R -1 ). Let G R = (Σ, Q, q 0 , δ, F ) be the automaton recognizing language R. We can build an automaton C k that recognizes words of length at least K, which suffixes of length K are at hamming distance at most k of suffixes of length K of words in R. We define C k = (Σ, Q suf k , q suf 0,k , δ suf k , F suf k

). This automaton can be computed as follows : first build G -1 R , the automaton that recognizes mirrors of suffixes of R. This can be easily done by setting as initial states the final states of R, and then reversing the transition relation. Then by adding a K-bounded counter to states of G -1 R , and setting as accepting states states of the form (q, K), we obtain an automaton B -1 that recognizes mirrors of suffixes of R of length K. Then, for every k ∈ [0..K], we can compute B k , the automaton that recognizes mirrors of words of length K that are at distance k from words in B -1 , by adding another counter to states that counts substitutions, and which final states are of the form (q, K, k). Then we can build (by sequential composition of automata for instance) the automaton C k that reads any word in Σ * and then recognizes a word in (B k ) -1 .

Fig. 1 :

 1 Fig. 1: An automaton G and the automaton G 3 Ham that recognizes words at Hamming distance ≤ 3 of L(G).

Figure 1 .Fig. 2 :

 12 Fig. 2: Evolution of suspicion wrt profile of Figure 1 when reading word w = a.a.a.c.b.b.a.c.b.a.a. distance d K (w [i.i+5] , P j ) at each letter of w (plain line), and the evolution of the suspicion function (dashed line).One can easily define a notion of passive opacity with respect to a suspicion threshold T . Again, verifying this property supposes finding a witness run of the system that leaks information without exceeding suspicion threshold, which can be done in PSPACE (assuming that T is smaller than 2 |Conf | ). As for profiled opacity, we can define Strat T the set of strategies of an user that never exceed suspicion level T . This immediately gives us the following definitions and results.Definition 16: Let K ∈ N be a suffix size, α, β ≤ K and T ∈ N be a suspicion threshold. S is opaque with suspicion threshold T iff ∀i = j, ∀w ∈ L(S i ) ∩ L(S), Ω j (w) < T implies π -1

  Proof: The winning path is of the form ρ = n 0 .n 1 . . . n b .n b+1 . . . n w . Let d b be the number of discrepancies in n 0 .n 1 . . . n b and λ b = d b b . Player u j can choose any integer value B and enforce path ρ B = n 0 .n 1 . . . n b .β B . The mean number of discrepancies in ρ B is equal to d b +B.d β i+B.|β| , i.e. as B increases, this number tends towards M β .

  s and ES is th set of pairs (C m , s m ) such that there exits a pair (C p , s p ) in ES, and a sequence ρ of transitions from C p to C m , labeled by a word w such that Π j (w) = σ, and one can move in S i from s p to s m by reading w. Note that this set of sequences needs not be finite, but one can find in O(|Conf |) the set of possible pairs that are accessible while reading σ.• (n, n ) ∈ δ G if n = (1, C, s, ES), n = (1, C , s , ES ) and there exists σ ∈ Σ j , a transition C σ -→ C in S, a transition (s, σ, s ) ∈-→ S i and ES is the set of pairs of the form (C m , s m ) such that there exists (C m , s m ) ∈ ES (C m , σ, C m ) ∈-→ and (s m , σ, s m

  • the current configuration C of S • the current state s of S i • an estimation ES of the system's configuration and secret's current state by u j ,ES j = {(C 1 , s 1 ), ...(C k , s k )}=⇒ C iff there exists a sequence of transitions of S which observation by u j is σ, and s from s to s in S i . Then we define moves among nodes as a relation δ

	We write C
	σ =⇒	S i s if there is
	such a sequence

σ

This entails that we assume that queries are faster than the rest of the system, i.e. not event can occur between a query and its answer. Hence we have L(S Γ ) ⊆ L(S) (Σ Γ .{tt.ff }) * . We could easily get rid of this hypothesis, by remembering in states of S Γ which query (if any) was sent by an user, and returning the answer at any moment.