A Correct-by-Construction Model for Request-Based Access Control
摘要
Information systems face a persistent threat from internal attacks perpetrated by privileged users. Traditional access control models, often relying on user trust, are inadequate in preventing such breaches. To address this, we propose a novel approach that eliminates the assumption of user trustworthiness. By extending the organization-based model with a dual control mechanism, we introduce a request approval process as a fundamental security measure. Critical or risky actions require authorization from the user’s chain of command, mitigating the risk of unauthorized access and malicious activities. This paper presents a formally verified model of our proposed approach, implemented using the Event-B language and Rodin tools. Finally, we implemented an authorisation system including dual control.