The formal analysis of security policy models is very important for DBMS to attain a higher assurance level.A novel formal analysis approach based on PVS for DBMS security polices was proposed.The modular system state, security properties and operation rules were presented by a series of algorithms and processes in our approach, which took advantage of the functional characteristic of PVS language.By analyzing the security of BeyonDB with the PVS theorem prover, it was shown that the approach can improve the efficiency of formal modeling and is effective in discovering system design faults
