Direction des Relations Européennes et Internationales (DREI)

# Programme INRIA "Equipes Associées"

## I. DEFINITION

 EQUIPE ASSOCIEE PRINTEMPS sélection 2006

 Projet INRIA : Comète Organisme étranger partenaire : Mc. Gill University Unité de recherche INRIA : Futurs Thème INRIA : Systèmes Communicants Pays : Canada

 Coordinateur français Coordinateur étranger Nom, prénom Palamidessi, Catuscia Panangaden, Prakash Grade/statut DR2 Full professor Organisme d'appartenance INRIA McGill University, School of Computer Science Adresse postale LIX, École Polytechnique, rue de Saclay, 91128 Palaiseau FRANCE 3480 rue University, Suite 318 Montreal, Quebec H3A 2A7 CANADA URL http://www.lix.polytechnique.fr/~catuscia/ http://rl.cs.mcgill.ca/~prakash/ Téléphone +33 (0)1 69 33 37 98 +1 514 3987074 Télécopie +33 (0)1 69 33 30 14 +1 514 3983883 Courriel catuscia at lix.polytechnique.fr prakash@cs.mcgill.ca

La proposition en bref
 Titre de la thématique de collaboration : Probabilité et Théorie de l'Information pour la protection de l'Anonymat et de l'Information Privée. PRINTEMPS: PRobability and INformation ThEory for Modeling anonymity, Privacy, and Secrecy Descriptif : The increasing diffusion of electronic services is accompanied by an increasing concern for the protection of private information. The design of protocols to ensure properties like anonymity, privacy, and secrecy, is therefore a very active topic of research, as well as the study of the formal aspects of such properties and the development of proper tools for ensuring the correctness of these protocols. However, despite the fact that much research has been done already, almost all the existing theories and verification techniques are along the lines of the so-called possibilistic approach, which is based on the principle of representing as nondeterministic the random mechanisms used in most of this class of protocols. The nondeterministic approximation however makes it impossible to capture the leakage of probabilistic information and prevent possible attacks based, for instance, on statistical analysis. For this reason, we feel that the theoretical foundations of anonymity and secrecy protection should take probability into account. In this cooperation, we aim at establishing a formal framework for expressing and reasoning about information-hiding properties, for helping the design of adequate protocols, and for verifying them. Our approach will be based on Information Theory. We believe that the body of concepts and results related to the notion of entropy, expressing the (lack of) information in a random variable, will provide a natural and solid framework for our goals.

### Présentation de l'Équipe Associée

1. Présentation du coordinateur étranger

Professor Panangaden received his Ph.D. in Physics from the University of Wisconsin in 1980, and a Master in Computer Science at the University of Utah, in 1985. After holding academic positions at Cornell University and at Queen's University, he joined the Department of Computer Science at McGill University. He has been invited speaker at a number of international conferences, including CONCUR'94, FSTTCS'95, PPDP'00, MFPS'01 and ISDT'04. He has been program committee chair of several conferences and workshops including EXPRESS'02, MFPS'03, and LICS'05. He is the Area Editor for Logic and Probability of the Journal on Logical Methods in Computer Science. He is also the author of 31 journal papers and 34 (refereed) conference papers, covering several research areas, including the theory of probabilistic systems, quantum computing, semantics for concurrent programming languages, and the relationships between logic and concurrent computation.

Présentation de l'équipe française

The French team is composed by Catuscia Palamidessi, some of the other members of the INRIA team Comète (see Point II.2. below for a more detailed description), and by Vincent Danos. Danos is not member of an INRIA team, but his current research interests are strongly related to this project, his background is in many ways complementary to that of Palamidessi, and he has an history of collaboration with Prakash Panangaden. Hence it seems very valuable for the project to involve him as a participant.

2. Historique de la collaboration

• 2.1. entre les équipes : Panangaden and Palamidessi have never collaborated in the past, although they have often been interested in the same research areas, and in many cases they have obtained similar or complementary results. To cite some of these cases, both Panangaden and Palamidessi have been working independently on the semantics of Concurrent Constraint Programming, using different approaches ( closure operators Panangaden and reactive sequences Palamidessi) which later have been shown equivalent. Both Panangaden and Palamidessi have been working on expressiveness results for concurrent languages, using different and and in a sense complementary techniques. Both Panangaden and Palamidessi have been working on probabilistic processes, attacking different problems (definition of metric and logic semantics Panangaden, development of an axiomatic theory Palamidessi).

We have often regretted the lack of occasions to collaborate, since we believe our research wold have greatly benefited by combining our expertises and ways of reasoning. Usually we would discover only a posteriori that we had been working on similar problems, and be surprised by how much we had been driven by similar goals and how parallel our research paths had been.

