August 18 – 23 , 2013, Dagstuhl Seminar 13341

Verifiably Secure Process-Aware Information Systems


Rafael Accorsi (Universität Freiburg, DE)
Jason Crampton (Royal Holloway University of London, GB)
Michael Huth (Imperial College London, GB)
Stefanie Rinderle-Ma (Universität Wien, AT)

For support, please contact

Dagstuhl Service Team


Dagstuhl Report, Volume 3, Issue 8 Dagstuhl Report
Aims & Scope
List of Participants


Business processes play a major role in many commercial software systems and are of considerable interest to the research communities in Software Engineering, and Information and System Security. A process-aware information system provides support for the specification, execution, monitoring and auditing of intra- as well as cross-organizational business processes.

Designing and enacting secure business processes is as tricky as "Programming Satan's Computer", as Ross Anderson and Roger Needham observed in a paper with that title. Recent fraud disasters show how subtle secure process engineering and control can be. The Swiss bank UBS suffered from a rogue trader scandal in 2011, which led to a loss of a then-estimated US$2 billion, was possible because the risk of trades could be disguised by using "forward-settling" Exchange-traded Funds (ETF) cash positions. Specifically, processes that implemented ETF transactions in Europe do not issue confirmations until after settlement has taken place. The exploitation of this process allows a party in a transaction to receive payment for a trade before the transaction has been confirmed. While the cash proceeds in this scheme cannot be simply retrieved, the seller may still show the cash on their books and possibly use it in further transactions. Eventually, the mechanics of this attack allowed for a carrousel of transactions, thereby creating an ever growing snowball. Similar analyses, usually based upon insider threats, can also be made for fraud cases such as the well-documented Société Générale case, but also for the WorldCom and Parmalat cases.

Addressing these problems requires, on the one hand, strong security and compliance guarantees. On the other hand, these guarantees must be substantiated by formal methods ensuring a verifiably secure business process enactment. It should be noted that these concerns are not confined to the financial service sector or to insider threats. For example, the planned unification of Eurpean data protection law into a sole Data Protection Regulation law is likely to change the statuatory duties of the private sector. Under this plan, companies will be legally required to report any breaches of this regulation and may be liable to penalties in the range of 2--5% of their global annual turnover. European industries seem to be ill-prepared to ensure that their information systems and processes will comply with the security requirements of that upcoming regulation, and the threat of substantial fines means that there is an urgent need to create more resilient systems and processes, which calls for more research within the thematic scope of this seminar.

At the interface of security requirements, business needs, and compliance methodologies we can ask many practically relevant research questions, and their answers are bound to have significant impact in academia and industry alike. Relatively little work has been done, however, on adapting or creating new formal methods with which one can check that processes are compliant with rules, preserve demanded privacy constraints, and enforce desired security policies at the same time.

One main purpose of the seminar was to present the state of the art in research within the three communities of Security, Verification, and Process-Aware Information Systems to all three communities in an accessible manner and with a view of identifying important research topics at the intersections of these communities. In addition, that exercise was also meant to explore what strategic activities could help in promoting research at the junction of these communities. This agenda was persued through a mix of keynotes, technical presentations, break-out groups under the WorldCafe method, sessions with free-style discussions, and tool demonstrations.

We now highlight some of the key questions and findings can emerged during that week of work - we refer to the online archive of presentation slides, papers, and abstracts for more detailed discussions and findings. Three action items that seemed of particular importance to the participants were:

  1. The need for a classification of security properties that are revelant for process-aware information systems, and an understanding of what formal methods might be able to analyse such properties.
  2. The need for a set of concrete examples of business processes that are annotated with security considerations or constraints. These might be examples from the real world that have been sufficiently sanatized and anonymized.
  3. The need for a review/survey article on the state of the art in formal methods, written for non-experts and ideally for an audience that deals with security, privacy, audit or business processes.

It was also asked what makes formal methods and tools "practical" in this problem space; their was concern about the scalability of these methods, but also about the considerable effort it would take to transfer foundational tools to real application domains - were such somewhat routine but important transfer may not be supported by standing funding models. Concerns were also voiced about the current research in security and privacy, which tends to ignore recent innovations in process composition, such as choreographies.

Another point of considerable interest made concerned the organization of research in this problem space. At the moment, researchers work on problems within their areas and when they begin to collaborate with people from another area this is then more of a bottom-up process where techniques and tools across areas are combined to see what problems one could now solve. It was remarked that it may often be more effective to take a top-down approach in which key problems of the inter-area domain are first formulated and then researchers from the areas get together and try to come up with solutions that draw from their own tool boxes but that may also invent new tools for the problem at hand.

There was also a lot of discussion about what is so distinctive about process-aware information systems, and whether these differences to conventional information systems offer perhaps also opportunities. For example, it was discussed whether there is value in validating such systems at a high level of abstraction without considering how such processes get implemented in IT infrastructures and abstraction layers. The participants had mixed views on such merits but it was felt that validation at that level would be easier to realize and that the identification of weaknesses or vulnerabilities at that layer would no doubt be of value.

Another problem mentioned was the need to support legacy systems, and that this need would not go away. Faced with this, it appears that formal validation techniques will have to be able to reason about composed systems in which some parts only have a somewhat well defined interface, but whose internal behavior cannot be guaranteed or predicted to a good degree.

Finally, it was also noted that some of the research problems that suggest themselves to the specialists may not be issues in the field. For example, we may want trusted system composition across organizations but there may not be the need to formally validate such trust since contractual or other legal mechanisms may be in place that incentivize parties to honor that trust, and that give parties a means of seeking damages in case that trust has been violated. On the other hand, such legal mechanisms may not be adequate in the upcoming Internet of Things were 2-party, end-to-end composition will be the exception and not the norm.

Summary text license
  Creative Commons BY 3.0 Unported license
  Rafael Accorsi, Jason Crampton, Michael Huth, and Stefanie Rinderle-Ma


  • Data Bases / Information Retrieval
  • Security / Cryptology
  • Verification / Logic


  • Model-based Abstraction Techniques
  • Process-aware Information Systems
  • Evolutionary Process Models
  • Process Mining
  • Security
  • Audit and Control
  • Policy Management and Enforcement
  • Formalization of Policies
  • Business Rules and Regulation
  • Verification


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.