Logic-Based Dynamical Security Policy Language and Verification

Expression, query evaluation and verification are great significant to dynamical security policy management, but they are very difficult to solve at present. This paper proposes a logic system, called SSML, which can be used to declare, evaluate and verify dynamic security policy. Firstly, we propose the syntax and the semantic of SSML (simple state modifying logic) based on logic programming theory, which shows that an SSML security policy can dynamically insert facts into itself or delete facts from itself. Then, we prove that the query evaluation problem of logic systems based on SSML is undecidable in general, which shows that there is no general algorithm to be able to evaluate all SSML security policies. So we turn to research on its sub-languages, and find two types of SSML security policies with limited syntax-NDel security policies and TDel security policies, and they have decidable evaluation algorithms. We actually give their query evaluation algorithms-OLDTE and OLDTT. They are complete and sound, and have polynomial computation complexity. Eventually, we show how to use SSML to verify a security policy through an actual example. We claim that OLDTE and OLDTT can be widely used in security policy management and verification.