Fabien André

Guillaume Artignan
email: artignan@lirmm.fr

Maxime Cordeil
email: cordeil@cena.fr

Raphaël Hoarau

Dong-Bach Vo

Exploration et gestion des connaissances des ressources en IHM

Keywords: gestion des connaissances, réseau sémantique, association d'idées, capitalisation H.3 Information Storage and Retrieval: Search process Human Factors knowledge management, semantic network, mental association, capitalization

Nous présentons dans l'article le résultat d'un travail réalisé à l'école de Printemps 2010 de l'AFIHM. L'analyse des activités liées à la réalisation d'un état de l'art nous montre qu'une des tâches les plus compliquées est la familiarisation avec un nouveau domaine. Pour outiller cette activité, nous présentons des pistes de réflexion basées sur une analogie avec la mémoire humaine.

INTRODUCTION

La production de publications scientifiques suit une croissance exponentielle [START_REF] Beaudouin-Lafon | Open access to scientific publications[END_REF]. L'IHM n'échappe pas à cette tendance et, malgré la relative jeunesse de cette discipline, se pose le problème d'organiser et de rendre accessible les nombreux travaux de recherche. L'école de printemps 2010 de l'AFIHM a été le lieu d'une réflexion sur cette capitalisation des connaissances en IHM. Les doctorants participant ont été invités à réaliser, par groupe, en collaboration et à distance, un état de l'art sur un domaine restreint. Notre groupe devait répondre à la question « Dans quelle mesure les anima-tions et leurs contrôles pourraient permettre d'améliorer la transmission d'information au travers d'une visualisation et ainsi permettre d'accélérer l'exploration de ressources numériques ? ». Cette mise en situation a permis de prendre du recul pour analyser nos pratiques. Nous avons complété les données issues de cette mise en situation grâce à nos expériences passées, mais aussi à l'aide d'interviews réalisées auprès de trois enseignants-chercheurs et six doctorants. Ceci nous a permis de produire une analyse de l'activité de réalisation d'un état de l'art, présentée en première partie de ce document. Cette activité est divisée en cinq tâches : exploration, organisation, travail, recherche et partage. Nous proposons ensuite une solution répondant à la problématique de l'exploration d'information.

ANALYSE DE L'ACTIVITE Exploration

