楊 帆，楊國(guó)武，郝玉潔

?

基于模型檢測(cè)的半量子密碼協(xié)議的安全性分析

楊 帆1，楊國(guó)武1，郝玉潔2

(1. 電子科技大學(xué)大數(shù)據(jù)研究中心 成都 611731；2. 電子科技大學(xué)計(jì)算機(jī)科學(xué)與工程學(xué)院 成都 611731)

對(duì)于密碼協(xié)議而言，安全性是其最核心的關(guān)鍵問題，對(duì)于量子密碼協(xié)議來說也一樣。研究人員可以通過各種手段證明這些協(xié)議是安全的，但存在極大的困難，因?yàn)檫@對(duì)數(shù)學(xué)功底有著很高的要求。該文利用全自動(dòng)化的技術(shù)——模型檢測(cè)，采用了形式化驗(yàn)證方法，即基于概率的模型檢測(cè)工具PRISM，來對(duì)半量子密碼協(xié)議進(jìn)行建模并驗(yàn)證其安全性。該方法避免了傳統(tǒng)基于數(shù)學(xué)方法驗(yàn)證的繁雜，提高了驗(yàn)證的速度和效率。驗(yàn)證的結(jié)果也表明，當(dāng)傳輸足夠多的光子時(shí)，檢測(cè)出竊聽的概率無限趨近于1，和全量子密碼協(xié)議一樣，半量子密碼協(xié)議也是安全的。

竊聽; 模型檢測(cè); PRISM; 半量子密碼

密碼學(xué)是在第三方(敵手)的存在下，保障安全通信的技術(shù)和實(shí)踐。量子密碼學(xué)是量子力學(xué)和傳統(tǒng)密碼學(xué)結(jié)合的產(chǎn)物，依靠微觀粒子的量子屬性實(shí)現(xiàn)對(duì)信息的保護(hù)。量子密碼學(xué)研究的主要目標(biāo)是抵抗量子計(jì)算攻擊的密碼算法和協(xié)議，是密碼學(xué)的一個(gè)重要分支。

1 半量子密碼協(xié)議

現(xiàn)階段，量子密碼協(xié)議主要包括量子密鑰分發(fā)協(xié)議(quantum key distribution, QKD)[1-2]、量子秘密共享協(xié)議(quantum secret sharing, QSS)[3-5]、量子簽名協(xié)議(quantum signature, QS)[6-7]、量子安全直接通信協(xié)議(quantum secure direct communication, QSDC)等。量子密鑰分發(fā)協(xié)議允許兩個(gè)合法的用戶Alice(A)和Bob(B)生成只有他們知道的密鑰來加密和解密信息，即便是在有竊聽者Eve(E)監(jiān)聽的情況下。著名的量子密鑰分發(fā)協(xié)議有BB84、B92、SARG04等，這些協(xié)議假設(shè)A和B都能進(jìn)行量子操作，如使用不同的測(cè)量基來制備和測(cè)量光子。

半量子密鑰分發(fā)協(xié)議(semi-quantum key distribution, SQKD)最早是在2007年提出的[8]，后來又有許多新的版量子密鑰分發(fā)協(xié)議被提出[9-15]。SQKD嘗試實(shí)現(xiàn)相同的目標(biāo)——生成安全的密鑰來抵抗敵手的攻擊。與量子密鑰分發(fā)協(xié)議不同的是，半量子密鑰分發(fā)協(xié)議中的一個(gè)用戶(通常為B)是無法進(jìn)行量子操作的。

一個(gè)SQKD協(xié)議通常通過如下過程來執(zhí)行。量子用戶A隨機(jī)選擇測(cè)量基制備一個(gè)量子比特并發(fā)送到信道中。該量子比特傳輸?shù)浇?jīng)典用戶B之后，B只能進(jìn)行如下兩種操作之一：

2) B可能直接將量子比特回傳給A而不進(jìn)行任何操作，B不會(huì)得知該比特的任何狀態(tài)信息。

不管B如何選擇，量子比特回傳到A之后，A可以進(jìn)行任意操作，如用任意測(cè)量基進(jìn)行測(cè)量。

本文對(duì)文獻(xiàn)[16]提出的半量子密鑰分發(fā)協(xié)議進(jìn)行詳細(xì)描述。

