Direction des Relations Européennes et Internationales (DREI)

Programme INRIA "Equipes Associées"





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
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

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

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

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


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.


  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:

2. Echanges

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



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