ETH Zuerich - Homepage
Information Security

Model-based Testing of Security Policies

The goal of this project is to use security policies as model-based specifications and to derive test-cases for them. The policies are specified in Higher-order logic and we use HOL-TestGen, a test-case generator based on the theorem prover Isabelle/HOL to generate the test cases. This approach has already been applied to automatically generate test-cases for firewall policies - for both stateless and stateful firewalls.

Currently, we are investigating the security policies for a large-scale patient data-management system: the access framework for the National Program for IT in the NHS England (NPfIT). We focus on the policies governing access to the Summary Care Records held in the SPINE. Access to patient data in this system is governed by several concepts:

The combination of these different concepts serves as a challenging scenario for model-based policy specification, policy analysis, and policy testing.



Involved People

The project is funded by BT Group plc and carried out by a collaboration between the Information Security Group at ETH Zurich and the LRI of the University Paris-Sud (Orsay). The involved persons are:


Lukas Brügger


Wichtiger Hinweis:
Diese Website wird in älteren Versionen von Netscape ohne graphische Elemente dargestellt. Die Funktionalität der Website ist aber trotzdem gewährleistet. Wenn Sie diese Website regelmässig benutzen, empfehlen wir Ihnen, auf Ihrem Computer einen aktuellen Browser zu installieren. Weitere Informationen finden Sie auf
folgender Seite.

Important Note:
The content in this site is accessible to any browser or Internet device, however, some graphics will display correctly only in the newer versions of Netscape. To get the most out of our site we suggest you upgrade to a newer browser.
More information

© 2011 ETH Zurich | Imprint | Disclaimer | 17 June 2011