Programme VerifiCard meeting, 7-9 January 2002

Abstracts

Sunday

• 19.30 PCC Meeting.
  There is a preliminary agenda (restricted access).

Monday

• 9.00- 9.15 Opening
• 9.15-10.00 Ludovic Casset (Gemplus).
  From formal specification to an implementation of an embedded verifier for JavaCard.
  Abstract Slides
• 10.00-10.30 Gilles Barthe, Guillaume Dufay, Line Jakubiec, Bernard Serpette, and Simao Sousa (INRIA/Marseille).
  A formal executable semantics of the JavaCard platform.
  Abstract Slides (Powerpoint)
• 10.30-11.00 Coffee break
• 11.00-11.30 Martin Strecker (TUM).
  Verification of a Java compiler in Isabelle.
  Abstract Slides
• 11.30-12.00 Thomas Genet, Thomas Jensen and Francois Monin (INRIA).
  Constructing a Java Card converter using a proof assistant.
  Abstract Slides
• 12.00-12.45 WP3 Discussion
• 12.45-14.30 Lunch
• 14.30-15.30 Pieter Hartel (Twente).
  Transacted memory for smart cards.
  Abstract Slides
• 15.30-16.00 Norbert Schirmer (TUM).
  Modelling the Package/Access concept of Java in Isabelle.
  Abstract Slides
• 16.00-16.30 Coffee break
• 16.30-17.00 Leonor Prensa Nieto (TUM).
  Verification of parallel programs with the Owicki-Gries and rely-guarantee methods in Isabelle/HOL.
  Abstract Slides
• 17.00-17.45 WP2 Discussion
• David Naccache (Gemplus). Applying cryptographic techniques to bytecode verification.
  

Tuesday

• 9.00-10.00 Chris Hankin (Imperial).
  Security through Static Analysis.
  Abstract Slides
• 10.00-10.30 Gilles Barthe, Dilian Gurov, and Marieke Huisman (SICS/INRIA).
  Verification of secure applet interactions.
  Abstract Slides
• 10.30-11.00 Coffee break
• 11.10-11.30 Gilles Barthe, Guillaume Dufay, Marieke Huisman, Simao Sousa and Sorin Stratulat (INRIA).
  Jakarta: a toolset to reason about JavaCard.
  Abstract Slides
• 11.30-12.00 Kerry Trentelman (ANU/INRIA).
  Extending JML with temporal logic.
  Abstract Slides
• 12.00-12.45 WP4 Discussion
• 12.45-14.30 Lunch
• 14.30-15.00 Nicole Rauch and Jorg Meyer (Hagen).
  Techniques for the Verification of JavaCard programs on the Source Code Level.
  Paper Slides (.ps) (.tar.gz)
• 15.00-15.30 Bernhard Beckert and Bettina Sasse (Karslruhe).
  Handling Java's abrupt termination in a Sequent Calculus for Dynamic Logic.
  Paper Slides
• 15.30-16.15 WP5 Discussion
• 16.15-16.45 Coffee
• 16.45-17.15 Joacim Halen (Ericsson).
  PEP: Personal Empowerment through Policies
• 17.15-17.45 Eduardo Giménez (Trusted Logic) and Olivier Ly (Schlumberger).
  Formal modeling and verification of the Java Card security architecture: from static checkings to embedded applet execution.
  Abstract (text) Slides

Wednesday

• 9.00- 9.30 Nestor Catano and Marieke Huisman (INRIA).
  Formal specification of Gemplus' electronic purse case study.
  Paper Slides (Powerpoint)
• 9.30-10.00 Cees-Bart Breunesse, Bart Jacobs and Joachim van den Berg (KUN).
  Specifying and Verifying an Example: a decimal representation in Java for smartcards.
  Paper Slides
• 10.00-10.30 Daniel Perovich (Montevideo/INRIA).
  Secure Object Sharing Development Kit for JavaCard.
  Paper Slides
• 10.30-11.00 Coffee break
• 11.00-11.30 Cees-Bart Breunesse, Bart Jacobs and Martijn Oostdijk (KUN).
  Voting using JavaCard smart cards: a case study.
  Paper Slides
• 11.30-12.15 WP6 Discussion
• 12.15-14.00 Lunch
• 14.00-17.00 EUP Session
• 14:00-15:00 brief presentations of the workpackages by the WP leaders
• 15:00-17:00 round-table session

Report on the End User Panel Meeting, 9/1/02, Marseille (html version)