Workshop on Formal Methods and Cryptography, Colocated with FM 2011, Limerick, 21 June 2011
Kemmy Business School, room KBG-13, starting at 9:00
In the 1990s, formal methods were successfully applied to the modelling and verification of security protocols at a high level of abstraction. However, modern cryptographic protocols contain probabilistic and complexity theoretic aspects which require a different set of abstractions. Several approaches for dealing with this have appeared since, including: automated proof-checking; compositional techniques; higher level proof structures; abstractions of computational models; and specialised logics.
The CryptoForma network (www.cryptoforma.org.uk) brings together UK and international researchers working in these areas, including experts on cryptography, on formal methods, and on their interconnection, both from academia and from industry.
The network organises a yearly international workshop. The first of these was co-located with the PKC conference in Paris in May 2010 (http://www.cryptoforma.org.uk/event/first-cryptoforma-workshop-paris/) and attracted speakers and audience from several countries.
At this second workshop, co-located with FM 2011, CryptoForma reaches out explicitly to the international formal methods community. We invited three kinds of papers:
- papers surveying aspects of the state of the art in formal methods for cryptographic protocols, possibly of a tutorial nature;
- papers highlighting the problems posed by cryptographic applications where formal methods have not yet provided satisfactory solutions; and
- papers describing possible solutions to such problems, possibly on the basis of case studies.
Programme
Session 1
Session chair: Steve Schneider
- 9:00 Opening
- 9:10-9:50 Gilles Barthe, Benjamin Gregoire, Sylvain Heraud and Santiago Zanella Beguelin. Towards Automating Code-Based Game-Playing Cryptographic Proofs
- 9:50-10:30 Sreekanth Malladi and Logan Drews. How to prevent type-flaw and multi-protocol attacks on cryptographic protocols under Exclusive-OR
- 10:30-11:00 coffee
Session 2
Session chair: James Heather
- 11:00-11:30 Matteo Avalle, Alfredo Pironti and Riccardo Sisto. Formal Verification of Security Protocol Implementations: A Survey
- 11:30-12:00 Myrto Arapinis, Mark Ryan and Eike Ritter. Verification of stateful processes in ProVerif
- 12:00-12:30 Stephanie Delaune, Steve Kremer, Mark Ryan and Graham Steel. Formal analysis of protocols based on TPM state registers
- 12:30-14:00 lunch break (lunch is at 13:00)
Session 3
Session chair: Mark Ryan
- 14:00-14:30 James Heather, Steve Schneider and Vanessa Teague. Cryptographic Protocols with Everyday Objects
- 14:30-15:00 Dusko Pavlovic. Towards categorical cryptography
- 15:00-15:30 Thai Son Hoang, Annabelle Mciver, Larissa Meinicke, Anthony Sloane and Enrico Susatyo. Automated analysis of non-interference security by refinement
- 15:30-16:00 tea
Session 4
Session chair: Eerke Boiten
- 16:00-16:30 Murat Moran, James Heather and Steve Schneider. Anonymity and CSP for Voting Systems
- 16:30-17:00 Jean Everson Martina and Lawrence C. Paulson. Verifying Multicast Security Protocols Using the Inductive Method
- 17:00 close
Afterwards …
The final outcome of this workshop will be a special issue of the journal Formal Aspects of Computing. Submissions for the workshop have been reviewed for relevance to the theme, scientific quality, and feedback; authors of presented papers will be invited to submit for inclusion in the journal special issue some months after the event. Informal proceedings including presented papers will be distributed at the workshop. To avoid any constraints on later publication, the selection process for inclusion in the workshop programme does not constitute formal reviewing, and inclusion in the informal proceedings does not constitute a refereed publication.
- 5 September 2011 Journal special issue submissions due
Program chairs
Eerke Boiten, University of Kent, UK
Steve Schneider, University of Surrey, UK
Program committee
- Karthikeyan Bhargavan, INRIA Paris-Rocquencourt, France
- Bruno Blanchet, ENS, Paris, France
- Liqun Chen, Hewlett-Packard, UK
- Alex Dent, Royal Holloway, UK
- Andrew D. Gordon, Microsoft Research, Cambridge, UK
- Joshua Guttman, Worcester Polytechnic Institute, US
- Jan Jürjens, TU Dortmund, Germany
- Annabelle McIver, Macquarie University, Australia
- Alfredo Pironti Politecnico di Torino, Italy
- Eike Ritter, University of Birmingham, UK
- Michael Roe, University of Hertfordshire, UK
- Mark Ryan, University of Birmingham, UK
- Peter Ryan, University of Luxemburg
- Riccardo Sisto, Politecnico di Torino, Italy
- Graham Steel, ENS-Cachan, France
- Bogdan Warinschi, University of Bristol, UK
CryptoForma contact information
- CryptoForma website
- Eerke Boiten to join the network or any queries or website updates.
- Join mailing list
- Join friends’ mailing list
- Facebook group
Comments are closed.