EECS 755

Software Requirements Modeling and Analysis


Project 3

The objective of this project is to develop and verify a Coq model of an encryption key server and encryption key processing. A key server performs the simple task of associating a name with an encryption key used to encrypt information for a particular user. Key processing involves obtaining and validating encryption keys. You will use the model of perfect cryptography developed in class as a basis for your project.

Public/private key encryption involves managing asymmetric encryption key pairs. Each private key is held in secret by its associated user and is used to decrypt messages encrypted using its associated public key and generate signatures that can be checked using its public key. A public key is shared by the user and can be used to encrypt information and check signatures generated by it’s associated private key. It is essential to remember that the private key decrypts and signs while the public key encrypts and checks signatures.

If User A wants to send a secure document to User B, A engages in the following tasks:

  1. Retrieve B’s public key
  2. Validate B’s public key
  3. Encrypt the secure data with B’s public key
  4. Sign the encrypted file with A’s privatekey

Upon receiving the signed, encrypted file, B engages in the following tasks:

  1. Retrieve A’s publickey
  2. Validate A‘spublickey
  3. Authenticate A’s signature
  4. Decrypt the secure data with B’s private key

This kind of information exchange must be supported by a key escrow system. Key escrow is simply a means for storing public keys in a networking system in a manner much like a domain name server (DNS). Given a key request, the key server looks up the key, signs it, and returns it. The signature assures the recipient that the key does in fact belong to the entity it is associated with.

You are to model two objects: (i) a key server; and (ii) objects making key requests and performing crypographic operations. As noted, key servers store keys for retrieval by nodes. They accept requests for keys and return keys when the name exists and error messages when it does not. Similarly, they accept requests to add and delete name/key/validation pairs returning appropriate error messages.

Three operations must modeled for a key server: (i) storage; (ii) retrieval; and (iii) signing. Storage is the act of storing an agent ID and associated public key. Retrieval is the opposite, returning a key associated with an ID. When the key is returned, it must be signed by an private key held by the key escrow system. The associated public key is known to all agents requesting data from the key escrow server. This allows the key to be checked by any agent retrieving the key. If the key has a good signature, it came from a good server. If it does not, it cannot be trusted.

Three operations must be modeled for an agent using keys: (i) key request and validation; (ii) encryption and signing; and (iii) decryption and signature checking. Key request and validation is requesting a key from the server and checking its signature. Encryption and signing is encryption with a recipient’s public key and signing with the sender’s private key. Decryption and signature checking is the dual of encryption and signing.

Your modeling task is to develop Coq models for: (i) key servers; (ii) an object that encrypts, signs and sends information; and (iii) an object that receives, authenticates, and decrypts information. Your verification task is to assure the correctness of the key escrow system. This involves making certain that any received information that is processed has not been modified and comes from the correct source. This includes at least the following:

  1. Any message leaving a sending node is encrypted and signed
  2. Any message processed by a receiving node is signed and encrypted
  3. All retrieved keys are validated before use
  4. A message is never processed if its signature cannot be authenticated using a validated key
  5. A message is never processed if it cannot be decrypted

You may or may not need to validate other properties in the system.

You may assume that there is a single key server, but that it is possible for that key server to produces bad signatures and bad keys.

Here is a Crypto theory that you should use to start your project. You will find functions for encrypting/decrypting and signing/checking messages. I’ve proved theorems and derived code for the various functions the way I would if I were doing this for a research project. Most of the techniques will be familiar, but some - using refine in particular - will require a bit of research to understand. You do not need to understand the proofs in this file to use the functions.