您的位置：山东大学 -> 科技期刊社 -> 《山东大学学报（理学版）》

《山东大学学报(理学版)》 ›› 2019, Vol. 54 ›› Issue (3): 18-27.doi: 10.6040/j.issn.1671-9352.2.2018.053

•   • 上一篇    下一篇

基于密码协议实现的行为安全分析模型

吴福生1(),张焕国2,*(),倪明涛2,王俊3   

  1. 1. 贵州财经大学贵州省经济系统仿真重点实验室, 贵州 贵阳 550004
    2. 武汉大学国家网络安全学院, 湖北 武汉 430072
    3. 中南民族大学计算机科学学院, 湖北 武汉 430074
  • 收稿日期:2018-09-20 出版日期:2019-03-20 发布日期:2019-03-19
  • 通讯作者: 张焕国 E-mail:wfskaoyan@163.com;liss@whu.edu.cn
  • 作者简介:吴福生(1974—),男,博士，副教授,研究方向为密码协议实现安全、软件实现安全和漏洞分析. E-mail:wfskaoyan@163.com
  • 基金资助:
    国家自然科学基金重点项目(61332019);国家重点基础研究发展规划项目计划(973计划)(2014CB340601);2018年度贵州财经大学引进人才科研启动项目

Security analysis model of behavior based on cryptographic protocols implement at source code level

Fu-sheng WU1(),Huan-guo ZHANG2,*(),Ming-tao NI2,Jun WANG3   

  1. 1. Guizhou Key Laboratory of Economics System Simulation, Guizhou University of Finance and Economics, Guiyang 550004, Guizhou, China
    2. School of National Cybersecurity, Key Laboratory of Aerospace Information Security and Trusted Computing, Ministry of Education, Wuhan University, Wuhan 430072, Hubei, China
    3. College of Computer Science, South-Central University for Nationalities, Wuhan 430074, Hubei, China
  • Received:2018-09-20 Online:2019-03-20 Published:2019-03-19
  • Contact: Huan-guo ZHANG E-mail:wfskaoyan@163.com;liss@whu.edu.cn
  • Supported by:
    国家自然科学基金重点项目(61332019);国家重点基础研究发展规划项目计划(973计划)(2014CB340601);2018年度贵州财经大学引进人才科研启动项目

RichHTML

12

PDF (PC)

277

摘要：

提出了一种基于密码协议实现的行为安全分析模型,该模型把密码协议实现分2个部分:一是外部行为(开放网络空间交互通信的行为);二是内部行为(代码实现的行为)。通过行为的可控性,能够发现、控制或纠正密码协议实现的安全。基于该分析模型方法,以经典的密码协议为实例进行模拟实验。实验结果表明,密码协议实现的行为安全是可控的。

关键词: 分析模型, 密码协议实现, 行为安全, 可控性

Abstract:

An analytical model of the behavior based on the cryptographic protocols implement at source code level is proposed. The cryptographic protocol implementations can be divided into two parts by the model that is proposed. One is an external behavior (the behavior of opening the interactive communications in cyberspace); the other is an internal behavior (the behavior of cryptographic protocol implements at the source code level). Though the behavior controllability, it is possible to find, control, or correct the security of the cryptographic protocol implementations at the source code level. Based on the analysis model method, a simulation experiment using classic cryptographic protocol as an example was given. The results show that the behavioral security of the cryptographic protocol implementations is controllable.

Key words: analysis model, cryptographic protocol implementation, behavior security, controllability

中图分类号: 

  • TP309

图1

密码协议实现的行为安全分析模型"

表1

协议代码实现函数返回值迹的数据"

协议名称 协议运行时函数返回值的迹
INS 48 1 134 216 112 144 53 5 101 128 128 128 128 176 1 214 216 128 128 144 176 53 208 128 128 216 216 175 244 0 0 128 128 244 216 216 216 122 0 0 1
NSL 48 1 118 216 112 144 53 5 72 128 128 128 128 176 1 200 216 240 16 53 1 215 128 128 128 128 144 176 53 5 208 128 167 216 216 167 244 16 0 128 128 244 216 216 216 216 122 0 0 1
NSMA 80 1 243 216 80 1 104 216 216 216 144 176 53 5 8 128 128 128 128 228 224 224 240 16 53 1 110 128 128 128 128 176 208 535 72 128 128 128 128 0 0 0 1 216 0 0 216 0

图2

Needham-Schroeder-Lowe协议参与者的部分源代码"

图3

不同密码协议代码实现时的行为"

表2

新模型与现有分析模型对比"

