detecting flaws in dynamic hierarchical key management schemes using specification animation

Abstract

In key assignment schemes for hierarchical access control systems, each access class has a key associated with it that can be used to derive the keys associated with every descendant of that class. Many recently proposed key assignment schemes support updates to the hierarchy such as addition and deletion of classes and class relationships. The dynamic changes entail a change to the hierarchy as well as re-computing of public and secret information. In this paper, we describe a software tool that supports the animation of specifications of dynamic schemes. The specification of a scheme, written in Prolog, corresponds to a symbolic model of the algorithms used by the scheme for key generation and for handling dynamic changes. The tool allows us to generate a test hierarchy, generate keys for the classes in the hierarchy, and simulate various dynamic operations. The animation search using the tool has shown to be useful in finding previously unreported attacks on several existing dynamic schemes.