本文采用的半量子密鑰分發(fā)協(xié)議是半量子的。半量子是進(jìn)行通信的雙方中，其中一個(gè)用戶(在本文中假設(shè)為B)無法進(jìn)行量子操作而只能進(jìn)行經(jīng)典操作，即B只能夠采用測(cè)量基對(duì)量子比特進(jìn)行測(cè)量和回傳，或者直接回傳。其次，該協(xié)議是一個(gè)單量子態(tài)的協(xié)議，即用戶A(A為量子用戶)在每一個(gè)循環(huán)中，必須傳輸一個(gè)量子比特狀態(tài)，且該量子比特狀態(tài)是單獨(dú)公開的。

本文協(xié)議的量子通信過程的執(zhí)行步驟如下：

2 模型檢測(cè)

形式化驗(yàn)證是證明一種實(shí)現(xiàn)是否與設(shè)計(jì)規(guī)范完全一致。在現(xiàn)代工業(yè)的硬軟件系統(tǒng)設(shè)計(jì)中，特別是在集成電路的設(shè)計(jì)中，得到了廣泛的大規(guī)模的應(yīng)用。形式化驗(yàn)證是在一個(gè)系統(tǒng)下，使用數(shù)學(xué)的形式方法證明或證偽設(shè)計(jì)算法對(duì)于某種形式規(guī)范或性質(zhì)的正確性。實(shí)踐證明，形式化驗(yàn)證在組合電路、密碼協(xié)議、以源代碼形式表示的軟件和具有內(nèi)部存儲(chǔ)器的數(shù)字電路等系統(tǒng)的正確性驗(yàn)證中是很有幫助的。

在復(fù)雜系統(tǒng)的構(gòu)建中，花費(fèi)在驗(yàn)證上的時(shí)間和精力遠(yuǎn)比設(shè)計(jì)多，所以人們一直在尋求更易實(shí)現(xiàn)并擴(kuò)大覆蓋范圍的技術(shù)。在安全協(xié)議的驗(yàn)證方面使用最多的技術(shù)就是模型檢測(cè)[17]。

模型檢測(cè)是指對(duì)一個(gè)給定的系統(tǒng)，使用抽象的方法得到一個(gè)模型，采用窮盡的方法自動(dòng)檢查該模型與所給定的規(guī)范是否相符合。這是一種能夠自動(dòng)驗(yàn)證有限狀態(tài)系統(tǒng)性能正確性的方法和手段。一類重要的模型檢測(cè)方法已開發(fā)出來，可用于檢查硬件和軟件設(shè)計(jì)的模型。這里的規(guī)范由時(shí)序邏輯公式給出。在模型檢測(cè)中，時(shí)序邏輯公式的開創(chuàng)性工作由文獻(xiàn)[18-21]完成。

使用模型檢測(cè)的方法對(duì)密碼協(xié)議進(jìn)行安全性驗(yàn)證所采用的基本思路是，建立一個(gè)相對(duì)小的能運(yùn)行相關(guān)協(xié)議的系統(tǒng)模型，以及能與協(xié)議交互的入侵者模型[22]。實(shí)現(xiàn)模型檢測(cè)的方法有很多，包括時(shí)序邏輯[23]、Büchi自動(dòng)機(jī)[24]和GSTE[25]等。

由于量子現(xiàn)象的過程是隨機(jī)的，所以使用基于概率隨機(jī)過程的模型檢測(cè)是最合適的方法。PRISM就是這樣一種概率模型檢測(cè)器，由伯明翰大學(xué)開發(fā)。PRISM能構(gòu)建并分析若干種概率模型，使用得最多的模型包括離散時(shí)間馬爾可夫鏈(DTMCs)、連續(xù)時(shí)間馬爾可夫鏈(CTMCs)、馬爾科夫決策過程(MDPs)、概率時(shí)間自動(dòng)機(jī)(PTAs)和概率自動(dòng)機(jī)(PAs)等。模型使用PRISM語言描述，是一種簡(jiǎn)單的、基于狀態(tài)的語言。

在量子密碼協(xié)議的驗(yàn)證中，模型檢測(cè)已經(jīng)表現(xiàn)出了強(qiáng)大的優(yōu)勢(shì)[26-28]。而對(duì)于半量子密碼協(xié)議來說，現(xiàn)有的方法都是通過數(shù)學(xué)證明驗(yàn)證其安全性，使用模型檢測(cè)來對(duì)其安全性進(jìn)行驗(yàn)證幾乎沒有。本文使用PRISM對(duì)文獻(xiàn)[16]中的SQKD協(xié)議進(jìn)行驗(yàn)證。

3 半量子密碼協(xié)議的安全性分析

