基于Petri网的数字媒体分发协议的安全性证明

Proof of the Security of Digital Media Distributing Protocol Based on Petri Net Models

安全协议的形式化证明是目前的一个热点和难点问题.本文以一种数字媒体分发协议(DMDP)为例,采用基于Petri网模型并结合进程代数和逻辑归纳方法对其进行形式化证明,新的方法有效避免了状态空间爆炸问题.在证明过程中,采用协议安全性等价原则,对分发协议进行简化,使证明更加简洁.文章同时对证明方法的完备性进行了讨论,说明了Petri网模型证明协议安全性的有效性.

The formal proof of the security protocol becomes a hot and hard issue. Taking the Digital Media Distribufion Protocol as an example, the Petri Net model is adopted which combined with the process algebra and the logical induction methods to formally prove the present security protocol and can avoid the state explosion problem. In this proof an equality principle is used to Iransform the security protocols to guarantee the simplicity of the proof. At the same lime, the completeness of the proof is discussed and what we have done shows the validity of proving the security of protocol with a Petri Net model.