模型类型 计算分析 形式化分析 代码实现行为分析
Model Extraction √ √ ×
Code Generation √ √ ×
Type Checking × √ ×
Our Model × √ √
1 张焕国, 韩文报, 来学嘉, 等. 网络空间安全综述[J]. 中国科学:信息科学, 2016, 46 (2): 125- 164.
ZHANG Huanguo , HAN Wenbao , LAI Xuejia , et al. Survey on cyberspace security[J]. Scientia Sinica(Informationis), 2016, 46 (2): 125- 164.
2 薛锐, 冯登国. 安全协议的形式化分析技术与方法[J]. 计算机学报, 2006, 29 (1): 1- 20.
doi: 10.3321/j.issn:0254-4164.2006.01.001
XUE Rui , FENG Dengguo . The approaches and technologies for formal verification of security protocols[J]. Chinese Journal of Computers, 2006, 29 (1): 1- 20.
doi: 10.3321/j.issn:0254-4164.2006.01.001
3 雷新锋, 宋书民, 刘伟兵, 等. 计算可靠的密码协议形式化分析综述[J]. 计算机学报, 2014, 37 (5): 993- 1016.
LEI Xinfeng , SONG Shumin , LIU Weibing , et al. A survey on computationally sound formal analysis of cryptographic protocols[J]. Chinese Journal of Computers, 2014, 37 (5): 993- 1016.
4 BHARGAVAN K, FOURNET C, GORDON A D. Modular verification of security protocol code by typing[C]//37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. New York: ACM, 2010: 445-456.
5 WU Fusheng , ZHANG Huanguo , WANG Wengqing , et al. A new method to analyze the security of protocol implementations based on ideal trace[J]. Security and Communication Networks, 2017, 2017: 1- 15.
6 MICHAEL B, MATTEO M, DOMINIQUE U. Computationally sound verification of source code[C]//17th Conference on Computer and Communications Security. Chicago: CCS, 2010: 387-398.
7 MATTEO A , ALFREDO P , RICCARDO S . Formal verification of security protocol implementations:a survey[J]. Formal Aspects of Computing, 2014, 26 (1): 99- 123.
doi: 10.1007/s00165-012-0269-9
8 JEAN G, FABRICE P. Cryptographic protocol analysis on real C code[C]//6th International Conference on Verification, Model Checking, and Abstract Interpretation. Berlin: Springer, 2005: 363-379.
9 NEEDHAM R , SCHROEDER M . Using encryption for authentication in large networks of computers[J]. Communications of the ACM, 1978, 21 (12): 993- 999.
doi: 10.1145/359657.359659
10 DOLEV D , YAO A . On the security of public key protocols[J]. IEEE Transactions on Information Theory, 1983, 29 (2): 198- 208.
doi: 10.1109/TIT.1983.1056650
11 SAGAR C, ANUPAM D. ASPIER: an automated framework for verifying security protocol implementations[C]//22th IEEE Computer Security Foundations Symposium. New York: CSF2009: 172-185.
12 AIZATULIN M, GORDON A, JURJENS J. Extracting and verifying cryptographic models from C protocol code by symbolic execution[C]//18th ACM Conference on Computer and Communications Security. Chicago: CCS, 2011: 331-340.
13 MIHHAI A, ANDREW D, GORDON A, JURJENS J. Computational verification of C protocol implementations by symbolicExecution[C]//19th. ACM Conference on Computer and Communications Security. North Carolina: CCS, 2012: 699-711.
14 ALIPOUR H , AL-NASHIF Y B , SATAM P , et al. Wireless anomaly detection based on IEEE 802.11 behavior analysis[J]. IEEE Transactions on Information Forensics and Security, 2015, 10 (10): 2158- 2170.
doi: 10.1109/TIFS.2015.2433898
15 PRATIK S , HAMID A , YOUSSIF A , et al. Anomaly behavior analysis of DNS protocol[J]. Journal of Internet Services and Information Security, 2015, 5 (4): 85- 97.
16 VERKIJIKA S F . Understanding smartphone security behaviors: an extension of the protection motivation theory with anticipated regret[J]. Computers & Security, 2017, 77: 860- 870.
17 ALSMADI D , PRYBUTOK V . Sharing and storage behavior via cloud computing: security and privacy in research and practice[J]. Computers in Human Behavior, 2018, 85: 218- 226.
doi: 10.1016/j.chb.2018.04.003
18 王元元. 计算机科学中的逻辑学[M]. 北京: 科学出版社, 1989.
WANG Yuanyuan . Logic in Computer Science[M]. Beijing: Science Press, 1989.
19 CREMERS C, MAUW S. Operational semantics[M]//CREMERS C, MAUW S. eds. Operational Semantics and Verification of Security Protocols. Berlin: Springer, 2012: 13-35.
20 魏欧, 石玉峰, 徐丙凤, 等. 软件模型检测中的抽象模型研究综述[J]. 计算机研究与发展, 2015, 52 (7): 1580- 1603.
WEI Ou , SHI Yufeng , XU Bingfeng , et al. Abstract modeling formalisms in software model checking[J]. Journal of Computer Research and Development, 2015, 52 (7): 1580- 1603.
21 ABADI M , BLANCHET B . Computer-assisted verification of a protocol for certified email[J]. Science of Computer Programming, 2005, 58 (1/2): 3- 27.
22 BLANCHET B . A computationally sound mechanized prover for security protocols[J]. IEEE Transactions on Dependable and Secure Computing, 2008, 5 (4): 193- 207.
doi: 10.1109/TDSC.2007.1005
23 唐朝京, 鲁智勇, 冯超. 基于计算语义的安全协议验证逻辑[J]. 电子学报, 2014, 42 (6): 1179- 1185.
doi: 10.3969/j.issn.0372-2112.2014.06.022
TANG Chaojing , LU Zhiyong , FENG Chao . A verification logic for security protocols based on computational semantics[J]. Acta Electronica Sinica, 2014, 42 (6): 1179- 1185.
doi: 10.3969/j.issn.0372-2112.2014.06.022
24 XIAO M H , DENG C Y , MA C L , et al. A novel approach to automatic security protocol analysis based on authentication event logic[J]. Chinese Journal of Electronics, 2015, 24 (1): 187- 192.
25 KUMAR N V N, SHYAMASUNDAR R K. POSTER: dynamic labelling for analyzing security protocols.[C]//22th ACM SIGSAC Conference on Computer and Communications Security. Denver: CCS, 2015: 1665-1667.
26 CONTI M , DRAGONI N , LESYK V . A survey of man in the middle attacks[J]. IEEE Communications Surveys & Tutorials, 2016, 18 (3): 2027- 2051.
27 YANG W C, HU J K, FERNANDES C, et al. Vulnerability analysis of iPhone 6[C]//2016 14th Annual Conference on Privacy, Security and Trust. New Zealand: [s.n.], 2016: 457-463.
[1] 崔静,梁秋菊. 分数布朗运动驱动的非局部随机积分微分系统的存在性与可控性[J]. 山东大学学报（理学版）, 2017, 52(12): 81-88.
[2] 邓磊, 赵建立, 刘华, 李莹. k-值控制网络的可控性与可观性[J]. 山东大学学报（理学版）, 2015, 50(04): 27-35.
Viewed
Full text


