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?

Instead of trying to derive the answers to those questions from first principles we are going to model the problem in Alloy and then plug in concrete implementation details to see what happens. We are going to leverage Alloy’s capabilities to tell us if our implementation is good or if it is equivalent to security theatre.

The model consists of people/groups, places, keys, and key properties. Keys can encrypt each other and keys can be stored in various places either in plaintext or encrypted forms. Those are the basic components so lets spell them out in Alloy

The above says that keys can encrypt other keys and they can appear in various places with some associated properties. Keys obviously are not allowed to encrypt themselves because there is no point to doing that. We will add more restrictions as we spell out more details of the model.

Keys can appear in places. Some keys will not have any place. You can think of place-less keys as passwords that are only stored in someone’s head.

There are two properties we care about at the moment when it comes to keys: encrypted, plaintext. For place-less keys we’ll leave their properties undefined because the assumption is they can’t be accessed anyway so their properties are mostly irrelevant.

This is the first constraint that spells out some non-trivial interactions between keys, places, and properties. The above says that the places where a key is stored in encrypted form is disjoint from the places where it is stored in plaintext. This kinda makes sense because if a key is stored in plaintext then there is no point to store it at the same place in encrypted form because we already have it in plaintext form.

This one says that if a key encrypts another key then the encrypted key must be stored somewhere in encrypted form, otherwise what was the point of encrypting the key? One could argue against this restriction but I’m trying to model the safe and durable storage of keys so in that setting this restriction makes sense.

Similarly if one key encrypts another then the encrypting key can not appear in plaintext form alongside the key that it encrypts because that defeats the purpose of the encryption and both keys are trivially recoverable which is something we want to avoid.

So far we only have keys and places and most of the these properties are obvious. We’d want them of any key hierarchy but keys in a hierarchy are kinda meaningless if there are no people that have access to the keys to use them. If you run the above model you will get some interesting results like cyclic hierarchies.

Let’s add people into the mix that have access to keys and places and spell out the invariants that must be satisfied for key ownership and key storage access

Hopefully the restriction is again obvious. If a person has access to a place then they have access to all the plaintext keys in that place.

Now we spell out a slightly more tricky constraints about keys, places, and people

The above says that if a person has access to a place and keys that encrypt other keys in that place then they have access to the keys in that place because they can just decrypt the keys and see them in plaintext.

Running this model now will also come up with circular key hierarchies but they won’t be trivial hierarchies because even if the encryption hierarchy is cyclic it doesn’t necessarily mean people can decrypt all the keys because they might not have access to all the places the keys are stored.

That’s probably enough for now. For the next post I’ll spell out some concrete implementation details so we can see what happens in a real world scenario.