1. Why were you initially drawn to the study of computation and randomness?

We encountered randomness in our different fields of interest, as unpredictable phenomena are omnipresent in natural and artificial processes. In classical physical systems (and by this we mean also relativistic ones) randomness may be defined as 'deterministic unpredictability'. That is, since Poincaré's results (on the Three Body Problem) and his invention of the geometry of dynamical systems, deterministic systems include various forms of chaotic ones, from weak (mixing) systems to ones highly sensitive to border conditions, where random behaviours are part of the deterministic evolutions. Randomness got a new status with the birth of quantum mechanics: access to information on a given systems passes through a nondeterministic process (measurement). In computer sciences, randomness is at the core of algorithmic information theory, all the while nondeterministic algorithms and networks present crucial random aspects. Finally, an extensive use of randomness is made also in biology.

Thus we wondered: all these different sciences refer to a concept of randomness, but is it really the same concept? And if they are different concepts, what is the relation between them?

Let us analyse in more detail the kind of randomness that emerges in the various disciplines.

Physical randomness (classical).

A kind of randomness can be viewed as a property of trajectories within classical dynamical systems, namely as unpredictability in finite time, over approximated physical measure with a given (non reducible) precision, [START_REF] Adler | Topological entropy and equivalence of dynamical systems[END_REF][START_REF] Alligood | Chaos: an introduction to Dynamical Systems[END_REF][START_REF] Devaney | An introduction to Chaotic Dynamical Systems[END_REF][START_REF] Bailly | Randomness and Determination in the interplay between the Continuum and the Discrete[END_REF][START_REF] Lighthill | The recent recognized failure of predictability in Newtonian dynamics[END_REF][START_REF] Laskar | Large scale chaos in the Solar System[END_REF]. Moreover, ergodicity (à la Birkhoff) provides a relevant and purely mathematical way to define randomness asymptotically, in the limit of infinite trajectories, which still applies for deterministic systems inspired by physics, but independently of chaotic properties (unpredictability) of physical processes, [START_REF] Cornfeld | Ergodic Theory[END_REF][START_REF] Longo | The Mathematics of Computing between Logic and Physics[END_REF]. In short, within these deterministic frames, randomness can be derived from a comparison between time averages (along a trajectory starting from a point) and space averages (over the entire space) of the chosen observables.

1.2. Physical randomness (quantum). Randomness in quantum mechanics has a special status, as it is of intrinsic origin. In contrast to other fields , including classical and relativistic physics, quantum randomness (QR) does not appear as a mean of "hiding" a kind of lack of knowledge, like, e.g., in statistical physics. The experimental evidence of the violation of the Bell's inequalities definitely proves that QR really belongs to the paradigm of the theory.

Yet, on the other side, QR fits perfectly well on the axiomatic setting of quantum mechanics, it is part of the 4 axioms of the so-called "Copenhagen" formalism, and the perfect coherence with the other postulates is a great success of the sciences of the last century.

Observe, in particular, that a quantum algorithm cannot avoid randomness, as it provides, as "output", i.e. the result of a final measurement process, a bunch of possibilities, one of them (fortunately the most probable) being the expected result. Therefore (easy) checking of the validity of a result must be part of the handled problem. The spectacular power of quantum algorithms, on the other side, overcomes this double constraint (randomness of the result and necessity of a posteriori validation of the "guess") and fully justifies this new branch of computer sciences. In this perspective, quantum randomness cannot be viewed as a form of (hidden or incomplete) determination, [START_REF] Feynman | Lectures in Physics[END_REF][START_REF] Anandan | Symmetries and Quantum Mechanics[END_REF].

1.3. Algorithmic randomness. Also recursion theory gave us a proper form of (asymptotic) randomness, for infinite sequences, in terms of Martin-Löf randomness, [START_REF] Martin-Loef | The definition of random sequences[END_REF] . This has been extensively developed by Chaitin, Schnorr, Calude and many others, [START_REF] Calude | Information and Randomness: An Algorithmic Perspective[END_REF], also in relation to physics, [START_REF] Rojas | Computability and Information in models of Randomness and Chaos[END_REF]. As a matter of fact, on the grounds of this theory one can give a precise meaning to vague notions such as "easily describable" and "regularities". In short, algorithmic randomness tests enables one to detect those elements whose regularities can be effectively tested, labeling them as "non-random". The elements that remain are called "random". Yet, the existing comparisons within (classical) physical randomness and algorithmic randomness are developed in formal space with insufficient physical generality. Some recent work went beyond this limit, [START_REF] Rojas | Computability and Information in models of Randomness and Chaos[END_REF].

1.4. Computer science randomness. Probabilistic and nondeterministic models of computation have been extensively investigated in the computer science literature, as well as their combination. Still there is no agreement about the precise nature of nondeterminism, and its relation with probability. In different areas the term nondeterminism refers to different concepts, and even in the same area people have different intuition and interpretation of nondeterministic models or phenomena (see for example [START_REF] Armoni | The Concept of Nondeterminism[END_REF] for a good survey). This confusion has brought consequences sometimes dramatic, especially when trying to transfer some theory or methodology from one field to another. One community which is particularly sensible to the problem is that of Computer Security. Although it was discovered only recently, the issue has rapidly become known and recognized as crucial, to the point that the organizers of the 2006 edition of the main forum in Computer Security, the IEEE FCS, set up a panel to discuss about nondeterminism.

In sequential computation the term nondeterminism refers to models in which the transition relation goes from one state to a set of states, like nondeterministic Turing machines. This is a useful device in specification, especially for search problems, in that it allows to explore alternative solutions without having to detail the backtracking policy. A characteristic of this kind of models is that their intended meaning is in terms of may-semantics, in the sense that the computation is considered successful if at least one of the alternative branches is successful. We argue that this has nothing to do with randomness: the re-execution of the system gives always the same result(s), and a deterministic implementation is always possible via backtracking (in a breath-first fashion to avoid that infinite branches would cause a pitfall).

In concurrency theory the situation is very different [START_REF]The difference between Sequential and Concurrent Computations[END_REF]: nondeterminism is inherent to the model, in the sense that it arises naturally from the concurrent execution and interaction of parallel processes. More precisely, it generates from the different ways in which processes may alternate their execution steps, cooperate with each other, compete for resources, etc. In general, these processes are assumed to run in different nodes of a distributed network, and the intended meaning is in terms of the must-semantics, in the sense that every branch must be successful, because the execution follows only one of the many alternatives, and backtracking is not an option (it would be too expensive, if possible at all, because all the processes would need to be backtracked, in order to ensure consistency). The reexecution of the system gives a different result each time, determined by run-time circumstances. In general we want to abstract from these, and we use the notion of scheduler to represent how the choices are resolved. 1.5. Biology. A common characteristic in the various forms of physical randomness is the predetermination of the spaces of possibilities: random results or trajectories are given among already known possible ones (the six sides of a dice, the spin-up/spin-down of a quanton...). In fact, in quantum physics, even in cases where new particles may be created, sufficiently "large" spaces are provided upstream (the Fock spaces of which Hilbert spaces): Fock's spaces capture all the possible states, infinitely many in general. The classical methods transfer successfully in molecular analysis in Biology, where only physical processes are observed, even though there are meant to happen within cells.