Nous appelons exploration, l'activité d'acquisition d'objets d'intérêt (OI) possédant un lien avec un thème ou un domaine de recherche. Un objet d'intérêt peut être un document académique ou non, un auteur, une conférence etc. Dans le cas d'un domaine inconnu, la démarche la plus courante est de se tourner vers une personne qui connaît le domaine. Nous proposons figure 1 la retranscription d'une discussion entre un doctorant devant réaliser un état de l'art sur les transitions animées et son directeur de thèse. En l'absence d'une telle personne dans son entourage, cette découverte peut se réaliser à l'aide de recherches sur internet. Ces recherches peuvent s'effectuer à partir de mots clefs (comme le nom du champ) sur des moteurs de recherche généralistes, ou académiques. Pour cette phase de familiarisation, les objets d'intérêt ne se limitent pas aux publications académiques. Ils incluent les blogs, les "wikis", les "news", les cours etc. Ils vont être destinés à comprendre des notions importantes, à assimiler le vocabulaire. Les documents récents, présentant un panorama comme des articles de synthèse, des manuels, des états de l'art de thèse ou des pages web sont particulièrement prisés. Cette découverte permet de diversifier et de préciser les mots-clefs. La transition se fait progressivement vers un processus d'extension des connaissances : recherche de travaux d'un même auteur, d'un même laboratoire, publié au même endroit, réutilisant certains mots-clefs, suivi de références et de citations etc. La phase d'exploration s'accompagne en permanence d'un processus de sélection dans les ressources nouvellement trouvées. Cette sélection est particulièrement difficile pour le néophyte qui se repose essentiellement sur l'ordre d'affichage des résultats dans les moteurs de recherche ainsi que sur la bibliométrie. Les critères d'évaluation évoluent et suivent l'acquisition de connaissances dans le domaine, par exemple l'évaluation d'un auteur sur sa réputation ou sur les articles précédemment lus plutôt que sur son h-index. Pour cette phase, l'objectif du chercheur est bien souvent l'acquisition de connaissances sur un sujet, mais peut également être de vérifier l'originalité d'une idée (ce qui ajoute la contrainte d'une certaine exhaustivité) ou encore de trouver une caution scientifique à une idée ou une intuition.

Travail

La phase de travail se caractérise par le besoin d'assimiler le contenu des OI, mais aussi de les enrichir et de produire de la connaissance. Il peut s'agir d'annoter directement le document (au format papier ou électronique) que ce soit en surlignant les passages importants ou en rédigeant des notes, ou encore de produire un résumé. Les buts sont multiples, notons qu'en premier lieu cela permet de faciliter et d'accélérer la relecture du document, mais que cela peut aussi être un vecteur favorisant la mémorisation par la production de texte. À des fins d'analyse ou de comparaison, les productions produites peuvent être un moyen de situer l'OI vis-à-vis d'autres travaux, d'en établir une critique, et d'en discuter avec d'autres personnes. À des fins de partage, l'objectif peut être de diffuser le fruit du travail réalisé au cours de cette phase dans l'idée de partager une bibliographie annotée par exemple.

Recherche

La phase de recherche se décrit par la nécessité de retrouver des OI parmi ceux auparavant obtenus lors de l'exploration. La façon de mener à bien cette tâche est alors fortement corrélée aux moyens déployés pour l'organisation. En cas d'organisation basée sur le système de fichiers, la recherche se réalise par la navigation dans la hiérarchie de dossiers, ou bien par l'utilisation de la fonctionnalité de recherche présente dans le système d'exploitation. Dans le cas où l'organisation s'est faite à l'aide d'outils, la recherche pourra s'exercer de manière plus précise en se basant sur des mots-clés associés à l'OI par exemple.

Partage

La dernière tâche que nous avons identifiée est le partage des OI et de leur enrichissement. Dans une optique de collaboration, le courrier électronique offre la possibilité de partager rapidement un nombre réduit d'OI. Si ce nombre est plus important, d'autres mécanismes sont mis en oeuvre comme l'utilisation d'un éditeur de texte en ligne pour la réalisation d'une bibliographie annotée, ou encore le partage de fichiers sur un système de ges-tion de versions. Encore une fois, des outils existent pour partager ces références (Mendeley, Zotero, Coviz). On retrouve dans cette activité de partage les mêmes préoccupations que pour les autres collecticiels : historique des actions, communication, conscience de groupe. Au delà du partage des seules références scientifiques, des idées comme l'utilisation d'un langage ou une boîte à outil graphique commune pour faciliter la réutilisation des techniques d'interaction produites par d'autres chercheurs circulent dans la communauté (par exemple UsiXML1 ). Certains chercheurs essayent également de maintenir à jour un corpus de connaissances sur leur domaine de travail, comme par exemple Me-nUA2 sur les menus ou encore le musée d'interaction 3 . Les relations sémantiques entre les informations permettent de naviguer d'une information à une autre ou d'une ressource à une autre. Chaque relation peut porter une signification spécifique fondée sur le contexte d'association dans lesquelles les informations ont été associées (Figure 3). Le contexte de ces associations est prépondérant à la stimulation de la mémoire épisodique. Ce type de mémoire enregistre les évènements et la relation spatiale et temporelle qui les lient [START_REF] Conway | Episodic memories[END_REF], notamment les expériences personnelles. Les souvenirs épisodiques sont essentiels dans l'acquisition de nouvelles connaissances [3]. Ainsi, l'exploration de ce graphe permet, pour un utilisateur novice, de faciliter la capitalisation mnésique des informations essentielles. Pour un utilisateur expert, elle favorise la stimulation de la mémoire épisodique pour la récupération d'information, aussi bien à partir du graphe que de sa mémoire.

GRAPHE D'EXPLORATION

CONCLUSION

Le travail réalisé dans le cadre de l'école de Printemps a permis de soulever certains problèmes que pose la capitalisation des connaissances scientifiques, et en particulier, dans le domaine de l'interaction Homme-

Figure 1

 1 Figure 1 Réponse d'un chercheur à la demande de points d'entrées bibliographiques sur les transitions animées. Organisation La tâche d'organisation correspond au besoin de classifier les OI afin de pouvoir s'y retrouver aisément. Très généralement les OI tels que les articles scientifiques sont, dans un souci de confort de lecture, obtenus sous format papier. Dans le monde physique, la notion de spatialité est importante; on range les objets à un endroit précis. L'organisation des OI dans le monde physique découle principalement des emplacements définis pour leurs rangements. Ce procédé est limité à une classification unique, par exemple, il n'est pas possible de ranger un même OI dans deux tiroirs différents. Ce rangement suit souvent un ordre chronologique. Réorganiser physiquement des articles par ordre alphabétique ou par date de parution est une tâche fastidieuse. L'outil informatique offre alors des moyens d'action supplémentaires : classement par date, nom etc. Dans le cadre d'une organisation de documents électroniques, le moyen le plus couramment mis en oeuvre s'appuie sur l'utilisation du système de fichiers. On procède alors par la création d'une hiérarchie de dossiers (par auteurs, thèmes, conférences...). Ce fonctionnement est très analogue à l'organisation de documents physiques, et présente l'avantage d'être supporté nativement par le

  Nous avons choisi de nous intéresser à la question de la découverte d'un champ de recherche inconnu. Cette tâche peut s'avérer difficile sans l'aide d'une personne connaissant le domaine. Les ressources acquises de cette manière présentent le double avantage de correspondre précisément au sujet étudié et d'être fiables. La difficulté provient en partie de la dispersion des informations sur différents médias, quand elles ne proviennent pas de discussions informelles, voire d'un savoir oral. Ces ressources possèdent des caractéristiques intrinsèques qui peuvent être différentes.

Figure 2

 2 Figure 2 Modèle de donnée

www.usixml.org

www.gillesbailly.fr/menua/

http://insitu.lri.fr/imuseum/ Bien que certains attributs puissent être communs à différentes ressources, les attributs différents, peuvent être liés par des relations (Figure 2) que nous allons définir par la suite. Ces ressources sont nombreuses et riches en informations. Chaque chercheur possède une certaine expérience qui lui confère une capacité à filtrer efficacement toutes ces ressources. Cependant, la mémoire humaine, reste limitée et il paraît impossible d'emmagasiner la totalité des informations délivrées. A partir des informations données par ces différentes ressources, un graphe de données hétérogènes peut être constitué. Nous proposons, ici, des éléments de conception permettant d'explorer un tel graphe. Nous pensons que son exploration peut, d'une part, amener à découvrir rapidement des informations essentielles et/ou peu diffusées grâce à des associations pertinentes entre informations et ressources, et d'autre part, stimuler la mémoire pour faciliter la récupération d'une information à partir du graphe ou de sa propre mémoire. Il est possible d'explorer les nombreuses informations issues de la capitalisation des ressources d'un domaine, en particulier le domaine de l'interaction hommemachine. Ces informations sont liées entre elles par une relation sémantique qui permet de naviguer d'une ressource à l'autre. Les ressources considérées dans cette approche sont les références de publications scientifiques, les conférences et les organisations telles que les laboratoires ou les sociétés savantes. Comme décrit précédemment, ces ressources sont constituées

Machine. La gestion des connaissances étant un domaine de recherche à part entière, notre modeste contribution se focalise sur l'exploration des connaissances. Nous espérons que les éléments de solution proposés dans cet article permettent d'alimenter une réflexion sur ces problématiques. Nous pensons que les méthodes de conception en interaction hommemachine, les domaines de la visualisation d'information et du travail collaboratif pourraient profiter au développement d'outils consacrés à cette capitalisation. Enfin, des initiatives comme le jeune "workshop" HCIR ("Human-Computer Interaction and Information Retrieval") doivent être reconduites et des rapprochements entre les communautés en IHM, en gestion des connaissances et en Science de l'Information et des Bibliothèques mériteraient d'être investigués.


Miguel E Andrés

Catuscia Palamidessi

Peter Van Rossum

Ana Sokolova

Information Hiding in Probabilistic Concurrent Systems

Information hiding is a general concept which refers to the goal of preventing an adversary to infer secret information from the observables. Anonymity and Information Flow are examples of this notion. We study the problem of information hiding in systems characterized by the coexistence of randomization and concurrency. It is well known that the presence of nondeterminism, due to the possible interleavings and interactions of the parallel components, can cause unintended information leaks. The most established approach to solve this problem is to fix the strategy of the scheduler beforehand. In this work, we propose a milder restriction on the schedulers, and we define the notion of strong (probabilistic) information hiding under various notions of observables. Furthermore, we propose a method, based on the notion of automorphism, to verify that a system satisfies the property of strong information hiding, namely strong anonymity or non-interference, depending on the context. Through the paper, we use the canonical example of the Dining Cryptographers to illustrate our ideas and techniques.

Introduction

The problem of information hiding consists in trying to prevent the adversary to infer confidential information from the observables. Instances of this issue are Anonymity and Information Flow. In both fields there is a growing interest in the quantitative aspects of the problem, see for instance [START_REF] Halpern | Anonymity and information hiding in multiagent systems[END_REF][START_REF] Bhargava | Probabilistic anonymity[END_REF][START_REF] Zhu | Anonymity vs. information leakage in anonymity systems[END_REF][START_REF] Clark | Quantified interference for a while language[END_REF][START_REF] Clark | Quantitative information flow, relations and polymorphic types[END_REF][START_REF] Malacaria | Assessing security threats of looping constructs[END_REF][START_REF] Malacaria | Lagrange multipliers and maximum information leakage in different observational models[END_REF][START_REF] Braun | Compositional methods for information-hiding[END_REF][START_REF] Clarkson | Belief in information flow[END_REF][START_REF] Chatzikokolakis | Anonymity protocols as noisy channels[END_REF][START_REF] Chatzikokolakis | On the Bayes risk in information-hiding protocols[END_REF][START_REF] Smith | On the foundations of quantitative information flow[END_REF]. This is justified by the fact that often we have some a priori knowledge about the likelihood of the various secrets (which we can usually express in terms of a probability distribution), and by the fact that protocols often use randomized actions to obfuscate the link between secret and observable, like in the case of the anonymity protocols of DC Nets [START_REF] Chaum | The dining cryptographers problem: Unconditional sender and recipient untraceability[END_REF], Crowds [START_REF] Reiter | Crowds: anonymity for Web transactions[END_REF], Onion Routing [START_REF] Syverson | Anonymous connections and onion routing[END_REF], and Freenet [START_REF] Clarke | Freenet: A distributed anonymous information storage and retrieval system[END_REF].

In a concurrent setting, like in the case of multi-agent systems, there is also another source of uncertainty, which derives from the fact that the various entities may interleave and interact in ways that are usually unpredictable, either because they depend on factors that are too complex to analyze, or because (in the case of specifications) they are implementation-dependent.

The formal analysis of systems which exhibit probabilistic and nondeterministic behavior usually involves the use of so-called schedulers, which are functions that, for each path, select only one possible (probabilistic) transition, thus delivering a purely probabilistic execution tree, where each event has a precise probability.

In the area of security, there is the problem that secret choices, like all choices, give rise to different paths. On the other hand, the decision of the scheduler may influence the observable behavior of the system. Therefore the security properties are usually violated if we admit as schedulers all possible functions of the paths: certain schedulers induce a dependence of the observables on the secrets, and protocols which would not leak secret information when running in "real" systems (where the scheduling devices cannot "see" the internal secrets of the components and therefore cannot depend on them), do leak secret information under this more permissive notion of scheduler. This is a well known problem for which various solutions have already been proposed [START_REF] Canetti | Task-structured probabilistic i/o automata[END_REF][START_REF] Canetti | Time-bounded task-PIOAs: A framework for analyzing security protocols[END_REF][START_REF] Chatzikokolakis | Making random choices invisible to the scheduler[END_REF][START_REF] Chatzikokolakis | Bisimulation for demonic schedulers[END_REF]. We will come back to these in the "Related work" section.

Contribution

We now list the main contribution of this work:

• We define a class of partial-information schedulers (which we call admissible), schedulers in this class are a restricted version of standard (fullinformation) schedulers. The restriction is rather flexible and has strong structural properties, thus facilitating the reasoning about security properties. In short, our systems consist of parallel components with certain restrictions on the secret choices and nondeterministic choices. The scheduler selects the next component (or components, in case of synchronization) for the subsequent step independently of the secret choices. We then formalize the notion of quantitative information flow, or degree of anonymity, using this restricted notion of scheduler.

• We propose alternative definitions to the property of strong anonymity defined in [START_REF] Bhargava | Probabilistic anonymity[END_REF]. Our proposal differs from the original definition in two aspects:

(1) the system should be strongly anonymous for all admissible schedulers instead of all schedulers (which is a very strong condition, never satisfied in practice), [START_REF] Andrés | Information hiding in probabilistic concurrent systems[END_REF] we consider several variants of adversaries, namely (in increasing level of power): external adversaries, internal adversaries, and adversaries in collusion with the scheduler (in a Dolev-Yao fashion). Additionally, we use admissible schedulers to extend the notions of multiplicative and additive leakage (proposed in [START_REF] Smith | On the foundations of quantitative information flow[END_REF] and [START_REF] Braun | Quantitative notions of leakage for one-try attacks[END_REF] respectively) to the case of a concurrent system.

• We propose a sufficient technique to prove probabilistic strong anonymity, and probabilistic noninterference, based on automorphisms. The idea is the following: In the purely nondeterministic setting, the strong anonymity of a system is often proved (or defined) as follows: take two users A and B and a trace in which user A is 'the culprit'. Now find a trace that looks the same to the adversary, but in which user B is 'the culprit' [START_REF] Halpern | Anonymity and information hiding in multiagent systems[END_REF][START_REF] Garcia | Provable anonymity[END_REF][START_REF] Mauw | A formalization of anonymity and onion routing[END_REF][START_REF] Hasuo | Probabilistic anonymity via coalgebraic simulations[END_REF]. This new trace is often most easily obtained by switching the behavior of A and B. Non-interference can be proved in the same way (where A and B are high information and the trace is the low information).

In this work, we make this technique explicit for anonymity in systems where probability and nondeterminism coexist, and we need to cope with the restrictions on the schedulers. We formalize the notion of switching behaviors by using automorphism (it is possible to switch the behavior of A and B if there exist an automorphism between them) and then show that the existence of an automorphism implies strong anonymity.

• We illustrate the problem with full-information schedulers in security, our solution providing admissible schedulers, and the application of our proving technique by means of the well known Dining Cryptographers anonymity protocol.

Related Work

The problem of the full-information scheduler has already been extensively investigated in literature. The works [START_REF] Canetti | Task-structured probabilistic i/o automata[END_REF] and [START_REF] Canetti | Time-bounded task-PIOAs: A framework for analyzing security protocols[END_REF] consider probabilistic automata and introduce a restriction on the scheduler to the purpose of making them suitable to applications in security. Their approach is based on dividing the actions of each component of the system in equivalence classes (tasks). The order of execution of different tasks is decided in advance by a so-called task scheduler. The remaining nondeterminism within a task is resolved by a second scheduler, which models the standard adversarial scheduler of the cryptographic community. This second entity has limited knowledge about the other components: it sees only the information that they communicate during execution. Their notion of task scheduler is similar to our notion of admissible scheduler, but more restricted since the strategy of the task scheduler is decided entirely before the execution of the system.

Another work along these lines is [START_REF] De Alfaro | Compositional methods for probabilistic systems[END_REF], which uses partitions on the statespace to obtain partial-information schedulers. However that work considers a synchronous parallel composition, so the setting is rather different from ours.

The work in [START_REF] Chatzikokolakis | Making random choices invisible to the scheduler[END_REF][START_REF] Chatzikokolakis | Bisimulation for demonic schedulers[END_REF] is similar to ours in spirit, but in a sense dual from a technical point of view. Instead of defining a restriction on the class of schedulers, they provide a way to specify that a choice is transparent to the scheduler. They achieve this by introducing labels in process terms, used to represent both the states of the execution tree and the next action or step to be scheduled. They make two states indistinguishable to schedulers, and hence the choice between them private, by associating to them the same label. Furthermore, their "equivalence classes" (schedulable actions with the same label) can change dynamically, because the same action can be associated to different labels during the execution.

In [START_REF] Alvim | Safe Equivalences for Security Properties[END_REF] we have extended the framework presented in this work (by allowing internal nondeterminism and adding a second type of scheduler to resolve it) with the aim of investigating angelic vs demonic nondeterminism in equivalencebased properties.

The fact that full-information schedulers are unrealistic has also been observed in fields other than security. With the aim to cope with general properties (not only those concerning security), first attempts used restricted schedulers in order to obtain rules for compositional reasoning [START_REF] De Alfaro | Compositional methods for probabilistic systems[END_REF]. The justification for those restricted schedulers is the same as for ours, namely, that not all information is available to all entities in the system. Later on, it was shown that model checking is unfeasible in its general form for the kind of restricted schedulers presented in [START_REF] De Alfaro | Compositional methods for probabilistic systems[END_REF]. See [START_REF] Giro | Quantitative model checking revisited: Neither decidable nor approximable[END_REF] and, more recently, [START_REF] Giro | Undecidability results for distributed probabilistic systems[END_REF].

To the best of our knowledge, this is the first work using automorphisms as a sound proof technique (in our case to prove strong anonymity and noninterference). The closest line of work we are aware of is in the field of model checking. There, isomorphisms can be used to identify symmetries in the system, and such symmetries can then be exploited to alleviate the state space explosion (see for instance [START_REF] Kwiatkowska | Symmetry reduction for probabilistic model checking[END_REF]).

A notion similar to that of authomorphism, namely bisimulation, has been used in several works to define and verify anonymity and privacy properties (see for instance [START_REF] Delaune | Verifying privacy-type properties of electronic voting protocols[END_REF]). However, the underlying models are different: we annotate the transitions with a label identifying the active component(s), which means that an automorphism can relate different states only if they result from different probabilistic choices. The notion of bisimulation used in the security literature, on the contrary, usually relates states resulting from different nondeterministic choices. In [START_REF] Alvim | Safe Equivalences for Security Properties[END_REF] we argue that the notion of bisimulation can be too permissive in certain cases.

A preliminary version of this work, without proofs, appeared in [START_REF] Andrés | Information hiding in probabilistic concurrent systems[END_REF].

Plan of the paper

Looking ahead, after reviewing some preliminaries (Section 2) we formalize the notions of systems and components (Section 3). In Section 4 we present admissible schedulers. We then formalize the notions of internal and external strong anonymity in a probabilistic and nondeterministic setting for admissible schedulers (Section 5). Finally, we turn our attention to the verification problem, in Section 6 we present a strong-anonymity proving technique based on automorphisms. We conclude and outline some future work in Section 7.

Preliminaries

In this section we gather preliminary notions and results related to probabilistic automata [START_REF] Segala | Probabilistic simulations for probabilistic processes[END_REF][START_REF] Segala | Modeling and Verification of Randomized Distributed Real-Time Systems[END_REF], information theory [START_REF] Cover | Elements of Information Theory[END_REF], and information leakage [START_REF] Smith | On the foundations of quantitative information flow[END_REF][START_REF] Braun | Quantitative notions of leakage for one-try attacks[END_REF].

Probabilistic automata

A function µ : Q → [0, 1] is a discrete probability distribution on a set Q if q∈Q µ(q) = 1. The set of all discrete probability distributions on Q is denoted by D(Q).
A probabilistic automaton is a quadruple M = (Q, Σ, q, θ) where Q is a countable set of states, Σ a finite set of actions, q the initial state, and θ a transition function θ : Q → P(D(Σ × Q)). Here P(X) is the set of all subsets of X.

If θ(q) = ∅, then q is a terminal state. We write q→µ for µ ∈ θ(q), q ∈ Q. Moreover, we write q a →r for q, r ∈ Q whenever q→µ and µ(a, r) > 0. A fully probabilistic automaton is a probabilistic automaton satisfying |θ(q)| ≤ 1 for all states. In case θ(q) = ∅ in a fully probabilistic automaton, we will overload notation and use θ(q) to denote the distribution outgoing from q. A path in a probabilistic automaton is a sequence σ = q 0 a1 → q 1 a2 → • • • where q i ∈ Q, a i ∈ Σ and q i ai+1 → q i+1 . A path can be finite in which case it ends with a state. A path is complete if it is either infinite or finite ending in a terminal state. Given a path σ, first(σ) denotes its first state, and if σ is finite then last (σ) denotes its last state. A cycle is a path σ such that last (σ) = first(σ). Let Paths q (M ) denote the set of all paths, Paths ⋆ q (M ) the set of all finite paths, and CPaths q (M ) the set of all complete paths of an automaton M , starting from the state q. We will omit q if q = q. Paths are ordered by the prefix relation, which we denote by ≤. The trace of a path is the sequence of actions in Σ * ∪ Σ ∞ obtained by removing the states, hence for the above path σ we have trace(σ) = a 1 a 2 . . .. If Σ ′ ⊆ Σ, then trace Σ ′ (σ) is the projection of trace(σ) on the elements of Σ ′ .

Let M = (Q, Σ, q, θ) be a (fully) probabilistic automaton, q ∈ Q a state, and let σ ∈ Paths ⋆ q (M ) be a finite path starting in q. The cone generated by σ is the set of complete paths σ = {σ ′ ∈ CPaths q (M ) | σ ≤ σ ′ }. Given a fully probabilistic automaton M = (Q, Σ, q, θ) and a state q, we can calculate the probability value, denoted by P q (σ), of any finite path σ starting in q as follows: P q (q) = 1 and P q (σ a → q ′ ) = P q (σ) µ(a, q ′ ), where last (σ) → µ.

Let Ω q def = CPaths q (M ) be the sample space, and let F q be the smallest σalgebra generated by the cones. Then P q induces a unique probability measure on F q (which we will also denote by P q ) such that P q ( σ ) = P q (σ) for every finite path σ starting in q. For q = q we write P instead of P q.

A (full-information) scheduler for a probabilistic automaton M is a function ζ : Paths ⋆ (M ) → (D(Σ×Q)∪{⊥}) such that for all finite paths σ, if θ(last (σ)) = ∅ then ζ(σ) ∈ θ(last (σ)), and ζ(σ) = ⊥ otherwise. Hence, a scheduler ζ selects one of the available transitions in each state, and determines therefore a fully probabilistic automaton, obtained by pruning from M the alternatives that are not chosen by ζ. Note that a scheduler is history dependent since it can take different decisions for the same state s according to the past evolution of the system.

Noisy Channels

This section briefly recalls the notion of noisy channels from Information Theory [START_REF] Cover | Elements of Information Theory[END_REF].

A noisy channel is a tuple C def = (X , Y, P (•|•)) where X = {x 1 , x 2 , . . . , x n } is a finite set of input values, modeling the secrets of the channel, and Y = {y 1 , y 2 , . . . , y m } is a finite set of output values, the observables of the channel. For x i ∈ X and y j ∈ Y, P (y j | x i ) is the conditional probability of obtaining the output y j given that the input is x i . These conditional probabilities constitute the so called channel matrix, where P (y j |x i ) is the element at the intersection of the i-th row and the j-th column. For any input distribution P X on X , P X and the channel matrix determine a joint probability P ∧ on X × Y, and the corresponding marginal probability P Y on Y (and hence a random variable Y ). P X is also called a priori distribution and it is often denoted by π. The probability of the input given the output is called a posteriori distribution.

Information leakage

We recall here the definitions of multiplicative leakage proposed in [START_REF] Smith | On the foundations of quantitative information flow[END_REF], and of additive leakage proposed in [START_REF] Braun | Quantitative notions of leakage for one-try attacks[END_REF] 4 . We assume given a noisy channel C = (X , Y, P (•|•)) and a random variable X on X . The a priori vulnerability of the secrets in X is the probability of guessing the right secret, defined as V(X) def = max x∈X P X (x). The rationale behind this definition is that the adversary's best bet is on the secret with highest probability. The a posteriori vulnerability of the secrets in X is the probability of guessing the right secret, after the output has been observed, averaged over the probabilities of the observables. The formal definition is V(X | Y) def = y∈Y P Y (y) max x∈X P (x | y). Again, this definition is based on the principle that the adversary will choose the secret with the highest a posteriori probability.

Note that, using the definition of conditional probability, we can write the a posteriori vulnerability in terms of the joint probability, or in terms of the channel matrix and the a priori distribution:

V(X | Y) = y∈Y max x∈X P ∧ (x, y). = y∈Y max x∈X (P (y | x)P X (x)) The multiplicative leakage is L × (C, P X ) def = V(X|Y) V(X) whereas the additive leak- age is L + (C, P X ) def = V(X|Y) -V(X).

Dining Cryptographers

This problem, described by Chaum in [START_REF] Chaum | The dining cryptographers problem: Unconditional sender and recipient untraceability[END_REF], involves a situation in which three cryptographers are dining together. At the end of the dinner, each of them is secretly informed by a central agency (master) whether he should pay the bill, or not. So, either the master will pay, or one of the cryptographers will be asked to pay. The cryptographers (or some external observer) would like to find out whether the payer is one of them or the master. However, if the payer is one of them, they also wish to maintain anonymity over the identity of the payer.

A possible solution to this problem, described in [START_REF] Chaum | The dining cryptographers problem: Unconditional sender and recipient untraceability[END_REF], is that each cryptographer tosses a coin, which is visible to himself and his neighbor to the left. Each cryptographer observes the two coins that he can see and announces agree or disagree. If a cryptographer is not paying, he will announce agree if the two sides are the same and disagree if they are not. The paying cryptographer will say the opposite. It can be proved that if the number of disagrees is even, then the master is paying; otherwise, one of the cryptographers is paying. Furthermore, in case one of the cryptographers is paying, neither an external observer nor the other two cryptographers can identify, from their individual information, who exactly is paying (provided that the coins are fair). The Dining Cryptographers (DC) will be a running example through the paper.

Systems

In this section we describe the kind of systems we are dealing with. We start by introducing a variant of probabilistic automata, that we call tagged probabilistic automata (TPA). These systems are parallel compositions of purely probabilistic processes, that we call components. They are equipped with a unique identifier, that we call tag, or label, of the component. Note that, because of the restriction that the components are fully deterministic, nondeterminism is generated only from the interleaving of the parallel components. Furthermore, because of the uniqueness of the tags, each transition from a node is associated to a different tag / pair of two tags (one in case only one component makes a step, and two in case of a synchronization step among two components).

Tagged Probabilistic Automata

We now formalize the notion of TPA.

Definition 1. A tagged probabilistic automaton (TPA) is a tuple (Q, L, Σ, q, θ), where

• Q is a set of states,
• L is a set of tags, or labels,

• Σ is a set of actions,

• q ∈ Q is the initial state,

• θ : Q → P(L × D(Σ × Q)) is a transition function.
with the additional requirement that for every q ∈ Q and every ℓ ∈ L there is at

most one µ ∈ D(Σ × Q) such that (ℓ, µ) ∈ θ(q).
A path for a TPA is a sequence σ = q 0 l1,a1

-→ q 1 l2,a2 -→ q 2 • • • .
In this way, the process with identifier l i induces the system to move from q i-1 to q i performing the action a i , and it does so with probability µ li (a i , q i ), where µ li is the distribution associated to the choice made by the component l i . Finite paths and complete paths are defined in a similar manner.

In a TPA, the scheduler's choice is determined by the choice of the tag. We will use enab(q) to denote the tags of the components that are enabled to make a transition. Namely,

enab(q) def = {ℓ ∈ L | ∃ µ ∈ D(Σ × Q) : (ℓ, µ) ∈ θ(q)} (1)
We assume that the scheduler is forced to select a component among those which are enabled, i.e., that the execution does not stop unless all components are blocked (suspended or terminated). This is in line with the spirit of process algebra, and also with the tradition of Markov Decision Processes, but contrasts with that of the Probabilistic Automata of Lynch and Segala [START_REF] Segala | Probabilistic simulations for probabilistic processes[END_REF]. However, the results in this paper do not depend on this assumption; we could as well allow the (more general) notion of schedulers which may decide to terminate the execution even though there are transitions which are possible from the last state. The reason we did not do it is because it would be confusing in the setting of process algebra, and also it would complicate the notation and the proofs. On the other hand, for the purposes of this paper the generality added by the second notion of scheduler can be captured by adding a component that performs only one observable action representing termination.

Definition 2. A scheduler for a TPA M = (Q, L, Σ, q, θ) is a function ζ : Paths ⋆ (M ) → (L ∪ {⊥}) such that for all finite paths σ, ζ(σ) ∈ enab(last (σ)) if enab(last (σ)) = ∅ and ζ(σ) = ⊥ otherwise.

Components

To specify the components we use a sort of probabilistic version of CCS [START_REF] Milner | Communication and Concurrency[END_REF][START_REF] Milner | Communicating and mobile systems: the π-calculus[END_REF]. We assume a set of secret actions Σ S with elements s, s 1 , s 2 , • • • , and a disjoint set of observable actions Σ O with elements a, a 1 , a 2 , • • • . Furthermore we have a disjoint set of communication actions of the form c(x) (receive x on channel c, where x is a formal parameter), or c v (send v on channel c, where v is a value on some domain V ). Sometimes we need only to synchronize without transmitting any value, in which case we will use simply c and c. We denote the set of channel names by C.

A component q is specified by the following grammar:

Components q ::= 0 termination | a.q observable prefix | i p i : q i blind choice | i p i : s i .q i secret choice | if x = v then q 1 else q 2 conditional | A process call Observables a ::= c | c simple synchronization | c(x) | c v synchronization

and communication

The p i , in the blind and secret choices, represents the probability of the i-th branch and must satisfy 0 ≤ p i ≤ 1 and i p i = 1. When no confusion arises, we use simply + for a binary choice. The process call A is a simple process identifier. For each of them, we assume a corresponding unique process declaration of the form A def = q. The idea is that, whenever A is executed, it triggers the execution of q. Note that q can contain A or another process identifier, which means that our language allows (mutual) recursion.

Note that each component contains only probabilistic and sequential constructs. In particular, there is no internal parallelism nor nondeterminism (apart from the input nondeterminism, which disappears in the definition of a system). Hence each component corresponds to a purely probabilistic automaton, as described by the operational semantics below. The main reason to dismiss the use of internal parallelism and nondeterminism is verification: as mentioned in the introduction we will present a proving technique for the different definitions of anonymity proposed in this work. This result would not be possible without such restriction on the components (see Example 5).

For an extension of this framework allowing the use of internal parallelism and nondeterminism we refer to [START_REF] Alvim | Safe Equivalences for Security Properties[END_REF]. There, the authors combine global nondeterminism (arising from the interleaving of the components) and local nondeterminism (allowed as a primitive and also arising from the internal parallelism of the components). The authors use such (extended) framework for a different purpose than ours, namely to define a notion of equivalence suitable for security analysis. No verification mechanisms are provided in [START_REF] Alvim | Safe Equivalences for Security Properties[END_REF].

Components' semantics: The operational semantics consists of probabilistic transitions of the form q→µ where q ∈ Q is a process, and µ ∈ D(Σ × Q) is a distribution on actions and processes. They are specified by the following rules:

PRF1 v ∈ V c(x).q → δ(c(v), q[v/x]) PRF2 a.q → δ(a, q) if a = c(x) INT i p i : q i → • i p i • δ(τ, q i ) SECR i p i : s i .q i → • i p i • δ(s i , q i ) CND1 if v = v then q 1 else q 2 → δ(τ, q 1 ) CND2 v = v ′ if v = v ′ then q 1 else q 2 → δ(τ, q 2 ) CALL q → µ A → µ if A def = q • i p i • µ i is the distribution µ such that µ(x) = i p i µ i (x)
. We use δ(x) to represent the delta of Dirac, which assigns probability 1 to x. The silent action, τ , is a special action different from all the observable and the secret actions. q[v/x] stands for the process q in which any occurrence of x has been replaced by v. To shorten the notation, in the examples throughout the paper, we omit writing explicit termination, i.e., we omit the symbol 0 at the end of a term.

Systems

A system consists of n processes (components) in parallel, restricted at the top-level on the set of channel names C:

(C) q 1 q 2 • • • q n .
The restriction on C enforces synchronization (and possibly communication) on the channel names belonging to C, in accordance with the CCS spirit. Since C is the set of all channels, all of them are forced to synchronize. This is to eliminate, at the level of systems, the nondeterminism generated by the rule for the receive prefix, PRF1.

Systems' semantics:

The semantics of a system gives rise to a TPA, where the states are terms representing systems during their evolution. A transition now is of the form q ℓ → µ where µ ∈ (D(Σ × Q)) and ℓ ∈ L is either the identifier of the component which makes the move, or a two-element set of identifiers representing the two partners of a synchronization. The following two rules provide the operational semantics rules in the case of interleaving and synchronisation/communication, respectively.

Interleaving.

q i → • j p j • δ(a j , q ij ) (C) q 1 • • • q i • • • q n i → • j p j • δ(a j , (C) q 1 • • • q ij • • • q n ) If a j ∈ C
where i indicates the tag of the component making the step.

Synchronization/Communication. q i → δ(c v , q ′ i ) q j → δ(c(v), q ′ j ) (C) q 1 • • • q i • • • q n {i,j} -→ δ(τ, (C) q 1 • • • q ′ i • • • q ′ j • • • q n )
here {i, j} is the tag indicating that the components making the step are i and j. For simplicity we write i,j

-→ instead of {i,j} -→. The rule for synchronization without communication is similar, the only difference is that we do not have v and (v) in the actions. Note that c can only be an observable action (neither a secret nor τ ), by the assumption that channel names can only be observable actions.

We note that both interleaving and synchronization rules generate nondeterminism. The only other source of nondeterminism is PRF1, the rule for a receive prefix c(x). However the latter is not real nondeterminism: it is introduced in the semantics of the components but it disappears in the semantics of the systems, given that the channel c is restricted at the top-level. In fact the restriction enforces communication, and when communication takes place, only the branch corresponding to the actual value v transmitted by the corresponding send action is maintained, all the others disappear.

Proposition 1. The operational semantics of a system is a TPA with the following characteristics:

(a) Every step q ℓ → µ is either a blind choice: µ = • i p i • δ(τ, q i ), or a secret choice: µ = • i p i • δ(s i , q i ), or a delta of Dirac: µ = δ(α, q ′ ) with α ∈ Σ O or α = τ . (b) If q ℓ → µ and q ℓ → µ ′ then µ = µ ′ .
Proof.

(a) The rules for the components and the rule for synchronization / communication can only produce blind choices, secret choices, or deltas of Dirac. Furthermore, because of the restriction on all channels, the transitions at the system level cannot contain communication actions. Finally, observe that the interleaving rule maintains these properties.

(b) At the component level, the only source of nondeterminism is PRF1, the rule for a receive prefix c(x). At the system level, this action is forced to synchronize with a corresponding send action, and, in a component, there can be only one such action available at a time. Hence the tag determines the value to be sent, which in turn determines the selection of exactly one branch in the receiving process. The only other sources of nondeterminism are the interleaving and the synchronization/communication rules, and they induce a different tag for each alternative.

Example 1. We now present the components for the Dining Cryptographers using the introduced syntax. They correspond to Figure 1 and to the automata depicted in Figure 3. As announced before, we omit the symbol 0 for explicit termination at the end of each term. The secret actions s i represent the choice of the payer. The operators ⊕, ⊖ represent the sum modulo 2 and the difference modulo 2, respectively. The test i == n returns 1 (true) if i = n, and 0 otherwise. The set of restricted channel names is The operation pay ⊕ coin 1 ⊕ coin 2 in Figure 2 is syntactic sugar, it can be defined using the if-then-else operator. Note that, in this way, if a cryptographer is not paying (pay = 0), then he announces 0 if the two coins are the same (agree) and 1 if they are not (disagree).

C = {c 0,0 , c 0,1 , c 1,1 , c 1,2 , c 2,0 , c 2,2 , m 0 , m 1 , m 2 }. Master def = p : m 0 0 . m 1 0 . m 2 0 + (1 -p) : 2 i=0 p i : s i . m 0 i == 0 . m 1 i == 1 . m 2 i == 2 Crypt i def = m i (pay) . c i,i (coin 1 ) . c i,i⊕1 (coin 2 ) . out i pay ⊕ coin 1 ⊕ coin 2 Coin i def = 0.5 : ci,i 0 . ci⊖1,i 0 + 0.5 : ci,i 1 . ci⊖1,i 1 System def = (C ) Master 2 i=0 Crypt i 2 i=0 Coin i
Master

• 1-p p Ô Ô • p0:s0 × × p1:s1 / / / # # / / / p2:s2 G G 5 5 G G G G G G G G • m0 0
( ( : : : : : : :

• m 0 1 • m 0 0 • m 0 0 • m1 0 • m 1 1 • m1 0 • m2 0 # # / / / / / / • m2 1 { { w w w w w w w w w • Coin i • τ 1 2 1 2 • ci,i 0 • ci,i 1 • ci⊖1,i 0 ' ' • ci⊖1,i 1 Ó Ó • Crypt i • mi(0) Ö Ö mi(1) $ $ • ci,i(0) ci,i(1) 8 8 L L L L L L L L L L L • ci,i(0) ci,i (1)
y y r r r r r r r r r r r

• ci,i⊕1(0) ci,i⊕1(1) 8 8 L L L L L L L L L L L • ci,i⊕1(0) ci,i⊕1 (1)
y y r r r r r r r r r r r

• outi(0) 4 4 • outi(1)

| | •

Admissible Schedulers

We now introduce the class of admissible schedulers. Standard (full-information) schedulers have access to all the information about the system and its components, and in particular the secret choices. Hence, such schedulers can leak secrets by making their decisions depend on the secret choice of the system. This is the case with the Dining Cryptographers protocol of Section 2.4: among all possible schedulers for the protocol, there are several that leak the identity of the payer. In fact the scheduler has the freedom to decide the order of the announcements of the cryptographers (interleaving), so a scheduler could choose to let the payer announce lastly. In this way, the attacker learns the identity of the payer simply by looking at the interleaving of the announcements.

The screens intuition

Let us first describe admissible schedulers informally. As mentioned in the introduction, admissible schedulers can base their decisions only on partial information about the evolution of the system, in particular admissible schedulers cannot base their decisions on information concerned with the internal behavior of components (such as secret choices).

We follow the subsequent intuition: admissible schedulers are entities that have access to a screen with buttons, where each button represents one (current) available option. At each point of the execution the scheduler decides the next step among the available options (by pressing the corresponding button). Then the output (if any) of the selected component becomes available to the scheduler and the screen is refreshed with the new available options (the ones corresponding to the system after making the selected step). We impose that the scheduler can base its decisions only on such information, namely: the screens and outputs he has seen up to that point of the execution (and, of course, the decisions he has made). Figure 4 shows the sequence of screens corresponding to a particular sequence of choices taken by the scheduler 5 . Interleaving and communication options are represented by yellow and red buttons, respectively. An arrow between two screens represents the transition from one to the other (produced by the scheduler pressing a button), additionally, the decision taken by the scheduler and corresponding outputs are depicted above each arrow. Note that this system has exactly the same problem as the DC protocol: a full-information scheduler could reveal the secret by basing the interleaving order (q first or t first) on the secret choice of the component r. However, the same does not hold anymore for admissible schedulers (the scheduler cannot deduce the secret choice by just looking at the screens and outputs). This is also the case for the DC protocol, i.e., admissible schedulers cannot leak the secret of the protocol.

The formalization

Before formally defining admissible schedulers we need to formalize the ingredients of the screens intuition. The buttons on the screen (available options) are the enabled options given by the function enab (see [START_REF] Alvim | Safe Equivalences for Security Properties[END_REF] in Section 3), the decision made by the scheduler is the tag of the selected enabled option, observable actions are obtained by sifting the secret actions to the schedulers by means of the following function:

sift (α) def = α if α ∈ Σ O ∪ {τ }, τ if α ∈ Σ S .
The partial information of a certain evolution of the system is given by the map t defined as follows.

Definition 3. Let q ℓ1,α1 -→ • • • ℓn,αn
-→ q n+1 be a finite path of the system, then we define t as:

t q ℓ1,α1 -→ • • • ℓn,αn -→ q n+1 def = (enab(q), ℓ 1 , sift (α 1 )) • • • (enab(q n ), ℓ n , sift (α n )) • enab(q n+1 ).
Finally, we have all the ingredients needed to define admissible schedulers.

Definition 4 (Admissible schedulers). A scheduler ζ is admissible if for all

σ, σ ′ ∈ Paths ⋆ t(σ) = t(σ ′ ) implies ζ(σ) = ζ(σ ′ ).
In this way, admissible schedulers are forced to take the same decisions on paths that they cannot tell apart. Note that this is a restriction on the original definition of (full-information) schedulers where t is the identity map over finite paths (and consequently the scheduler is free to choose differently).

In the kind of systems we consider (the TPAs) the only source of nondeterminism are the interleaving and interactions of the parallel components. Consequently, in a TPA the notion of scheduler is quite simple: its role, indeed, is to select, at each step, the component or pair of components which will perform the next transition. In addition, the TPA model allows us to express in a simple way the notion of admissibility: in fact the transitions available in the last state of σ are determined by the set of components enabled in the last state of σ, and t(σ) gives (among other information) such set. Therefore t(σ) = t(σ ′ ) implies that the last states of σ and σ ′ have the same possible transitions, hence it is possible to require that ζ(σ) = ζ(σ ′ ) without being too restrictive or too permissive. In more general systems, where the sources of nondeterminism can be arbitrary, it is difficult to impose that the scheduler"does not depend on the secret choices", because different secret choices in general may give rise to states with different sets of transitions, and it is unclear whether such difference should be ruled out as "inadmissible", or should be considered as part of what a "real" scheduler can detect.

Information-hiding properties in presence of nondeterminism

In this section we revise the standard definition of information flow and anonymity in our framework of controlled nondeterminism.

We first consider the notion of adversary. We consider three possible notions of adversaries, increasingly more powerful.

Adversaries External adversaries:

Clearly, an adversary should be able, by definition, to see at least the observable actions. For an adversary external to the system S, it is natural to assume that these are also the only actions that he is supposed to see. We also assume that an external adversary has no way to know whether an internal synchronization has taken place. To this purpose, we need to abstract from the τ actions. Therefore, we define the observation domain, for an external adversary, as the set of the (finite) sequences of observable actions, namely:

O e def = Σ * O .
Correspondingly, we need a function t e : Paths ⋆ (S) → O e that extracts the observables from the executions:

t e q 0 ℓ1,α1 -→ • • • ℓn,αn -→ q n+1 def = sieve(α 1 ) • • • sieve(α n )
where

sieve(α) def = α if α ∈ Σ O , ǫ if α ∈ Σ S ∪ {τ }.
Note that the difference between sift and sieve is that the latter transforms the τ actions in empty string, thus making completely invisible to the external adversary whether an internal synchronization has taken place or not.

Internal adversaries: An internal adversary may be able to see, besides the observables, also the interleaving and synchronizations of the various components, i.e. which component(s) are active, at each step of the execution. Hence it is natural to define the observation domain, for an internal adversary, as the sequence of pairs of observable action and tag (i.e. the identifier(s) of the active component(s)), namely:

O i def = (L × (Σ O ∪ {τ })) * .
Analogously to the case of the external adversaries, we need a function t i : Paths ⋆ (S) → O i that extracts the observables from the executions:

t i q 0 ℓ1,α1 -→ • • • ℓn,αn -→ q n+1 def = (ℓ 1 , sieve(α 1 )) • • • (ℓ n , sieve(α n )).
Note that, in contrast to the case of t e , in the definition of t i we could have used, equivalently, sift instead of sieve.

Adversaries in collusion with the scheduler: Finally, we consider the case in which the adversary is in collusion with the scheduler, or possibly the adversary is the scheduler. To illustrate the difference between this kind of adversaries and internal adversaries, consider the scheduler of an operating system. In such scenario an internal adversary is able to see which process has been schedule to run next (process in the "running state") whereas an adversary in collusion with the scheduler can see as much as the scheduler, thus being able to see (in addition) which processes are in the "ready state" and which processes are in the "waiting / blocked" state. We will show later that such additional information does not help the adversary to leak information (see Proposition 4). The observation domain of adversaries in collusion with the scheduler coincides with the one of the scheduler:

O s def = (P(L) × L × (Σ O ∪ {τ })) * .
The corresponding function

t s : Paths ⋆ (S) → O s
is defined as the one of the scheduler, i.e. t s = t.

Information leakage

In the fields of information flow and anonymity there is a converging consensus for formalizing the notion of leakage as the difference or the ratio between the a priori uncertainty that the adversary has about the secret, and the a posteriori uncertainty, that is, the residual uncertainty of the adversary once it has seen the outcome of the computation. The uncertainty can be measured in different ways. One popular approach is the information-theoretic one, according to which the system is seen as a noisy channel between the secret inputs and the observable output, and uncertainty corresponds to the entropy of the system (see preliminaries -Section 2). In this approach, the leakage is represented by the so-called mutual information, which expresses the correlation between the input and the output.

In most of the approaches in the information flow literature the notion of entropy uses is Shannon entropy. However Cachin, in his PhD thesis [START_REF] Cachin | Entropy Measures and Unconditional Security in Cryptography[END_REF], had already argued that the right notion of entropy should depend on the notion of adversary, and on the way we measure its success. More recently, Köpf and Basin have considered again this intuition, and have developed an informationtheoretic schema to define leakage in terms of mutual information for a large class of adversaries [START_REF] Köpf | An information-theoretic model for adaptive side-channel attacks[END_REF].

In his recent paper, Smith has considerd again the question of the most suitable notion of entropy, focusing on the particular case of one-try attacks [START_REF] Smith | On the foundations of quantitative information flow[END_REF]. He has argued that Shannon entropy is not suitable to represent the security threats in the case in which the adversary is interested in figuring out the secret in one try, and he has proposed to use Rényi's min entropy instead, or equivalently, the average probability of guessing the secret in one try. This leads to interpret the uncertainty in terms of the notion of vulnerability defined in the preliminaries (Section 2). The corresponding notion of leakage, in the pure probabilistic case, has been investigated in [START_REF] Smith | On the foundations of quantitative information flow[END_REF] (multiplicative case) and in [START_REF] Braun | Quantitative notions of leakage for one-try attacks[END_REF] (additive case).

Here we adopt the vulnerability-based approach to define the notion of leakage in our probabilistic and nondeterministic context. The Shannon-entropybased approach could be extended to our context as well, because in both cases we only need to specify how to determine the conditional probabilities which constitute the channel matrix, and the marginal probabilities that constitute the input and the output distribution.

We will denote by S the random variable associated to the set of secrets S = Σ S , and by O x the random variables associated to the set of observables O x , where x ∈ {e, i, s}. So, O x represents the observation domains for the various kinds of adversaries defined above.

As mentioned before, our results require some structural properties for the system: we assume that there is a single component in the system containing a secret choice and this component contains a single secret choice. This hypothesis is general enough to allow expressing protocols like the Dining Cryptographers, Crowds, voting protocols, etc., where the secret is chosen only once. Assumption 1. A system contains exactly one component with a syntactic occurrence of a secret choice, and such a choice does not occur in the scope of a recursive call.

Note that the assumption implies that the choice appears exactly once in the operational semantics of the component. It would be possible to relax the assumption and allow more than one secret choice in a component, as long as there are no observable actions between the secret choices. But for the sake of simplicity in this paper we impose the more restrictive requirement. As a consequence, we have that the operational semantics of systems satisfies the following property: Proposition 2. If q ℓ → µ and q ′ ℓ ′ → µ ′ are both secret choices, then ℓ = ℓ ′ and there exist p i 's, q i 's and q ′ i 's such that:

µ = ⊙ i p i • δ(s i , q i ) and µ ′ = ⊙ i p i • δ(s i , q ′ i )
i.e., µ and µ ′ differ only for the continuation states.

Proof. Because of Assumption 1, there is only one component that can generate a secret choice, and it generates only one such choice. Due to the different possible interleavings, this choice can appear as an outgoing transition in more than one state of the TPA, but the probabilities are always the same, because the interleaving rule does not change them.

Given a system, each scheduler ζ determines a fully probabilistic automaton, and, as a consequence, the probabilities

P ζ (s, o) def = P ζ σ | σ ∈ Paths ⋆ (S), t x (σ) = o, secr (σ) = s
for each secret s ∈ S and observable o ∈ O x , where x ∈ {e, i, s}. Here secr is the map from paths to their secret action. From these we can derive, in standard ways, the marginal probabilities P ζ (s), P ζ (o), and the conditional probabilities

P ζ (o | s).
Every scheduler leads to a (generally different) noisy channel, whose matrix is determined by the conditional probabilities as follows: Definition 5. Let x ∈ {e, i, s}. Given a system and a scheduler ζ, the corresponding channel matrix C x ζ has rows indexed by s ∈ S and columns indexed by o ∈ O x . The value in (s, o) is given by

P ζ (o | s) def = P ζ (s, o) P ζ (s)
Given a scheduler ζ, the multiplicative leakage can be defined as L × (C x ζ , P ζ ), while the additive leakage can be defined as L + (C x ζ , P ζ ) where P ζ is the a priori distribution on the set of secrets (see preliminaries, Section 2). However, we want a notion of leakage independent from the scheduler, and therefore it is natural to consider the worst case over all possible admissible schedulers.

Definition 6 (x-leakage). Let x ∈ {e, i, s}. Given a system, the multiplicative leakage is defined as

ML x × def = max ζ∈Adm L × (C x ζ , P ζ ),
while the additive leakage is defined as

ML x + def = max ζ∈Adm L + (C x ζ , P ζ ),
where Adm is the class of admissible schedulers defined in the previous section.

We have that the classes of observables e, i, and s determine an increasing degree of leakage: Proposition 3. Given a system, for the multiplicative leakage we have

1. For every scheduler ζ, L × (C e ζ , P ζ ) ≤ L × (C i ζ , P ζ ) ≤ L × (C s ζ , P ζ ) 2. ML e × ≤ ML i × ≤ ML s ×
Similarly for the additive leakage.

Proof.

1. The property follows immediately from the fact that the domain O e is an abstraction of O i , and O i is an abstraction of O s .

2. Immediate from previous point and from the definition of ML x × and ML x + .

Strong anonymity (revised)

We consider now the situation in which the leakage is the minimum for all possible admissible schedules. In the purely probabilistic case, we know that the minimum possible multiplicative leakage is 1, and the minimum possible additive one is 0. We also know that this is the case for all possible input distributions if and only if the capacity of the channel matrix is 0, which corresponds to the case in which the rows of the matrix are all the same. This corresponds to the notion of strong probabilistic anonymity defined in [START_REF] Bhargava | Probabilistic anonymity[END_REF]. In the framework of information flow, it would correspond to probabilistic non-interference. Still in [START_REF] Bhargava | Probabilistic anonymity[END_REF], the authors considered also the extension of this notion in presence of nondeterminism, and required the condition to hold under all possible schedulers. This is too strong in practice, as we have argued in the introduction: in most cases we can build a scheduler that leaks the secret by changing the interleaving order. We therefore tune this notion by requiring the condition to hold only under the admissible schedulers.

Definition 7 (x-strongly anonymous). Let x ∈ {e, i, s}. We say that a system is x-strongly-anonymous if for all admissible schedulers ζ we have

P ζ (o | s 1 ) = P ζ (o | s 2 )
for all s 1 , s 2 ∈ Σ S , and o ∈ O x .

The following corollary is an immediate consequence of Proposition 3.

Corollary 8.

1. If a system is s-strongly-anonymous, then it is also i-strongly-anonymous.

2. If a system is i-strongly-anonymous, then it is also e-strongly-anonymous.

The converse of point [START_REF] Andrés | Information hiding in probabilistic concurrent systems[END_REF], in the previous corollary, does not hold, as shown by the following example:

s 2 . c 2 ) Q def = c 1 . o T def = c 2 . o
It is easy to check that S is e-strongly anonymous but not i-strongly anonymous, showing that (as expected) internal adversaries can "distinguish more" than external adversaries.

On the contrary, for point (1) of Corollary 8, also the other direction holds: Proposition 4. A system is s-strongly-anonymous if and only if it is i-stronglyanonymous.

Proof. Corollary 8 ensures the only-if part. For the if part, we proceed by contradiction. Assume that the system is i-strongly-anonymous but that P

ζ (o | s 1 ) = P ζ (o | s 2 ) for some admissible scheduler ζ and observable o ∈ O s . Let o = (enab(q), ℓ 1 , sift (α 1 )) • • • (enab(q n ), ℓ n , sift (α n )) and let o ′ be the projection of o on O i , i.e. o ′ = (ℓ 1 , sift (α 1 )) • • • (ℓ n , sift (α n )). Since the system is i-strongly- anonymous, P ζ (o ′ | s 1 ) = P ζ (o ′ | s 2 )
, which means that the difference in probability with respect to o must be due to at least one of the sets of available processes. Let us consider the first set L in o which exhibits a difference in the probabilities, and let o ′′ be the prefix of o up to the tuple containing L. Since the probabilities are determined by the distributions on the probabilistic choices which occur in the individual components, the probability of each ℓ ∈ L to be available (given the trace o ′′ ) is independent of the other labels in L. At least one such ℓ must therefore have a different probability, given the trace o ′′ , depending on whether the secret choice was s 1 or s 2 . And, because of the assumption on L, we can replace the conditioning on trace o ′′ with the conditioning on the projection o ′′′ of o ′′ on O i . Consider now an admissible scheduler ζ ′ that acts like ζ up to o ′′ , and then selects ℓ if and only if it is available. Since the probability that ℓ is not available depends on the choice of s 1 or s 2 , we have

P ζ (o ′′′ | s 1 ) = P ζ (o ′′′ | s 2 )
, which contradicts the hypothesis that the system is i-strongly-anonymous.

Intuitively, this result means that an s-adversary can leak information if and only if an i-adversary can leak information or, in other words, s-adversaries are as powerful as i-adversaries (even when the former can observe more information).

On the verification of strong anonymity: a proving technique based on automorphisms

As mentioned in the introduction, several problems involving restricted schedulers have been shown undecidable (including computing maximum/minimum probabilities for the case of standard model checking [START_REF] Giro | Quantitative model checking revisited: Neither decidable nor approximable[END_REF], [START_REF] Giro | Undecidability results for distributed probabilistic systems[END_REF]). These results are discouraging in the aim to find algorithms for verifying strong anonymity/noninterference using our notion of admissible schedulers (and most definitions based on restricted schedulers). Despite the fact that the problem seems to be undecidable in general, in this section we present a sufficient (but not necessary) anonymity proving technique: we show that the existence of automorphisms between each pair of secrets implies strong anonymity. We conclude this section illustrating the applicability of our proving technique by means of the DC protocol, i.e., we prove that the protocol does not leak information by constructing automorphisms between pairs of cryptographers. It is worth mentioning that our proving technique is general enough to be used for the analysis of leakage information of a broad family of protocols, namely any protocol that can be modeled in our framework.

The proving technique

In practice proving anonymity often happens in the following way. Given a trace in which user A is the 'culprit', we construct an observationally equivalent trace in which user B is the 'culprit' [START_REF] Halpern | Anonymity and information hiding in multiagent systems[END_REF][START_REF] Garcia | Provable anonymity[END_REF][START_REF] Mauw | A formalization of anonymity and onion routing[END_REF][START_REF] Hasuo | Probabilistic anonymity via coalgebraic simulations[END_REF]. This new trace is typically obtained by 'switching' the behavior of users A and B. We formalize this idea by using the notion of automorphism, cf. e.g. [START_REF] Rutten | Universal coalgebra: A theory of systems[END_REF].

Definition 9 (Automorphism). Given a TPA (Q, L, Σ, q, θ) we say that a bijection f :

Q → Q is an automorphism if it satisfies f (q) = q and q ℓ → ⊙ i p i • δ(α i , q i ) ⇐⇒ f (q) ℓ → ⊙ i p i • δ(α i , f (q i )).
In order to prove anonymity it is sufficient to prove that the behaviors of any two 'culprits' can be exchanged without the adversary noticing. We will express this by means of the existence of automorphisms that exchange a given pair of secret s i and s j .

Before presenting the main theorem of this section we need to introduce one last definition. Let S = (C) q 1 || • • • || q n be a system and M its corresponding TPA. We define M τ as the automaton obtained after "hiding" all the secret actions of M . The idea is to replace every occurrence of a secret s in M by the silent action τ . Note that this can be formalized by replacing the secret choice by a blind choice in the corresponding component q i of the system S.

We now formalize the relation between automorphisms and strong anonymity. We will first show that the existence of automorphisms exchanging pairs of secrets implies s-strong anonymity (Theorem 1). After, we will show that the converse does not hold, i.e., s-strongly-anonymous systems are not necessarily automorphic (Example 4).

Theorem 1. Let S be a system satisfying Assumption 1 and M its tagged probabilistic automaton. If for every pair of secrets s i , s j ∈ Σ S there exists an automorphism f of M τ such that for any state q we have q ℓ,si

-→ M q ′ =⇒ f (q) ℓ,sj -→ M f (q ′ ), (2)
then S is s-strongly-anonymous.

Proof. Assume that for every pair of secrets s i , s j we have an automorphism f satisfying the hypothesis of the theorem. We have to show that, for every admissible scheduler ζ we have:

∀ o ∈ O s : P ζ (o | s 1 ) = P ζ (o | s 2 ) .
We start by observing that for s i , by Proposition 2, there exists a unique p i such that, for all transitions q l → µ, if µ is a (probabilistic) secret choice, then µ(s i , -) = p i . Similarly for s j , there exists a unique p j such that µ(s j , -) = p j for all secret choices µ.

Let us now recall the definition of P ζ (o | s):

P ζ (o | s) def = P ζ (o ∧ s) P ζ (s) where P ζ (o ∧ s) def = P ζ ({π ∈ CPaths | t s (π) = o ∧ secr (π) = s})
with secr (π) being the (either empty or singleton) sequence of secret actions of π, and

P ζ (s) def = P ζ ({π ∈ CPaths | secr (π) = s}) .
Note that, since a secret appears at most once on a complete path, we have:

P ζ (s i ) = P ζ {π ℓ,si -→ σ ∈ CPaths | π, σ} = π ℓ,s i -→qi∈Paths ⋆ P ζ π ℓ,si -→ q i = last (π)
P ζ (o ∧ s i ) = P ζ π ℓ,si -→ σ ∈ CPaths | t s (π ℓ,si -→ σ) = o = π last (π) ℓ →µ µ secret choice P ζ (π) • p i • σ π ℓ,s i -→ σ∈Paths ⋆ ts(π ℓ,s i -→ σ)=o∧last (te(σ)) =τ P ζ (σ)
again using that a secret appears at most once on a complete path. Moreover, note that we have overloaded the notation P ζ by using it for different measures when writing P ζ (σ), since σ need not start in the initial state q. Analogously we have:

P ζ (o ∧ s j ) = P ζ π ℓ,sj -→ σ ∈ CPaths | t s (π ℓ,sj -→ σ) = o = π last(π) ℓ →µ µ secret choice P ζ (π) • p j • σ π ℓ,s j -→ σ∈Paths ⋆ ts(π ℓ,s j -→ σ)=o∧last (te(σ)) =τ P ζ (σ)
Therefore, we derive

P ζ (o | s i ) = π last (π) ℓ →µ µ secret choice σ π ℓ,s i -→ σ∈Paths ⋆ ts(π ℓ,s i -→ σ)=o∧last(te(σ)) =τ P ζ (π) • P ζ (σ) last (π) ℓ →µ µ secret choice P ζ (π) (3)
P ζ (o | s j ) = π last (π) ℓ →µ µ secret choice σ π ℓ,s j -→ σ∈Paths ⋆ ts(π ℓ,s j -→ σ)=o∧last (te(σ)) =τ P ζ (π) • P ζ (σ) last (π) ℓ →µ µ secret choice P ζ (π) (4)
Observe that the denominators of both formulae (3) and ( 4) are the same. Also note that, since f is an automorphism, for every path π, f (π) obtained by replacing each state in π with its image under f is also a path. Moreover, since f satisfies (2), for every path π ℓ,si -→ σ we have that f (π) ℓ,sj -→ f (σ) is also a path. Furthermore f induces a bijection between the sets

{(π, σ) | last (π) ℓ ′ → µ s.t. µ secret choice, π ℓ,si -→ σ ∈ Paths ⋆ t s (π ℓ,si -→ σ) = o, last (t e (σ)) = τ } and {(π, σ) | last (π) ℓ ′ → µ s.t. µ secret choice, π ℓ,sj -→ σ ∈ Paths ⋆ t s (π ℓ,sj -→ σ) = o, last (t e (σ)) = τ } given by (π, σ) ↔ (f (π), f (σ)).
Finally, since ζ is admissible, t s (π) = t s (f (π)), and f is an automorphism, it is easy to prove by induction that P ζ (π) = P ζ (f (π)). Similarly, P ζ (σ) = P ζ (f (σ)). Hence the numerators of ( 3) and ( 4) coincide which concludes the proof.

Note that, since s-strong anonymity implies i-strong anonymity and e-strong anonymity, the existence of such an automorphism implies all the notions of strong anonymity presented in this work. We now proceed to show that the converse does not hold, i.e., strongly-anonymous systems are not necessarily automorphic. + 0.5 : s 2 .(0.5 : (q : a + (1-q) : b) + 0.5 : ((1-q) : a + q : b))

It is easy to see that such system is s-strongly-anonymous, however if p = q and p = 1q there does not exist an automorphism for the pair of secrets (s 1 , s 2 ).

The following example demonstrates that our proving technique does not carry over to systems whose components admit internal parallelism. where q 1 |q 2 represents the parallel composition of q 1 and q 2 . It is easy to show that there exists an automorphism for s 1 and s 2 . However, admissible schedulers are able to leak such secrets. This is due to the fact that component r synchronizes with q and t on different channels, thus a scheduler of S is not restricted to select the same transitions on the branches associated to s 1 and s 2 (remember that schedulers can observe synchronization).

For the same reason, our proving technique does not extend to systems whose components contain nondeterminism. An example proving this point can be obtained from the previous one by replacing the parallel composition q 1 |q 2 with the nondeterministic composition q 1 + q 2 .

We now show that the definition of x-strong-anonymity is independent of the particular distribution over secrets, i.e., if a system is x-strongly-anonymous for a particular distribution over secrets, then it is x-strongly-anonymous for all distributions over secrets. This result is useful because it allows us to prove systems to be strongly anonymous even when their distribution over secrets is not known. Theorem 2. Consider a system S = (C) q 1 • • • q i • • • q n . Let q i be the component which contains the secret choice, and assume that it is of the form j p j : s j . q j . Consider now the system S ′ = (C) q 1 • • • q ′ i • • • q n , where q ′ i is identical to q i except for the secret choice, which is replaced by j p ′ j : s j . q j . Then we have that: 1. For every s i , s j there is an automorphism on S satisfying the assumption of Theorem 1 if and only if the same holds for S ′ .

2. S is x-strongly-anonymous if and only if S ′ is x-strongly-anonymous.

Note: 1) does not imply 2), because in principle neither S not S ′ may have the automorphism, and still one of the two could be strongly anonymous.

