量子密碼協(xié)議的概率形式化研究.pdf

1、量子密碼學(xué)是利用量子力學(xué)的性質(zhì)來實現(xiàn)加密的科學(xué)，是經(jīng)典密碼學(xué)與量子力學(xué)相結(jié)合的產(chǎn)物，是一個對科學(xué)研究具有重要意義的交叉學(xué)科。由于量子密碼具備量子力學(xué)的基本屬性：海森堡不確定性和不可克隆原理，對整個量子密碼系統(tǒng)中的任何部分進(jìn)行測量都不可避免的會給整個系統(tǒng)帶來擾動，而這些擾動又必然會被檢測到，從而這就從根本上保證了量子密碼的無條件安全性（Unconditional Security）。在歷經(jīng)了三十多年的快速發(fā)展后，量子密碼協(xié)議的研究取得了長

2、足的進(jìn)展，成為密碼學(xué)中的一個重要分支，也是最重要的研究熱點之一。
　　雖然量子力學(xué)保證了量子密碼協(xié)議的無條件安全性，但是量子密碼協(xié)議安全性的證明一直是目前研究的重點和難點之一。目前對于量子密碼協(xié)議安全性的證明主要是基于傳統(tǒng)的數(shù)學(xué)理論方法，這要求很高的數(shù)學(xué)功底與個人能力。而形式化驗證的方法具有自動化的特點，能夠極大的降低驗證過程的難度，簡化了驗證過程的繁雜程度。
　　量子密碼協(xié)議中最關(guān)鍵的問題就是其安全性。這些協(xié)議的安全性是可

3、以被證明的，但是在方法上存在很大的困難。形式化驗證是指根據(jù)某個或某些形式規(guī)范或?qū)傩?，對其的正確性或非正確性，給出嚴(yán)格的采用數(shù)學(xué)方法的證明。模型檢測是形式化驗證的一種，它能夠全自動地檢驗一個有限狀態(tài)系統(tǒng)是否滿足其設(shè)計規(guī)范。模型檢測使用的是基于狀態(tài)空間搜索的方法，其優(yōu)點在于它有全自動化的檢測過程且驗證速度快、效率高。
　　本論文以國家自然科學(xué)基金項目為依托，主要研究了多種量子密碼協(xié)議的安全性問題，包括了量子密鑰分發(fā)協(xié)議、量子隱私比較協(xié)

4、議、半量子密鑰分發(fā)協(xié)議等，并使用基于概率的模型檢測這一形式化驗證方法，對各種量子密碼協(xié)議的安全性進(jìn)行了分析，建立了量子密碼協(xié)議的攻擊方式模型庫，取得了若干研究成果，主要體現(xiàn)在以下幾個方面：
　　在對量子密碼學(xué)進(jìn)行了簡要介紹的基礎(chǔ)上，描述了著名的量子密鑰分發(fā)協(xié)議BB84和B92協(xié)議，并使用基于概率的模型對協(xié)議的執(zhí)行過程進(jìn)行了抽象，通過建立系統(tǒng)模型對其安全性進(jìn)行了研究。
　　在量子隱私比較協(xié)議方面，介紹了量子隱私比較協(xié)議的發(fā)展過

5、程，使用了新近提出的一種多體糾纏態(tài)的量子隱私比較協(xié)議，創(chuàng)新性的采用了模型檢測的方法對其安全性進(jìn)行了分析，得到的結(jié)果表明量子隱私比較協(xié)議在抵抗截獲重傳攻擊上是安全的。
　　在半量子密碼協(xié)議方面，引入了最近十年新出現(xiàn)的半量子密鑰分發(fā)協(xié)議，我們使用基于概率的形式化驗證方法，將其協(xié)議執(zhí)行過程進(jìn)行抽象建模，驗證了其對截獲重傳攻擊、隨機替換攻擊和一般攻擊方式的安全性。
　　對于不管是經(jīng)典協(xié)議或者量子協(xié)議來說，安全性都是其最重要的屬性，在