An Extended Strand Space Method for Fairness Analysis of Non-Repudiation Protocols

您当前的位置：

首页 >

文章列表页 >

An Extended Strand Space Method for Fairness Analysis of Non-Repudiation Protocols

更新时间：2025-07-09

- An Extended Strand Space Method for Fairness Analysis of Non-Repudiation Protocols
- Vol. 44, Issue 6, Pages: 16-20(2010)
- 作者机构：
  
  西安电子科技大学综合业务网国家重点实验室,西安,710071
- 作者简介：
- 基金信息：
- DOI：
  CLC： TN918
- Online First：10 June 2010，
  
  Published：2010
- 稿件说明：
移动端阅览
An Extended Strand Space Method for Fairness Analysis of Non-Repudiation Protocols[J]. 2010, 44(6): 16-20.
DOI：

An Extended Strand Space Method for Fairness Analysis of Non-Repudiation Protocols[J]. 2010, 44(6): 16-20. DOI：

摘要

针对在非否认协议公平性的形式化分析中

如何弱化初始假定和避免状态空间爆炸等问题

提出了扩展串空间方法.通过将签名运算引入串空间理论

从而对串空间理论的项集合进行重新定义

进一步通过对子项关系、攻击者迹和自由加密假定的扩展

并结合丛概念

构成了扩展串空间.分析非否认协议的公平性

首先将协议行为归纳为攻击者串、发送者串、接收者串和可信第3方串

以此构造协议的扩展串空间模型

然后结合协议迹和定理证明验证丛中存在发送者串等价于丛中存在接收者串

从而证明非否认协议公平性.通过扩展串空间方法对Zhou-Gollmann协议公平性的分析

得到了与Kailar逻辑和Lanotte自动验证方法相同的结果.与Kailar逻辑相比

扩展串空间方法仅使用自由加密假定

弱化了初始假定; 与Lanotte自动验证方法相比

扩展串空间方法无需使用状态空间搜索

避免了状态空间爆炸问题.

Abstract

A new formal analysis method using extended strand space is presented to weaken initial assumptions and to avoid state space explosion in analyzing the fairness of non-repudiation protocols. Signature operations are introduced into the strand space theory

so that the set of terms and sub-term relations are redefined in the strand space theory. Then

an extended strand space model is constructed by inducing the action of protocols to the penetrating strand

the origin strand

the receiver strand

and the trusted third party strand. The fairness of non-repudiation protocols is analyzed by verifying that the existence of the origin strand in the bundle is equivalent to the existence of the receiver strand in the bundle depending on the measure of theorem proving. Analyzing results on Zhou-Gollmann protocol show that the proposed method can weaken initial assumptions compared with the logic method

and can avoid state space explosion compared with the state space method.

关键词

Keywords

references

KREMER S, MARKOWITCH O, ZHOU J. An intensive survey of fair non-repudiation protocols [J]. Computer Communications, 2002, 25(17): 1606-1621.

KAILAR R. Accountability in electronic commerce protocols [J]. IEEE Transactions on Software Engineering, 1996, 22(5): 313-328.

周典萃, 卿斯汉,周展飞. 一种分析电子商务协议的新工具[J]. 软件学报, 2001, 12(9): 1318-1328.

ZHOU Diancui, QING Sihan, ZHOU Zhanfei. New approach for the analysis of electronic commerce protocols[J]. Journal of Software, 2001, 12(9): 1318-1328.

黎波涛,罗军舟. 不可否认协议时限性的形式化分析[J]. 软件学报, 2006, 17(7): 1510-1516.

LI Botao, LUO Junzhou. Formal analysis of timeliness in non-repudiation protocols [J]. Journal of Software, 2006, 17(7): 1510-1516.

韩志耕,罗军舟. 多方不可否认协议时限性分析与改进[J]. 电子学报, 2009, 37(2): 377-381.