In System Biology, however, phase or reference spaces (that is, the spaces of possible evolutions) are far from being predetermined. Typically, the proper biological observables of Darwinian Evolution, namely phenotypes and species [26,[START_REF] Lecointre | Classification phylogénétique du vivant[END_REF], are not pre-given or there is no way to give them in advance within a space of all possible evolutions, in a sound theory. And, of course, there is no way to pre-give the possible molecular interactions (internal and systemic) as well as the feedbacks, from the forthcoming ecosystems onto molecular cascades. An analysis of Species Evolution, in terms of a diffusion equation (thus of underlying random paths) is given in [START_REF] Bailly | Biological Organization and Anti-Entropy[END_REF]. Our attention to the problem of randomness in System Biology was stimulated by these analogies and differences w. r. to Physics.

What have we learned?

Randomness is nowadays part of our culture. It appears everywhere. But, as mentioned before, it reflects very different kinds of conceptual (and mathematical) settings. Let us more closely review different forms of knowledge dealing with randomness in modern sciences.

Physical randomness (classical).

In classical dynamics, it is possible to give a notion of individual random element. More precisely, in a dynamical systems, with a transformation T preserving a measure µ, there exists a natural class of (asymptotic) properties allowing a definition of "random state" with respect to the dynamic T and the equilibrium distribution defined by µ. This class is the one associated to the Birkhoff ergodic theorem which states that for each (integrable) function f : X → R (representing a quantified observation), the time average of f along the orbit O(x) = {x, T (x), T 2 (x), ...} converges to the spacial mean f dµ with probability one. Such points are called typical for T [START_REF] V'yugin | Ergodic Theorems for Individual Random Sequences[END_REF]. Though given asymptotically, the definition has a robust physical meaning and it may be given for weakly chaotic dynamical systems : the mixing ones (that is, dynamical systems where observable decorrelates with time, see [START_REF] Galatolo | Effective symbolic dynamics, random points, statistical behavior, complexity and entropy[END_REF], [START_REF] Galatolo | A Constructive Borel-Cantelli lemma. Constructing orbits with required statistical properties[END_REF]).

Physical randomness (quantum).

The appearance of non-determinism in quantum mechanics was a shock. In the '20s Physics was still very rooted in the classical deterministic view of the world. Therefore it took a lot of time to accept this fact, although it appears totally natural now to us that a description on the world could be fully statistical. This randomness flavour of quantum mechanics is usually handled in the so-called field of "conceptual aspects" of the theory, [START_REF] Jammer | The philosophy of quantum mechanics : the interpretations of quantum mechanics in historical perspective[END_REF]. Facing these conceptual aspects with new experimental physics is not so frequent, and the relationship with other fields, as the ones presented here, are even less often considered. At the meantime recent works (see [START_REF] Paul | La méeanique quantique vue comme processus dynamique[END_REF][START_REF] Paul | Échelles de temps pour l'évolution quantique à petite constante de Planck[END_REF][START_REF] Paul | Semiclassical analysis and sensitivity to initial conditions[END_REF][START_REF] Paul | À propos du formalisme mathématique de la Mécanique Quantique[END_REF]) started invoking these links. Let us finally mention a kind of philosophical morality: the high new power of quantum algorithms relies on randomness, that is, releasing determinism (in a way of keeping probability predictions) increases drastically efficiency.

Algorithmic randomness.

As already mentioned, the notion of individual random infinite sequence has been effectively modeled with the tools of computability theory. The idea is that statistical tests may be "effectively given", that is one can effectively look for regularities along infinite sequences. Then an infinite sequence is random if it passes all effective tests. This algorithmic modelling of randomness has been formalized in different ways and there exist several definitions (the one by Martin-Löf's, in [START_REF] Martin-Loef | The definition of random sequences[END_REF], being the most celebrated, see [START_REF] Calude | Information and Randomness: An Algorithmic Perspective[END_REF] for a survey book).

In these approaches, being random yields a high degree of "non-computability", as a random sequence has no infinite recursively enumerable subset. The role of algorithmic randomness in dynamical systems, especially in ergodic ones, has already be the subject of previous research. However, without a more general theory of randomness, all this work is restricted to "symbolic spaces" (spaces of strings), with little physical meaning. The non-obvious results recently obtained proved an equivalence, in very general and "physically meaningful" dynamical spaces, of the (classical) physical randomness, à la Birkhoff, and algorithmic randomness, for infinite trajectories (see the PhD theses by M. Hoyrup and C. Rojas (June 2008) and [START_REF] Galatolo | Effective symbolic dynamics, random points, statistical behavior, complexity and entropy[END_REF][START_REF] Galatolo | A Constructive Borel-Cantelli lemma. Constructing orbits with required statistical properties[END_REF][START_REF] Longo | Randomness and Determination, from Physics and Computing towards Biology[END_REF]).

As for finite time computations, Chaitin, Levin, Calude and many others, following Kolmogorof, deeply analysed also (finite) sequence incompressibility (sequences whose length coincides with their shortest generating program) and showed that for infinite sequences, under suitable conditions, the incompressibility of initial segments yields Martin-Löf asymptotic randomness. But, in our opinion, unless the physical generating process is spelled out, a finite incompressible sequence is not random, it is just algorithmically incompressible. In other words, it is pseudorandom in the strongest way and it is impossible to see in it any regularity whatsoever. Conversely, it is a reasonable thesis to assume that a physical random sequence is incompressible, in principle, but the converse is false or ill defined. That is, if one stays within theory of computation and no physical process is mentioned, there is no other way to give/conceive it but by a program, a formal/linguistic matter, a priori with no physical meaning. A closer analysis of this issue is part of our project, in view of our experience on the relation physical (dynamical) vs. algorithmic randomness.

2.4.

Randomness in computer science. As argued in previous section, sequential systems are inherently deterministic (despite the use of the adjective 'nondeterministic' for the automata whose transition relation is one-to-many). Concurrency, on the contrary, seems to give rise to a true notion of randomness, due to the unpredictable and unbacktrable nature of interaction between independent and asynchronous agents.

The fact that computation in concurrent systems seems to have features which are basically different from those of sequential computation has inspired some intriguing lines of research, with the common goal of defining a 'good' notion of expressiveness for concurrent formalisms. One of the most successful approaches is based on the notions of 'encoding', and it has produced some interesting results concerning the mechanisms of guarded choice, which are intimately related to the nature of nondeterminism in concurrency. We mention in particular the works by Nestmann and Pierce [START_REF] Nestmann | Decoding Choice Encodings[END_REF], and by Palamidessi [START_REF] Palamidessi | Comparing The Expressive Power Of The Synchronous And Asynchronous Pi-Calculi[END_REF][START_REF] Parrow | Expressiveness of Process Algebras[END_REF]. The first have shown that a certain form of choice (input-guarded choice) can be encoded in parallelism, while the latter has shown that mixed-guarded choice is essentially more expressive.

Another line of investigation has been pursued by Wegner and his collaborators. Starting from the principle that interaction is more expressive than algorithms, Wagner has written an intriguing position paper where he justifies this claim, essentially on the basis of the intuition that interaction can express random computation [START_REF] Wegner | Interactive Foundations of Computing[END_REF]. In the technical development of this idea in subsequent papers [START_REF] Wegner | Coinductive Models of Finite Computing Agents[END_REF][START_REF] Goldin | Turing Machines, Transition Systems, and Interaction[END_REF] the authors considered a sort of interactive Turing machines (persistent Turing machines) and showed that they cannot be reduced to standard Turing machines. However the approach is based on the conventional interpretation of nondeterminism in automata theory.

An interesting result has bee found recently by Busi and her colleagues [START_REF] Busi | Replication vs. Recursive Definitions in Channel Based Calculi[END_REF]: they investigate a process calculus (CCS with replication) and show that in this calculus the existence of a divergent path is decidable. Still, in a subsequent paper [START_REF] Busi | Comparing Recursion, Replication, and Iteration in Process Calculi[END_REF] they show that this formalism can encode Turing machines. The explanation of this apparent paradox is that the nondeterminism of the language is essential to achieve Turing-completeness: any attempt to eliminate it in an effective way is doomed to fail, because otherwise decidability of (existence of) divergence would imply decidability of termination.

In all the above investigations nondeterminism plays a central role: since in concurrency there is no backtracking, it becomes important to control nondeterminism as much as possible, and the expressive power of a concurrent language usually lies on the capability to exert such control.

In a more practical fashion, nondeterminism has been used in concurrency theory as a convenient abstraction from run-time information. Essentially, a concurrent program is nondeterministic because when we write it we do not know yet what will determine at run-time the choice of a particular path, so all the possibilities must be considered.

A common misconception of nondeterminism is to consider it a probabilistic mechanism with uniform distribution. The confusion probably originates from epistemic considerations: the total lack of knowledge about which of the available alternatives will be chosen, in a nondeterministic process, evokes the concept of maximum entropy. But maximum entropy represents the maximum degrees of uncertainty within the probabilistic setting. Nondeterminism is outside the realm of probability and it represents an even higher degree of uncertainty. In any case, confusing nondeterminism with uniform probability has induced wrong approaches. We argue that this due to several aspects: not only a nondeterministic property cannot express the quantitative aspects of a probabilistic one, but also this transformation requires angelic nondeterminism (nondeterminism working in favour of the property), which is a strong assumption usually not guaranteed in a concurrent setting (where nondeterminism is typically demonic).

2.5. Biology. We have no doubt that the issue of randomness in biology is extremely difficult, yet it is amazing to observe that leading biologists, still now and along the lines of Crick and Monod ( [40]), contrapose determination and randomness according to Laplace's split: deterministic means predictable and random is its opposite (non-deterministic), to be analyzed by statistics and probabilities. Along these laplacian lines, deterministic, as it implies predictability (Laplace's conjecture), yields "programmable", which leads to the the idea that the "DNA is a program" (see [START_REF] Keller | The Century of the Gene[END_REF] for an history.) Yet, since Poincaré (1890), we know that classical randomness is deterministic unpredictability and that unpredictability pops out almost everywhere in non-linear systems (see [START_REF] Longo | The differential method and the causal incompleteness of Programming Theory in Molecular Biology[END_REF] for a critique of the claim that "DNA is a program" from the point of view of Physics and Programming Theory.)

