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

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