Modelling Encryption Key Hierarchies with Alloy

Setting up key hierarchies with the proper access rights can be a little tricky because reasoning through the implications of access and storage can get a little convoluted. Some questions I had when I was trying to do this at work was how do I set things up so that people can have the access they need without jumping through too many hoops and how many hoops do I need for non-trivial security properties? Also, which keys need to encrypt which other keys and where/how can they be stored without sacrificing security? Continue reading