Verification of a Signature Architecture with HOL-Z
Verification of a Signature Architecture with HOL-Z
复制标题
使用 HOL-Z 验证签名架构
DOI：
10.1007/11526841_19
复制
发表时间：
2005
期刊：
影响因子：
--
通讯作者：
B. Wolff
中科院分区：
文献类型：
--
作者：
D. Basin;Hironobu Kuruma;K. Takaragi;B. Wolff
我们报告的案例研究中使用HOL-Z，Z嵌入在高阶逻辑，指定和验证管理数字签名的安全体系结构。我们已经使用HOL-Z来形式化和联合收割机面向数据和面向过程的架构视图。然后，我们在Z中形式化了时态需求，并在高阶逻辑中进行了验证。
相同的体系结构之前已经使用SPIN模型检查器进行了验证。在此基础上，我们提供了一个详细的比较这两种不同的方法来形式化（无限状态与丰富的数据类型与有限状态）和验证（定理证明与模型检查）。与通常的看法相反，我们的案例研究表明，Z非常适合于对具有丰富数据的过程模型进行时态推理。此外，我们的比较突出了这种方法的优点，并提供证据表明，在有经验的用户手中，定理证明既不比模型检查更耗时，也不更复杂。
We report on a case study in using HOL-Z, an embedding of Z in higher-order logic, to specify and verify a security architecture for administering digital signatures. We have used HOL-Z to formalize and combine both data-oriented and process-oriented architectural views. Afterwards, we formalized temporal requirements in Z and carried out verification in higher-order logic.
The same architecture has been previously verified using the SPIN model checker. Based on this, we provide a detailed comparison of these two different approaches to formalization (infinite state with rich data types versus finite state) and verification (theorem proving versus model checking). Contrary to common belief, our case study suggests that Z is well suited for temporal reasoning about process models with rich data. Moreover, our comparison highlights the advantages of this approach and provides evidence that, in the hands of experienced users, theorem proving is neither substantially more time-consuming nor more complex than model checking.