In short, determination as "necessity" in life phenomena, understood in a laplacian way, is far from the frameworks of modern determination in physics, classical or quantum, even if it is supplemented by a few speckles of randomness (le "hasard"). Crick's "central dogma" ("Genetic Information" goes one-way, from DNA to RNA to proteins -and to the phenotype) and the "one gene -one enzyme" hypothesis in Molecular Biology are good examples of this. They guided research for decades and, the first, is still nowadays believed by many, modulo the addition of a few "epigenetic factors" and "norms of reaction" (for an alternative view, see [START_REF]Le hasard au coeur de la cellule[END_REF]; more discussions and references are in [START_REF] Longo | The differential method and the causal incompleteness of Programming Theory in Molecular Biology[END_REF]). By their linear causality, these assumptions do not seem to have still integrated the views on the interplay of interactions in XXth century physics, that is the richness of the approaches to physical determination and randomness. In these modern physical frames, causes become interactions and these interactions themselves dynamically constitute the fabric of the processes and of their manifestations; reshaping this fabric modifies the interactions, intervening upon the interactions appears to reshape the fabric, [START_REF] Bailly | Mathématiques et sciences de la nature. La singularité physique du vivant[END_REF].

Our recent work on entropy in System Biology, [START_REF] Bailly | Biological Organization and Anti-Entropy[END_REF], has been extensively borrowing from the work on far-from-equilibrium thermodynamics, in particular dissipative systems ( [START_REF] Nicolis | Self -Organization in Nonequilibrium Systems[END_REF][START_REF] Nicolis | Dissipative systems[END_REF]). Note that entropy provides a measure for "increasing randomness" also for dynamical systems and this establishes a link, developed by many, with other areas of physics (thermodynamics).

What are the most important open problems in the field?

"Random" is not the opposite of "deterministic", in spite of the opposition of these concepts that is commonly made in Computer Science and Biology. As a matter of fact, the analysis of randomness is part of the proposal for a structure of determination of physical processes, in particular in classical dynamics, where randomness is deterministic unpredictability. But it is so also when it is related the very precise and specific notion of quantum indetermination and quantum measure of "deterministic evolutions of the state function" (determined by Schrödinger equation).

As seen in the previous sections, randomness and nondeterminism appear at least in four thematic fields (mathematics, physics, biology and computer sciences). Yet, they cover different, sometimes antinomic meanings.

3.1. Algorithmic randomness. Since Chaitin's 1975 construction of the first random infinite word, an entire robust field has been opened concerning the combinatorial properties of randomness in discrete frames. This is leading to an interesting analysis of infinite sequences and cycles in de Bruijn graphs, for example, and a lot more in finite and infinite combinatorics.

A way to stress the difference and the strength of the approach we worked at, is that, given a measurable space of measure µ, classical theorems like "property P holds for µ-almost every point" can be converted into "property P holds for every µ-random point", and this in physical dynamics. Now, the notion of "being (µ-)random", relatively to a measure µ, is fully understood, by the many result in algorithmic randomness and, in particular, by our team's work on asymptotic randomness, relating classical (dynamical) and algorithmic randomness. In short, a major point of these results, is given by the use of discrete, though asymptotic, tools from algorithmic randomness, in applications to continuous dynamics. By this, our approach, by its relation to physically meaningful dynamical systems, complements the relevant existing work on algorithmic randomness. Further applications (or correlations between) the recent ideas in algorithmic randomness, like the ones developed by the authors above, and our understanding of classical (and quantum) dynamics is one of the paths to be explored. In particular, a typical example of cross interest is given by the analysis of normality in the sense of Borel1 : a real number is absolutely normal with probability one, but constructing such points is extremely complicate [START_REF] Becher | An example of a computable absolutely normal number[END_REF]. However, it is widely accepted that computable simulations show the right ergodic behaviour [START_REF] V'yugin | Ergodic Theorems for Individual Random Sequences[END_REF]. Is it the case also while modelling relevant physical dynamics? and which ones? We will hint below on how a relation to our approach can be developed.

Computer science.

In section 2, we mentioned the ambiguities we see in the transfer of notions from algorithmic randomness (an asymptotically well-defined notion) to finite time computations. Some may see our questioning as referring to a terminological nuance, yet too much confusion in computing deserves clarification. Consider, say, a so called "non-deterministic" Turing Machine. This is just a formal, deterministic device, associating a set of numbers to a number. Its evolution is determined by an ill-typed input-output function. Indeed, it is a useful device as it allows to speed up computations by a form of basic parallelism. Yet, as long a physical process, choosing, at each step, one or a few of the elements in the output set, is not proposed, one cannot discuss about "determination" nor "randomness": is it classical? quantum? This is an analogue of the problem posed for finite "random" (incompressible!) sequences mentioned above. A major clarification is needed here, as the relation between the abuses of "non-deterministic", "random" in Computer Science deserve a close analysis in terms of their relation to the underlying physical processes.

We need to tackle this problem within the relevant area which mostly interests, concurrency and networks. In particular, the following three main objectives seem relevant:

Clarify the nature of nondeterminism in concurrency. As discussed in previous sections, there is a lot of confusion about this concept, especially in the way the notions and tools developed in the area of concurrency get applied in other areas. We feel that this is because the concept of nondeterminism is still missing a proper characterization, formalization, and theoretical foundations. The way it is formalized in process calculi, indeed, makes it easy to confuse it with the 'nondeterminism' of automata theory, which, as argued previously, has a radically different nature.

Investigate and formalize the difference of concurrent computations with respect to sequential ones. With respect to Wegner's claim that 'interaction is more powerful than algorithms' on the basis of the fact that interactive (concurrent) systems can create real random sequences, our position is: we actually do not believe that it is a matter of interaction having a superior expressive power (if anything, it should be the reverse -randomization witnesses a lack of control capabilities), but certainly the capability of producing randomness sharply separates interactive (concurrent) computations from algorithmic (sequential) ones. Once this characterization in terms of randomness is given, we can also explore whether we can characterize different classes of random sequences, which would induce a separation in the concurrent formalisms (and mechanisms) that can produce them.

Explore the use of physical randomness (classical and quantum) for computer science applications that use randomized mechanism to protect secret information. Typically randomization is used to obfuscate the link between secrets and observables, and the use of really unpredictable mechanisms (in contrast to the pseudo random ones) is critical. Examples of such applications are protocols for privacy, anonymity, and confidentiality [START_REF] Schneider | CSP and Anonymity[END_REF], like Crowds and DCnets. How non-linear systems, reflecting classical randomness, or intrinsic quantum randomness can help in the developments of these areas? 3.3. Biology. A long term ambition would be to obtain, by mathematics if possible, a clarification of the not so much explored problem of randomness in System Biology (again, in Molecular Biology, randomness plays a novel but fundamental role, but the tools and concepts are borrowed from Physics, via Chemistry). As we said, in a systemic approach to Biology, one of the challenges, as for our project, is that species (and phenotypes) are co-constituted with their environment.

