August 15 – 18 , 2011, Dagstuhl Seminar 11332

Security and Rewriting


Hubert Comon-Lundh (ENS – Cachan, FR)
Ralf Küsters (Universität Trier, DE)
Catherine Meadows (NRL – Washington, US)

For support, please contact

Dagstuhl Service Team


Dagstuhl Report, Volume 1, Issue 8 Dagstuhl Report
List of Participants


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?


  • Security / Cryptography
  • Semantics / Formal Methods
  • Verification / Logic


  • Rewriting
  • Security
  • Protocols
  • Formal methods


In the series Dagstuhl Reports each Dagstuhl Seminar and Dagstuhl Perspectives Workshop is documented. The seminar organizers, in cooperation with the collector, prepare a report that includes contributions from the participants' talks together with a summary of the seminar.


Download overview leaflet (PDF).

Dagstuhl's Impact

Please inform us when a publication was published as a result from your seminar. These publications are listed in the category Dagstuhl's Impact and are presented on a special shelf on the ground floor of the library.


Furthermore, a comprehensive peer-reviewed collection of research papers can be published in the series Dagstuhl Follow-Ups.