Specifying Access Control in Event-B
dc.contributor.author
Hoang, Thai S.
dc.contributor.author
Basin, David
dc.contributor.author
Abrial, Jean-Raymond
dc.date.accessioned
2018-03-08T13:12:05Z
dc.date.available
2017-06-08T21:55:04Z
dc.date.available
2018-03-08T13:12:05Z
dc.date.issued
2009
dc.identifier.uri
http://hdl.handle.net/20.500.11850/15887
dc.identifier.doi
10.3929/ethz-a-006733720
dc.description.abstract
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. [6] 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.
en_US
dc.format
application/pdf
dc.language.iso
en
en_US
dc.publisher
ETH, Department of Computer Science
en_US
dc.rights.uri
http://rightsstatements.org/page/InC-NC/1.0/
dc.subject
ACCESS CONTROL (OPERATING SYSTEMS)
en_US
dc.subject
Security
en_US
dc.subject
SPEZIFIKATIONSSPRACHEN (SOFTWARE ENGINEERING)
en_US
dc.subject
SPECIFICATION LANGUAGES (SOFTWARE ENGINEERING)
en_US
dc.subject
Event-B
en_US
dc.subject
Access control
en_US
dc.subject
Temporal property
en_US
dc.subject
ZUGRIFFSKONTROLLE (BETRIEBSSYSTEME)
en_US
dc.title
Specifying Access Control in Event-B
en_US
dc.type
Report
dc.rights.license
In Copyright - Non-Commercial Use Permitted
ethz.journal.title
Technical report
ethz.journal.volume
624
en_US
ethz.size
17 p.
en_US
ethz.code.ddc
DDC - DDC::0 - Computer science, information & general works::004 - Data processing, computer science
en_US
ethz.notes
Technical Reports D-INFK.
en_US
ethz.identifier.nebis
006733720
ethz.publication.place
Zurich
en_US
ethz.publication.status
published
en_US
ethz.leitzahl
ETH Zürich::00002 - ETH Zürich::00012 - Lehre und Forschung::00007 - Departemente::02150 - Dep. Informatik / Dep. of Computer Science
en_US
ethz.leitzahl
ETH Zürich::00002 - ETH Zürich::00012 - Lehre und Forschung::00007 - Departemente::02150 - Dep. Informatik / Dep. of Computer Science::02660 - Institut für Informationssicherheit / Institute of Information Security::03634 - Basin, David / Basin, David
en_US
ethz.leitzahl.certified
ETH Zürich::00002 - ETH Zürich::00012 - Lehre und Forschung::00007 - Departemente::02150 - Dep. Informatik / Dep. of Computer Science::02660 - Institut für Informationssicherheit / Institute of Information Security::03634 - Basin, David / Basin, David
ethz.date.deposited
2017-06-08T21:55:15Z
ethz.source
ECOL
ethz.source
ECIT
ethz.identifier.importid
imp59366b140365242733
ethz.identifier.importid
imp59364c5ac7e7539387
ethz.ecolpid
eth:4727
ethz.ecitpid
pub:27716
ethz.eth
yes
en_US
ethz.availability
Open access
en_US
ethz.rosetta.installDate
2017-07-20T14:09:40Z
ethz.rosetta.lastUpdated
2022-03-28T19:23:11Z
ethz.rosetta.versionExported
true
ethz.COinS
ctx_ver=Z39.88-2004&rft_val_fmt=info:ofi/fmt:kev:mtx:journal&rft.atitle=Specifying%20Access%20Control%20in%20Event-B&rft.jtitle=Technical%20report&rft.date=2009&rft.volume=624&rft.au=Hoang,%20Thai%20S.&Basin,%20David&Abrial,%20Jean-Raymond&rft.genre=report&
Files in this item
Publication type
-
Report [6798]