优化的匿名电子现金支付协议及其形式化验证  

Optimization of anonymous e-cash payment protocol and its formal verification

作　　者：陈莉[1] 刘军[1] 

机构地区：[1]河南财经学院计算中心,郑州450002

出　　处：《计算机应用研究》2010年第8期3053-3057,共5页Application Research of Computers

基　　金：国家"863"计划资助项目(2007AA01Z471);国家自然科学基金资助项目(60473021);河南省重点科技攻关项目(072102210029);河南省科技攻关项目(0624260017);河南省教育厅自然科学研究计划项目(2010A520004)

摘　　要：针对匿名电子现金支付协议存在的缺陷,提出了一种能够满足多种安全属性的优化协议。将会话密钥的协商与使用分为两个阶段进行,确保协议密钥保密性的实现;引入电子证书证明交易主体的身份,确保协议非否认性的实现;借助可信方传递付款收据,避免交易主体不诚实所导致的公平性缺失;引入FTP传输方式传送电子货币和付款收据,确保实现可追究性与公平性,进一步增强协议的鲁棒性。对优化协议进行形式化验证,结果表明,优化协议满足密钥保密性、非否认性、公平性、可追究性、原子性等安全属性。In response on the existing problems of anonymous e-cash payment protocol,the paper proposed an optimal protocol,which could meet a variety of security properties. To ensure the realization of its key confidentiality,the agreement and use of the session key were divided into two stages. To realize its non-repudiation,the certificates were used to prove the identities of the transaction entities. To avoid unfairness arisen by the dishonest transaction entities,the transmission of payment receipt was achieved by the trusted party. The proposed protocol used FTP to transmit electronic cashes and payment receipts, which ensured achievement of accountability and fairness,and enhanced the robustness of the protocol. Formal verification results indicate that the optimal protocol satisfies key confidentiality,non-repudiation,accountability,fairness and atomicity.

关 键 词：安全属性 形式化验证 密钥保密性 非否认性 公平性 原子性 

分 类 号：TP393[自动化与计算机技术—计算机应用技术]