Now we are both interested in a new subject, namely the development of a logic based on Information Theory, and its application to Security. We feel that, even more than in the past, the potential benefits of our collaboration are huge. Security is a central theme in the INRIA team Comète lead by Catuscia Palamidessi. She and other members of the group have contributed to the foundations of Anonymity, and have recently started studying Information Theory in view of its applications to Anonymity and Secrecy. Prakash Panangaden, besides his Master degree in Computer Science, has a PhD in Physics which makes him able to understand in depth the sophisticated concepts and techniques of Information Theory. Furthermore, Panangaden has a solid background in Logics and Category Theory, which have been main topics in his research for the last several years. In conclusion, in this project proposal we believe that we have an ideal situation, as we have the same interests, and competences which are in large part complementary.

The other members of Comète have not collaborated with Panangaden or other members of his team either.

On the other hand, Vincent Danos and Prakash Panangaden have already a long history of collaboration on topics related to the present proposal: Bisimulation for Probabilistic Systems, Approximations of Markov Processes, Conditional Expectation. The results of this collaboration have been published in prestigious conferences and journals (see first list of publications below). These works have contributed to deepen the understanding of probabilistic behaviors and models in computer systems, and they are therefore a reference point for some of the investigations we intend to pursue in this project.

Vincent Danos and Prakash Panangaden have also been collaborating on other topics not directly related to this proposal. In particular, they have been working together in Quantum Computing (see second list of publications below).

Joint publications related to the proposal

1. Bisimulation and Cocongruence for Probabilistic Systems (Information & Computation, 2005) Vincent Danos, Josee Desharnais, François Laviolette, Prakash Panangaden.

2. Labelled Markov Processes: stronger and faster approximations (ENTCS 87, 2004) Vincent Danos, Josée Desharnais, Prakash Panangaden.