根據(jù)第1節(jié)中的敘述，本文使用PRISM語言來重新描述協(xié)議。

3.1 協(xié)議描述

在PRISM中，將半量子密鑰分發(fā)協(xié)議的執(zhí)行過程分解為若干模塊，每個(gè)模塊代表系統(tǒng)的一個(gè)部分。在本文中，半量子密鑰分發(fā)協(xié)議中的每個(gè)部分都有一個(gè)模塊與其一一對(duì)應(yīng)。同時(shí)，單獨(dú)使用一個(gè)模塊來表示量子信道。在每個(gè)模塊中，都有若干操作和僅在該模塊中起效的局部變量。

按照協(xié)議的執(zhí)行過程，將其分為用戶A模塊(即Alice)、用戶B模塊(即Bob)、信道模塊和竊聽者模塊(即Eve)4個(gè)部分。每一個(gè)模塊又按照?qǐng)?zhí)行順序分為若干個(gè)狀態(tài)。當(dāng)執(zhí)行某一個(gè)具體的操作時(shí)，整個(gè)模塊的狀態(tài)就會(huì)發(fā)生改變。

1) 用戶A(Alice)模塊

①在Alice將光子(量子比特)發(fā)送到信道中后，狀態(tài)由初始狀態(tài)“0”變?yōu)椤?”；② Alice得到Bob回傳的光子后，狀態(tài)變?yōu)椤?”；③ Alice選擇測(cè)量基，狀態(tài)由“2”遷移到“3”；④ Alice對(duì)光子進(jìn)行測(cè)量，狀態(tài)變?yōu)椤?”；⑤ Alice進(jìn)行錯(cuò)誤率的檢測(cè)。若錯(cuò)誤率≥閾值，則檢測(cè)到Eve，狀態(tài)變位“5”；⑥判斷光子傳輸是否結(jié)束。若未完成，返回到“0”；否則，狀態(tài)變?yōu)椤?”終止。

具體的過程如圖1所示。

2) 用戶B(Bob)模塊

初始狀態(tài)也為“0”，如圖2所示。

① Bob選擇進(jìn)行何種操作，狀態(tài)變?yōu)椤?”；② Bob進(jìn)行測(cè)量，狀態(tài)變?yōu)椤?”；③ Bob得到結(jié)果，狀態(tài)變?yōu)椤?”；④ Bob將光子回傳給Alice，狀態(tài)由“3”遷移到“4”；⑤判斷傳輸是否結(jié)束。若未完成，狀態(tài)返回“0”；若完成，變?yōu)椤?”結(jié)束。

3) 信道模塊

初始狀態(tài)為“0”，執(zhí)行過程如圖3所示。

① Alice將光子傳輸?shù)叫诺乐?，模塊狀態(tài)變?yōu)椤?”；② Eve截獲到光子，信道狀態(tài)由“1”變?yōu)椤?”；③ Eve將光子重新傳到信道中，狀態(tài)變?yōu)椤?”；④ Bob從信道中接收到光子，狀態(tài)遷移到“4”；⑤ Bob將光子回傳到信道中，狀態(tài)由“4”遷移到“5”；⑥ Alice得到光子，信道狀態(tài)回到初始態(tài)“0”。

圖1 Alice模塊

圖2 Bob模塊

圖3 信道模塊

4) 竊聽者模塊(Eve)

由于存在多種攻擊方式，不同的攻擊方式中對(duì)Eve的建模過程和描述均存在不同，將在下一小節(jié)中具體討論。

3.2 攻擊描述

竊聽是借助技術(shù)設(shè)備和手段，竊取語言信息、數(shù)據(jù)、文字、圖像等在合法用戶中傳輸?shù)拿孛苄畔ⅰ，F(xiàn)存的攻擊的方法有很多，本文對(duì)截獲重傳攻擊、隨機(jī)替換攻擊和一般攻擊這3種常見的攻擊進(jìn)行分析。

3.2.1 截獲重傳攻擊(intercept-resend attack)

執(zhí)行過程：Alice將光子傳送入信道后，Eve對(duì)該光子進(jìn)行截獲，再隨機(jī)選擇一組基對(duì)該光子進(jìn)行測(cè)量并記錄結(jié)果。隨后Eve制備一個(gè)新的與測(cè)量結(jié)果相同的光子并傳入信道。

本文采用3.1節(jié)中的描述方法來描述該攻擊過程。Eve的初始狀態(tài)為“0”，如圖4所示。

