Concrete Key Hierarchy with Alloy

Last time we had a model that spelled out what we wanted from a secure key hierarchy. This time I’ll spell out a concrete hierarchy that satisfies the properties of the model. There was one change I made based on a review from Kaoru Kohashigawa: all keys must now be somewhere or be owned by a person

I won’t explain every detail of the concrete model but will just show the whole thing and then show the diagram that Alloy generates because it is easy to see what is going on from the diagram. Basically we have two people/groups that have access to certain keys and places. Alloy verifies that the model is consistent so if you believe the original model is secure then the concrete model is also secure because it satisfies all the requirements. You can find the entire model at experimental-dustbin/alloy-models

Alloy diagram of an encryption key hierarchy

Encryption Key Hierarchy