Proof. We note that the PAs generated by S and S ′ coincide except for the probability distribution on the secret choices. Since the definition of automorphism and the assumption of Theorem 1 do not depend on these probability distributions, (1) is immediate. As for (2), we observe that x-strong anonymity only depends on the conditional probabilities P ζ (o | s). By looking at the proof of Theorem 1, we can see that in the computation of P ζ (o | s) the probabilities on the secret choices (i.e. the p j 's) are eliminated. Namely P ζ (o | s) does not depend on the p j 's, which means that the value of the p j 's has no influence on whether the system is x-strong anonymous or not.

An Application: Dining Cryptographers

Now we show how to apply the proving technique presented in this section to the Dining Cryptographers protocol. Concretely, we show that there exists an automorphism f exchanging the behavior of the Crypt 0 and Crypt 1 ; by symmetry, the same holds for the other two combinations.

Consider the automorphisms of Master and Coin 1 indicated in Figure 5. The states that are not explicitly mapped (by a dotted arrow) are mapped to themselves.

Also consider the identity automorphism on Crypt i (for i = 0, 1, 2) and on Coin i (for i = 0, 2). It is easy to check that the product of these seven automorphisms is an automorphism for Crypt 0 and Crypt 1 .

Conclusion and future work

We have defined a class of partial-information schedulers which can only base their decisions on the information they have available. In particular they cannot base their decisions on the internal behavior of the components. We have used admissible schedulers to resolve nondeterminism in a realistic way, and to tune the definition of strong anonymity proposed in [START_REF] Bhargava | Probabilistic anonymity[END_REF].

Furthermore, we have presented a technique to prove the various definitions of strong anonymity proposed in the paper. This is particularly interesting considering that many problems related to restricted schedulers have been shown to be undecidable. In particular we have shown how to use the technique to original one w.r.t. anonymity. The following example illustrates our intuition. Example 6. Consider an electronic voting system EVS consisting of two components, P and Q, who can vote for two candidates 0 and 1. Each component selects the candidate by making a probabilistic choice: EVS = (p : 0.P [0]) + ((1p) : 1.P [START_REF] Alvim | Safe Equivalences for Security Properties[END_REF]) (q : 0.Q[0]) + ((1q) : 1.Q [START_REF] Alvim | Safe Equivalences for Security Properties[END_REF]).

We can transform EVS in the following system EVS ′ where the probabilistic choices are "centralized" and combined into one single choice, as follows:

EVS ′ = (c, d) VotesGenerator c(v).P [v] d(v).Q[v]
where VotesGenerator = (p q : c 0 . d 0 ) + (p (1q) : c 0 . d 1 ) + ((1p) q : c 1 . d 0 ) + ((1p) (1q) : c 1 . d 1 )

We believe that EVS and EVS ′ are equivalent, in the sense that EVS satisfies strong anonymity iff EVS ′ satisfies strong anonymity.

Figure 1 :

 1 Figure 1: Chaum's system for the Dining Cryptographers ([13])

Figure 2 :

 2 Figure 2: Dining Cryptographers CCS

Figure 3 :

 3 Figure 3: Dining Cryptographers Automata

Example 2 .

 2 Consider S def = ({c 1 , c 2 }) r q t, where r def = 0.5 : s 1 .c 1 .c 2 + 0.5 : s 2 .c 1 .c 2 , q def = c 1 .(0.5 : a 1 + 0.5 : b 1 ), t def = c 2 .(0.5 : a 2 + 0.5 : b 2 ).

Figure 4 :

 4 Figure 4: Screens intuition

Example 3 .

 3 Consider the system S def = ({c 1 , c 2 }) P || Q || T where P def = (0.5 : s 1 . c 1 ) + (0.5 :

  P ζ (π) • p i and analogously P ζ (s j ) = P ζ {π ℓ,sj -→ σ ∈ CPaths | π, σ} P ζ (π) • p j Let us now consider P ζ (o | s i ) and P ζ (o | s j ). We have:

Example 4 .

 4 Consider the following (single component) system 0.5 : s 1 .(0.5 : (p : a + (1-p) : b) + 0.5 : ((1-p) : a + p : b))

Example 5 .

 5 Consider S def = ({c 1 , c 2 }) r q t, where r def = 0.5 : s 1 .c 1 + 0.5 : s 2 .c 2 , q def = c 1 .(a | b), t def = c 2 .(a | b).

The notion proposed by Smith in[START_REF] Smith | On the foundations of quantitative information flow[END_REF] was given in a (equivalent) logarithmic form, and called simply leakage. For uniformity sake we use here the terminology and formulation of[START_REF] Braun | Quantitative notions of leakage for one-try attacks[END_REF].

The transitions from screens 4 and 5 represent 2 steps each (for simplicity we omit the τ -steps generated by blind choices)

Acknowledgement

The authors wish to thank Flavio Garcia, Pedro D'Argenio, Sergio Giro, and Mariëlle Stoelinga for useful comments on an earlier version of this paper, as well as the anonymous reviewers for thoroughly reading the paper and providing thoughtful recommendations.

 [START_REF] Alvim | Safe Equivalences for Security Properties[END_REF]Supported by NWO project 612.000.526. 2 Supported by the ANR project PANDA. 3 Supported by the Austrian Science Fund (FWF), Project V00125.

Master

( ( : : : : : : : prove that the DC protocol is strongly anonymous when considering admissible schedulers, in contrast to the situation when considering full-information schedulers.

We think that the results of this paper would hold also if we considered probabilistic schedulers (instead than deterministic ones). In a sense, the issue of probabilistic versus deterministic schedulers is orthogonal to the issue of partial versus full information schedulers, and to the problem of "taming" nondeterminism to avoid leakage.

For future work, we plan to investigate the decidability problem for the various definitions of strong anonymity we have proposed. Another interesting direction for future work is to extend well known isomorphism-checking algorithms and tools (see [START_REF] Foggia | A performance comparison of five algorithms for graph isomorphism[END_REF] for a survey) to our setting in order to verify automatically strong anonymity (in case an automorphism exists -recall that this is not a necessary condition).

Moreover, we plan to investigate the type of protocols that can be captured by our framework. We believe that we can cope also with systems which do not satisfy the restriction of secret choices being generated by a single component (Assumption 1). More precisely, we believe that our framework can be applied also to the case of system in which secret choices can occur in more than one component, provided that they occur at the beginning of the code (as it is often the case). The idea is to automatically transform the system into a new one satisfying Assumption 1, whose secret choice corresponds to the combination of the original ones, and in such a way that the new system is equivalent to the