ORCID
Shiu-Kai Chin: 0009-0007-5318-923X
Document Type
Article
Date
Summer 6-20-2026
Keywords
access-control logic, HOL-4, formal methods, modal logic, Kripke semantics, theorem proving, speaks-for, integrity policy, principal, machine-checked proof
Language
English
Disciplines
Electrical and Computer Engineering
Description/Abstract
This manual documents the embedding of an access-control logic (ACL) — as presented in the textbook Access Control, Security, and Trust: A Logical Approach (Chin and Older, 2011) — within the Cambridge Higher-Order Logic theorem prover HOL-4. The logic is a multi-agent modal logic with Kripke semantics. Its purpose is to reason about authentication, authorization, integrity, security, and trust. The inference rules of the ACL are proved to be sound. The inference rules are a command-and-control (C2) calculus. The value of the ACL is its support for rigorous, verified, and trustworthy policies for complete mediation, i.e., where all actions are authenticated and authorized.
The manual presents the logic's syntax, semantics, and inference rules, then details their mechanized implementation in HOL-4 as HOL types, definitions, and proved theorems. Inference rules from the textbook are rendered as HOL inference rules and tactics, enabling machine-checked proofs of access-control properties. Worked examples — including a Biba-style integrity example — illustrate how to construct proofs interactively within HOL-4.
Appendices provide a complete reference for all ACL inference rules, tactics, and theories (aclfoundation, aclsemantics, aclrules, and aclDrules), together with full Standard ML source files. The manual serves as both a user's guide and a reference for researchers and practitioners who wish to apply machine-checked formal methods to access control, security policy analysis, and trust reasoning. It was developed in conjunction with the Air Force Research Laboratory's Advanced Course in Engineering Cybersecurity Boot Camp and Syracuse University's Cyber Engineering Semester program.
Recommended Citation
Chin, Shiu-Kai, "An Access-Control Logic in HOL (Trindemossen 2)" (2026). Electrical Engineering and Computer Science - All Scholarship. 254.
https://surface.syr.edu/eecs/254
Source
submission
Creative Commons License
This work is licensed under a Creative Commons Attribution 4.0 International License.
