安全协议的测试与证明

doi:10.3778/j.issn.1002-8331.2009.04.008

计算机工程与应用 ›› 2009, Vol. 45 ›› Issue (4): 26-29.DOI: 10.3778/j.issn.1002-8331.2009.04.008

安全协议的测试与证明

乔海燕

中山大学，广州 510275

收稿日期:2008-09-19 修回日期:2008-11-10 出版日期:2009-02-01 发布日期:2009-02-01
通讯作者: 乔海燕

Testing and proving security protocols

QIAO Hai-yan

Zhongshan University，Guangzhou 510275，China

Received:2008-09-19 Revised:2008-11-10 Online:2009-02-01 Published:2009-02-01
Contact: QIAO Hai-yan

摘要/Abstract

摘要： 提出通过测试来证明安全协议的方法。以NS和NSL协议为例，首先将协议形式化为事件序列，协议的性质可以表示为序列上的性质。协议的完整运行可以系统地生成，因此，协议的性质可以系统地测试。形式化和测试在函数程序设计语言Haskell中完成。

关键词: 测试, Needham-Schroeder-Lowe协议, 函数程序设计

Abstract: It is shown how security protocols can be systematically tested，hence proved in Haskell.That is demonstrated by analyzing NS（Needham-Schroeder） and NSL（Needham-Schroeder-Lowe） protocols：runs of the protocols are formalized as event traces and properties on traces are tested.Complete runs of a protocol with a penetrator can be generated systematically，and properties of the protocol can be tested systematically.Lowe’s attack is easily revealed by testing NS protocol and authentication and secrecy are proved valid for NSL protocol by testing.

Key words: testing, Needham-Schroeder-Lowe（NSL） protocol, functional programming

乔海燕. 安全协议的测试与证明[J]. 计算机工程与应用, 2009, 45(4): 26-29.

QIAO Hai-yan. Testing and proving security protocols[J]. Computer Engineering and Applications, 2009, 45(4): 26-29.

[1]	徐辰华，骆珠光，吴冠宏，刘斌. 基于正弦因子和量子局部搜索的灰狼优化算法[J]. 计算机工程与应用, 2021, 57(24): 83-89.
[2]	李舵，董超群，司品超，何曼，刘钱超. 神经网络验证和测试技术研究综述[J]. 计算机工程与应用, 2021, 57(22): 53-67.
[3]	左阔，李宁，田英爱，侯霞. 流式文档排版效果自动化测试方法[J]. 计算机工程与应用, 2021, 57(2): 273-278.
[4]	胡鹤，赵毅，王宪贺. IB网上CPU-GPU异构超算平台容器性能评估及优化[J]. 计算机工程与应用, 2021, 57(18): 82-85.
[5]	伍旭东，唐麒，张伟，张健，魏急波，王一军. 基于扩展有限状态机的SCA符合性测试方法研究[J]. 计算机工程与应用, 2021, 57(16): 263-268.
[6]	谭莉娟，郑巍，刘友林，樊鑫，杨丰玉. 面向适航标准的机载软件测试验证方法综述[J]. 计算机工程与应用, 2021, 57(15): 9-22.
[7]	刘友林，郑巍，谭莉娟，樊鑫，杨丰玉. 面向适航标准的机载软件测试验证工具综述[J]. 计算机工程与应用, 2021, 57(11): 1-10.
[8]	唐维军，徐琨，柳有权，夏悬. 自动驾驶汽车虚拟测试中的树木点云生成方法[J]. 计算机工程与应用, 2021, 57(11): 185-192.
[9]	吴欣舟，方芳，王伟. 3D SoC并行测试中TAM调度优化设计[J]. 计算机工程与应用, 2020, 56(4): 31-36.
[10]	张洪泽，洪征，周胜利，冯文博. 基于协议状态机遍历的模糊测试优化方法[J]. 计算机工程与应用, 2020, 56(4): 82-91.
[11]	冯纾，王军锋，蔡勇，冯登明，王文军. 低光照度下人机界面背景色眼动分析评价研究[J]. 计算机工程与应用, 2020, 56(4): 262-267.
[12]	沈鑫，邹德旋，张强. 采用双变异策略的自适应差分进化算法及应用[J]. 计算机工程与应用, 2020, 56(4): 146-157.
[13]	马原东，罗子江，倪照风，徐斌，吴凤娇，孙收余，杨秀璋. 改进SSD算法的多目标检测[J]. 计算机工程与应用, 2020, 56(23): 23-30.
[14]	沈晴，牟永敏. 函数调用路径测试用例自动生成的方法研究[J]. 计算机工程与应用, 2020, 56(18): 238-246.
[15]	刘佳洛，姚奕，黄松，惠战伟，陈强，寇大磊，张仲伟. 机器学习图像分类程序的蜕变测试框架[J]. 计算机工程与应用, 2020, 56(17): 69-77.

安全协议的测试与证明

Testing and proving security protocols

PDF

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 15

编辑推荐

Metrics