基于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 网建模奠定一定理论基础，为下一步实现量子通信协议的计算机自动化分析与验证做准备。