To make an analogy with the reasons for chaos in planetary systems, some sort of "resonance effect" takes place in this co-constitutive process. The difference is that in the physical deterministic case, the resonance happens at one (and conceptually simple) level: the gravitational interactions between a few planets, fully determined by Newton-Laplace equations. In Evolution (but also in ontogenesis), the resonance takes place between different levels of organization, each deserving an analysis on terms of an appropriate structure of determination (typically, fractal structures or geodetics in morphogenesis, see [START_REF] Jean | Phyllotaxis : a systemic study in plant morphogenesis[END_REF], vs. networks dynamics in cellular/neural tissues, see [START_REF] Hertz | Introduction to the Theory of Neural Computation[END_REF].

That is, a systemic approach requires an analysis of interactions between species, individuals, physical landscapes, but also organs and tissues and, very importantly, by two ways interactions between these levels and molecular activities, starting with DNA expression. Moreover, molecular events belong to microphysics, thus possibly subject to quantum analysis, thus, quantum probabilities. By this, one would need a theory encompassing both classical randomness, which may better fit the description of macroscopic interactions, and quantum randomness, as they may be retroacting one on top of the other. We are far form having such a theory, even in Physics.

In conclusion, Physics has been able to propose two different notions of randomness in finite time: classical deterministic unpredictability and quantum randomness. As we mentioned, we proved that they merge in infinite time. Biology badly needs its own notion, while in search, of course, for unification with physical (molecular?) structures of determination. We observe that the notions of "extended criticality" and "anti-entropy" (the opposite of "increasing disorganization or randomness", yet differing from the classical negative entropy) recently proposed in [START_REF] Bailly | Biological Organization and Anti-Entropy[END_REF], [START_REF] Bailly | Extended Critical Situations[END_REF] seem pertinent. They deeply involve randomness in Biology, by the role of fluctuations in extended criticality and of random paths in the formation and growths of anti-entropy. Feasibility of the construction of quantum computers is certainly one of the most challenging perspective in physics. More generally experimental exhibition of single phenomena in quantum mechanics is certainly one of the most striking success of sciences of the last 25 years. In the mean time computer science developed, independently, in a direction where non-determinism took an increasing place. An objective would be to exhibit links between these two independent developments, together with possible oppositions. As a bi-product, incidence of the rich computer network theory on quantum mechanics is also expected to be strengthened. [START_REF] Anandan | Symmetries and Quantum Mechanics[END_REF]. What are the prospects for progress? 4.1. Quantum randomnesses. One of the subjects that should be seriously carried out is the difference, in quantum mechanics, between two different type of randomnesses: the one obtained through decoherence and the one of the measurement process (see [START_REF] Haroche | Exploring the quantum : atoms, cavities and photons[END_REF]). Indeed it is often said that decoherence presents a satisfactory "explanation" of quantum measurement. Let us remind that the phenomenon of decoherence is the action on a "small" quantum system of the big quantum surrounding system (e.g. the apparatus). In the limit of infinite "reservoir" the state of the small system gets a diagonal feature that one can identify with a statistical mixture. This last one is sometimes and wrongly presented as reflecting the quantum randomness, as randomness in statistical mechanics. This point of view, driven by a pure statistical perception of quantum phenomena, must be corrected, as more and more single events in quantum mechanics are nowadays shown experimentally. It seems to us that a clarification of the link between this dichotomy between (not intrinsic) randomness and the true (intrinsic) one on the quantum side, and the same kind of distinction in the other fields presented all a long this paper, would be a major achievement. 4.2. Pseudo-randomness and algorithmic randomness. Computer simulations (the trajectory given in some initial condition and drawn on the screen) has become a very important component of the analysis of physical dynamics. The problem is that an algorithmically random point is strongly non-computable, and consequently it is impossible to observe the trajectory of such a point in a computer simulation. Worst, the set of computable points has probability 0! From the simulation point of view, the fact that a given property holds with probability one says nothing about its observability with a computer. A typical example is (absolute) normality in the sense of Borel, but, as we mentioned, constructing such points is extremely complicate.

As already mentioned, in spite of this intrinsic (mathematical) difficulties, it is widely accepted that computable simulations display the right ergodic behaviour. The evidence is mostly heuristic. More precisely, most arguments are based on the various "shadowing" theorems. By these results, it is possible to prove that in a suitable system any "pseudo"-trajectory, that is a trajectory obtained by a simulation with round-off, is approximated by a real (continuous) trajectory of the system (but, in general, not the converse). The main limit of this approach is however that shadowing results hold only in particular systems ("hyperbolic" dynamics), while many physically interesting systems do not need to belong to this class. Can we extend this frame for shadowing to an analysis of randomness for the systems of biological and physical relevance, both for finite and infinite processes? What does this mean in a quantum perspective? Moreover and as observed in the previous sections, algorithmically random points are those points which have the "generic" behavior, as prescribed by the underlying measure. In a sense, they are physically "randomized", as they do not possess any artificial feature related to the particular supporting space. An open issue would be to turn this into a mathematical frame, where the only role of the measure would be to distinguish the set of random points and give them a topological structure. Once this is done, probabilistic theorems can be formulated and proved using the structure of the random set and topological methods (without referring to the measure). 4.3. Computer science. The objectives proposed in previous section should be pursued by applying the following approaches and methodologies:

Clarify the nature of nondeterminism in concurrency. The results and perspectives developed in mathematics and physics and quoted above should be more closely used to get new insights that can be used to understand in depth the notion of nondeterminism in concurrency, in its intrinsically random nature. On this basis:

Formalize the difference between concurrent and sequential computation in terms of randomness. What about the applicability of Martin-Löf definition of randomness to give this characterization? Explore the use of physical randomness (classical and quantum) for computer science applications. Typically, it should be explored the possible use of different kinds of randomness in quantum mechanics (see the paragraph on quantum randomnesses in this section), as well as the extensively studied relations between computational and dynamical randomness in enriching/clarifying randomness in finite computing: how can this affect computing? (on a conceptual basis? by the relevance of hardware?) 4.4. Extended Criticality in Biology. In recent work [START_REF] Bailly | Extended Critical Situations[END_REF] we proposed to analyze the state of living matter as "extended critical state". The idea is that an organism is in a permanent critical transition, constantly reconstructing its own organization. The well established domain called "physics of criticality" [START_REF] Lagues | Invariance d'echelle[END_REF] necessarily deals with point-wise critical transitions: this is part of the very definition of phase transition and it is used in an essential way by the main mathematical tool in the approach, the "renormalization methods" ( [START_REF] Delamotte | A hint of renormalization[END_REF]) In ongoing work, we consider, instead, a set (whose closure is) of null-measure, an extended interval of criticality w.r. t. all pertinent parameters (time, temperature, pressure...). It is as if a snow flake (a "coherence structure", formed at a critical transition) could stand variations within a relatively large interval of its control parameters by continually reconstructing itself, in a permanent "going through" the critical transition (extended criticality applies to far from equilibrium, dissipative and not necessarily steady states). One then has an extended, permanently reconstructed global organization in a dynamic interaction with local structures, as the global/local interaction is proper to critical transitions. The role of randomness in these context is crucial, yet to be explored: the structural stability of the system may be seen as stability w. r. t. perturbations within the margins of criticality. Moreover, the very construction of the coherent state is obtained from fluctuations from an initial relatively stable state. The point now is to turn these conceptually robust ideas into sound mathematics. As the normalization methods cannot work, by principle (non-pointwise nature of the critical "transition"), how to describe and handle rigorously extended criticality and its main properties (the establishment and maintainance of the global coherent structure, its structural stability and complexity, in particular in relation to random events)?

Extended criticality, a notion modeling organisms as "extended coherence structures" (our proposal for structurally stable systems), needs also to be merged with the work on entropy and anti-entropy in Species Evolution, mentioned above, see [START_REF] Bailly | Biological Organization and Anti-Entropy[END_REF]. The possible technical link may reside in the role of randomness in both analyses. This shows up in fluctuations and resistance to perturbations (average behaviours?), as for extended criticality, in diffusion equations (thus, in underlying random paths) as for entropy and anti-entropy. In this frame, one needs to further analyse the role of time and of diffusion equations (which average random paths) both in phylogenesis (we already carried on a mathematical analysis of this in [START_REF] Bailly | Biological Organization and Anti-Entropy[END_REF]) and in ontogenesis, an open issue. 4.5. Comparison. It should be clear that the many forms of randomness above differ or, in some cases, are not or ill formalized. Yet, as already mentioned, some recent results of our's prove that they merge, asymptotically. In particular, we recall, one of us proved an asymptotic merging of quantum and classical randomness at the so-called "semi-classical limit" [START_REF] Paul | Semiclassical analysis and sensitivity to initial conditions[END_REF] and the team of another of us proved a form of equivalence between Birkhoff physical randomness, a limit notion, and algorithmic randomness ( [START_REF] Longo | Randomness and Determination, from Physics and Computing towards Biology[END_REF] for a survey). This poses several open questions, for example in the correlations in finite time of classical, quantum and algorithmic randomness, an issue extensively studied by many, since the asymptotic analysis may propose a new perspective. Moreover, as we said, the computational approach (algorithmic randomness) is far from being related to the modern forms of randomness in networks and concurrency. Not to mention the very difficult and rather confusing situation we can witness in Biology, when coming from more mathematized disciplines.

3. 4 .

 4 Quantum mechanics. Since the beginning of the '80s, and especially the fundamental experiments by Aspect et al, showing the violation of Bell's inequalities, quantum mechanics has got the status of "true" theory of the microscopic world. Roughly at the same time appeared the beginning of what is called now quantum information and quantum computing.

A "normal number" is a real number whose digits in every base show a uniform distribution, with all digits being equally likely, all pairs of digits equally likely, all triplets of digits equally likely, etc..[START_REF] Becher | Turing's unpublished algorithm for normal numbers[END_REF]


Mário S Alvim

Miguel E Andrés

Catuscia Palamidessi

Peter Van Rossum

Safe Equivalences for Security Properties

In the field of Security, process equivalences have been used to characterize various information-hiding properties (for instance secrecy, anonymity and non-interference) based on the principle that a protocol P with a variable x satisfies such property if and only if, for every pair of secrets s1 and s2, P [ s 1 /x] is equivalent to P [ s 2 /x]. We argue that, in the presence of nondeterminism, the above principle relies on the assumption that the scheduler "works for the benefit of the protocol", and this is usually not a safe assumption. Non-safe equivalences, in this sense, include complete-trace equivalence and bisimulation. We present a formalism in which we can specify admissible schedulers and, correspondingly, safe versions of these equivalences. We prove that safe bisimulation is still a congruence. Finally, we show that safe equivalences can be used to establish information-hiding properties.

Introduction

One of the fundamental problems in computer security is the protection from information leaks, namely how to make sure that a system does not reveal, by observations that can be made during the execution, some information that we wish to maintain secret.

One way to prevent an attacker to infer the secret from the observables is to create noise, namely to make sure that for every execution in which a given secret produces a certain observable, there is at least another execution in which a different secret produces the same observable. In practice this is often done by using randomization, see for instance the DCNet [START_REF] Chaum | The dining cryptographers problem: Unconditional sender and recipient untraceability[END_REF] and the Crowds [START_REF] Reiter | Crowds: anonymity for Web transactions[END_REF] protocols.

In the literature about the foundations of Computer Security, however, the quantitative aspects are often abstracted away, and probabilistic behavior is replaced by nondeterministic behavior. Correspondingly, there have been various approaches in which information-hiding properties are expressed in terms of equivalences based on nondeterminism, especially in a concurrent setting. For instance, [START_REF] Schneider | CSP and anonymity[END_REF] defines anonymity as follows 1 : A protocol S is anonymous if, for every pair of culprits a and b, S[ a / x ] and S[ b / x ] produce the same observable traces. A similar definition is given in [START_REF] Abadi | A calculus for cryptographic protocols: The spi calculus[END_REF] for secrecy, with the difference that S[ a / x ] and S[ b / x ] are required to be bisimilar. In [START_REF] Delaune | Verifying privacy-type properties of electronic voting protocols[END_REF], an electoral system S preserves the confidentiality of the vote if for any voters v and w, the observable behavior of S is the same if we swap the votes of v and w. Namely,

S[ a / v | b / w ] ∼ S[ b / v | a / w ],
where ∼ represents bisimilarity.

These proposals are based on the implicit assumption that all the nondeterministic executions present in the specification of S will always be possible under every implementation of S. Or at least, that the adversary will believe so. In concurrency, however, as argued in [START_REF] Chatzikokolakis | Bisimulation for demonic schedulers[END_REF], nondeterminism has a rather different meaning: if a specification S contains some nondeterministic alternatives, typically it is because we want to abstract from specific implementations, such as the scheduling policy. A specification is considered correct, with respect to some property, if every alternative satisfies the property. Correspondingly, an implementation is considered correct if all executions are among those possible in the specification, i.e. if the implementation is a refinement of the specification. There is no expectation that the implementation will actually make possible all the alternatives indicated by the specification.

We argue that the use of nondeterminism in concurrency corresponds to a demonic view: the scheduler, i.e. the entity that will decide which alternative to select, may try to choose the worst alternative. Hence we need to make sure that "all alternatives are good", i.e. satisfy the intended property. In the above mentioned approaches to the formalization of security properties, on the contrary, the interpretation of nondeterminism is angelic: the scheduler is expected to actually help the protocol to confuse the adversary and thus protect the secret information.

There is another issue, orthogonal to the angelic/demonic dichotomy, but relevant for the achievement of security properties: the scheduler should not be able to make its choices dependent on the secret, or else nearly every protocol would be insecure, i.e. the scheduler would always be able to leak the secret to an external observer (for instance by producing different interleavings of the observables, depending on the secret). This remark has been made several times already, and several approaches have been proposed to cope with the problem of full-information scheduler (aka almighty, omniscient, clairvoyant, etc.), see for example [START_REF] Canetti | Taskstructured 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][START_REF] Andrés | Information hiding in probabilistic concurrent systems[END_REF].

