一级黄色片免费播放|中国黄色视频播放片|日本三级a|可以直接考播黄片影视免费一级毛片

高級搜索

留言板

尊敬的讀者、作者、審稿人, 關(guān)于本刊的投稿、審稿、編輯和出版的任何問題, 您可以本頁添加留言。我們將盡快給您答復。謝謝您的支持!

姓名
郵箱
手機號碼
標題
留言內(nèi)容
驗證碼

安全協(xié)議的形式化規(guī)范

胡成軍 鄭援 呂述望 沈昌祥

胡成軍, 鄭援, 呂述望, 沈昌祥. 安全協(xié)議的形式化規(guī)范[J]. 電子與信息學報, 2004, 26(4): 556-561.
引用本文: 胡成軍, 鄭援, 呂述望, 沈昌祥. 安全協(xié)議的形式化規(guī)范[J]. 電子與信息學報, 2004, 26(4): 556-561.
Hu Cheng-jun, Zheng Yuan, Lǚ Shu-wang, Shen Chang-xiang. Formal Specification of Security Protocols[J]. Journal of Electronics & Information Technology, 2004, 26(4): 556-561.
Citation: Hu Cheng-jun, Zheng Yuan, Lǚ Shu-wang, Shen Chang-xiang. Formal Specification of Security Protocols[J]. Journal of Electronics & Information Technology, 2004, 26(4): 556-561.

安全協(xié)議的形式化規(guī)范

Formal Specification of Security Protocols

  • 摘要: 該文給出用PVS(Prototype Verification System)對安全協(xié)議進行形式化規(guī)范的一種方法。該方法以高階邏輯為規(guī)范語言,利用trace模型來描述協(xié)議的行為,并假設系統(tǒng)中存在強攻擊者和理想加密系統(tǒng)。重要的結(jié)構(gòu)如消息、事件、協(xié)議規(guī)則等都通過語義編碼方式定義。
  • Needham R M, Schroeder N D. Using encryption for authentication in large network of computers[J].Communications of the ACM.1978, 21(12):993-999[2]Steiner J G, Neuman B C, Schiller J I. Kerberos: an authentication service for open network systems. In Usenix Conference Proceedings, Dallas, Texas, 1988: 191-202.[3]CCITT. CCITT Recommendation X.509, The directory authentication framework, version 7,1987.[4]Owre S, Rushby J, Shankar N, Henke F. Formal verification for fault-tolerant architectures:Prolegomena to the design of PVS. IEEE Trans. on Software Engineering, 1995, SE-21(2): 107-125.[5]Paulson L. The inductive approach to verifying cryptographic protocols. Journal of Computer Security, 1998, 6(1): 85-128.[6]Millen J.[J].H. Rue. Protocol-independent secrecy. In 2000 IEEE Symposium on Security and Privacy, Oakland California, USA, IEEE Computer Society Press.2000,:-[7]Lowe G. A hierarchy of authentication specifications. In Proc. of The 10th Computer Security Foundations Workshop, Rockport, Massachusetts, USA, IEEE Computer Society Press, 1997:31-43.[8]Burrows M, Abadi M, Needham R. A logic of authentication[J].ACM Trans. on Computer Systems.1990, 8(1):18-36[9]Guttman J D, Thayer F J. Authentication tests. In 2000 IEEE Symposium on Security and Privacy, Oakland, California, USA, IEEE Computer Society Press, 2000: 96-109.[10]Roscoe A W. Modeling and verifying key-exchange protocols using CSP FDR. In Proc. of the 1995 IEEE Computer Security Foundations Workshop IIX, Dromquinna Manor, Kenmare,County Kerry, Ireland, IEEE Computer Society Press, 1995: 98-107.[11]Thayer J, Herzog J, Guttman J. Strand spaces: Why is a security protocol correct? In Proc. of the 1998 Symposium on Security and Privacy, Oakland California, USA, IEEE Computer Society Press, 1998: 160-171.[12]Paulson L. Isabelle: A Generic Theorem Prover. Berlin, New York: Springer, 1994.[13]胡成軍,鄭援,沈昌祥.密碼協(xié)議的秘密性證明.計算機學報,2003,26(3):367-372.
  • 加載中
計量
  • 文章訪問數(shù):  2150
  • HTML全文瀏覽量:  142
  • PDF下載量:  491
  • 被引次數(shù): 0
出版歷程
  • 收稿日期:  2002-11-28
  • 修回日期:  2003-02-28
  • 刊出日期:  2004-04-19

目錄

    /

    返回文章
    返回