论文标题:密码协议的逻辑分析与设计
Logic Analysis and Design of Cryptographic Protocols
论文作者 郑东
论文导师 王育民,论文学位 博士,论文专业 密码学
论文单位 西安电子科技大学,点击次数 534,论文页数 81页File Size2491k
1999-06-01论文网 http://www.lw23.com/lunwen_73063687/ 认证协议;BAN－逻辑;并行攻击;分布式系统;电子商务;公平交换; 电子彩票;微电子彩票
Authentication protocol, BAN-logic, Parallel attack, Distributed systems, Electronic commence, Fair exchange, Lottery, Micro-Lottery.
在安全的分布式系统中，用户需要向通信的对方证实自己的身份，同时也需要建立秘密的会话秘钥，认证协议是使用户达到认证及交换会话秘钥的密码方案。但是认证协议的设计是容易出现错误而又难以发现的。因此，研究如何发现认证协议的漏洞及如何设计安全的认证协议是密码学中非常重要的研究领域。到目前为止，已有许多方法用于验证认证协议的安全性，其中，最著名的形式方法是由Burows, Abadi, Needham提出的BAN-逻辑。但这种逻辑具有许多局限性，其主要原因是没有精确的语义定义和形式的协议理想化方法。本文主要从下列几个方面研究BAN逻辑方法及若干协议的设计：●研究了BAN-逻辑中存在的问题，完善了逻辑分析过程中协议的理想化方法。●对消息重放攻击给出了详细的分类，并提出了防止重放攻击的方法：协议运行时，主体通过对敏感信息的判断，能够判断在协议的并行运行中，是否存在并行攻击。●指出了TMN-协议中存在的漏洞与两种可能的攻击，并对TMN-协议作了进一步的改进。●提出了BAN-逻辑新的语义定义及新的逻辑推理规则，这种语义定义及逻辑推理保留了BAN-逻辑中的大部分思想。区别是推理规则是基于逻辑真值的推理规则，使得“相信”公式具有“正确相信”与“错误相信”的区别。●详细讨论了多方/多项交换的公平性要求及公平交换框架；并设计了多项公平交换的协议，该协议是在“半-信任的”的第三方参与的假设下实施。●讨论了电子彩票及微电子彩票的性质与要求；提出了两种有效的电子彩票发行方案及微电子彩票的实施方案。
In secure distributed systems it is essential that principals could prove their identities to each other and establish a session key. Authentication protocols are used to ensure authentication and related purposes, but the design of authentication protocols is error pone. It is a valuable filed on how to find out the flaws of a cryptographic protocols and how to design the correct protocol in various environments There are various methods that bave been proposed and applied to the analysis of cryptographic protocols. Among those methods , the best known and most influential one is that developed by Burows , Abadi, Needhani, commonly known as BAN-logic. This is due to its simplicity and efficiency. The main research work and results on the designing and analyzing of cryptographic protocol are as follows: ?The weakness of the BAN-logic is presented, the method of protocol idealization is made perfect. ?The attacks of message replay are classified, The parallel attack is discussed from the semantics, and the method of decision is presented. ?Two attacks on the TMN-protocol is sho~red, and an improved TMN-protocol is given. ?Some errors m BAN-Logic is pointed out, a modified version of the BAN-logic, which has a sound semantics and correct logic rules , is also presented, that is some new BAN-logic semantics and rules are presented, its language has , apart from the constructs taken from BAN, a few additional constructs. ?A classification of types of barter schemes is developed, and new cryptographic protocols for multi-item exchange with fairness are presented, These protocols assume the presence of a 搒emi-trusted neutral party? ?The properties of lottery and micro-lottery is discussed, two protocols of lottery and micro-lottery are presented, in which the result of the lottery is determined by the ticket number purchased. These protocols are the applications of a cryptographic component-bit commitment.
|
