Direction des Relations Européennes et Internationales (DREI)

Programme INRIA "Equipes Associées"

I. DEFINITION

II. PREVISIONS 2006

Programme de travail

Research plans for 2006

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

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.