Automatic verification of temporal-epistemic properties of cryptographic protocols
Automatic verification of temporal-epistemic properties of cryptographic protocols
复制标题
DOI：
10.3166/jancl.19.463-487
复制
发表时间：
2009-01
影响因子：
--
通讯作者：
Ioana Boureanu;Mika Cohen;A. Lomuscio
中科院分区：
文献类型：
--
作者：
Ioana Boureanu;Mika Cohen;A. Lomuscio
我们提出了一种自动验证主流规范语言 CAPSL 中指定的密码协议的技术。我们定义了从 CAPSL 模型到解释系统的翻译，这是时间认知逻辑的流行语义，并将 CAPSL 目标重写为时间认知规范。我们提出了一个实现这种翻译的编译器。编译器链接到符号模型检查器 MCMAS。我们根据自定义保密和身份验证要求评估 Clark-Jacobs 库和 SPORE 存储库中的协议技术。
We present a technique for automatically verifying cryptographic protocols specified in the mainstream specification language CAPSL. We define a translation from CAPSL models into interpreted systems, a popular semantics for temporal-epistemic logic, and rewrite CAPSL goals as temporal-epistemic specifications. We present a compiler that implements this translation. The compiler links to the symbolic model checker MCMAS. We evaluate the technique on protocols in the Clark-Jacobs library and in the SPORE repository against custom secrecy and authentication requirements.