3. Conditional Expectation and the Approximation of Labelled Markov Processes (CONCUR'03) Vincent Danos, Josée Desharnais, Prakash Panangaden.

Joint publications not directly related to the proposal

1. Distributed measurement-based quantum computation (quant-ph/0506070, QPL'05) Vincent Danos, Ellie D'Hondt, Elham Kashefi, Prakash Panangaden.

2. The Measurement Calculus (quant-ph/0412135) Vincent Danos, Elham Kashefi, Prakash Panangaden.

3. Robust and parsimonious realisations of unitaries in the one-way model (quant-ph/0411071, to appear in Phys. Rev. A) Vincent Danos, Elham Kashefi, Prakash Panangaden.
• 2.2. entre l'INRIA et l'organisme partenaire :

To our knowledge there are the following ongoing collaborations between McGill and INRIA teams (the data are from the INRIA International - Cooperation with Canada web site)

• Project McGILL-ISA, with the team ISA (Lorraine), on 3D Visibility, in the context of the Associated Teams program.
• Project with the INRIA team Odyssée on Biomedical Image Analysis, in the context of the France-Canada Fund Call 2003.
• Cooperation with the INRIA team Mirho on OO programming and adaptive systems. Note: the Mirho team is now terminated, we don't know if the collaboration is still going on with the ex-members of the team.

3. Impact : indiquez en quoi, à votre avis, cette association aurait un impact important :

• 3.1. sur la collaboration déjà existante avec votre partenaire
• Not applicable in the case of Comète, since there are no previous collaborations.

• 3.2. sur la collaboration avec d'autres projets INRIA
• We expect that also the INRIA project SECSI, leaded by Jean Goubault-Larrecq, will benefit from the visits of Prakash Panangaden and his team in Paris. The central theme of SECSI is Security, and the study of probabilistic aspects has an important role in that project.

SECSI and Comète are actually preparing a joint ARC proposal on the combination of nondeterminism and probability, with the goal of establishing the foundations for certain aspects of Security, and studying the possible implications for probabilistic Model Checking. Other partners in this proposal will be Vincent Danos, Marta Kwiatowska, and Roberto Segala. There are several possible relations between the two proposals, along the lines of Probability, Security, and Model Checking. If both proposal are accepted, we plan to organize a joint workshop in Paris, in summer 2006, in which all partners (from this project and the ARC one) are expected to participate.

In any case, the SECSI team will be kept informed about the visits of the McGill partners in Paris, and will be invited to attend to the talks and discussions that will take place during those occasions.

• 3.3. sur la collaboration avec d'autres équipes de l'organisme étranger partenaire.

Two other groups at McGill that would be very much influenced by this work are the quantum information theory group headed by Claude Crepeau and Patrick Hayden and the machine learning group headed by Prof. Doina Precup and Joelle Pineau.

In the Quantum Information Theory group they study both quantum cryptography and foundational aspects of quantum information. There have already been extensive discussions between Panangaden, Patrick Hayden and John Yard (a visitor to Hayden's equipe) about Information Theory. There is an active collaboration between Panangaden, Pineau and Precup on aspects of probabilistic automata, duality and learning. The formulation of a logic of information would fit right in with aspects of learning probabilistic automata.

4. Divers : toute autre information que vous jugerez utile d'ajouter.

## II. PREVISIONS 2006

### Programme de travail

#### Research plans for 2006

The planned research for the year 2006 is articulated along the following lines:

#### 1. Foundations of Anonymity, Privacy, and Secrecy

Anonymity, privacy and secrecy are instances of a general issue that we could call partial hiding of information. Anonymity refers to keeping secret the identity of a user performing a certain action, while in general the effects of the action are supposed to become public. Privacy refers to the protection of certain data, like for instance the credit card number of a user, while making other data available. Secrecy, or Confidentiality, refers to the fact that certain information has to be kept hidden from certain users but not from others.

We intend to establish a theory of information-hiding based on the concept of entropy. Briefly, the idea is the following: Assuming that X is a random variable representing the information that we want to hide, and Y is the random variable representing the information that we want to make public, H(X|Y) (the entropy of X given Y) expresses the lack of information that we have w.r.t. X despite the complete knowledge of Y.

We plan to give a formal justification of the hierarchy of Reiter and Rubin [9] in our framework. This hierarchy is a classification of various degrees of anonymity protection that a protocol can achieve, and was defined only informally by Reiter and Rabin. For instance, we believe that Perfect Anonymity can be expressed in our framework by the formula H(X|Y) = H(X) (where H(X) is the entropy of X), i.e. the observation of Y does not reveal anything about X.

It is worth noting that, although there have been some attempts to define formally the above concepts, the definitions given in literature do not reflect what Reiter and Rubin have used in practice to prove the correctness of their protocols, see [3] for a discussion. An exception is represented by [2] and [3] which have formalized Strong Anonymity and Probable Innocence, although the definitions given there are rather ad hoc. We are confident that Information Theory will allow us to develop an elegant and unified theory for Anonymity and all the other information-hiding properties.

Participants: Prakash Panangaden, Kostas Chatzikokolakis, Catuscia Palamidessi

#### 2. A Logic based on Information Theory

In many proofs in Information Theory there is a consistent repetitive pattern. This can especially be noticed in channel capacity theorems. We are seeking to abstract the logical (or categorical) essence of these proofs and unify many of these ideas.

In searching a common logical core we are led to consider categories where Markov processes are captured naturally. There is a fundamental idea, due to Lawvere orginally but developed by Michele Giry, that one should work with the Kleisli category of the probabilistic powerset monad. This category, named SRel by Panangaden, has been studied as the category capturing the notion of stochastic relations [8]. It turns out to have some interesting logical properties - it supports a nuclear ideal - and is an ideal candidate to start our study of the logic of probabilistic processes. The morphisms in this category are exactly Markov kernels and composition is just the composition of probabilistic transitions (what is called the Chapman-Kolmogorov equation in stochastic process theory) [1].

We plan to beging by asking how Information Theory fits in the SRel logic. Panangaden and his colleagues have already begun to look at this in the Quantum Information Theory setting.

Participants: Prakash Panangaden, Vincent Danos, Peng Wu

#### 3. A process calculus and its semantics

The formalism for describing the protocols should be suitable for verification, that is, have a simple syntax and a clear semantics. Such formalism should allow to express concurrency, communication, and quantitative aspects related to entropy. A process calculus, extended with some kind of construct suitable to represent random variables, seems therefore the natural choice. As a starting point, the probabilistic pi-calculus of [7] is a possible candidate. Suitable choices for the semantics include the probabilistic bisimulations [4] or the more ambitious approaches based on metrics [5], [6].

In particular, in [6], Desharnais, Gupta, Jagadeesan and Panangaden have already started an information-theoretic investigation. They analyzed weak probabilistic bisimulation for a probabilistic process calculus with nondeterminism, probabilistic choice and hidden internal actions, and they developed a metric analogue of weak bisimulation. They showed that the channel capacity is a continuous function of the metric and they showed that all the process combinators are contractive in this metric.

One advantage of working with a process calculus is that it provides a natural framework to prove properties like compositionality of security. The channel capacity is a measure of the propensity of a system to leak information. If we have a system S in a context C[.], and we know that C[S] is secure, and if we know that S' is close to S according to the metric, then we know that C[S'] is secure as well since C[S'] must be close to C[S] (contractivity) and hence almost as secure (continuity of channel capacity). This is, of course, a preliminary intuition, but it shows that the recently developed quantitative tools (metric analogues of bismulation) for semantics of probabilistic process algebra will fit naturally with our idea of investigating security properties from an information-theoretic perspective.

Participants: Prakash Panangaden, Romain Beauxis, Catuscia Palamidessi, Peng Wu

#### Long-term research plans

In the long term, we expect our results to lay the foundations for automated verification techniques tailored to the information-hiding protocols. A good starting point could be the current probabilistic verification tools like PRISM. The extension we envisage would be based on the logic described in Point 2, on one hand, and the process-calculus formalism described in Point 3, on the other.

The verification of a property expressing protection of information will typically involve the calculation of some quantities related to entropy. We believe that this issue will lead to new perspectives in probabilistic model checking, and require totally new techniques.

In the long term, Panangaden and Palamidessi plan to have a PhD student in co-supervision who will investigate the above topics as his or her thesis project.

#### References

1. Samson Abramsky, Richard Blute and Prakash Panangaden. Nuclear and Trace Ideals in $\otimes-*$-categories, Journal Of Pure And Applied Algebra, Vol: 143, Issue: 1-3, Pages 3-47, 1999.

2. Mohit Bhargava and Catuscia Palamidessi. Probabilistic Anonymity. In Proceedings of CONCUR 2005, LNCS 3653, pages 171-185, Springer-Verlag, 2005.
3. Kostantinos Chatzikokolakis and Catuscia Palamidessi. Probable Innocence Revisited. In Proceedings of FAST 2005, To appear in the LNCS series of Springer Verlag.
4. Yuxin Deng and Catuscia Palamidessi. Axiomatizations for probabilistic finite-state behaviors. In Proceedings of FOSSACS 2005 (Part of ETAPS 2005), LNCS 3441, pages 110-124, Springer-Verlag, 2005.
5. Josée Desharnais, Vineet Gupta, Radha Jagadeesan and Prakash Panangaden. Metrics for Labelled Markov Processes. In Theoretical Computer Science 318(3), pages 323-354, 2005.
6. Josée Desharnais, Vineet Gupta, Radha Jagadeesan and Prakash Panangaden. The Metric Analogue of Weak Bisimulation for Probabilistic Processes. In the Proceedings of the Seventeenth Annual IEEE Symposium On Logic In Computer Science, pages 413-422, IEEE 2002.
7. Catuscia Palamidessi and Mihaela O. Herescu. A randomized encoding of the π-calculus with mixed choice. In Theoretical Computer Science, 335(2-3): 373-404, 2005.
8. Prakash Panangaden. The Category of Markov Processes, ENTCS, Vol 22, 1999.
9. Michael K. Reiter and Aviel D. Rubin. Crowds: anonymity for Web transactions. ACM Transactions on Information and System Security, Vol 1, n. 1, pages 66-92, 1998.

### Activités prévisionnelles 2006

1. People

The French team is composed by:

• Catuscia Palamidessi, DR2 INRIA, leader of the INRIA team Comète.
• Vincent Danos, DR2 CNRS, member of the PPS lab, University of Paris VII.
• Peng Wu, Postdoc, member of Comète, working on Probabilistic Model Checking.
• Kostas Chatzikokolakis, PhD student, member of Comète, working on Security Protocols for Anonymity and Secrecy.
• Romain Beauxis, PhD student, member of Comète, working on expressiveness issues in the pi-calculus. This is one of the formalisms used nowadays to specify Security Protocols and to verify their correctness.

2. Echanges

The expected missions from the French team to McGill are the following:

• In February 2006 Prakash Panangaden has scheduled a visit to Paris. This will be an occasion to set-up a kick-off meeting, with the purpose of establishing a detailed action plan.
• Later during spring 2006 we plan to organize a workshop at McGill, of a duration of two or three days, in which all the members of the French team and of the McGill team are expected to participate and present their research interests and achievements related to the project. This will be an occasion for all the members of the two teams to get introduced to each other, to identify common interests, and envisage possible collaborations on specific topics among inter-teams subgroups. These topics will include those detailed in the Programme de Travail, but it is possible that the stimulating atmosphere of a physical meeting will induce to discover further issues of interest for the project. The workshop will be followed by a few days visit, to articulate specific collaborations and get started on them. For participating to these events, all the members of the French team plan a trip of about one week to McGill University.
• The McGill team members plan to visit the French partners for another week during summer 2006, to continue the collaborations started with the previous meeting. We will probably organize a second workshop and invite other INRIA teams involved in Probability and Security, in particular SECSI, and possibly the other partners of the ARC proposal described in the point I. 3.2 above.
• Each member of the French team plans another trip of about one weak to McGill to complete the collaborations with the Canadian partners. These trips will take place later in 2006, probably during fall.

© INRIA - mise à jour le 21/10/2005