Continuous Verification for Cryptographic Protocol Development

The proliferation of connected devices has motivated a surge in the development of cryptographic protocols to support a diversity of devices and use cases. To address this trend, we propose continuous verification, a methodology for secure cryptographic protocol design that consists of three principles: (1) repeated use of verification tools; (2) judicious use of common message components; and (3) inclusion of verifiable model specifications in standards. Our recommendations are derived from previous work in the formal methods community, as well as from our past experiences applying verification tools to improve standards. Through a case study of IETF protocols for the IoT, we illustrate the power of continuous verification by (i) discovering flaws in the protocols using the Cryptographic Protocol Shapes Analyzer (CPSA); (ii) identifying the corresponding fixes based on the feedback provided by CPSA; and (iii) demonstrating that verifiable models can be intuitive, concise and suitable for inclusion in standards to enable third-party verification and future modifications.