1) Eve選擇測(cè)量基，狀態(tài)遷移到“1”；2) Eve對(duì)光子進(jìn)行測(cè)量并記錄結(jié)果，狀態(tài)分別由“1”變?yōu)椤?”，再變?yōu)椤?”；3) 當(dāng)Eve制備光子并傳回到信道中，整個(gè)模塊回到“0”。

圖4 截獲重傳攻擊

3.2.2 隨機(jī)替換估計(jì)(random substitute attack)

執(zhí)行過程：Alice將光子傳送入信道后，Eve對(duì)該光子進(jìn)行截獲，再隨機(jī)選擇一組基對(duì)該光子進(jìn)行測(cè)量并記錄結(jié)果。隨后Eve隨機(jī)制備一個(gè)新量子比特并傳入信道。同樣的，模塊的初始狀態(tài)為“0”，如圖5所示。

1) Eve隨機(jī)選擇測(cè)量基，狀態(tài)由“0”遷移到“1”；2) Eve對(duì)光子進(jìn)行測(cè)量，狀態(tài)由“1”變?yōu)椤?”；3) Eve得到測(cè)量結(jié)果，狀態(tài)遷移到“3”；4) Eve將隨機(jī)制備的光子傳回到信道，模塊狀態(tài)回到初始“0”。

圖5 隨機(jī)替換攻擊

3.2.3 一般攻擊(general attack)

執(zhí)行過程為：1) 當(dāng)Eve選擇測(cè)量基后，狀態(tài)由初始狀態(tài)“0”遷移到“1”；2) Eve對(duì)光子進(jìn)行測(cè)量，狀態(tài)變?yōu)椤?”；3) Eve得到測(cè)量結(jié)果，狀態(tài)變?yōu)椤?”；4) Eve進(jìn)行攻擊方式選擇，模塊狀態(tài)遷移到“4”；5) 當(dāng)Eve把光子傳回到信道后，狀態(tài)回到“0”。如圖6所示。

圖6 一般攻擊

4 驗(yàn)證結(jié)果

式中，為中協(xié)議執(zhí)行過程傳輸?shù)墓庾拥目倲?shù)。那么檢測(cè)到竊聽者Eve的概率為：

圖7 驗(yàn)證結(jié)果I(無噪聲)

從圖7的結(jié)果可知，傳輸?shù)墓庾訑?shù)較少時(shí)，檢測(cè)到Eve的概率較低，而當(dāng)傳輸?shù)墓庾訑?shù)達(dá)到50時(shí)，檢測(cè)到Eve的概率已經(jīng)很接近于1；當(dāng)繼續(xù)增加傳輸?shù)牧孔訑?shù)時(shí)，檢測(cè)概率持續(xù)上升并無限趨近于1。

在實(shí)際中，無噪聲的信道是不存在的，真實(shí)信道中的噪聲總是存在的。為了驗(yàn)證在有噪聲干擾的情況下協(xié)議的安全性，需將PRISM中對(duì)信道的描述進(jìn)行更改，就可以計(jì)算在噪聲干擾的條件下，檢測(cè)到竊聽者的概率。

假設(shè)信道在由狀態(tài)“0”遷移到狀態(tài)“1”時(shí)噪聲產(chǎn)生干擾(如圖3所示)。在無噪聲信道中，該操作可以表達(dá)為：

式中，cs表示信道的狀態(tài)；cd是信道的數(shù)據(jù)；cb表示信道的測(cè)量基；ad表示Alice的數(shù)據(jù)；ab表示Alice選擇的測(cè)量基。當(dāng)加入噪聲后，該描述變?yōu)椋?/p>

由式(3)、式(4)可以得到，信道狀態(tài)遷移到正確狀態(tài)的概率為0.7，遷移到錯(cuò)誤狀態(tài)的概率為0.3。此處的錯(cuò)誤狀態(tài)有3種，分別為：選擇了錯(cuò)誤的測(cè)量基、得到錯(cuò)誤的數(shù)據(jù)、或者兩者都有。圖8為有噪聲時(shí)的驗(yàn)證結(jié)果。

圖8 驗(yàn)證結(jié)果II(有噪聲)

從圖8可以得到，在存在噪聲干擾的條件下，且信道中傳輸?shù)墓庾訑?shù)較少時(shí)，檢測(cè)到竊聽者的概率依然較低，并且出現(xiàn)了下降(即比無噪聲時(shí)低)。當(dāng)傳輸?shù)墓庾訑?shù)增加到50個(gè)左右時(shí)，檢測(cè)概率已接近于1；當(dāng)傳輸?shù)墓庾訑?shù)持續(xù)增加時(shí)，檢測(cè)到Eve的概率也持續(xù)上升且無限趨近于1。

