个非否认协议ZG的形式化分析.PDF

维普资讯 第 1期 电 子 学 报 V0J．33 No．1 2005年 1月 A(A EUeCIR0N10 SIM 0 Jan． 20晒 一 个非否认协议 ZG的形式化分析 范 红 ，冯登 国 (中科院研究生院信息安全国家重点实验室，北京 100039) 摘 要： 非否认性是电子商务协议的一个重要性质，其形式化分析问题引起了人们的密切关注．本文运用SVO 逻辑对一个非否认协议实例进行了有效的形式化分析，并对协议的缺陷进行了改进． 关键词： 非否认协议；形式化分析；SVO逻辑 中图分类号： TN91 文献标识码： A 文章编号： 0372—2112(2005)01—0171-03 FOrmaIAnalysisofaNon—RepudiationProtocolZG FAN Hong，FENG Deng—guo (StateKeyLaboratoryof 钿 Security ChineseAcademyof／ence，Rej／,／~100039，Odna) AI ： Non-repudiationisakeypropertyofelectroniccommerceprotocols，anditsformalanalysishasdrawpeople’Satten— tion．Thispaperanalyzesanon-repudiationprotocolusingformalmethods，andm0d essomeflawsoftheprotoco1． Keywords-, non-repudiationprotocol；formalanalysis；SVOlogic 而且在协议运行结束时应能够提供有效的证据用以证明主体 1 引言 声称的某一行为的出现或不出现是一个不可反驳的事实．即 近几年，随着电子商务协议的出现，一些新的安全性质及 保证交易的公平性和证据的有效性．前者避免了产生否认的 其形式化分析引起人们的密切关注，如协议的非否认性(non- 客观条件，后者保证一旦出现否认则可通过仲裁依据证据进 repudiation)_1J．在认证和密钥分配协议中，主体双方的目标是 行裁定加以解决．非否认协议的实现包括证据的生成，证据的 一 致的，如共享一个 良好的会话密钥等．而与之不同的是在有 交换，证据的验证 以及纠纷的解决，方法一般有两种：一是双 些协议中，主体的目标各不相同，因而主体可根据其各 自的目 方进行同时(或接近同时)的秘密交换_55_；另一种是借助一个 的与利益需求对其已发生行为进行否认 ．当出现此类情况时 可信第三方(丌P)．第一种方法实现起来较为麻烦，它要求协 需要非否认技术来解决问题，非否认协议则是非否认技术的 议双方具有同等的计算能力，这是不现实的．因此，往往采用 一 种具体实现，它通过协议设计使得协议主体无法否认其行 第二种方法．非否认协议提供的两个基本证据为：NRO(non- 为，即达成协议的非否认性．一个协议能否实现非否认性即非 repudiationoforigin)，NRR(non-repudiationofreceipt)．如果协议 否认协议的分析可借助于形式化工具来分析．形式化分析技 中有可信第三方 兀P的介入，则还需要下面两个证据：NRS 术从出现到