JOURNAL OF SHANDONG UNIVERSITY(NATURAL SCIENCE) ›› 2019, Vol. 54 ›› Issue (3): 18-27.doi: 10.6040/j.issn.1671-9352.2.2018.053

•   • Previous Articles     Next Articles

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)

278

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

CLC Number: 

  • TP309

Fig.1

The mode implementing protocol security analysis"

Table 1

The data of function returns value of protocol code implementing"

协议名称 协议运行时函数返回值的迹
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

Fig.2

The part of the source code of Needham-Schroeder-Lowe's participants"

Fig.3

The behaviors of different protocols implementation"

Table 2

Comparison of new models with existing analytical models"

模型类型 计算分析 形式化分析 代码实现行为分析
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] CUI Jing, LIANG Qiu-ju. Existence and controllability of nonlocal stochastcic integro-differential equations driven by fractional Brownian motion [J]. JOURNAL OF SHANDONG UNIVERSITY(NATURAL SCIENCE), 2017, 52(12): 81-88.
[2] DENG Lei, ZHAO Jian-li, LIU Hua, LI Ying. Controllability and observability of k-valued control networks [J]. JOURNAL OF SHANDONG UNIVERSITY(NATURAL SCIENCE), 2015, 50(04): 27-35.
Viewed
Full text


Abstract

Cited
  Shared   
  Discussed   
[1] YANG Yong-wei1, 2, HE Peng-fei2, LI Yi-jun2,3. On strict filters of BL-algebras#br#[J]. JOURNAL OF SHANDONG UNIVERSITY(NATURAL SCIENCE), 2014, 49(03): 63 -67 .
[2] ZHAO Tong-xin1, LIU Lin-de1*, ZHANG Li1, PAN Cheng-chen2, JIA Xing-jun1. Pollinators and pollen polymorphism of  Wisteria sinensis (Sims) Sweet[J]. JOURNAL OF SHANDONG UNIVERSITY(NATURAL SCIENCE), 2014, 49(03): 1 -5 .
[3] GUO Lan-lan1,2, GENG Jie1, SHI Shuo1,3, YUAN Fei1, LEI Li1, DU Guang-sheng1*. Computing research of the water hammer pressure in the process of #br# the variable speed closure of valve based on UDF method[J]. JOURNAL OF SHANDONG UNIVERSITY(NATURAL SCIENCE), 2014, 49(03): 27 -30 .
[4] LI Min1,2, LI Qi-qiang1. Observer-based sliding mode control of uncertain singular time-delay systems#br#[J]. JOURNAL OF SHANDONG UNIVERSITY(NATURAL SCIENCE), 2014, 49(03): 37 -42 .
[5] HAN Ya-fei, YI Wen-hui, WANG Wen-bo, WANG Yan-ping, WANG Hua-tian*. Soil bacteria diversity in continuous cropping poplar plantation#br# by high throughput sequencing[J]. JOURNAL OF SHANDONG UNIVERSITY(NATURAL SCIENCE), 2014, 49(05): 1 -6 .
[6] WANG Kai-rong, GAO Pei-ting. Two mixed conjugate gradient methods based on DY[J]. JOURNAL OF SHANDONG UNIVERSITY(NATURAL SCIENCE), 2016, 51(6): 16 -23 .
[7] MA Yuan-yuan, MENG Hui-li, XU Jiu-cheng, ZHU Ma. Normal distribution of lattice close-degree based on granular computing[J]. JOURNAL OF SHANDONG UNIVERSITY(NATURAL SCIENCE), 2014, 49(08): 107 -110 .
[8] XU Jun-feng. On the growth of the meromorphic solutions of complex algebraic differential equations[J]. J4, 2010, 45(6): 91 -93 .
[9] PEI Sheng-yu，ZHOU Yong-quan. A mult-objective particle swarm optimization algorithm based on  the  chaotic mutation[J]. J4, 2010, 45(7): 18 -23 .
[10] DU Ji-xiang1,2, YU Qing1, ZHAI Chuan-ming1. Age estimation of facial images based on non-negative matrix factorization with sparseness constraints[J]. J4, 2010, 45(7): 65 -69 .
Copyright 2018 © Editorial office of JOURNAL OF SHANDONG UNIVERSITY(NATURAL SCIENCE)
Supported by Beijing Magtech Co.Ltd