Key Encapsulation Mechanisms

This file defines a type to represent protocols for key encapsulation mechanisms. We also define basic correctness and security properties for these protocols.