5 結(jié)束語

本文使用了基于概率的模型檢測(cè)器PRISM對(duì)半量子密鑰分發(fā)協(xié)議的安全性進(jìn)行驗(yàn)證。所采用的技術(shù)是通過抽象方法對(duì)協(xié)議執(zhí)行的過程和攻擊過程建立起對(duì)應(yīng)的模型?，F(xiàn)在針對(duì)量子密碼協(xié)議安全性驗(yàn)證的方法絕大多數(shù)是采用數(shù)學(xué)證明的方法，這要求協(xié)議的設(shè)計(jì)者具備很扎實(shí)的數(shù)學(xué)功底。本文采用的模型檢測(cè)方法則是一種全自動(dòng)化的工具，通過抽象的方法對(duì)協(xié)議執(zhí)行的過程和攻擊過程建立起對(duì)應(yīng)的模型，再使用相應(yīng)的模型檢測(cè)器就可以得到驗(yàn)證解結(jié)果。這就避免了使用傳統(tǒng)方法驗(yàn)證的復(fù)雜程度和對(duì)個(gè)人能力的要求，提高了整個(gè)驗(yàn)證過程的速度和效率。驗(yàn)證結(jié)果表明，無論在有無噪聲干擾的信道中，隨著傳輸光子數(shù)的增多，針對(duì)截獲重傳攻擊、隨機(jī)替換攻擊和一般攻擊這3種攻擊方式來說，檢測(cè)到竊聽者Eve的概率會(huì)無限趨近于1。在有噪聲干擾的信道中，傳輸光子數(shù)較少時(shí)，Eve的檢測(cè)概率會(huì)出現(xiàn)下降，但當(dāng)傳輸?shù)墓庾訑?shù)達(dá)到足夠多時(shí)，檢測(cè)到竊聽者的概率會(huì)逐漸增大并無限趨近于1，這證明了該半量子密鑰分發(fā)協(xié)議是安全的。對(duì)于其他不同的攻擊方法，依然能夠使用PRISM來進(jìn)行安全性的驗(yàn)證。同樣的，量子密碼協(xié)議的其他方面性質(zhì)的驗(yàn)證也可以使用PRISM來進(jìn)行。

[1] BENNETT C H, BRASSARD G. Quantum cryptography: Public key distribution and coin tossing[C]//In Proc of IEEE International Conference on Computers, Systems, and Signal Processing. Bangalore, India: IEEE, 1984: 175-179.

[2] BENNETT C H, BESSETTE F, BRASSARD G, et al. Experimental quantum cryptography[J]. Journal of Cryptology, 1992, 5(1): 3-28.

[3] HILLERY M, BUZEK V, BERTHIAUME A. Quantum secret sharing[J]. Physical Review A, 1999, 59(3): 1829-1834.

[4] SHI R H, HUANG L S, YANG W, et al. Multiparty quantum secret sharing with Bell states and Bell measurements[J]. Optics Communications, 2010, 283(11): 2476-2480.

[5] RAHAMAN R, PARKER M G. Quantum scheme for secret sharing based on local distinguishability[J]. Physical Review A, 2015, 91(2): 91. 022330.

[6] CHUANG I, GOTTESMAN D. Quantum digital signatures: US, US 7246240 B2[P]. 2007.

[7] ZENG G H, CHRISTOPH K. An arbitrated quantum signature scheme[J]. Physev A, 2002, 65: 042312.

[8] BOYER M, KENIGSBERG D, MOR T. Quantum key distribution with classical bob[C]//First International Conference on Quantum, Nano, and Micro Technologies, 2007, ICQNM'07. [S.l.]: IEEE, 2007, 99(14): 10-10.

[9] KRAWEC W. Mediated semiquantum key distribution[J]. Physical Review A, 2015, 91(3): 032323.

[10] BOYER M, GELLES R, KENIGSBERG D, et al. Semiquantum key distribution[J]. Phys Rev A, 2009, 79: 032341.

[11] YU K F, YANG C W, LIAO C H, et al. Authenticated semi-quantum key distribution protocol using Bell states[J]. Quantum Information Processing, 2014, 13(6): 1-9.

[12] KRAWEC W. Mediated semiquantum key distribution[J]. Physical Review A, 2015, 91(3): 032323.

