Invited Speakers

Sebastian Mödersheim

Technical University of Denmark
Title: Rewriting Privacy

Privacy properties are very relevant for security protocols, e.g., privacy of votes in electronic voting, privacy of personal data in e-health care applications, or unlinkability of several transactions by the same user. The de-facto standard to express these properties is via bisimilarity of two processes, e.g. that an intruder cannot distinguish two processes of electronic voting that differ only by swapping the vote of two honest voters. This yields rather technical specifications of systems and their properties, so that it is hard to convince oneself that this specification truly captures all the intuitive privacy goals one wishes to achieve. Moreover verification with bisimilarity in general is hard to automate, and several approaches choose to consider very restricted notions in order to achieve an automated verification procedure.

Together with my colleagues, we have developed an alternative approach called Alpha-Beta-Privacy. The fundamental difference to previous approaches is that we do not describe privacy as a distinction between two possible states of the word, but rather as a single world and logically reasoning what the intruder can find out about this world. We describe every state of the world by two logical formulas in First-Order Logic with Herbrand universes: alpha is a formula that describes high-level information that is considered public (e.g., that there are N binary votes, and R of them are “yes”), and beta describes low-level information (e.g., all the cryptographic messages the intruder has observed and what he knows about their structure). Privacy then means that every model of alpha can be extended to a model of beta, i.e., the technical messages the intruder can observe do not allow him to learn anything that is not entailed by the official information alpha.

Based on such worlds (alpha,beta) we define transition systems that arise from the intruder interacting with several participants (augmenting beta), and gradually information being released (augmenting alpha). This models what the intruder can derive when knowing the processes that the honest agents are executing (but not necessarily the concrete values they work with) in a rewriting based evaluation. This makes privacy actually a reachability problem: can the system reach a state where the intruder learns a statement something he should not be able to.

While in general the underlying problems are undecidable, we show that using rewriting techniques and symbolic representations we can obtain an effective procedure for a bounded number of sessions with a standard algebraic theory of the cryptographic operators.


  • 01/2003-03/2007 Doctoral Student at ETH Zürich, Advisor David Basin (Information Security Group)
  • 04/2007-05/2010 Postdoc at IBM Research Laboratory Zürich
  • 06/2010-10/2012 Assistant Professor at Technical University of Denmark (DTU), Computer Science Department
  • Since 11/2012 Associate Professor

Main interests: automated verification and interactive theorem proving for security, compositional reasoning, and privacy

Gwen Salaün

Technical University of Denmark
Title: Modelling and Quantitative Analysis of BPMN Processes using Maude

Business process modelling and optimization is a strategic activity in organizations because of its potential to increase profit margins and reduce operating costs. The Business Process Model and Notation (BPMN) is a graphical modeling language for specifying business processes using a workflow-based notation. BPMN collaboration diagrams are particularly convenient for describing processes consisting of several participants interacting by exchanging messages. Providing automated techniques for analyzing and optimizing BPMN processes is a challenging problem. In this work, we first propose to encode the BPMN syntax and execution semantics in rewriting logic. Then, we rely on the rewriting logic framework and use the Maude system to stochastically simulate multiple concurrent executions of a process instance that compete for the shared resources. This simulation allows us to automatically compute several properties of interest such as average execution time, synchronization times for merge gateways or resource occupancy over time. We will illustrate these ideas with several examples including realistic processes with large workloads.

Gwen Salaün received a PhD degree in Computer Science from the University of Nantes (France) in 2003. In 2003-2004, he held a post-doctoral position at the University of Rome "La Sapienza" (Italy). In 2004-2006, he held a second post-doctoral position at Inria (Grenoble, France). In 2006-2009, he was research associate at the University of Malaga (Spain). He was associate professor at Ensimag / Grenoble INP (France) from 2009 to 2016. He is currently full professor at Université Grenoble Alpes. His topics of interest are formal methods, automated verification, distributed systems and software engineering.