期刊文献+

颜色Petri网一种专有协议的描述和验证 被引量:1

Formal Description and Validation of a Private Protocol Based on Coloured Petri Nets
下载PDF
导出
摘要 介绍了我们在一个网络安全项目中设计的点到点链路层协议,然后利用颜色Petri网和CPN Tools对该协议建模、分析和验证。首先建立了协议模型,然后运用仿真方法和状态空间分析方法考察协议行为特征。通过建模分析方法有助于我们找到协议中的疏漏,体现了协议设计过程中形式化建模和分析方法的优点和遇到的挑战。 This paper describes the formal description and validation of a private point to point protocol at the data link layer, using a CPN (Coloured Petri Net) model. It begins with the design and construction of a CPN model with formal specification. Then we investigate the protocol behaviour using simulation approach and state space analysis to identify some bugs and errors in the protocol design. The results demonstrate the benefits and challenge of formal analysis in a protocol design process.
出处 《系统仿真学报》 CAS CSCD 北大核心 2007年第A01期62-64,89,共4页 Journal of System Simulation
基金 国家自然科学基金资助项目(60673185)
关键词 有色PETRI网 颜色PETRI网 专有协议 CPNs CP-nets CPN Tools private protocol
  • 相关文献

参考文献9

  • 1罗军舟,seu.edu.cn,沈俊,顾冠群.从Petri网到形式描述技术和协议工程[J].软件学报,2000,11(5):606-615. 被引量:41
  • 2潘红艳,于全.用于通信网络协议开发的形式化方法[J].计算机工程,2004,30(2):129-130. 被引量:8
  • 3袁崇义.Petri网原理和应用[M].北京:电子工业出版社,2005.
  • 4Jensen K. An introduction to the theoretical aspects of colored Petri nets [J]. Computer Science, 1994, (803): 230-272.
  • 5University of Aarhus CPN Group Computer Tool for Coloured Petri Nets [EB/OL]. http://wiki.daimi.au.dk/cpntools/cpntools.wiki
  • 6黎波涛,罗军舟.不可否认协议的Petri网建模与分析[J].计算机研究与发展,2005,42(9):1571-1577. 被引量:11
  • 7Kristensen Lars M. The practitioner's guide to colored Petri nets [J]. International Journal on Software Tools for Technology Transfer, 1998, 2(2): 98-132.
  • 8Jensen K. A Brief Introduction to Colored Petri Nets. Lecture Notes In Computer Science [J/OL]. 1997, 1217: 203-208.
  • 9Kurt Jensen, Sφren Christensen, Lars M Kristensen. CPN Tools State Space Manual [EB/OL]. http://wiki.dalmi.au.dk/cpntools-help/_files/ manual.pdf.

二级参考文献22

  • 1G. Norman, V. Shmatikov. Analysis of probabilistic contract signing. In: Proc. BCS-FACS Formal Aspects of Security (FASec'02). New York: Springer-Verlag, 2002. 81~96.
  • 2L. Buttyun, J. P. Pierre Hubaux, S. Capkun. A formal analysis of Syverson' s rational exchange protocol. In: Proc. the 15th IEEE Computer Security Foundations Workshop. Nova Scotia,Canada: Cape Breton, 2002. 24~26.
  • 3S. Kremer, J. F. Raskin. Formal verification of non-repudiation protocols-A game approach. Formal Methods for Computer Security (FMCS 2000), Chicago, USA, 2000.
  • 4M. Abadi, B. Blanchet. Computer-assisted verification of a protocol for certified email. The 10th Int'l Symposium (SAS'03), San Diego, California, 2003.
  • 5V. Shmatikov, J. C. Mitchell. Finite-state analysis of two contract signing protocols. Theoretical Computer Science, 2002,283(2): 419~450.
  • 6B. B. Nieh, S. E. Tavares. Modeling and analyzing cryptographic protocols using Petri nets. In: Proc. AUSCRYPT'92. New York: Springer-Verlag, 1993.
  • 7N. Behki, S. E. Tavares. An integrated approach to protocol design. The 1989 IEEE Pacific Rim Conf. Computers,Communications and Signal Processing, BC, Canada, 1989.
  • 8T. Aura. Modelling the Needham-Schroeder authentication protocol with high level Petri nets. Helsinki University of Technology, Technical Report: B14, 1995.
  • 9A.M. Basyouni, S. E. Tavares. New approach to cryptographic protocol analysis using coloured Petri nets. In: Proc. Canadian Conf. Electrical and Computer Engineering. Nfld., Canada: St.Johns, 1997. 334~337.
  • 10J. Zhou, D. Gollmann. A fair non-repudiation protocol. The 1996 IEEE Symposium on Security and Privacy, Oakland, CA,1996.

共引文献55

同被引文献9

引证文献1

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

内容加载中请稍等...
;
使用帮助 返回顶部