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

GUO Ying-jiu; LIN Chuang; YIN Hao; TIAN Li-qin

您当前的位置：

首页 >

文章列表页 >

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

更新时间：2025-07-16

- Proof of the Security of Digital Media Distributing Protocol Based on Petri Net Models
- Acta Electronica Sinica Vol. 37, Issue 5, Pages: 1030-1036(2009)
- 作者机构：
  
  1. 北京科技大学信息工程学院,北京,100083
  2. 清华大学计算机科学与技术系,北京,100084
  3. 北京科技大学信息工程学院北京,100083
  4. 清华大学计算机科学与技术系北京,100084
- 作者简介：
- 基金信息：
- DOI：
  CLC： TP309
- Published：2009
- 稿件说明：
移动端阅览
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：

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

Views

1181

下载量

CSCD

Alert me when the article has been cited

提交

Tools

Publicity Resources

Formal Analysis of Security Protocols Using Petri Nets

A Supply Chain Modeling Technology Based on RFID Discovery Service

Soundness Analysis of the Multi-cases Workflow Model Based on Home State

Dining Cryptographer Protocol and Its Engineering Analysis

Petri Net Based Scheduling for Integrated Circuits Manufacturing

Related Author

BAI Shuo

Guo Li

LIU Dao-bin

FONT

WANG Li-fu

ZHANG Shi-kun

YUAN Chong-yi

LIU Dian-xing

Related Institution

Institute of Computing Technology,Chinese Academy of Sciences

北京大学信息科学技术学院软件研究所高可信软件技术教育部重点实验室

北京大学软件工程国家工程研究中心

1.北京大学信息科学技术学院

School of Information Science and EngineeringShandong University of Science and TechnologyQingdaoShandong 266510China

⁰