A Generic Algebraic Model for the Analysis of Cryptographic-Key Assignment Schemes

One of the means to implement information flow policies is by using a cryptographic approach commonly referred to as key assignment schemes. In this approach, information is made publicly available to users but in an encrypted form. Then, keys are assigned to users such that each key reveals a specified part of the information. Usually the distribution of keys follows a predefined scheme that specifies the ability of users to reveal information.In this paper, we present an algebraic approach based on idempotent commutative semirings to define, specify, and analyse key assignment schemes. Then, we illustrate its usage on two key assignment schemes selected from the literature. Also, we propose amendments to the studied schemes to extend their scopes. The proposed generic algebraic approach enables the verification of security properties at an abstract level in systems that use key assignment schemes. The verification takes into consideration the algebraic properties of schemes, and the considered relationships among the assigned keys. Then, it enables the verification of the secrecy properties of the system through algebraic calculations. All the calculations can be automated using a theorem prover such as Prover9.