The risk of a naive use of nondeterminism to specify a security property, is not only that it may rely on an implicit assumption that the scheduler behaves angelically, but also that it is clairvoyant (fully-informed), i.e. that it peeks at the secrets (that it is not supposed to be able to see) to achieve its angelic strategy.

Example 1. Consider the following system, in a CCS-like syntax:

S def = (c)(A H 1 H 2 Corr ), with A def = c sec , H 1 def = c(s).out a , H 2 def = c(s).out b , Corr def = c(s).out s .
Here is the parallel operator, c sec is a process that sends sec on channel c, c(s).P is a process that receives s on channel c and then continues as P , and (c) is the restriction operator, enforcing synchronization on c. The name sec represents a secret.

It is easy to see that we have S [ a / sec ] ∼ S b / sec . Note that, in order to simulate the third branch in S [ a / sec ], the process S b / sec needs to select its first branch. Viceversa, in order to simulate the third branch in S b / sec , the process S [ a / sec ] needs to select its second branch. This means that, in order to achieve bisimulation, the scheduler needs to know the secret, and change its choice accordingly.

This example shows a system that intuitively is not secure, because the third component, Corr , reveals whatever secret it receives. However, according to the equivalencebased notions of security discussed above, it is secure. But it is secure thanks to a scheduler that angelically helps the system to protect the secret, and it does so by making its choices dependent on the secret. We consider these assumptions on the scheduler excessively strong.

We do not claim, however, that we should rule out the use of angelic nondeterminism in security: on the contrary, angelic nondeterminism can be a powerful specification concept. We only advocate a cautious use of this notion. In particular, it should not be used in a context in which the scheduler may be in collusion with the attacker. The goal of this paper is to define a framework in which we can combine both angelic and demonic nondeterminism in a setting in which also probabilistic behavior may be present, and in a context in which the scheduler is restricted (i.e. not fully-informed). We define "safe" variant of typical equivalence relations (complete traces and bisimulation), and we show how to use them to characterize information-hiding properties.

Contribution

The main novelties of our work can be articulated as follows:

• We propose a formalism for concurrent systems which accounts for both probabilistic and nondeterministic behaviour, and in which the latter is of two kinds: global and local. The first represents the possible interleavings produced by the parallel components, which may be influenced by the attacker. The second is associated to the possible choices internal to each component, which may depend on the secrets or other unknown parameters, not controlled by the attacker. Correspondingly, we split the scheduler in two constituents: global and local. The latter is actually a tuple of local schedulers, one for each component of the system. • We propose a notion of admissible scheduler for the above systems, in which the global constituent is not allowed to see the secrets, and each local constituent is not allowed to see any information about the other components. We then generalize the standard definition of strong (probabilistic) information hiding (such as nointerference and strong anonymity) to the case in which also nondeterminism is present, under the assumption that the schedulers are admissible. • We use admissible schedulers to define safe versions of complete-trace equivalence and bisimilarity especially tuned for security (in this paper we often refer to complete traces as simply traces). This means that we account for the possibility that the global constituent of the scheduler is in collusion with the attacker, and therefore does not necessarily help the system to obfuscate the secret. We show that the latter is still a congruence, like in the classical case. • We finally show that our notions of safe trace equivalence and bisimilarity imply strong information hiding in the above sense.

A function µ : Q → [0, 1] is a discrete probability distribution on a set Q if the support of µ is countable and 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 α is a transition function α : Q → P(Σ×D(Q)). Here P(X) is the set of all finite subsets of X. If α(q) = ∅ then q is a terminal state. We write q a → µ for (a, µ) ∈ α(q). Moreover, we write q a →r whenever q a → µ and µ(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. 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 . . .. We denote by Traces(M ) the complete traces of M , i.e. Traces(M

) def = {trace(σ) | σ ∈ CPaths(M )}. 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 (σ)•µ(q ), where last(σ) a → µ. 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 scheduler for a probabilistic automaton M is a function 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 ζ. A scheduler is history dependent since it takes into account the path and not only the current state. It may be partial, i.e. it may halt the execution at any time2 .

ζ : Paths (M ) → (Σ × D(Q) ∪ {⊥}) such that for all finite path σ, if α(last(σ)) = ∅ then ζ(σ) ∈ α(last(σ)),

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 probabilistic processes, called components. Each component is equipped with a unique identifier, called tag. Whenever a component (or a pair of components in case of synchronization) makes a step, the corresponding transition will be decorated with the associated tag (or pair of tags).

Similar systems have been already introduced in [START_REF] Andrés | Information hiding in probabilistic concurrent systems[END_REF]. The main differences are that here the components may contain nondetermism, and a secret can label any transition.

Tagged Probabilistic Automata

We now formalize the notion of TPA.

Definition 1. A Tagged Probabilistic Automaton is a tuple (Q, L, Σ, q, α), where Q is a set of states, L is a set of tags, Σ is a set of actions, q ∈ Q is the initial state, α : Q → P(L × Σ × D(Q)) is a transition function.
In the following we write q l:a -→ µ for ( , a, µ) ∈ α(q), and we use enab(q) to denote the tags of the components that are enabled to make a transition. Namely, enab(q

) def = { ∈ L | there exists a ∈ Σ, µ ∈ D(Q) such that q l:a -→ µ}.
In these systems, we can decompose the scheduler in two: a global scheduler, which decides which component or pair of components makes the move next, and a local scheduler, which solves the internal nondeterminism of the selected component.

We assume that the local scheduler can only select enabled transitions, and that the global scheduler can only select enabled components. This means that the execution does not stop unless all components are blocked. This is in line with the tradition of process algebra and of Markov Decision Processes, but contrasts with that of Probabilistic Automata [START_REF] Segala | Probabilistic simulations for probabilistic processes[END_REF]. However, the results in this paper do not depend on this assumption. Definition 2. Let M = (Q, L, Σ, q, α) be a Tagged Probabilistic Automaton.

Components

We are going to use a simple probabilistic process calculus (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]) to specify the components.

