張盛 馬詠輝

（武警海警學(xué)院 浙江省寧波市 315801）

1 引言

作為未來最有前景的技術(shù)之一，量子通信為許多傳統(tǒng)方法無法完成的任務(wù)提供了解決方案，例如量子稠密編碼[1,2]和量子隱形態(tài)傳送[3,4]，并因此廣為人知。當(dāng)前，在眾多量子通信協(xié)議中，量子秘鑰分配成為全世界的研究重點，同時也取得了巨大的成功。但是，這類協(xié)議的安全性證明[6,7]是一個重大的問題，這就妨礙了它以一種合理的費用來為日新月異的信息系統(tǒng)服務(wù)。因此，正如形式化理論應(yīng)用在經(jīng)典秘鑰協(xié)議[8,9,10,11,12,13,14,15]上一樣，它們也被引入到量子協(xié)議的模擬、分析和證明中去。

盡管量子密鑰分配協(xié)議的形式化證明引起廣泛關(guān)注，但是其他量子通信協(xié)議依然有待于用形式化分析的方法進(jìn)行研究。例如，F(xiàn)eng 等人用qCCS[11]形式化分析了量子隱形態(tài)傳送和量子超稠密編碼協(xié)議。本文計劃引入一個新的形式化理論Petri 網(wǎng)[16]去繼續(xù)這項工作，即基于Petri網(wǎng)的量子反直觀通信協(xié)議分析。

量子反直觀通信的概念起源于無相互作用測量[17,18,19]，這是一種不需要直接測量物體的現(xiàn)象。這一概念最早由Noh 在一篇QKD的協(xié)議中實現(xiàn)[20]。之后，這一理論被進(jìn)一步優(yōu)化，應(yīng)用到確定性秘鑰分配的協(xié)議[21]中。與傳統(tǒng)的QKD 協(xié)議完全不同的是，上述這類協(xié)議是違反直覺的——其中承載信息的量子態(tài)從來不通過信道。這樣，量子反直觀通信基于變相的不可克隆原理阻止了竊聽者獲取任何私人秘鑰的信息。更加有趣的是，Salih 等人進(jìn)一步豐富了量子反直觀通信領(lǐng)域。他們通過運用量子芝諾效應(yīng)[22]，提出了一個具有更高效率的協(xié)議。

本文針對幾種量子通信協(xié)議中涉及的概念和結(jié)構(gòu)，設(shè)計了相應(yīng)的Petri 網(wǎng)模型，解決了量子通信協(xié)議Petri 網(wǎng)建模相關(guān)基礎(chǔ)理論問題。

2 基于Petri網(wǎng)的量子通信形式化基礎(chǔ)

2.1 量子態(tài)的Petri網(wǎng)描述

量子態(tài)作為分析量子通信的基本單位，有著極其重要的研究價值。量子態(tài)指的是電子做穩(wěn)恒的運動，具有完全確定的能量的穩(wěn)恒的運動狀態(tài)。它是由一組量子本征態(tài)組成，這組量子本征態(tài)的向量和即為該量子態(tài)。這里，符號表示為：

圖1：加法運算(a)

圖2：加法運算(b)

圖3：乘法運算(a)

圖4：乘法運算(b)

這里，需要指出k 值的精確度很大程度上取決于計算復(fù)雜度。比如，如果Ci是一個實數(shù)，k=1，那么本征態(tài)的概率幅就等于庫所pi中的令牌數(shù)目。這樣，就建立了量子系統(tǒng)與Petri 網(wǎng)之間的聯(lián)系。下面以此為基礎(chǔ)建立Petri 網(wǎng)運算模型。

2.2 概率幅的四則運算模型

Petri 網(wǎng)作為一種狀態(tài)機(jī)，可以在實數(shù)域內(nèi)表示數(shù)據(jù)的狀態(tài)變化。在建立量子反直觀通信協(xié)議的Petri 網(wǎng)模型前，先對協(xié)議中應(yīng)用到的運算規(guī)則進(jìn)行建模。

2.2.1 加法運算

該運算法則可以通過一個有名的例子來描述：1+1=2，如圖1和圖2所示，在三個相對獨立的places 中各裝入1 個token，其中P1作為開始端，經(jīng)過transition t，token 值與arcs 相乘，結(jié)果裝入place P4，此后，transition t 不會被觸發(fā)。

規(guī)則說明：圖1 是指transition t 觸發(fā)前的標(biāo)記；圖2 是指transition t 觸發(fā)后的標(biāo)記，這里t 不會被觸發(fā)。

2.2.2 乘法運算

該運算法則可以通過一個典型的例子來描述：2×3=6，如圖3和圖4所示，在place P2中裝入2 個token，place P3中裝入3 個token，P1作為開始端，經(jīng)過transition t，token 值與arcs 相乘，結(jié)果裝入place P4，此后，transition t 不會被觸發(fā)。

規(guī)則說明：圖3 是指transition t 觸發(fā)前的標(biāo)記；圖4 是指transition t 觸發(fā)后的標(biāo)記，這里t 不會被觸發(fā)。

2.3 臨界模型

為了實現(xiàn)Petri 網(wǎng)自動化處理反直觀量子通信協(xié)議中存在的狀態(tài)變換，依據(jù)程序語言中的臨界條件判定，對于Petri 網(wǎng)進(jìn)行臨界操作的建模。

該規(guī)則可以通過模擬一個C 語言程序來描述，如圖5 和圖6所示，在place P1中裝入2 個token，place P2中裝入3 個token，P3作為開始端，經(jīng)過transition t，token 值與arcs 相乘，結(jié)果裝入place P4，此后，transition t 不會被觸發(fā)。

C 語言程序:

圖5：臨界模型(a)

圖6：臨界模型(b)

圖7：異步模型(a)

圖8：異步模型(b)

規(guī)則說明：圖5 是指transition t 觸發(fā)前的標(biāo)記；圖6 是指transition t 觸發(fā)后的標(biāo)記，這里t 不會被觸發(fā)。

2.4 異步模型

在進(jìn)行迭代運算時，經(jīng)常要將某個變量的舊值清除，再將賦予新值，這種操作便是異步的一種形式。在Petri 網(wǎng)模擬反直觀量子通信協(xié)議中的狀態(tài)變換時，要經(jīng)常用到異步這一概念。這里，對協(xié)議中用的異步概念進(jìn)行建模。

這一概念可以通過模擬一個C 語言程序進(jìn)行描述，如圖7 和圖8所示，在place P1中裝入一個token，P1作為開始端，經(jīng)過transition t1，最終數(shù)據(jù)裝入place P2，此后，transition t1不會被觸發(fā)。

C 語言程序：

規(guī)則說明：圖7 是指transition t1 觸發(fā)前的標(biāo)記；圖8 是指transition t1觸發(fā)后的標(biāo)記，這里t1不會被觸發(fā)。

從圖8 中P2消除舊數(shù)據(jù)和填充新數(shù)據(jù)以及P4清除緩存之間的時間間隔，可以看出異步起到了延時的作用。

3 小結(jié)

本文利用Petri 網(wǎng)形式化工具對量子態(tài)、四則運算、異步模式與臨界模型等量子通信協(xié)議中涉及的一些基礎(chǔ)概念進(jìn)行了建模，其意義在于為實現(xiàn)對任意給定量子通信協(xié)議的Petri 網(wǎng)建模奠定一定理論基礎(chǔ)，為下一步實現(xiàn)量子通信協(xié)議的計算機(jī)自動化分析與驗證做準(zhǔn)備。