FocusST Solution for Analysis of Cryptographic Properties

TL;DR

This paper introduces FocusST, a formal theory for specifying and verifying cryptographic properties of distributed systems, demonstrated through a TLS protocol example, enabling automatic correctness proofs.

Contribution

The paper presents a new formal framework, FocusST, for systematic analysis and verification of cryptographic properties in distributed systems, including automatic interface correctness demonstration.

Findings

Identified a security flaw in TLS using the proposed approach

Successfully verified cryptographic composition properties

Demonstrated semi-automatic theorem proving with Isabelle/HOL

Abstract

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.