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

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

作　　者：郭迎九[1,2] 林闯[2] 尹浩[2] 田立勤[1] 

机构地区：[1]北京科技大学信息工程学院,北京100083 [2]清华大学计算机科学与技术系,北京100084

出　　处：《电子学报》2009年第5期1030-1036,共7页Acta Electronica Sinica

基　　金：国家自然科学基金(No.60673184,No.60673187,No.60673054,No.90412012);973计划前期研究专项(No.2006CB708301);中国移动通信研究院项目;教育部科技创新培育重点项目(No.707005)

摘　　要：安全协议的形式化证明是目前的一个热点和难点问题.本文以一种数字媒体分发协议(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.

关 键 词：PETRI网 安全协议 数字媒体 

分 类 号：TP309[自动化与计算机技术—计算机系统结构]