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

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

单位：北京科技大学信息工程学院; 北京100083; 清华大学计算机科学与技术系; 北京100084