[13] KRAWEC W. Security proof of a semi-quantum key distribution protocol to appear[C]//IEEE ISIT 2015. [S.l.]: IEEE, 2015.

[14] KRAWEC W. Semi-quantum key distribution[D]. [S.l.]: Stevens Institute of Technology, 2015.

[15] KRAWEC W. Security of a semi-quantum protocol where reflections contribute to the secret key[J]. Quantum Information Processing, 2015, 15(5): 1-24.

[16] KRAWEC W. Restricted attacks on semi-quantum key distribution protocols[J]. Quantum Information Processing, 2014, 13(11): 2417-2436.

[17] BAIER C, KATOEN J P. Principles of model checking [M]. Cambridge, USA: The MIT Press, 2008.

[18] EMERSON E A, CLARKE E M. Characterizing correctness properties of parallel programs using fixpoints[M]//Automata, Languages and Programming. Berlin, Heidelberg: Springer-Verlag, 1980: 169-181.

[19] CLARKE E M, EMERSON E A. Design and synthesis of synchronization skeletons using branching time temporal logic[J]. Proc Workshop on Logic of Programs, 1982, 131: 52-71.

[20] CLARKE E M, EMERSON E A, SISTLA A P. Automatic verification of finite-state concurrent systems using temporal logic specifications[C]//ACM Transactions on Programming Languages and Systems. New York: ACM, 1986: 244-263.

[21] QUEILLE J P, SIFAKIS J. Specification and verification of concurrent systems in CESAR[C]//In Proc 5th Colloquium on Int Symp Programming. London: Springer, 1982: 337-351.

[22] BASAGIANNIS S, KATSAROS P, POMBORTSIS A. Synthesis of attack actions using model checking for the verification of security protocols[J]. Secur Comm Networks, 2011, 4(2): 147-161.

[23] BEN-ARI M, PNUELI A, MANNA Z. The temporal logic of branching time[J]. Acta Informatica, 1983, 20(3): 207-226.

[24] GASTIN P, ODDOUX D. Fast LTL to büchi automata translation[J]. Lecture Notes in Computerence, 2001, 2102: 53-65.

[25] YANG J, SEGER C H J. Generalized symbolic trajectory evaluation - abstraction in action[M]//Formal Methods in Computer-Aided Design, LNCS. Berlin, Heidelberg: Springer-Verlag, 2002: 70-87.

[26] YANG F, YANG G W, HAO Y J, et al. Security analysis of multi-party quantum private comparison protocol by model checking[J]. Modern Physics Letters B, 2015, 29(18): 717-755.

[27] YANG F, YANG G W, HAO Y J. The modeling library of eavesdropping methods in quantum cryptography protocols by model checking[J]. International Journal of Theoretical Physics, 2016, DOI: 10.1007/s10773-016-2969-z.

[28] ELBOUKHARI M, AZIZI M. Analysis of the security of bb84 by model checking[J]. International Journal of Network Security & Its Applications, 2010, 2(2): 87-98.

[29] CHANG Y J, TSAI C W, HWANG T. Multi-user private comparison protocol using GHz class states[J]. Quantum Information Processing, 2013, 12(2): 1077-1088.

編 輯 漆 蓉

Security Analysis of Semi-Quantum Cryptography Protocols by Model Checking

YANG Fan1, YANG Guo-wu1, and HAO Yu-jie1

(1. Big Data Research Center, University of Electronic Science and Technology of China Chengdu 611731;2. School of Computer Science and Engineering, University of Electronic Science and Technology of China Chengdu 611731)

For cryptography protocols, security is its most core issue, and is the same for quantum cryptography protocols. Researchers can adopt many methods to prove that these protocols are secure, but there exists much difficulty. By using the method of formal verification and the technique of model checking, a fully automated probabilistic model checking tool - PRISM can be used to model these protocols and verify the security properties. Such a methodology can not only avoid the computational complexity of the traditional verification methods based on mathematics, but also improve efficiency and accelerate the verification process. The verification results show that the detection rate of eavesdropping is approximately close to 1 when sufficient photons are transmitted. The semi-quantum cryptography protocols is as secure as the full quantum protocols.

eavesdropping; model checking; PRISM; semi-quantum cryptography

TP301.2

A

10.3969/j.issn.1001-0548.2017.05.013

2016-03-21；

2017-03-06

國(guó)家自然科學(xué)基金(61272175, 61572019, U1230106)

楊帆(1985-)，男，博士生，主要從事形式化方法和量子密碼協(xié)議方面的研究.