安全协议形式化分析的不变式生成技术

doi:10.7523/j.issn.2095-6134.2002.1.013

中国科学院大学学报 ›› 2002, Vol. 19 ›› Issue (1): 91-96.DOI: 10.7523/j.issn.2095-6134.2002.1.013

安全协议形式化分析的不变式生成技术

范红¹, 冯登国¹, 郭金庚²

1. 中国科学院研究生院信息安全国家重点实验室, 北京 100039;
2. 解放军信息工程大学安全学院计算机系, 郑州 450004

收稿日期:2001-09-19 修回日期:2001-10-19 发布日期:2002-01-10
作者简介:范红,女,1969年7月生,博士生;E-mail:pkfanhong@sina.com
基金资助:
973资助项目(G1999035802);国家杰出青年科学基金资助项目(60025205)

Invariant Generation Techniques in Cryptographic Protocol Analysis

FAN Hong¹, FENG DengGuo¹, GUO JinGeng²

1. State Key Laboratory of Information Security,Graduate School, Chinese Academy of Sciences,Beijing 100039;
2. Institute of Information Security, PLA University of Information Engineering,Zhengzhou 450004

Received:2001-09-19 Revised:2001-10-19 Published:2002-01-10

摘要/Abstract

摘要：

给出了应用于不同系统的不变式的概述, 分析了彼此之间的关系, 进行了分类, 并探讨了其未来发展趋势.密码协议的形式化分析日渐引起人们的广泛关注.这导致了不变式生成与描述技术的发展.不变式是对入侵者可知和不可知消息的定义, 可用于协议认证和秘密性的证明, 从而成为许多协议形式化分析工具和技术的核心

关键词: 协议, 形式化分析, 不变式

Abstract:

Formal methods for cryptographic protocol analysis has drawn attention in recent years This leads to a development of the generation and specification techniques of invariant Invariantis defined what messages an intruder can and cannot learn and can be used to prove authentication as well as secrecy results, appear to be central This paper introducls an overview of invariant in different systems, analyzes their relationships to each other, develops a simple taxonomy, and discuses some of the implications for future research.

Key words: cryptographic protocols, formal analysis, invariant

中图分类号:

TP309

范红, 冯登国, 郭金庚. 安全协议形式化分析的不变式生成技术[J]. 中国科学院大学学报, 2002, 19(1): 91-96.

FAN Hong, FENG DengGuo, GUO JinGeng. Invariant Generation Techniques in Cryptographic Protocol Analysis[J]. , 2002, 19(1): 91-96.

[1]	薛开平, 柳彬, 李威, 洪佩琳. 一种面向未知链路帧的格式特征提取与分类算法[J]. 中国科学院大学学报, 2018, 35(4): 521-528.
[2]	林雪燕, 林璟锵, 管乐, 王雷. 在桌面虚拟化系统中实施国产密码算法[J]. 中国科学院大学学报, 2015, 32(5): 701-707.
[3]	余晟, 尚德重, 周猛, 张宝贤. 基于可调节局部洪泛更新的移动WSN路由协议[J]. 中国科学院大学学报, 2015, 32(2): 273-280.
[4]	郭冠华, 焦臻桢, 周猛, 张宝贤. 基于地理位置和多阶邻节点辅助的编码感知无线多跳网络路由协议[J]. 中国科学院大学学报, 2015, 32(1): 140-144.
[5]	姜福凯, 卢汉成. 基于跨层包大小优化的DTN节点存储资源管理机制[J]. 中国科学院大学学报, 2014, 31(6): 836-842.
[6]	黄桂芳, 胡磊. 统计绑定的非交互的非延展承诺[J]. 中国科学院大学学报, 2013, 30(2): 264-271.
[7]	罗成, 张玉清, 王龙, 刘奇旭. 基于符号表达式的未知协议格式分析及漏洞挖掘[J]. 中国科学院大学学报, 2013, 30(2): 278-284.
[8]	刘书明, 刘建伟, 毛剑. 一种改进的AODV安全路由协议[J]. 中国科学院大学学报, 2011, 28(6): 801-805.
[9]	赫卫卿, 杨寿保, 滕达, 胡云. 802.11s无线Mesh网络中协作多样性感知的路由度量和协作路由协议[J]. 中国科学院大学学报, 2011, 28(4): 522-530.
[10]	张子坤, 吕克伟. Σ-保密的隐秘信息检索协议[J]. 中国科学院大学学报, 2011, 28(3): 389-397.
[11]	邵秀凤, 李荣花. 关于一个数值比较协议的安全性证明[J]. 中国科学院大学学报, 2011, 28(2): 262-265.
[12]	郭婵, 洪佩琳, 薛开平. IEEE 802.11无线网状网中的一种干扰感知的多径路由协议[J]. 中国科学院大学学报, 2010, 27(6): 809-817.
[13]	黄桂芳, 胡磊, 林东岱. 从Σ-协议到公共参考串模型下可否认零知识的高效编译器[J]. 中国科学院大学学报, 2010, 27(6): 831-837.
[14]	丁治国, 朱学永, 雷迎科. 基于码分多址和防碰撞功能的RFID安全认证协议[J]. 中国科学院大学学报, 2010, 27(3): 397-403.
[15]	胡云, 杨寿保, 郭晓雷, 沈庆伟. 面向Internet接入的WMN负载平衡路由策略[J]. 中国科学院大学学报, 2010, 27(2): 234-244.

安全协议形式化分析的不变式生成技术

Invariant Generation Techniques in Cryptographic Protocol Analysis

PDF (PC)

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 15

编辑推荐

Metrics

本文评价

访问统计

联系我们