一种新的双方不可否认密码协议及其形式化分析

不可否认服务是电子商务中重要数据和敏感信息通过网络传输的安全基础.不可否认协议正是专门为了提供不可否认服务而设计的网络协议.现有的密码协议很少有满足严格意义上的不可否认性的.我们对现有的一种双方不可否认密码协议进行了分析和改进.新的双方不可否认密码协议既克服了原协议的不足,能抵制中间人攻击.冒充攻击,重放攻击,又满足公平性,不可否认性等安全性要求;既避免了可信第三方的性能瓶颈问题,保证了传输信息的机密性和完整性,又达到了严格意义上的不可否认性.采用SVO逻辑进一步分析和证明了新协议的双方不可否认性质.     

应用逻辑推导图方法对一个不可否认协议的分析

以之前所提出基于模态逻辑的协议推导分析方法为基础, 用Java专家系统外壳(JESS)实现了协议推导分析工具, 对一个具体的不可否认协议进行分析,以验证逻辑推导图方法的作用.分析结果清晰地显示各协议内容对协议目标实现的作用, 并以此为基础说明协议内容中的冗余.通过与传统协议分析方法进行比较, 说明了这一方法可以更清晰地说明协议内容对协议目标的贡献作用.同时,也在分析过程中指出了SVO逻辑协议分析方法对假设的过度依赖性这一缺陷.     

网络安全中的两种认证协议及安全性分析

研究对称密钥算法产生的安全问题. 根据网络安全的特点设计了两种简单认证协议: 点到点简单认证协议和可信第三方的简单认证协议. 通过使用形式化分析方法（基于知识与信念推理的模态逻辑方法〖CD2〗SVO逻辑）, 对以上两个认证协议进行了安全性分析, 证实其达到了面向密钥的目标、 密钥确认目标和相互信任密钥目标.     

基于PCL的改进型Helsinki协议的形式化分析

针对改进型的Helsinki协议安全性问题,利用协议组合逻辑PCL对协议进行形式化分析.首先使用基于"Cords演算"的程序描述语言对协议本身进行形式化描述,然后通过协议逻辑描述协议的安全属性,最后给出性质和定理,并通过逻辑推理证明改进型Helsinki协议满足其安全要求,该协议是安全的.     

非否认协议公平性分析的扩展串空间方法

针对在非否认协议公平性的形式化分析中,如何弱化初始假定和避免状态空间爆炸等问题,提出了扩展串空间方法.通过将签名运算引入串空间理论,从而对串空间理论的项集合进行重新定义,进一步通过对子项关系、攻击者迹和自由加密假定的扩展,并结合丛概念,构成了扩展串空间.分析非否认协议的公平性,首先将协议行为归纳为攻击者串、发送者串、接收者串和可信第3方串,以此构造协议的扩展串空间模型,然后结合协议迹和定理证明验证丛中存在发送者串等价于丛中存在接收者串,从而证明非否认协议公平性.通过扩展串空间方法对Zhou-Gollmann协议公平性的分析,得到了与Kailar逻辑和Lanotte自动验证方法相同的结果.与Kailar逻辑相比,扩展串空间方法仅使用自由加密假定,弱化了初始假定;与Lanotte自动验证方法相比,扩展串空间方法无需使用状态空间搜索,避免了状态空间爆炸问题.     

一种安全DSR协议的形式化分析方法

目前安全 DSR协议由于缺乏有效的形式化分析方法,难以发现一些隐蔽的安全漏洞.针对这一问题,通过分析DSR协议路由过程,给出了安全DSR协议的安全目标.提出了一种基于逻辑的安全DSR协议形式化分析方法,定义了能够反映安全DSR协议特性的基本逻辑构件(包括主体、目标和公式)和推理规则.首先用逻辑公式描述协议初始假设及过程,然后用推理规则进行推导产生推导结果,最后依据推导结果判断协议安全性.使用这种方法对SADSR协议进行了形式化分析与改进,发现了SADSR协议存在的安全漏洞.分析结果表明,提出的方法能够用于安全DSR协议形式化分析,能够发现一些较为隐蔽的安全缺陷.     

一体化网络体系架构中一种新型接入机制

要对网络体系做出重大调整,在新的协议设计之初将网络安全问题考虑在内越来越成为安全研究领域的共识.本文在国家"973"项目"一体化网络体系"的基础上,提出以具备自验证功能的地址结构实现端节点标识符,并在此基础上设计了一种新型接入机制,给出了相应的协议流程和协议格式,有效保障了"一体化网络体系"中信息源的真实性.最后使用SVO形式化逻辑对其安全性进行了详细的证明.     

Kailar逻辑推理中初始状态假设

Kailar逻辑用于分析电子商务协议的可追究性,但初始状态假设引入不当会导致Kailar逻辑分析协议失败.通过对利用Kailar逻辑证明CMP1(b)协议与CMP1协议可追究性的过程以及对初始状态假设进行分析研究,针对初始状态假设所存在的问题,给出了初始状态假设应遵循的两个原则.实例表明,遵循该原则能够发现初始状态假设存在的问题,从而修正不适当的假设、补充新的假设,避免其引入不当所导致的Kailar逻辑分析协议失败问题.     

分离机制下一种互联网安全接入方法

重点研究身份与位置分离机制下源地址真实性保障方面的方法,提出了身份与位置分离网络中唯一且不变的终端身份标识EID结构,并设计了一种保障源地址真实性的安全接入方法,并且给出了相应的协议流程和协议格式,保证了身份与位置分离网络中源地址即终端身份标识EID的真实性.最后使用SVO形式化逻辑对其安全性进行了证明.     

密钥交换协议JFK的分析与研究

