The verification of an industrial payment protocol: the SET purchase phase
The verification of an industrial payment protocol: the SET purchase phase
复制标题
工业支付协议的验证：SET购买阶段
DOI：
10.1145/586110.586113
复制
发表时间：
2002
期刊：
影响因子：
--
通讯作者：
F. Massacci
中科院分区：
文献类型：
--
作者：
G. Bella;Lawrence Charles Paulson;F. Massacci
安全电子交易（SET）协议是由信用卡公司和软件公司组成的财团提出的，目的是确保电子商务交易的安全。当客户进行购买时，SET双重签名保证了真实性，同时对商家保密客户的账户详细信息，对银行保密客户选择的商品。本文报告了SET完整采购阶段的第一次验证结果。使用Isabelle和归纳法，我们证明了信用卡详细信息确实是保密的，客户、商家和银行可以确认交易的大部分细节，即使其中一些细节对他们保密。复杂的协议结构使得证明更加困难，但仍然是可行的。尽管可以证明足够多的目标使人们对SET有信心，但双签名中缺乏明确性使得一些协议属性失败：无法证明客户有意将其信用卡详细信息发送给接收它们的支付网关。
The Secure Electronic Transaction (SET) protocol has been proposed by a consortium of credit card companies and software corporations to secure e-commerce transactions. When the customer makes a purchase, the SET dual signature guarantees authenticity while keeping the customer's account details secret from the merchant and his choice of goods secret from the bank.This paper reports the first verification results for the complete purchase phase of SET. Using Isabelle and the inductive method, we showed that the credit card details do remain confidential and customer, merchant and bank can confirm most details of a transaction even when some of those details are kept from them. The complex protocol construction makes proofs more difficult but still feasible.Though enough goals can be proved to give confidence in SET, a lack of explicitness in the dual signature makes some agreement properties fail: it is impossible to prove that the customer meant to sent his credit card details to the payment gateway that receives them.