密码学性质分析的FocusST解
FocusST Solution for Analysis of Cryptographic Properties
摘要：
为了系统地分析分布式系统的密码学性质，需要一种形式化的理论。在本文中，我们提出了一个理论，允许（1）正式指定分布式系统，（2）验证其密码wrt。组合属性，以及（3）自动证明指定系统组件的语法接口的正确性。为了证明这种方法的可行性，我们使用了一个典型的例子，从域的基于密码的系统：一个变种的互联网安全协议TLS。使用半自动定理证明器Isabelle/HOL发现了TLS规范初始版本中的安全漏洞。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
