University of Illinois at Chicago
Martinoia_Diego.pdf (482.28 kB)
Download file

Proving Correctness within an Access Control Evaluation Framework

Download (482.28 kB)
posted on 2013-10-24, 00:00 authored by Diego Martinoia
This thesis presents the proofs developed to demonstrate correctness of a case study within the Access Control Evaluation Framework (ACEF). ACEF is a theoretical framework developed at the University of Illinois at Chicago, aimed at creating application-sensitive implementations of access control policies, using well-known access control systems, while preserving some desirable properties. As the formal proof of these properties, including correctness, is usually a tedious process prone to error, a mixed approach was used, which relies on both human high-level abstraction and insight for the outlining of the proof sketches, and then verifies their formal correctness using a formal prover system. To achieve this, a generic template for ACEF for the Prototype Verification System formal prover was developed. The process of generating the proofs for this specific case study was also a benchmark for the validity of the template, as a first step towards the realization of a more automated approach to ACEF. In the conclusions, the validity of the approach is analyzed and possible future steps to improve it are outlined.



Zuck, Lenore


Computer Science

Degree Grantor

University of Illinois at Chicago

Degree Level

  • Masters

Committee Member

Hinrichs, Timothy Lanzi, Pier Luca

Submitted date



  • en

Issue date


Usage metrics


    No categories selected