We assume a set of actions or channel names Σ with elements a, a 1 , a 2 , • • • , including the special symbol τ denoting a silent step. Except τ , each action a has a co-action ā ∈ Σ and we assume ā = a. Components are specified by the following grammar:

q ::= 0 | a.q | q 1 + q 2 | i p i : q i | q 1 |q 2 | (a)q | A
The constructs 0, a.q, q 1 + q 2 , q 1 |q 2 and (a)q represent termination, prefixing, nondeterministic choice, parallel composition, and the restriction operator, respectively. i p i : q i is a probabilistic choice, where p i represents the probability of the i-th branch and must satisfy 0 ≤ p i ≤ 1 and i p i = 1. The process call A is a simple process identifier. For each identifier, 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. We will denote by f n(q) the free channel names occurring in q, i.e. the channel names not bound by a restriction operator.

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

PRF a.q a → δ q NDT q 1 a → µ q 1 + q 2 a → µ PRB i p i : q i τ → • i p i • δ qi PAR q 1 a → µ q 1 | q 2 a → µ | q 2 CALL q a → µ A a → µ if A def = q COM q 1 a → δ r1 q 2 ā → δ r2 q 1 | q 2 τ → δ r1|r2 RST q a → µ (b)q a → (b)µ a,ā =b
We assume also the symmetric versions of the rules NDT, PAR and COM. The symbol δ q is the delta of Dirac, which assigns probability 1 to q and 0 to all other processes. The symbol • i is the summation on distributions. Namely,

• i p i • µ i is the distribution µ such that µ(x) = i p i • µ i (x).
The notation µ | q represents the distribution µ such that µ (r) = µ(q ) if r = q | q, and µ (r) = 0 otherwise. Similarly, (b)µ represents the distribution µ such that µ (q) = µ(q ) if q = (b)q , and µ (q) = 0 otherwise.

Systems

A system has the form (A) q 1 q 2 • • • q n , where the q i 's are components and A ⊆ Σ. The restriction on A enforces synchronization on the channel names belonging to A, in accordance with the CCS spirit.

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 :a -→ µ where a ∈ Σ, µ ∈ D(Q), and ∈ L is either the tag of the component which makes the move, or a (unordered) pair of tags representing the two partners of a synchronization. We can simply define L as L = I ∪ I 2 where I = {1, 2, . . . , n}.

Interleaving q i a → • j p j • δ qij (A) q 1 • • • q i • • • q j • • • q n i:a -→ • j p j • δ (A)q1 ••• qij ••• qn a ∈A
where i is the tag indicating that the component i is making the step. Note that we assume that probabilistic choices are finite. This implies that every transition q :a -→ µ can be written q :a -→ • i p i • δ qi , and justifies the notation used in the interleaving rule.

Synchronization q i a → δ q i q j ā → δ q j (A) q 1 • • • q i • • • q j • • • q n {i,j}:τ -→ δ (A)q1 ••• q i ••• q j ••• qn
here {i, j} is the tag indicating that the components making the step are i and j. Note that it is an unordered pair. Sometimes we will write i, j instead of {i, j}, for simplicity. In this section we restrict the discerning power of the global and local schedulers in order to avoid the problem of the information leakage induced in security by clairvoyant schedulers. We impose two kinds of restrictions: For the global scheduler, following [START_REF] Andrés | Information hiding in probabilistic concurrent systems[END_REF], we assume that it can only see, and keep memory of, the observable actions and the components that are enabled, but not the secret actions. As for the local scheduler, we assume that the local nondeterminism of each component is solved on the basis of the view of the history local to that component, i.e. the projection of the history of the system on that component. In other words, each component has to make decisions based only on the history of its own execution; it cannot see anything of the other components.

ζ(σ) def =                {1, 4} if σ = S [ a / sec ] , 2 if σ = S [ a / sec ] 1,2:τ -→ ( -|| out a || -|| -), 3 if σ = S [ a / sec ] 1,3:τ -→ ( -|| -|| out b || -), 4 if σ = S [ a / sec ] 1

Restricting Global Schedulers

We assume that the set of actions Σ is divided in two parts, the secret actions S and the observable actions O. The secret actions are supposed to be invisible to the global scheduler. Formally, this can be achieved using a function sift with sift(a) equals τ if a ∈ S and equals a otherwise. Then, we restrict the power of the global scheduler by forcing it to make the same decisions on paths he cannot tell apart.

Definition 3. Given a TPA M , a global scheduler ζ for M is admissible if for all paths σ 1 and σ 2 we have t(σ

1 ) = t(σ 2 ) implies ζ(σ 1 ) = ζ(σ 2 ), where t q l1:a1 -→ q 1 l2:a2 -→ • • • ln:an -→ q n+1 def = (enab(q), sift(a 1 ), l 1 )(enab(q 1 ), sift(a 2 ), l 2 )• • •(enab(q n ), sift(a n ), l n ).
The idea is that t sifts the information of the path that the scheduler can see. Since sift "hides" the secrets, the scheduler cannot take different decisions based on secrets.

Restricting Local Schedulers

The restriction on the local scheduler is based on the idea that a step of the component i of a system can only be based on the view that i has of the history, i.e. its own history. In order to formalize this restriction, it is convenient to introduce the concept of i-view of a path σ, or projection of σ on i, which we will denote by σ i . We define it inductively:

(σ :a -→ µ) i =      σ i i:b -→ δ qi if = {i, j} and µ = δ (A) q1 ... qi ... qj ... qn σ i i:a -→ µ if = i σ i otherwise
In the above definition, the first line represents the case of a synchronization step involving the component i, where we assume that the premise for i is of the form q i b -→ δ qi . The second line represents an interleaving step in which i is the active component. The third line represents step in which the component i is idle.

The restriction to the local scheduler can now be expressed as follows:

Definition 4. Given a TPA M and a local scheduler ξ for M , we say that ξ is admissible if for all paths σ and σ , if ξ(σ) = ( , a, µ), and ξ(σ ) = ( , a , µ ) we have:

• if = = i and σ i = σ i , then ξ(σ) = ξ(σ ),
• if = = {i, j}, σ i = σ i , and σ j = σ j then ξ(σ) = ξ(σ ).

A pair of compatible schedulers (ζ, ξ) is called admissible if ζ and ξ are admissible.

Safe equivalences

In this section we revise process equivalence notions to make them safe for security.

Safe Complete Traces

We define here a safe version of complete-trace semantics. The idea is that we compare two processes based not only on their traces, but also on the choices that the global scheduler makes at every step. We do this by recording explicitly the tags in the traces.

Definition 5.

• Given a TPA M = (Q, L, Σ, q, α), the (complete) safe traces of M , denoted here by Traces s , are defined as the probabilities of sequences of tags and actions corresponding to all possible complete executions, i.e. where P M,ζ,ξ is the probability measure in M under (ζ, ξ), and trace ta extracts from a path the sequence of tags and actions, i.e. trace ta ( ) = (on the empty path trace ta gives the empty string) and trace ta (q :a -→ σ) = : a • trace ta (σ). • We denote by Traces s (q) the safe traces of the automaton associated to a system q.

• Two systems q 1 and q 2 are safe-trace equivalent, denoted by q 1 s q 2 , if and only if Traces s (q 1 ) = Traces s (q 2 ).

The following example points out the difference between s and the standard (complete) trace equivalence.

