Introduction

Encryption key hierarchies are by their nature hierarchical structures and the Alloy analyzer is very good at modeling such structures. In this post I'll outline some informal properties that we want out of such hierarchies and then formalize them in Alloy.

The model will consist of various relations like keys encrypting other keys, keys being owned by people/groups, keys being stored in various places in plaintext or encrypted forms, and people/groups having access to various places.

These are some of the informal properties that I came up with after thinking about it for a bit so I'm not claiming that this is security advice or that it will make your encryption key hierarchy bullet proof but they seem reasonable to me so here they are:

• No key encrypts itself (and in general the encryption relation is acyclic)
• If a key is stored somewhere in encrypted form then it is not stored in plaintext form at the same place because that defeats the purpose of encrypting the key in the first place
• Every key must be stored somewhere or be owned by some person/group (this is mostly to prevent random noise in the model because we don't want any dangling keys)
• If one key k encrypts another key k' then k can not be stored in plaintext form alongside k' because that would defeat the purpose of encrypting k'
• If a person has access to some place then they have access to all the plaintext keys in that place
• If a person owns a key k that encrypts another key k' and the place that k' is stored is accessible to that person then they also have access to k' because they can just decrypt k'

These properties are neither exhaustive nor minimal but they seem like sensible properties we'd want out of an encryption key hierarchy. If Alloy doesn't find any contradictions after we spell out all the details then we can be sure that the hierarchy satisfies all the properties we spelled out and assuming our formalization conforms to our intuitions we can be sure we're not violating any of the properties we formalized.

Specifying the Model in Alloy

First we'll specify the pieces we are working with along with some basic properties they must satisfy

abstract sig Key {
  // Keys can encrypt each other
  encrypts: set Key,
  // Keys can be stored in places in plaintext or encrypted form
  places: set (Property -> set Place)
} {
  // No key encrypts itself
  no (this & encrypts)
}

// Keys are stored in places
abstract sig Place { }

// Keys have properties that are associated with a place the key is at
enum Property { Encrypted, Plaintext }

// People that have access to places
abstract sig Person {
  // Person has access to places
  access: set Place,
  // They can also have access to keys
  keys: set Key
} {
  // If a person has access to a place then they have access to plaintext keys in that place
  all k: Key | Plaintext in k.places.access => k in keys
}

This gives us all the components along with various relations and properties we expect them to have. The important piece in the above specification is probably

all k: Key | Plaintext in k.places.access => k in keys

That's the property about plaintext keys being accessible to anyone that has access to the place where the key is stored in plaintext form.

Next we'll specify all the remaining properties as facts along with comments explaining which informal property they correspond to

// The hierarchy is acyclic
fact {
  all k: Key | no (k & k.^encrypts)
}

// Every key must be owned by a person or be in some place
fact {
  all k: Key | (some k.places || some p: Person | k in p.keys)
}

// If a key is encrypted in some place then it is not stored in
// plaintext at same place
fact {
  all k: Key | no (k.places[Encrypted] & k.places[Plaintext])
}

// If a key encrypts another key then the encrypted key
// must appear encrypted somewhere
fact {
  all k: Key, k': k.encrypts | some k'.places[Encrypted]
}

// If a key encrypts another key then it can not be
// stored in plaintext alongside it
fact {
  all k: Key, k': k.encrypts | no (k.places[Plaintext] & k'.places[Property])
}

// If a person has access to a key and that key encrypts
// another key that is placed somewhere the person
// has access to then that person also has access to that key
fact {
  all p: Person, k: p.keys, k': k.encrypts {
    some k'.places[Property] & p.access => k' in p.keys
  }
}

The last property is the most complicated one because it relates all 3 components to each other. I like how the informal explanation is actually longer than the logical specification. I think it shows the power of a good language for specifying models and how concise things can be when expressed in a logical language.

So far everything is mostly abstract and there are no details about a concrete hierarchy. If you run this model you will get some results but without further restrictions they're not that interesting so that's what we'll do next.

Specifying Concrete Details

One reason I started working on this model was because I wanted to verify a specific hierarchy was actually valid (in the sense that it satisfied all the informal properties I expected from key hierarchies). To fill in those details we can abstract what we have so far into an Alloy module and then import and use it in another module that lists the concrete details. If this was for production purposes then that's what I'd do but for demonstration purposes keeping everything in a single file/module is good enough so that's what we'll do.

Extending the abstract model with concrete details is pretty simple. We'll specify the concrete components and put in the relations we expect to hold for them (If you're following along then I recommend running the model after adding each component to see how it affects the kinds of models that Alloy finds)

// These are some places we will be storing keys
one sig Git, Lastpass, Production extends Place { }

// These are some people that will have access to keys and places
one sig InfraPerson, DevPerson extends Person { }

// Keys and their relationships
one sig DevKey, InfraKey,
  InfraKeyPassword, DevKeyPassword,
  LastpassPassword extends Key { }

// Facts about InfraPerson
fact {
  // Infra person has all the infra keys and passwords
  (InfraKey + InfraKeyPassword + LastpassPassword) in InfraPerson.keys
  // InfraPerson can access everything
  Place = InfraPerson.access
}

// Facts about DevPerson
fact {
  // Dev person can access the dev key password
  DevKeyPassword in DevPerson.keys
  // They can access Git and Production
  (Git + Production) = DevPerson.access
}

// Key encryption facts
fact {
  // The infra key password encrypts infra key
  InfraKey = InfraKeyPassword.encrypts
  // Lastpass encrypts infra key password and infra key
  (InfraKeyPassword + InfraKey) = LastpassPassword.encrypts
  // Dev key password encrypts dev key
  DevKey = DevKeyPassword.encrypts
  // Infra key encrypts dev key password
  DevKeyPassword = InfraKey.encrypts
}

// Where each key is stored
fact {
  // Infra keys are stored in lastpass
  (Encrypted -> Lastpass) = InfraKeyPassword.places
  (Encrypted -> Lastpass) = InfraKey.places
  // Dev keys are stored in git and one of the keys is stored in production in plaintext
  (Encrypted -> Git) = DevKeyPassword.places
  (Encrypted -> Git + Plaintext -> Production) = DevKey.places
}

// Few more facts about the keys to rule out extraneous models
fact {
  // Dev key does not encrypt any other keys
  no DevKey.encrypts
  // Dev person does not have access to infra keys
  no (InfraKey + InfraKeyPassword + LastpassPassword) & DevPerson.keys
  // Lastpass password is not stored anywhere and is just owned by the infra person
  no LastpassPassword.places
}

Running this specification in Alloy we see that it finds a model which means everything is logically consistent with what we wanted out of an encryption key hierarchy

Further Work

If you got this far then good work and here are a few directions you can take this.

One idea is to modify the model so that it synthesizes a list of instructions for rotating a key. I've often been in places where key rotation was an undefined operation because no one knew all the places various keys were used and stored. If they'd used Alloy to specify their key hierarchy then they wouldn't have had that problem but you know, what are you gonna do, can't save everyone. But if this kind of tool had existed then it would have saved people a whole bunch of trouble and maybe could indeed have saved them.

Another idea is to verify the specification agrees with industry practices for key hierarchies. Maybe some of the properties in this model actually make it broken in real world scenarios. Finding that out would definitely be useful.

The code for this lives over at GitHub and any improvements and suggestions for improvements are all welcome.

$ ./keygen.sh 6428f5771007cf005037d47c9aeac9bfcc8925f9  -