This paper presents an optimized and refined methodology to specify crypto-based distributed software and to verify their composition properties in a formal way. We suggest to specify all components in Focus, a framework for formal specification and development of interactive systems. Having a formal Focus representation of a protocol components, one can argue about their properties and composition in a methodological way, referring to the approach ``Focus on Isabelle'' and checking the defined properties formal proofs using the theorem prover Isabelle/HOL, as well as make automatic correctness proofs of syntactic interfaces for specified system components. As a running example, a variant of the Internet security protocol TLS is presented. We analyzed one of the versions of the protocol using refined Focus specification and demonstrated a security flaw in this version formally, using Isabelle/HOL. We also used the extended approach to harden the protocol in a formal way, and showed how to construct a new version of the secure channel on the basis of the corrected formal specification of the protocol. The formal proof that the discussed flaw no more exist in this corrected version of the protocol was done also in Isabelle/HOL. On the base of these protocol we specified secure channels that adopt the main protocol properties.     «

This paper presents an optimized and refined methodology to specify crypto-based distributed software and to verify their composition properties in a formal way. We suggest to specify all components in Focus, a framework for formal specification and development of interactive systems. Having a formal Focus representation of a protocol components, one can argue about their properties and composition in a methodological way, referring to the approach ``Focus on Isabelle'' and checking t...     »