论文标题:公钥密码协议的形式化分析与设计研究
Research on Formal Analysis and Design of Public Key Protocols
论文作者 王滨
论文导师 张少武,论文学位 硕士,论文专业 密码学
论文单位 解放军信息工程大学,点击次数 305,论文页数 67页File Size2416k
2004-03-01论文网 http://www.lw23.com/lunwen_202617257/ 公钥密码协议;形式化方法;BAN类逻辑;强身份认证;前向保密性;原型;拒绝服务攻击
Public Key Protocols; Formal Methods; BAN-like Logic; Strong Authentication Protocol; Forward Secrecy; Prototypes; DoS Attack
目前，密码系统中大量地使用基于公钥的密码协议，这些协议的安全性直接影响着网络系统的安全。一个安全的网络系统要求主体能够实现相互间的身份认证和建立并交换会话密钥，但是密码协议的设计是非常容易出现错误的，而且这些错误是很难被发现的。研究如何检测密码协议中存在的安全漏洞并加以改进，是密码学的一个重要研究领域。迄今为止，已经有很多方法用来检测密码协议中的安全漏洞，其中最著名的是由Burows，Abadi，Needham提出的BAN—逻辑形式化分析方法，以及以BAN—逻辑为基础的一系列BAN类逻辑分析方法，但是这些方法都具有其局限性，而且大都应用于对称密码体制设计的密码协议。 本文对基于公钥密码体制的密码协议的设计与分析方法进行了研究，取得了如下结果： 1．提出了基于实体认证和密钥认证模型的协议分析方法，该方法以确定协议的模型和目标为基础，实现对协议的安全性分析； 2．对基于公钥的密码协议进行原型抽象和分类，给出了基于协议原型的协议设计方法； 3．提取了Diffie-Hellman密钥交换协议抽象原型，分析了该协议原型的的前向保密性特点，继而利用单向函数和公钥密码体制，设计了一个具有前向保密的新的密码协议原型； 4．给出了一个抵抗拒绝服务攻击(DoS)的协议设计策略，设计了一个基于口令认证的强身份认证协议，并利用我们提出的协议分析方法，分析了该协议的安全性。
Today we have seen more and more public key protocols use in networked and distributed systems, so we must select an secure public key protocol otherwise it will jeopardy the secrecy of networks. In secure networked 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 and how to design the correct protocol in various environments,there are various methods that have been proposed and applied to the analysis of cryptographic protocol. Among those methods,the best known and most influential one is that developed by Burows, Abadi, Needham, commonly known as BAN -logic and BAN-like Logic. This is due to its simplicity and efficiency. But this method is useless when it analysis public key protocols.This paper studies pulic key protocols from the point of view of designing and analyzing. My main works are listed as follow:1. This paper devised a new model of entity authentication and key authentication to analyse the security of the public key cryptographic protocols with regard to their model and protocol goal structures;2. A new model of classification method that based on the prototypes of the public-key authentication protocols,the prototypes abstracted from the protocols.Then give out a design method which based on the classification method for public key protocols;3. This paper through analysed the prototype of Diffle-Hellman key agreement protocol and then gain a new prototype which can provided forward secrecy and can apply to any asymmetric cryptosystem. The new prototype use of the one-way founction and asymmetric cryptosystem;4. Given A countermeasure against Denial-of-Service Attacks in cryptographic authentication protocols,and then this paper designed a strong identity authentication protocols,and we used the analyse method proved previously draw the conclusion that it is a secure protocol.
|
