FocusST Solution for Analysis of Cryptographic Properties
This work addresses the need for formal verification in cryptographic distributed systems, offering a method to detect flaws like in TLS, but it appears incremental as it builds on existing theorem-proving techniques.
The paper tackles the problem of systematically analyzing cryptographic properties in distributed systems by presenting a formal theory that enables specification, verification of composition properties, and automatic correctness demonstration of syntactic interfaces, demonstrated by revealing a security flaw in a TLS variant using Isabelle/HOL.
To analyse cryptographic properties of distributed systems in a systematic way, a formal theory is required. In this paper, we present a theory that allows (1) to specify distributed systems formally, (2) to verify their cryptographic wrt. composition properties, and (3) to demonstrate the correctness of syntactic interfaces for specified system components automatically. To demonstrate the feasibility of the approach we use a typical example from the domain of crypto-based systems: a variant of the Internet security protocol TLS. A security flaw in the initial version of TLS specification was revealed using a semi-automatic theorem prover, Isabelle/HOL.