Formal Verification of Cardholder Registration in SET

Formal Verification of Cardholder Registration in SET
复制标题

SET 中持卡人注册的正式验证

DOI：
10.1007/10722599_10
复制
发表时间：
2000
期刊：
--
影响因子：
--
通讯作者：
Piero Tramontano
Piero Tramontano
中科院分区：
--
文献类型：
--
作者：
G. Bella;F. Massacci;Lawrence Charles Paulson;Piero Tramontano

文献摘要

被引文献

相似文献

SET协议的第一阶段，即持卡人登记，已被归纳建模。概述了这一阶段，并描述了其形式化模型。使用Isabelle/HOL证明了该协议的一些基本引理，并证明了一个定理，即一个证书颁发机构最多只能证明一个给定的密钥一次。在使议定书正式化时，注意到许多含糊、矛盾和遗漏之处。
The first phase of the SET protocol, namely Cardholder Registration, has been modelled inductively. This phase is presented in outline and its formal model is described. A number of basic lemmas have been proved about the protocol using Isabelle/HOL, along with a theorem stating that a certification authority will certify a given key at most once. Many ambiguities, contradictions and omissions were noted while formalizing the protocol.