Modelling and verifying dynamic access control policies using knowledge-based model checking

摘要: This thesis advances the modelling and verification of access control policies by using automated knowledge-based symbolic model checking techniques. The key contributions this are threefold: firstly, a language that expresses dynamic with compound actions update multiple variables; secondly, algorithm verifies properties over an policy has actions; finally, tool, called X-Policy, which implements algorithm. This research enables us to verify for web-based collaborative systems. We analyse number conference management systems their security properties. propose appropriate modifications rectify when possible. Ultimately, will allow more help avoid current situation.