Formal Verification of the Horn-Preneel Micropayment Protocol
Formal Verification of the Horn-Preneel Micropayment Protocol
复制标题
Horn-Preneel 小额支付协议的形式验证
DOI：
10.1007/3-540-36384-x_20
复制
发表时间：
2002
期刊：
影响因子：
--
通讯作者：
K. Futatsugi
中科院分区：
文献类型：
--
作者：
K. Ogata;K. Futatsugi
我们已经正式验证了Horn-Preneel微支付协议具有重要的安全性质。这种财产在本文中被称为非超额收费财产，即经纪人不能将超过付款人打算支付的金额计入受款人的贷方。通过将协议建模为考虑恶意主体的观察转移系统，在CafeOBJ中对模型进行描述，在CafeOBJ中编写证明脚本，并在CafeOBJ系统上执行证明脚本，从而完成了对协议的验证。文中描述了协议的建模和验证过程。
We have formally verified that the Horn-Preneel micropayment protocol possesses an important safety property. The property, called non-overcharge property in this paper, is that a payee cannot be credited amount more than what a payer intends to pay by the broker. The verification has been done by modeling the protocol as an observational transition system considering malicious principals, describing the model in CafeOBJ, writing proof scripts showing that the protocol possesses the property in CafeOBJ, and executing the proof scripts with the CafeOBJ system. We describe the modeling of the protocol and the verification in this paper.