/ sec ]) = {f 1 , f 2 , f 3 } where f 1 ({1, 2} : τ • 2 : out a ) = f 2 ({1, 3} : τ • 3 : out b ) = f 3 ({1, 4} : τ • 4 : out a }) = 1, and f i (t) = 0 otherwise (for i ∈ {1, 2, 3}), while Traces s (S b / sec ) = {f 1 , f 2 , f 4 } with f 1 , f 2 as above, and f 4 ({1, 4} : τ • 4 : out b ) = 1, f 4 (t) = 0 otherwise.

Safe Bisimilarity

In this section we propose a security-safe version of strong bisimulation, that we call safe bisimulation. This is an equivalence relation stricter than safe-trace equivalence, with the advantage of being a congruence. Since in this paper schedulers can always observe which component is making a step (even a silent step), it does not seem natural to consider weak bisimulation.

We start with some notation. Given a TPA M = (Q, L, Σ, q, α), and a global scheduler ζ, we write q a -→ ζ µ if there exists σ ∈ Paths (M ) such that ζ(σ) = ⊥, (ζ(σ), a, µ) ∈ α(q), and q = last(σ). Note that the restriction to ζ still allows nondeterminism, i.e. there may be µ 1 , µ 2 , such that q

a1 -→ ζ µ 1 and q a2 -→ ζ µ 2 (with either a 1 = a 2 or a 1 = a 2 ).
We now define the notion of safe bisimulation. The idea is that, if q and q are bisimilar states, then every move from q should be mimicked by a move from q using the same (admissible) scheduler. Definition 6. Given a TPA M = (Q, L, Σ, q, α), we say that a relation R ⊆ Q × Q is a safe bisimulation if, whenever q 1 R q 2 , then enab(q 1 ) = enab(q 2 ), and for all admissible global schedulers ζ for M such that ζ(σ 1 ) = ζ(σ 2 ) whenever last(σ 1 ) = q 1 and last(σ 2 ) = q 2 :

• if q 1 a -→ ζ µ 1 , then there exists µ 2 such that q 2 a -→ ζ µ 2 and µ 1 R µ 2 , and • if q 2 a -→ ζ µ 2 , then there exists µ 1 such that q 1 a -→ ζ µ 1 and µ 1 R µ 2 ,
where µ 1 R µ 2 means that for all equivalence classes X ∈ Q R, we have µ 1 (X) = µ 2 (X), where R is the smallest equivalence class induced by R.

The following result is analogous to the case of standard bisimulation: Proposition 1. The union of all the safe bisimulations is still a safe bisimulation.

Therefore the largest safe bisimulation exists, and coincides with the union of all safe bisimulations. We call it safe bisimilarity, and we denote it by ∼ s .

Given two TPAs on the same L and Σ, M 1 = (Q 1 , L, Σ, q1 , α 1 ) and M 2 = (Q 2 , L, Σ, q2 , α 2 ), we can define bisimulation and bisimilarity across their states, i.e. as relations on (Q 1 ∪ Q 2 ), in the obvious way, by constructing the TPA M with a new initial state q and two transitions to δ q1 and to δ q2 , respectively.

Given two components or systems, q 1 and q 2 , we will say that q 1 and q 2 are safely bisimilar, denoted by q 1 ∼ s q 2 , if the initial states of the corresponding TPAs are safely bisimilar. Note that q 1 ∼ s q 2 is possible only if q 1 and q 2 have the same number of active components, where "active", for a component, means that during the execution of the system it will make at least one step. Note that in the case of components, or of systems constituted by one component only, safe bisimulation and safe bisimilarity coincide with standard bisimulation and bisimilarity (denoted by ∼), respectively. This is not the case for systems, as shown by the following example: Example 4. Consider again the TPAs of Example 2. As pointed out in the introduction, we have S [ a / sec ] ∼ S b / sec . However S [ a / sec ] ∼ s S b / sec . To show this, let us construct a new TPA (as described before) with initial state q such that q :τ -→ S [ a / sec ] and q :τ -→ S b / sec . Now consider the (admissible) global scheduler ζ such that

ζ(σ) def =                                            if σ = q, {1, 4} if σ = q :τ -→ S [ a / sec ] , 2 if σ = q :τ -→ S [ a / sec ] 1,2:τ -→ ( -|| out a || -|| -), 3 if σ = q :τ -→ S [ a / sec ] 1,3:τ -→ ( -|| -|| out b || -), 4 if σ = q :τ -→ S [ a / sec ] 1,4:τ -→ ( -|| -|| -|| out a ), {1, 4} if σ = q :τ -→ S b / sec , 2 if σ = q :τ -→ S b / sec 1,2:τ -→ ( -|| out a || -|| -), 3 if σ = q :τ -→ S b / sec 1,3:τ -→ ( -|| -|| out b || -), 4 if σ = q :τ -→ S b / sec 1,4:τ -→ ( -|| -|| -|| out b ), ⊥ otherwise.
It is easy to see that S b / sec cannot mimic the transition 4 : out a produced by S [ a / sec ] using the same scheduler ζ.

It turns out that safe bisimulation is a congruence with respect to all the operators of our language, as expressed by the following theorem. (Statements 2(a) and 2(b) are just the standard compositionality result for probabilistic bisimulation.) Theorem 1.

1. ∼ s is an equivalence relation. 2. Let a ∈ Σ and A, B, B ⊆ Σ. Let p 1 , . . . , p n be probability values, and let q, q 1 , q 2 , . . . , q n , q 1 , q 2 , . . . , q n be components.

(a) If q 1 ∼ s q 2 , then a.q 1 ∼ s a.q 2 , q 1 + q ∼ s q 2 + q, (a)q 1 ∼ s (a)q 2 , and q 1 | q ∼ s q 2 | q. (b) If q 1 ∼ s q 1 , . . . , q n ∼ s q n , then i p i : q i ∼ s i p i : q i . (c) If (B) q 1 . . . q n ∼ s (B ) q 1 . . . q n , and f n(q) ∈ B ∪ B , then

(A ∪ B) q 1 . . . q . . . q n ∼ s (A ∪ B ) q 1 . . . q . . . q n .
The following property shows that bisimulation is stronger than safe-trace equivalence, like in the standard case.

Proposition 2. If q 1 ∼ s q 2 then q 1 s q 2 .
Like in the standard case, the vice-versa does not hold, and safe-trace equivalence is not a congruence3 .

Safe Nondeterministic Information Hiding

In this section we define the notion of information hiding under the most general hypothesis that the nondeterminism is handled partly in a demonic way and partly in an angelic way. We assume that the demonic part is in the realm of the global scheduler, while the angelic part is controlled by the local scheduler. The motivation is that in a protocol the local components can be thought of as programs running locally in a single machine, and locally predictable and controllable, while the network can be subject to attacks that make the interactions unpredictable.

We recall that, in a purely probabilistic setting, the absence of leakage, such as nointerference and strong anonymity, is expressed as follows (see for instance [START_REF] Bhargava | Probabilistic anonymity[END_REF]). Given a purely probabilistic automaton M , and a sequence ã = a 1 a 2 . . . a n , let P M ([ã]) represent the probability measure of all complete paths with trace ã in M . Let S be a protocol containing a variable action secr , and let s be secret actions. Let M s be the automaton corresponding to S[ s / secr ]. Define Pr (ã | s) as P Ms ([ã]). Then S is leakage-free if for every observable trace ã , and for every secret s 1 and s 2 , we have

Pr (ã | s 1 ) = Pr (ã | s 2 ).
In a purely nondeterministic setting, on the other hand, the absence of leakage has been characterized in the literature by the property S[ s1 / secr ] ∼ = S[ s2 / secr ], where ∼ = is an equivalence relation like trace equivalence, or bisimulation. As we have argued in the introduction, this definition assumes an angelic interpretation of nondeterminism.

We want to combine the above notions so to cope with both probability and nondeterminism. Furthermore, we want to extend it to the case in which part of the nondeterminism is interpreted demonically. Let us first introduce some notation.

Let S be a system containing a variable action secr . Let s be a secret action. Let M s be the TPA associated to S[ s / secr ] and let (ζ, ξ) be a compatible pair of global and local schedulers for M s . The probability of an observable trace ã given s is defined as

Pr ζ,ξ (ã | s) = P Ms,ζ,ξ ([ã]).
The global nondeterminism is interpreted demonically, and therefore we need to ensure that the conditional of an observable, given the two secrets, are calculated with respect to the same global scheduler. On the other hand, the local scheduler is interpreted angelically, and therefore we can compare the conditional probabilities generated by the two secrets as sets under different schedulers. In other words, we have the freedom to match conditional probability from the first set with one of the other set, without requiring the local scheduler to be the same.

