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

郭迎九; 林 闯; 尹 浩; 田立勤

您当前的位置：

首页 >

文章列表页 >

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

论文 | 更新时间：2025-07-16

- 基于Petri网的数字媒体分发协议的安全性证明
- Proof of the Security of Digital Media Distributing Protocol Based on Petri Net Models
- 电子学报 2009年37卷第5期页码：1030-1036
- 作者机构：
  
  1. 北京科技大学信息工程学院,北京,100083
  2. 清华大学计算机科学与技术系,北京,100084
  3. 北京科技大学信息工程学院北京,100083
  4. 清华大学计算机科学与技术系北京,100084
- 作者简介：
- 基金信息：
  
  国家自然科学基金 (No.60673184,No.60673187,No.60673054,No.90412012);973计划前期研究专项 (No.2006CB708301);中国移动通信研究院项目和教育部科技创新培育重点项目 (No.707005)
- DOI：
  中图分类号： TP309
- 纸质出版：2009
- 稿件说明：
移动端阅览
郭迎九, 林闯, 尹浩, 等. 基于Petri网的数字媒体分发协议的安全性证明[J]. 电子学报, 2009,37(5):1030-1036.

GUO Ying-jiu, LIN Chuang, YIN Hao, et al. Proof of the Security of Digital Media Distributing Protocol Based on Petri Net Models[J]. Acta Electronica Sinica, 2009, 37(5): 1030-1036.
郭迎九, 林闯, 尹浩, 等. 基于Petri网的数字媒体分发协议的安全性证明[J]. 电子学报, 2009,37(5):1030-1036. DOI：

GUO Ying-jiu, LIN Chuang, YIN Hao, et al. Proof of the Security of Digital Media Distributing Protocol Based on Petri Net Models[J]. Acta Electronica Sinica, 2009, 37(5): 1030-1036. DOI：

摘要

安全协议的形式化证明是目前的一个热点和难点问题.本文以一种数字媒体分发协议(DMDP)为例

采用基于Petri网模型并结合进程代数和逻辑归纳方法对其进行形式化证明

新的方法有效避免了状态空间爆炸问题.在证明过程中

采用协议安全性等价原则

对分发协议进行简化

使证明更加简洁.文章同时对证明方法的完备性进行了讨论

说明了Petri网模型证明协议安全性的有效性.

Abstract

The formal proof of the security protocol becomes a hot and hard issue.Taking the Digital Media Distribution 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 transform the security protocols to guarantee the simplicity of the proof.At the same time

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.

关键词

Keywords

references

浏览量

1181

下载量

CSCD

文章被引用时，请邮件提醒。

提交

工具集

关联资源

基于Petri网的安全协议形式化分析

基于RFID发现服务的一种供应链建模技术

基于家态的多事务工作流完整性分析

Dining Cryptographer安全协议及工程分析

面向集成电路制造的基于Petri网的生产调度