高级检索
    王焕宝 张佑生 李 援. 安全协议的串空间图表示[J]. 计算机研究与发展, 2006, 43(12): 2062-2068.
    引用本文: 王焕宝 张佑生 李 援. 安全协议的串空间图表示[J]. 计算机研究与发展, 2006, 43(12): 2062-2068.
    Wang Huanbao, Zhang Yousheng, and Li Yuan. A Diagram of Strand Spaces for Security Protocols[J]. Journal of Computer Research and Development, 2006, 43(12): 2062-2068.
    Citation: Wang Huanbao, Zhang Yousheng, and Li Yuan. A Diagram of Strand Spaces for Security Protocols[J]. Journal of Computer Research and Development, 2006, 43(12): 2062-2068.

    安全协议的串空间图表示

    A Diagram of Strand Spaces for Security Protocols

    • 摘要: 串空间是安全协议的一种形式化描述,串空间图是它的图示化表示.定义开丛为串空间图的构造单元,并在开丛集上定义前缀算子和组合算子.通过开丛之间的前缀和组合运算,给出了无穷并发运行安全协议串空间图的生成方法.定义了开丛互模拟以及串空间图之间的互模拟等价关系,并给出用于消除串空间图冗余结构的化简规则.案例分析和与相关工作的比较表明,无冗余的串空间图为无穷并发运行安全协议的安全属性验证提供了一个有效的分析模型.

       

      Abstract: The strand space model illustrated with the diagram of strand spaces is adopted as a formalism of security protocols. The open bundle is defined, which is only one element for composing diagrams of strand spaces. And the two operators such as prefixing and parallel composition over the set of open bundles are defined. A novel method is proposed to generate diagrams of strand spaces of security protocols that run in an infinite concurrent way through operating of prefixing and parallel composition between open bundles. The bi-simulation equivalence relation between diagrams of strand spaces based on the bi-simulation between open bundles is defined. Reduction rules for eliminating redundancies of diagrams of strand spaces are also proposed. The case analysis and the comparison between this work and other related work show that the diagram of strand spaces can be used as an effective model for proving security properties of cryptographic protocols that run in an infinite concurrent way.

       

    /

    返回文章
    返回