快速密钥交换（JFK）协议是一种新的密钥交换协议，它的安全性引起了人们的重视。文中通过使用BAN类逻辑方法针对其安全目标进行了分析与研究。首先简介了JFK协议的两种形式和报文交互的工作原理，在此基础上指出了它所达到的安全目标，然后介绍了BAN类逻辑方法的符号语义说明和逻辑规则，并通过使用它对JFK协议中一种具体形式JFKr的安全性进行了分析证明。得出了JFK协议满足密钥交换协议的基本安全需求的结论。     

Fair non-repudiation for web services transactions

To safeguard the interests of transacting parties, non-repudiation mechanisms need to assure fairness and timeliness. The non-repudiation service currently implemented usually does not consider the requirement of fairness and the fair non-repudiation protocols to date can not be suitably applied in real environment due to its complex interaction. This paper discusses the transaction-oriented non-repudiation requirement for Web services transaction, analyzes the constraints of the traditional model for the available fair non-repudiation protocols and designs a new Online-TTP fair non-repudiation protocol. The new protocol provides a fair non-repudiation solution to secure Web services transactions and can be embedded into a single Web service call. The protocol adopts evidence chained to decreasing the overhead of evidence verification and management and alleviates the overhead of certificate revocation checking and time-stamp generation for signatures. The protocol has strong fairness, timeliness, efficiency and practicability.     

A protocol for fair electronic purchase based on concurrent signatures

E-commerce protocols for the electronic purchase of goods are difficult to design and implement due to their complexity and high security demands. Fairness of such protocols in literature highly depends on an additional TTP（trusted third party）. However, it is difficult to find such a TTP in some situations. In addition, fairness for customers has been neither fully considered nor well satisfied in existing electronic purchasing protocols. In this paper, a new protocol FEP （fair electronic purchase） without a special TTP but an online bank is presented based on a concurrent digital signature scheme. The FEP protocol guarantees fair electronic purchase of goods via electronic payment between consumers, merchants and their online banks. The protocol is practical and the analysis based on the game logics shows that it achieves the properties of viability, fairness, and timeliness.     

An Improved Non-Repudiation Protocol and Its Security Analysis

This paper proposes an improved non-repudia-tion protocol after pointing out two attacks on an existing non-repudiation protocol. To analyze the improved protocol,it also proposes an extension of Kailar logic. Using the extended Kailar logic, the security analysis of the improved protocol has been presented.     

BAN逻辑与串空间的比较

研究了2种安全协议的分析方法,即BAN逻辑和串空间.利用这2种方法分别分析了Needham-Schroeder公钥协议,指出了这2种方法各自的优点和缺点.在对这2种方法进行了比较后,指出了这2种方法有2种结合方式.1种是利用串空间给出BAN逻辑的语义,另外1种结合方式是串行,即对于需要分析的协议,先利用BAN逻辑进行分析,然后再利用串空间进行分析,使分析出的结果更加可靠.     

一种安全协议的形式化验证方法

BAN(Burrows,Abadi and Needham)类逻辑可以辅助设计、分析和验证网络和分布式系统中的安全协议。介绍BAN逻辑的产生、成分和分析步骤，指出BAN逻辑的缺陷，由此而产生的改进BAN逻辑和现状，并对BAN类逻辑作全面的回顾与展望，得出：BAN类逻辑仍然是密码协议分析和设计的主要工具，但理想化步骤是BAN类逻辑的致命缺陷的结论。展望了BAN类逻辑研究。对未来协议的形式化分析工作具有指导意义。     

新的公平的反拒认协议

反拒认是实现电子商务的重要前提之一。公平性、安全性是电子交易中的追求目标。本文在电子证据的基础上提出了两个新的公平的反拒认协议。效率高、实用性强是其特点，它高效解决了收发双方拒认问题。     

BAN类逻辑的由来与发展

BAN(Burrows,Abadi and Needham)类逻辑可以辅助设计、分析和验证网络和分布式系统中的密码协议。该文介绍了 BAN逻辑的产生、成分和分析步骤 ,进而全面指出了 BAN逻辑的缺陷 ,由此而产生的改进的 BAN逻辑和现状 ,从而对 BAN类逻辑作了全面的回顾与展望 ,并得出结论 :BAN类逻辑仍然是密码协议分析和设计的主要工具 ,但理想化步骤是 BAN类逻辑的致命缺陷。指出了 BAN类逻辑研究工作的展望。这些结论对未来协议的形式化分析工作具有指导意义     

基于椭圆曲线的公平交换协议

基于椭圆曲线密码体制,提出了一个数字签名方案,并据此建立了一个适用于电子商务的公平交换协议,该协议通过在交易双方之间建立一个安全承诺作为凭证交换数字签名,以达到摆脱可信第三方参与的目的。此公平交换协议具有一般椭圆曲线密码体制密钥较短、安全性能良好的特点,能够摆脱第三方参与,提高运行效率,并同时保证交换双方的模糊性。分析证明,该协议具有可验证性、不可否认性、不可滥用性以及公平性等特点。     

Atomic Electronic Contract Protocol Based on Convertible Signature

A new class of atomicity, namely contract atomicity is presented. A new technical strategy based on convertible signature and two-phase commitment is proposed for implementing atomicity of electronic contract protocol. A new atomic contract signing protocol is given out by using EIGamal like convertible undeniable signature and commitment ofconversion key, and another new atomic contract signing protocol is brought forward by using RSA based convertible undeniable signature scheme and commitment of conversion key. These two new protocols are proved to be of atomicity, fairness, privacy, non repudiation.     

基于ATL的KM非否认协议形式化分析

研究ATL逻辑及其在电子商务协议形式化分析中的应用,用ATL逻辑语言对KM协议进行描述与分析,并对协议的各参与方和可信第三方TTP的基本行为进行建模.