Modeling and Verification of Access Rights in Take-Grant Protection Model Using Colored Petri Nets

Abstract

Take-Grant protection model (TGPM) is a powerful method for modeling access rights in a wide range of systems. It is graph based formal method that can be used for studying situations that rights may unintentionally be transferred as rights leakage. Deduction of new rights using rules of this model is difficult and time-consuming task especially for systems that have numerous parties and many rights between them. In this paper a novel model of TGPM using colored Petri net is presented. Using model checking of state space of the model we can prove that a party in the system can have specific right over other party or not? If a right leakage exists, model checking of state space of the model can generate automatic proof for it.