### 27 février 2017

**Serge Haddad**(LSV)

We consider opacity questions where an observation function provides

to an external attacker a view of the states along executions and

secret executions are those visiting some secret state from a fixed

subset. Disclosure occurs when the observer can deduce from a finite

observation that the execution is secret. In a probabilistic and non

deterministic setting, where an internal agent can choose between

actions, there are two points of view, depending on the status of

this agent: the successive choices can either help the attacker

trying to disclose the secret, if the system has been corrupted, or

they can prevent disclosure as much as possible if these choices are

part of the system design. In the former situation, corresponding to

a worst case, the disclosure value is the supremum over the

strategies of the probability to disclose the secret (maximisation),

whereas in the latter case, the disclosure is the infimum

(minimisation). We address quantitative problems (relation between

the optimal value and a threshold) and qualitative ones (when the

threshold is zero or one) related to both forms of disclosure for a

fixed or finite horizon. For all problems, we characterise their

decidability status and their complexity. Surprisingly, while in

maximisation problems optimal strategies may be chosen among

deterministic ones, it is not the case for minimisation problems,

but more minimisation problems than maximisation ones are decidable.