Abstract

Cited
  Shared   
  Discussed   
[1] 杨永伟1,2,贺鹏飞2,李毅君2,3. BL-代数的严格滤子[J]. 山东大学学报（理学版）, 2014, 49(03): 63 -67 .
[2] 赵同欣1,刘林德1*,张莉1,潘成臣2,贾兴军1. 紫藤传粉昆虫与花粉多型性研究[J]. 山东大学学报（理学版）, 2014, 49(03): 1 -5 .
[3] 郭兰兰1,2,耿介1,石硕1,3,苑飞1,雷丽1,杜广生1*. 基于UDF方法的阀门变速关闭过程中的#br# 水击压强计算研究[J]. 山东大学学报（理学版）, 2014, 49(03): 27 -30 .
[4] 李敏1,2,李歧强1. 不确定奇异时滞系统的观测器型滑模控制器[J]. 山东大学学报（理学版）, 2014, 49(03): 37 -42 .
[5] 韩亚飞,伊文慧,王文波,王延平,王华田*. 基于高通量测序技术的连作杨树人工林土壤细菌多样性研究[J]. 山东大学学报（理学版）, 2014, 49(05): 1 -6 .
[6] 王开荣,高佩婷. 建立在DY法上的两类混合共轭梯度法[J]. 山东大学学报（理学版）, 2016, 51(6): 16 -23 .
[7] 马媛媛, 孟慧丽, 徐久成, 朱玛. 基于粒计算的正态粒集下的格贴近度[J]. 山东大学学报（理学版）, 2014, 49(08): 107 -110 .
[8] 徐俊峰. 关于复代数微分方程亚纯解的增长级[J]. J4, 2010, 45(6): 91 -93 .
[9] 裴胜玉，周永权*. 一种基于混沌变异的多目标粒子群优化算法[J]. J4, 2010, 45(7): 18 -23 .
[10] 杜吉祥1,2,余庆1,翟传敏1. 基于稀疏性约束非负矩阵分解的人脸年龄估计方法[J]. J4, 2010, 45(7): 65 -69 .
版权所有 © 2018 《山东大学学报(理学版)》编辑部　
地址: 山东省济南市山大南路27号山东大学中心校区（250100）　电话: +86-0531-88366917　E-mail: xblxb@sdu.edu.cn
本系统由北京玛格泰克科技发展有限公司设计开发