HAN Zhigeng, LUO Junzhou. Analysis and improvement of timeliness of a multi-party non-repudiation protocol [J]. Acta Electronica Sinica, 2009, 37(2): 377-381.

LANOTTE R, MAGGIOLO-SCHETTINI A,TROINA A. Automatic analysis of a non-repudiation protocol [J]. Electronic Notes in Theoretical Computer Science, 2005, 112(S): 113-129.

GUO Yingjun, LIN Chuang, YIN Hao. Formal proof of the IDOP_SP protocol based on the Petri net [C]∥Proceedings of the 2008 IEEE International Conference on NAS. Piscataway, NJ, USA: IEEE, 2008: 161-162.

FABREGA F J T, HERZOG J C, GUTTMAN J D. Strand spaces: why is a security protocol correct?[C]∥Proceedings of the IEEE Computer Society Symposium on Research in Security and Privacy. Los Alamitos, CA, USA: IEEE Computer Society, 1998: 160-171.

FABREGA F J T, HERZOG J C, GUTTMAN J D. Honest ideals on strand spaces [C]∥Proceedings of the Computer Security Foundations Workshop.Los Alamitos, CA, USA: IEEE Computer Society, 1998: 66-77.

FABREGA F J T, HERZOG J C, GUTTMAN J D. Mixed strand spaces [C]∥Proceedings of the Computer Security Foundations Workshop. Los Alamitos, CA, USA: IEEE Compute Society, 1999: 72-82.

FABREGA F J T, HERZOG J C, GUTTMAN J D. Strand spaces: proving security protocols correct [J]. Journal of Computer Security, 1999, 7(2): 191-230.

GUTTMAN J D, FABREGA F J T. Authentication tests [C]∥Proceedings of the IEEE Computer Society Symposium on Research in Security and Privacy. Los Alamitos, CA, USA: IEEE Computer Society, 2000: 96-109.

ZHOU J, GOLLMANN D. A fair non-repudiation protocol [C]∥Proceedings of the 1996 IEEE Symposium on Security and Privacy. Piscataway, NJ, USA: IEEE, 1996: 55-61.

采用中国剩余定理的群签名方案的安全性分析与改进. 西安交通大学学报,2009, 43(2): 77-80.

具有局部验证者撤销的短群签名方案. 西安交通大学学报,2008, 42(10): 1250-1253.

排序问题的多方保密计算协议.西安交通大学学报, 2008, 42(2): 231-233.

一种防破坏广播型匿名通信网的多路访问协议.西安交通大学学报, 2007, 41(6): 674-678.

基于SWIM卡公钥认证的二阶段握手加密套接层协议.西安交通大学学报, 2007, 41(6): 669-673.

码率约束抗丢包伸缩码流保护的码率分配方法.西安交通大学学报, 2006, 40(12): 1432-1435.

一个可验证的秘密共享新个体加入协议.西安交通大学学报, 2006, 40(2): 207-210.

集合相交问题的双方保密计算.西安交通大学学报, 2006, 40(10): 1091-1093.

Views

下载量

CSCD

Alert me when the article has been cited

提交

Tools

Publicity Resources

Model-Checking Security Protocol with Propositional Projection Temporal Logic

An Object Distribution Algorithm Based on Arc and Two-Layer Mapping

Knowledge Graph Representation Learning Driven by Semantic Discrimination and Subgraph Integration

Influence of Structural Parameters on the Summer Operational Characteristics of a Three-Tower-in-One Indirect Air-Cooling System

Bi-Level Multi-Obj ective Optimization of a Wind-Solar Coupled Hydrogen Production System Based on the Synergy of Hybrid Electrolyzer Arrays

Related Author

杨琛 1

段振华 1

王小兵 1

聂世强

伍卫国

崔金华

Related Institution

Institute of Computing Theory and Technology, Xidian University

State Key Laboratory of Software Engineering, Wuhan University

School of the Electronic and Information Engineering, Xi'an Jiaotong University, Xi'an 710049, Chian

⁰