基于Petri網的量子通信協議建模

張盛 馬詠輝

（武警海警學院 浙江省寧波市 315801）

1 引言

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

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

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

本文針對幾種量子通信協議中涉及的概念和結構，設計了相應的Petri 網模型，解決了量子通信協議Petri 網建模相關基礎理論問題。

2 基于Petri網的量子通信形式化基礎

2.1 量子態的Petri網描述

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

圖1：加法運算(a)

圖2：加法運算(b)

圖3：乘法運算(a)

圖4：乘法運算(b)

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

2.2 概率幅的四則運算模型

Petri 網作為一種狀態機，可以在實數域內表示數據的狀態變化。在建立量子反直觀通信協議的Petri 網模型前，先對協議中應用到的運算規則進行建模。

2.2.1 加法運算

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

規則說明：圖1 是指transition t 觸發前的標記；圖2 是指transition t 觸發后的標記，這里t 不會被觸發。

2.2.2 乘法運算

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

規則說明：圖3 是指transition t 觸發前的標記；圖4 是指transition t 觸發后的標記，這里t 不會被觸發。

2.3 臨界模型

為了實現Petri 網自動化處理反直觀量子通信協議中存在的狀態變換，依據程序語言中的臨界條件判定，對于Petri 網進行臨界操作的建模。

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

C 語言程序:

圖5：臨界模型(a)

圖6：臨界模型(b)

圖7：異步模型(a)

圖8：異步模型(b)

規則說明：圖5 是指transition t 觸發前的標記；圖6 是指transition t 觸發后的標記，這里t 不會被觸發。

2.4 異步模型

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

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

C 語言程序：

規則說明：圖7 是指transition t1 觸發前的標記；圖8 是指transition t1觸發后的標記，這里t1不會被觸發。

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

3 小結

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