Machine Readable Travel Documents

In the context of Machine Readable Travel Documents several security issues arise whose criticality demands for the use of formal methods. One of these issues is concerned with the secure communication between the travel document with its integrated RFID-Chip keeping the biometric reference data and the local inspection system.
In the MRTD project the underlying cryptographic protocol has been completely formalized and verified with the help of the VSE system. In the course of the project the library of specification primitives for cryptographic protocols as well as heuristics for the automation of proof generation developed in Verisoft and one of its predecessor projects has been extended.

Secure Agent-Based Pervasive Computing

Main goal of SCALLOPS is to develop a coherent, methodological framework for the design and implementation of secure agent-based pervasive computing applications. Basic research is on innovative means for flexible agent-coordinated semantic Web service discovery and composition, and effective data and service privacy enforcement in open, large scale pervasive computing environments. For this purpose, we will draw in particular on our expertise in the areas of security, multiagent systems, and service co-ordination. Research on the pervasive computational infrastructure is outside the scope of this project, instead we will rely on existing and appropriate standards, techniques, and open source software in this area where necessary. The application domain of our research will be Personal Health Information (Health-SCALLOPS).

Formalization and Verification of Security Policies for OS

The DFG-project UmSicht is concerned with the development and application of formal security policies based on the notion of possibilistic information flow. A main goal of UmSicht is to explore the transfer of the developed principles for specifying information flow policies (e.g. MAKS) to realistic applications. Arising problems are concerned with an appropriate notion of action refinements or the embedding of cryptographical operations in this framework.

Pervasive formal verification of computer systems

Verisoft aims at the pervasive verification of large systems On the one hand this includes formal modelling techniques that connect the various system and abstraction levels - from hardware to application level programs. On the other hand it also comprises an integrated deductive technology that allows for a combination of fully automatic (push button) approaches with interactive theorem proving. A more advanced version of VSE is used within Verisoft for security modelling and for the development of concurrent applications that ultimately will be implemented in C0, a subset of C considered in Verisoft. Verisoft is an integrated project with partners from industry and academia and is funded by BMBF.