ProNoBiS
Probability and Nondeterminism, Bisimulations and Security

The new² ProNoBis logo (with background by Maurits Cornelis Escher).
Courtesy of Catuscia.
Note the duality between demonic and angelic nondeterminism, as a context around a typically probabilistic process.

1  Goal of the Project

2  Consortium

3  Events

3.1  Events pertaining to ProNobis per se

• The GeoCal'06 residential session includes several workshops. Amongst these, the one on Probabilistic Transition Systems (Feb. 27–March 3, 2006) has direct relationships with ProNobis. C. Palamidessi, J. Goubault-Larrecq, and V. Danos were among the speakers. Organized by P. Panangaden and V. Danos.
  • Catuscia's talk on “Probabilistic and Nondeterministic Aspects of Anonymity” (with Mohit Bhargava), March 1st: as a pdf file, or a keynote archive (the latter readable only on Macinstoshes).
  • Jean's talk on “Capacities, Games, and Previsions”, March 2nd: sorry, this was a blackboard talk, no slides... but here is a draft of the supporting notes (in French). (Note that this versiond is evolving. The version presented at GeoCal'06 was eventually dated March 16. Then there were version 2 of June 06, version 3 of July 03, version 4 of July 07, and version 5 of July 28, 2006.)
    
    A great thanks to Prakash, who allotted the author one hour more than what he was entitled to initially!
  • Vincent's talk on “Compression of Markov Processes” (with Gordon Plotkin), March 3rd: sorry, again a blackboard talk, no slides...
  
  
  
• May 8–19, 2006: Visit of Peng Wu (Catuscia's group) to Marta Kwiatkowska's group (Birmingham) to collaborate with Dave Parker in developing an implementation of the probabilistic pi-calculus in PRISM.
  
  
• The first (official) ProNobis meeting will take place at ENS Cachan on Monday, May 22, 2006, 10h-17h.
  
  To come to Cachan, please follows the instructions. The precise venue is Pavillon des Jardins, first floor (the large conference room). This is both close to the entrance of ENS Cachan and to LSV: see the campus map.
  
  Program (updated post meeting):
  • 10h-12h30: One talk from each group giving a summary of the current activities of the group (30 min each).
    • 10h-10h30: Jean (SECSI, LSV). No slide from Jean (who for once did not use more than his allotted time!), but here are some from Simon Pinot (LSV).
    • 10h30-11h: Catuscia (Comète). Activities related to ProNobis.
    • 11h-11h45: Roberto (Verona). ProNobis activities in Verona. Also in Powerpoint format.
    • 11h45-12h30: Angelo Troina (Pisa), Time and Probability based Information Flow Analysis.
  • 12h30-15h. Lunch. “In France, we are on time—in the morning. But we do take lunch seriously.” (Jean.)
  • Afternoon: Other scientific talks, 45 min. each.
    • 15h-15h45: Jean Goubault-Larrecq, an introduction to capacities, games, and previsions (rerun of GeoCal talk, but shorter). Still no slides.
    • 15h45-16h40: Catuscia Palamidessi, Probabilistic and Nondeterministic Aspects of Anonymity.
    • 16h40-18h: Dave Parker. Summary of activities in Birmingham. Includes report on joint work with Peng/Catuscia, and should have included an update on biological case studies. Instead lots of non-biologically inspired, very interesting stuff was presented.
  • 18h-18h02: business meeting. (Nothing administrative to discuss. Only great science lurking ahead...)
  Jean also took some ASCII notes. While they are mostly unreadable (this is ASCII...), they probably give a more synthetic view of what happened during this meeting.
  
  
• September 01, 2006. Angelo Troina, troina@di.unipi.it is coming to LSV and LIX for a one year postdoc position on the ARC ProNoBiS. More information: Angelo's resume and a preliminary version of his PhD thesis. Here is a preliminary work programme.
  
  
• October 29-November 05, 2006. Jean went to visit Vincent in Boston, MA. (Vincent is now working for Plectics, Inc.)
  
  
• February 02, 2007. Jean talked about his work at the Journées Nationales du GDR Informatique Mathématique. Here are the slides. For more details, see either the draft, or the two research reports LSV-07-06 on Continuous Capacities on Continuous State Spaces and LSV-07-07 on Continuous Previsions.

3.2  Related events

• Olivier Pereira at the LSV seminar, Tuesday, May 16, 2006, on Using Task-Structured PIOAs to Analyze Cryptographic Protocols.
  
  Abstract: The Probabilistic I/O Automata framework of Lynch, Segala and Vaandrager provides tools for precisely specifying protocols and reasoning about their correctness using multiple levels of abstraction, based on implementation relationships between these levels. We enhance this framework to allow analyzing protocols that use cryptographic primitives. This requires resolving and reconciling issues such as nondeterministic behavior and scheduling, randomness, resource-bounded computation, and computational hardness assumptions. The enhanced framework allows for more rigorous and systematic analysis of cryptographic protocols in a composable security context.
  
  
• John Mullins at the Comète and Parsifal seminar, Friday, June 23, 2006, on Analyse de flux d'information dans les protocoles cryptographiques.
  
  Abstract: Les protocoles cryptographiques sont des règles d'échange entre les points d'un réseau qui permettent de sécuriser les communications. Il est notoire que leur conception est un exercice difficile et que la moindre faille peut avoir des répercussions économique énormes. Il n'est donc pas étonnant que ces dernières années, l'application des méthodes formelles à l'analyse des protocoles cryptographiques se soit imposée comme un champ de recherche émergent. Après un bref rappel sur les protocoles de cryptographies et des problèmes qu'ils posent au concepteur, nous présenterons plus spécifiquement les méthodes d'analyse basées sur la détection de flux d'information developpées au laboratoire CRAC de l'école Polytechnique de Montréal.
  
  
• The LIX Colloquium on Emerging Trends in Concurrency Theory, LIX, Ecole Polytechnique, November 13-15, 2006. Special guest: Robin Milner. And plenty of others!

4  Miscellanea

• Private links, accessible to members of the project only.

Publications

[1]

Kostantinos Chatzikokolakis and Catuscia Palamidessi. Probable innocence revisited. Theoretical Computer Science, 2006. To appear. http://www.lix.polytechnique.fr/~catuscia/papers/Anonymity/reportPI.pdf.

[2]

Jean Goubault-Larrecq. Continuous capacities on continuous state spaces. Research Report LSV-07-06, Laboratoire Spécification et Vérification, ENS Cachan, France, January 2007. 37 pages.

[3]

Jean Goubault-Larrecq. Continuous previsions. Research Report LSV-07-07, Laboratoire Spécification et Vérification, ENS Cachan, France, January 2007. 29 pages.

[4]

Catuscia Palamidessi, Vijay Saraswat, Frank Valencia, and Bjorn Victor. On the expressiveness of linearity vs. persistence in the asychronous pi-calculus. In Proceedings of the Twenty First Annual IEEE Symposium on Logic in Computer Science (LICS), 2006. To appear. http://www.lix.polytechnique.fr/~catuscia/papers/Frank/LICS_06/main.pdf.

[5]

Sylvain Pradalier and Catuscia Palamidessi. Expressiveness of probabilistic π-calculi. In Proceedings of QAPL, 2006. To appear. http://www.lix.polytechnique.fr/~catuscia/papers/Sylvain/QAPL06/FinalBis.pdf.

This document was translated from L^AT_EX by H^EV^EA.