Distributed Key-Manager Verification

This package contains the F# and F7 source files to aid in the verification of a distributed key-management system. This new component implements a data-protection API for groups of clients. To enable long-term data protection, it supports cryptographic agility so cryptography algorithms and policies can evolve for protecting fresh data while preserving access to old data. To verify the security of our design and production code, written in C#, we write a reference implementation in F#. Formally, we verify our F# code against a logical cryptographic model using F7, a refinement type checker coupled with a model checker. Experimentally, we test that the corresponding C# and F# code fragments are interchangeable.