Challenges in Automating Formal Methods for Cryptographic Algorithm Validation and Protocol Verification—The Use of Experimental Platform (G31c)
This talk will address the challenges of automating the application of formal methods in the validation of cryptographic algorithms and verification of cryptographic protocols using experimental validation platform. Using equivalent checking methods for validating hardware implementations of cryptographic algorithms will be discussed. Furthermore, the presentation will explore the prospects of extending the platform to incorporate third-party algorithms and methods, as well as evaluating their correctness using formal approaches. Regarding cryptographic protocols, we present the automatic protocol formal verification process developed on our platform. The platform enables clients to provide protocol specifications in an AnB-like language. Such specifications are automatically translated on the platform to the formats that allow an analysis of security properties. We provide insights on the soundness of our translation approach, discuss practical use cases of our tool, and outline potential future research directions.