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

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

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

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

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