量子密码协议的概率形式化研究

发布时间：2018-01-15 12:09

本文关键词：量子密码协议的概率形式化研究　出处：《电子科技大学》2016年博士论文　论文类型：学位论文

【摘要】：量子密码学是利用量子力学的性质来实现加密的科学,是经典密码学与量子力学相结合的产物,是一个对科学研究具有重要意义的交叉学科。由于量子密码具备量子力学的基本属性:海森堡不确定性和不可克隆原理,对整个量子密码系统中的任何部分进行测量都不可避免的会给整个系统带来扰动,而这些扰动又必然会被检测到,从而这就从根本上保证了量子密码的无条件安全性(Unconditional Security)。在历经了三十多年的快速发展后,量子密码协议的研究取得了长足的进展,成为密码学中的一个重要分支,也是最重要的研究热点之一。虽然量子力学保证了量子密码协议的无条件安全性,但是量子密码协议安全性的证明一直是目前研究的重点和难点之一。目前对于量子密码协议安全性的证明主要是基于传统的数学理论方法,这要求很高的数学功底与个人能力。而形式化验证的方法具有自动化的特点,能够极大的降低验证过程的难度,简化了验证过程的繁杂程度。量子密码协议中最关键的问题就是其安全性。这些协议的安全性是可以被证明的,但是在方法上存在很大的困难。形式化验证是指根据某个或某些形式规范或属性,对其的正确性或非正确性,给出严格的采用数学方法的证明。模型检测是形式化验证的一种,它能够全自动地检验一个有限状态系统是否满足其设计规范。模型检测使用的是基于状态空间搜索的方法,其优点在于它有全自动化的检测过程且验证速度快、效率高。本论文以国家自然科学基金项目为依托,主要研究了多种量子密码协议的安全性问题,包括了量子密钥分发协议、量子隐私比较协议、半量子密钥分发协议等,并使用基于概率的模型检测这一形式化验证方法,对各种量子密码协议的安全性进行了分析,建立了量子密码协议的攻击方式模型库,取得了若干研究成果,主要体现在以下几个方面:在对量子密码学进行了简要介绍的基础上,描述了著名的量子密钥分发协议BB84和B92协议,并使用基于概率的模型对协议的执行过程进行了抽象,通过建立系统模型对其安全性进行了研究。在量子隐私比较协议方面,介绍了量子隐私比较协议的发展过程,使用了新近提出的一种多体纠缠态的量子隐私比较协议,创新性的采用了模型检测的方法对其安全性进行了分析,得到的结果表明量子隐私比较协议在抵抗截获重传攻击上是安全的。在半量子密码协议方面,引入了最近十年新出现的半量子密钥分发协议,我们使用基于概率的形式化验证方法,将其协议执行过程进行抽象建模,验证了其对截获重传攻击、随机替换攻击和一般攻击方式的安全性。对于不管是经典协议或者量子协议来说,安全性都是其最重要的属性,在量子密码协议的研究过程中,对攻击方式的研究总是必不可少的。而由于不同的量子密码协议其构造体系存在差异,即便是相同的攻击方式,在具体的执行过程中,也存在着区别。我们通过对不同的攻击方式进行抽象建模,建立了通用的攻击方式模型库。使用者只需要对攻击模型的描述进行适当的修改调整,就能在其各自的研究中使用,大大简化了验证的难度,提高了验证的速度和效率,这本就是形式化方法自动验证想要达到的目标之一。
[Abstract]:Quantum cryptography is the nature of the use of quantum mechanics to achieve encryption science, is a product of the combination of classical cryptography and quantum mechanics, it has important significance for scientific research subject. Because of the basic properties of quantum cryptography with quantum mechanics: Heisenberg uncertainty principle and the no cloning and measurement are inevitable for any part of the quantum cryptography in the system for the entire system disturbance, and these disturbances will be detected, so it is the fundamental guarantee for the unconditional security of quantum cryptography (Unconditional Security). After thirty years of rapid development, has made considerable progress in the research of quantum cryptography protocol and become an important branch of cryptography, one of the most important research hotspot. Although quantum mechanics to ensure the unconditional security of quantum cryptographic protocols However, proof of quantum cryptography protocol security has been one of the emphases and difficulties of current research. The proof of quantum cryptography protocol security is mainly based on the traditional theory of mathematics, mathematical knowledge and personal ability which is very demanding. The formal verification method has the characteristics of automation, can greatly reduce the the difficulty of the verification process, simplify the complexity of the verification process. The key problem of quantum cryptography protocol is its security. The security of these protocols can be proved, but there are great difficulties in the method. The formal verification refers to one or some form of specification or property, the correct or incorrect, proved by mathematics method rigorously. Model checking is a formal verification, it can automatically test whether a finite state system to meet The design specification. The model is detected using a method based on state space search, it has the advantages of automatic detection and verification process of fast speed, high efficiency. In this paper, the National Natural Science Foundation project, the main problems of research on various quantum cryptographic protocols, including quantum key distribution protocol quantum, privacy comparison protocol, semi quantum key distribution protocol, and use the verification method in the form of probabilistic model checking based on, for security of quantum cryptographic protocols are analyzed, a quantum cryptographic protocol attack model base, has made some research results, mainly reflected in the following aspects: Based on quantum cryptography are introduced briefly on the description of the quantum key distribution protocol BB84 and the famous B92 protocol, and use the probability model for the implementation of the agreement based on The process of abstraction, through the establishment of the system model is studied for its safety. In the comparison protocol of quantum privacy, this paper introduces the developing process of comparing protocol quantum privacy, quantum privacy using a multiple entanglement of the newly proposed protocol is innovative, using the method of model checking is analyzed for its safety, the obtained results show that the comparison protocol of quantum privacy against intercepted retransmission attack is safe. In the semi quantum cryptography protocol, introduced the new semi quantum key distribution protocol in recent ten years, we used a formal verification method based on probability, the protocol implementation process model to verify its interception, replay attack, random replacement of security attacks and general attack. Whether it is classical or quantum protocol protocol, security is the most important attribute In the course of the study, quantum cryptography protocol, research on attack mode is always essential. But because of the different quantum cryptographic protocol and its structural system are different, even the same attack, in the specific implementation process, there are also differences. We abstract modeling of different attack methods, established general attack model library. Users only need to describe the attack model was modified to adjust, can be used in their study, greatly simplifies the difficulty of verification, improve the verification speed and efficiency, this is one of the formal methods for automatic verification of target to achieve.

【学位授予单位】：电子科技大学
【学位级别】：博士
【学位授予年份】：2016
【分类号】：O413;TN918.1

【相似文献】