Prolog based approach to reasoning about dynamic hierarchical key assignment schemes

Abstract

The problem of allowing the higher level users access the information related to lower level is called Hierarchical Access Control Problem. In a hierarchical access control system, users are partitioned into a number of classes - called security classes, which are organized in a hierarchy. Hierarchies arise in systems where some users have higher privileges than others and a security class inherits the privileges of its descendant classes. A basic Hierarchical Key Assignment Scheme is a method of assigning an encryption key to each class in the hierarchy. In literature, there are number of such hierarchy schemes are available and many of them have formal proof models for security properties. Now a days mostly all the schemes have a solution for Dynamic Access Control problem. We found that for dynamic schemes no formal proof model is available so we can not make any arguments on security properties of such schemes. We present a new approach for automatic veri cation using Prolog for the analysis of existing dynamic and static hierarchical key assignment schemes and verify their security properties. We discover some new attacks on existing schemes and proposed a new scheme to overcome those attacks.