The IRMA Community
Newsletters
Research IRM
Click a keyword to search titles using our InfoSci-OnDemand powered search:
|
Formal Verification of Access Control Policies for Critical IoT Systems
Abstract
This paper proposes a formally verifiable access control framework that integrates structured eXtensible access control markup language policy specification with finite-state abstraction and symbolic model checking using NuSMV. To evaluate the proposed framework, a simulated 150-node Internet of Things-based critical infrastructure environment was developed in MATLAB. The framework models three operational states, namely normal, abnormal, and emergency, while incorporating a contextual risk threshold of 0.8 for role-based authorization involving operator, emergency responder, adversary, and policymaker roles. Access control policies were transformed into a finite-state transition system and formally verified for safety, liveness, and non-interference properties. Experimental validation across five consecutive verification runs confirmed that all specified properties were satisfied without counterexamples. Performance evaluation demonstrated an average authorization latency of 0.154 ms, mean CPU utilization of 58%, and average energy consumption of 1.5 J.
Related Content
|
Xixiang Yin.
© 2026.
15 pages.
|
|
Lihua Wang, Pengfei Pei, Yiran He, Zihuan Huang, Shuai Hu.
© 2026.
23 pages.
|
|
Shivalaxmi Arumugham, P. Ranjit Jeba Thangaiah.
© 2026.
20 pages.
|
|
Yuqian Liu, Kairui Li, Mi Li.
© 2026.
13 pages.
|
|
Waleed A. Alrodhan.
© 2026.
33 pages.
|
|
Ling An.
© 2025.
19 pages.
|
|
Mi Li.
© 2025.
18 pages.
|
|
|