Game-Theoretic and Formal Approaches to Securing Non-human Accounts in Identity and Access Management
摘要
NHAs, such as service accounts, bots, and IoT devices, are an essential component of today’s computing ecosystems, but continue to be under-addressed in the current IAM frameworks 1. Being privileges without supervision, such an enhanced role of responsibility becomes often exposed to being a point of frequent exploitation, misuse and policy misconfiguration. To fill this void, we present a hybrid security framework for combining game-theoretic attack–defense modeling with formal verification of IAM policies. The game-theoretic model yields optimal defense strategies for preventing resource abuse, whereas formal methods (such as Z3, Alloy, SPIN) guarantee correctness and resilience to misconfigurations. In contrast, previous IAM methods consider them separately 3, our dual-pronged model preserves NHAs with end-to-end pipeline. Experimental results show the proposed approach could decrease access violation by 94 percent and improve average response time by 1–2 s over the traditional IAM solutions. This paper presents a strict, scalable and verifiable solution to NHA security, it is theoretical and application-oriented, suitable for enterprise and cloud.