Hoang, Thai S.
Rights / licenseIn Copyright - Non-Commercial Use Permitted
We investigate the idea of developing access control systems in Event-B by specifying separately the "insecure" target system and the security authorisation, then combining them together in order to construct a secure system. This is based on the work by Basin et. al.  where the chosen language is CSP-OZ. Moreover, in order to verify the secure system against some safety temporal properties, we propose an approach of constructing several abstract models corresponding to these properties, and using refinement to prove that the final system satisfies these properties Show more
External linksSearch via SFX
Journal / seriesTechnical report
PublisherETH, Department of Computer Science
SubjectACCESS CONTROL (OPERATING SYSTEMS); Security; SPEZIFIKATIONSSPRACHEN (SOFTWARE ENGINEERING); SPECIFICATION LANGUAGES (SOFTWARE ENGINEERING); Event-B; Access control; Temporal property; ZUGRIFFSKONTROLLE (BETRIEBSSYSTEME)
Organisational unit02150 - Dep. Informatik / Dep. of Computer Science
03634 - Basin, David / Basin, David
NotesTechnical Reports D-INFK.
MoreShow all metadata