In this talk, I will describe how Amazon Web Services verifies the cryptographic protocols that are used to secure its cloud platform. This verification is accomplished through the mechanization of cryptographic security proofs in the computational model. In some cases, we mechanize proofs in existing tools, such as EasyCrypt. In order to reason about complex protocols, we developed Quivela, which is capable of proving asymptotic indistinguishability between real and ideal functionalities in a universally composable setting. Verified protocols include the domain management protocol used by the AWS Key Management Service, and the compromise-resilient signature protocol that authenticates all AWS requests.

Protocol verification is a useful component of design/architecture verification at AWS, and it allows us to identify issues in existing designs, and explore alternatives in new designs. By producing verified protocol models, we also get closer to the eventual goal of a fully verified design and implementation, in which the model serves as a functional specification for the implementation.