Either angelic or demonic, we want to avoid the clairvoyant schedulers, i.e. a scheduler should not be able to use the secret information to achieve its goals. For this purpose, we require both the global and the local scheduler to be admissible. The safe equivalences defined in Section 5 imply the absence of leakage: Theorem 2. Let S be a system with a variable action secr and assume S[ s1 / secr ] s S[ s2 / secr ] for every pair of secrets s 1 and s 2 . Then S is leakage-free.

Note that the vice versa is not true, i.e. it is not the case that the leakage-freedom of S implies S[ s1 / secr ] s S[ s2 / secr ]. This is because in the definition of safe-trace equivalence we compare the set of probability functions (determined by the schedulers) on traces, while in the definition of leakage-freedom we compare the set of probabilities of each trace, which may come from different functions. This additional degree of freedom generated by the local scheduler helps the system to obfuscate the secret, and provides further justification for the adjective "angelic" for the local nondeterminism.

From the above theorem and from Proposition 2, we also have the following corollary (with the same premises as the previous theorem):

Corollary 1. If S[ s1 / secr ] ∼ s S[ s2 / secr ]
for every pair of secrets s 1 and s 2 , then S is leakage-free.

Related Work

The problem of deriving correct implementations from secrecy specifications has received a lot of attention already. One of the first works to address the problem was [START_REF] Jacob | On the derivation of secure components[END_REF], which showed that the fact that an implementation is a consistent refinement w.r.t. a specification does not imply that the (information-flow) security properties are preserved. More recently, [START_REF] Alur | Preserving secrecy under refinement[END_REF] has proposed a notion of secrecy-preserving refinement, and a simulation-based technique for proving that a system is the refinement of another. [START_REF] Clarkson | Hyperproperties. In CSF[END_REF] argues that important classes of security policies such as noninterference and average response time cannot be expressed by traditional notion of properties, which consist of sets of traces, and proposes to use hyperproperties (sets of properties) instead. [START_REF] Dubreil | Supervisory control for opacity[END_REF] addresses the problem of supervisory control, i.e, given a critical system G that may leak confidential information, how to design a controller C so that the system G|C dos not leak. An effective algorithm is presented to compute the most permissible controller such that the system is still opaque w.r.t. a secret.

Concerning angelic and demonic nondeterminism, there are various works which investigate their relation and possible combination. In [START_REF] Back | Combining angels, demons and miracles in program specifications[END_REF] it is shown that angelic and demonic nondeterminism are dual. [START_REF] Martin | Modelling angelic and demonic nondeterminism with multirelations[END_REF] uses multi-relations to express specifications involving both angelic and demonic nondeterminism. There are two kinds of agents, demonic and angelic ones, and there is the point of view of the internal system and the one of the external adversary. [START_REF] Morgan | The shadow knows: Refinement and security in sequential programs[END_REF] considers the problem of refining specifications while preserving ignorance. While the focus is on the reduction of demonic nondeterminism of the specification, the hidden values are treated essentially in a angelic way.

The problem of the leakage caused by full-information schedulers has also been investigated in literature. [START_REF] Canetti | Taskstructured probabilistic i/o automata[END_REF] and [START_REF] Canetti | Time-bounded task-PIOAs: A framework for analyzing security protocols[END_REF] work in the framework of probabilistic automata and introduce a restriction on the scheduler to the purpose of making them suitable to applications in security protocols. 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, which is historyindependent and therefore much more restricted than our notion of global scheduler. [START_REF] Andrés | Information hiding in probabilistic concurrent systems[END_REF] proposes a notion of system and admissible scheduler very similar to our notion of system and admissible global scheduler. The main difference is that in that work the components are deterministic and therefore there is no notion of local scheduler.

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. We believe that every scheduler in our formalism can be expressed in theirs, too. In [START_REF] Chatzikokolakis | Bisimulation for demonic schedulers[END_REF] they also consider the problem of defining a safe version of bisimulation for expressing security properties. They call it demonic bisimulation. The main difference with our work is that we consider a combination of angelic and demonic nondeterminism, and this affects also the definition of bisimulation. Similarly, our definition of leakage-freedom reflects this combination. In [START_REF] Chatzikokolakis | Bisimulation for demonic schedulers[END_REF] the aspect of angelicity is not considered, although they may be able to simulate it with an appropriate labeling.

The fact that full-information schedulers are unrealistic has also been observed in fields other than 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. However that work considers a synchronous parallel composition, so the setting is rather different from ours. Later on, it was shown that model checking is unfeasible in its general form for the restricted schedulers 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]). Despite of undecidability, not all results concerning such schedulers have been negative as, for instance, the technique of partial-order reduction can be improved by assuming that schedulers can only use partial information [START_REF] Giro | Partial order reduction for probabilistic systems: A revision for distributed schedulers[END_REF].

Conclusion and Future work

We have observed that some definitions of security properties based on process equivalences may be too naive, in that they assume the scheduler to be angelic, and, worse yet, to achieve its angelic strategy by peeking at the secrets. We have presented a formalism allowing us to specify a demonic constituent of the scheduler, possibly in collusion with the attacker, and an angelic one, under the control of the system. We have also considered restrictions on the schedulers to limit the power of what they can see, and extended to our nondeterministic framework the (probabilistic) information-hiding properties like non interference and strong anonymity. We then have defined "safe" equivalences. In particular we have defined the notions of safe trace equivalence and safe bisimilarity, and we have shown that the latter is still a congruence. Finally, we have shown that the safe equivalences can be used to prove information-hiding properties.

For the future, we plan to extend our framework to quantitative notions of information leakage, possibly based on information theory. We also plan to implement model checking techniques to verify information hiding properties for our kind of systems. A natural candidate for the implementation would be PRISM. Of course, we would need to restrict the class of schedulers in PRISM so to meet the admissibility criteria.

•

  A global scheduler for M is a function ζ : Paths (M ) → (L ∪ {⊥}) such that for all finite paths σ, if enab(last(σ)) = ∅ then ζ(σ) ∈ enab(last(σ)), and ζ(σ) = ⊥ otherwise. • A local scheduler for M is a function ξ : Paths (M ) → (L × Σ × D(Q) ∪ {⊥}) such that, for all finite paths σ, if α(last(σ)) = ∅ then ξ(σ) ∈ α(last(σ)), and ξ(σ) = ⊥ otherwise. • A global scheduler ζ and a local scheduler ξ for M are compatible if, for all finite paths σ, ξ(σ) = ( , a, µ) implies ζ(σ) = , and ξ(σ) = ⊥ implies ζ(σ) = ⊥. • A scheduler is a pair (ζ, ξ) of compatible global and local schedulers.

Example 2 .

 2 Consider the systems of Example 1. Figures 1(a) and 1(b) show the TPAs of S [ a / sec ] and of S b / sec respectively. For simplicity we do not write the restriction on channels c and out, and the termination symbol 0. We use '-' to denote a component that is stuck. The corresponding tags are indicated in the figure with numbers above the components. The set of enabled transitions should be clear from the figures. For instance, we have enab(S b / sec ) = {{1, 2}, {1, 3}, {1, 4}} and enab( -|| out a || -|| -) = {2}. The scheduler ζ defined as

Fig. 1 .

 1 Fig. 1. Automata S [ a sec ] and S b / sec

  Traces s (M ) = { f : (L × Σ) ∞ → [0, 1] | there exists an admissible scheduler (ζ, ξ) s.t.∀t ∈ (L × Σ) ∞ f (t) = P M,ζ,ξ ({σ ∈ CPaths(M ) | trace s (σ) = t}) }

Example 3 .

 3 Consider the TPAs of Example 2. The two TPAs have the same complete traces. In fact Traces(S [ a / sec ]) = {τ • out a , τ • out b } = Traces(S b / sec ). On the other hand, we have Traces s (S [ a

Definition 7 .

 7 A system is leakage-free if, for every secrets s 1 and s 2 , every admissible global scheduler ζ, and every observable trace ã, {Pr ζ,ξ (ã | s 1 ) | ξ admissible and compatible with ζ} = {Pr ζ,ξ (ã | s 2 ) | ξ admissible and compatible with ζ}.

This work has been partially supported by the project ANR-09-BLAN-0169-01 PANDA and by the INRIA DRI Equipe Associée PRINTEMPS.[START_REF] Abadi | A calculus for cryptographic protocols: The spi calculus[END_REF] The actual definition of[START_REF] Schneider | CSP and anonymity[END_REF] is more complicated, but the spirit is the same.

Probabilistic AutomataIn 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].

In this paper, however, we will consider only total schedulers, to be more in line with the standard semantics of CCS.

This is because we are considering the complete traces.

Acknowledgement. The authors wish to thank the anonymous reviewers for their useful comments, and Pedro D'Argenio for helpful discussion.