Secrecy and Information Flow in Shared Document Bases

The subject of this project is the analysis of secrecy and information flow in applications where multiple users execute a workflow while sharing a common document base. Our objective is to generalize classic notions of secrecy such as noninterference so that the designer can precisely state the intended information flow as it changes over time in response to changes in the state of the workflow as well as strategic choices by the different users of the system. The new specification language will be supported by a semantically substantiated security analysis based on a multi-player game model of the interaction between the users. Extending counterexample-guided abstraction refinement (CEGAR) to such models, we will obtain automatic methods for verification and certificate synthesis.

Principal Investigators

• Bernd Finkbeiner, Universität des Saarlandes
• Helmut Seidl, TU München