Access Control for Next Generation Systems


This project started on the 12th of January 2012 and has been successfully completed.


Petar Tsankov (ETH)
Prof. David Basin (ETH)
Paul Studerus (dormakaba)


Modern physical access control systems indicate a trend of abandoning traditional physical keys and moving towards contactless, Internet-based access media solutions. In recent years, access control systems have vastly benefited from formal languages, which divorce a policy specification from an actual PDP implementation. The emerging access control systems will allow for previously impossible use cases. For example, a person can book a hotel room and access it directly using a smart-phone, without having to queue at the reception desk. The increased complexity of these systems in combination with the high-security requirements of security critical areas such as airports makes the ask of designing and building such access control systems challenging.

In this project, we focus on formal specification, verification, and synthesis of access control systems for physical spaces. In particular, we address the following research topics:
– Design of expressive declarative languages with efficient evaluation
– Design of realistic attacker models
– Verification of access control specifications against requirements
– Synthesis of access control enforcement mechanisms from global,
system-wide requirements


Petar Tsankov, Srdjan Marinovic, Mohammad Torabi Dashti, David Basin
Fail-Secure Access Control
ACM Conference on Computer and Communication Security (CCS), 2014

Petar Tsankov, Srdjan Marinovic, Mohammad Torabi Dashti, David Basin
Decentralized Composite Access Control