TOP
Search the Dagstuhl Website
Looking for information on the websites of the individual seminars? - Then please:
Not found what you are looking for? - Some of our services have separate websites, each with its own search option. Please check the following list:
Schloss Dagstuhl - LZI - Logo
Schloss Dagstuhl Services
Seminars
Within this website:
External resources:
  • DOOR (for registering your stay at Dagstuhl)
  • DOSA (for proposing future Dagstuhl Seminars or Dagstuhl Perspectives Workshops)
Publishing
Within this website:
External resources:
dblp
Within this website:
External resources:
  • the dblp Computer Science Bibliography


Dagstuhl Seminar 11332

Security and Rewriting

( Aug 15 – Aug 18, 2011 )

(Click in the middle of the image to enlarge)

Permalink
Please use the following short url to reference this page: https://www.dagstuhl.de/11332

Organizers

Contact


Summary

Security is a fundamental problem in computer science. Because of the possible catastrophic problems that can arise from poor security, the ability to mathematically prove and formally verify the security of computer systems is vital. Research has been ongoing in this area since the 1970's and has been the subject of many Dagstuhl seminars, including (in the last three years) “Theoretical Foundations of Practical Information Security" (August 2008), and “Formal (Cryptographic) Protocol Verification Applied" (October 2007).

Research on formal proofs of security has demonstrated that rewriting techniques, including completion, narrowing, unification, play a central role in this area, for example:

  • Formally modeling the properties of cryptographic primitives: fundamental properties of the cryptographic primitives are presented as algebraic theories and used as a basis for security analysis.
  • Automatically proving security protocols: both the protocol and the attacker's possible actions can be modeled as a rewrite system and unification algorithms play a central role in the security analysis of such systems.
  • Formally specifying and verifying security policies: the (possibly infinite) set of allowed transitions may be a represented as a finite rewriting system. The views on a documents or a class of documents may be specified by tree automata.
  • Modeling and analysis of other security-critical applications: rewrite techniques are used to model and analyze the security of web services, APIs and systems for access control.

The goal of this seminar was (i) to bring together researchers who have a background in rewriting techniques and researchers who have a background in security applications (or both) (ii) to answer, among others, the following questions:

  • Are there specific problems in rewriting that stems from security applications and would deserve some further research? For instance, do the algebraic theories of cryptographic primitives enjoy some specific properties? Are there restrictions that are relevant to the applications and that would yield more efficient unification/rewriting algorithms? Which new challenges does the addition of an arbitrary attacker context bring? What are the specific problems on tree automata that are brought by security applications?
  • What are the limits/successes/failures of rewriting techniques in security applications?
  • What are the emerging research areas at the intersection of security and rewriting?

Participants
  • Myrto Arapinis (University of Birmingham, GB)
  • Alessandro Armando (University of Genova, IT) [dblp]
  • Yannick Chevalier (Paul Sabatier University - Toulouse, FR)
  • Hubert Comon-Lundh (ENS - Cachan, FR)
  • Cas Cremers (ETH Zürich, CH) [dblp]
  • Stéphanie Delaune (ENS - Cachan, FR) [dblp]
  • Dan Dougherty (Worcester Polytechnic Institute, US)
  • Santiago Escobar (Technical University of Valencia, ES)
  • Maribel Fernandez (King's College London, GB)
  • Cédric Fournet (Microsoft Research UK - Cambridge, GB) [dblp]
  • Joshua D. Guttman (Worcester Polytechnic Institute, US)
  • Hélène Kirchner (INRIA - Le Chesnay, FR) [dblp]
  • Steve Kremer (INRIA Lorraine - Nancy, FR) [dblp]
  • Ralf Küsters (Universität Trier, DE) [dblp]
  • Christopher Lynch (Clarkson University - Potsdam, US) [dblp]
  • Catherine Meadows (NRL - Washington, US)
  • José Meseguer (University of Illinois - Urbana-Champaign, US) [dblp]
  • Sebastian Mödersheim (Technical University of Denmark - Lyngby, DK)
  • Paliath Narendran (University of Albany - SUNY, US)
  • Vivek Nigam (LMU München, DE) [dblp]
  • Michaël Rusinowitch (INRIA Lorraine - Nancy, FR)
  • Mark D. Ryan (University of Birmingham, GB) [dblp]
  • Ralf Sasse (University of Illinois - Urbana-Champaign, US) [dblp]
  • Benedikt Schmidt (ETH Zürich, CH)
  • Helmut Seidl (TU München, DE) [dblp]
  • Slawomir Staworko (University of Lille III, FR)
  • Carolyn L. Talcott (SRI - Menlo Park, US) [dblp]
  • Sophie Tison (Lille I University, FR) [dblp]
  • Alwen Tiu (Australian National University - Canberra, AU)
  • Tomasz Truderung (University of Wroclaw, PL)
  • Luca Vigano (University of Verona, IT) [dblp]
  • Christoph Weidenbach (MPI für Informatik - Saarbrücken, DE) [dblp]

Classification
  • security / cryptography
  • semantics / formal methods
  • verification / logic

Keywords
  • Rewriting
  • Security
  • Protocols
  • Formal methods