非否认协议公平性分析的扩展串空间方法

李磊 1; 陈静 2; 王育民 1

您当前的位置：

首页 >

文章列表页 >

非否认协议公平性分析的扩展串空间方法

更新时间：2025-07-09

- 非否认协议公平性分析的扩展串空间方法
- An Extended Strand Space Method for Fairness Analysis of Non-Repudiation Protocols
- 西安交通大学学报 2010年44卷第6期页码：16-20
- 作者机构：
  
  西安电子科技大学综合业务网国家重点实验室,西安,710071
- 作者简介：
- 基金信息：
  
  : 2009-10-02. 作者简介: 李磊(1974-),男,博士生;王育民(联系人),男,教授,博士生导师. 基金项目: 国家自然科学基金资助项目(60473027);国家自然科学基金委员会-广东联合基金重点资助项目(U0835004)
- DOI：
  中图分类号： TN918
- 网络首发：2010-06-10，
  
  纸质出版：2010
- 稿件说明：
移动端阅览
李磊 1, 陈静 2, 王育民 1. 非否认协议公平性分析的扩展串空间方法[J]. 西安交通大学学报, 2010,44(6):16-20.

An Extended Strand Space Method for Fairness Analysis of Non-Repudiation Protocols[J]. 2010, 44(6): 16-20.
李磊 1, 陈静 2, 王育民 1. 非否认协议公平性分析的扩展串空间方法[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.

浏览量

下载量

CSCD

文章被引用时，请邮件提醒。

提交

工具集

关联资源

面向命题投影时序逻辑的安全协议模型检测

采用弧映射的双层对象分布算法

EBSILON软件在热电联产系统优化中的应用综述

张角凹坑气膜孔对双层壁气膜冷却特性的影响

冷库水平空气幕热湿阻隔性能数值模拟研究