基于密码协议实现的行为安全分析模型
|
摘要
提出了一种基于密码协议实现的行为安全分析模型,该模型把密码协议实现分2个部分:一是外部行为(开放网络空间交互通信的行为);二是内部行为(代码实现的行为)。通过行为的可控性,能够发现、控制或纠正密码协议实现的安全。基于该分析模型方法,以经典的密码协议为实例进行模拟实验。实验结果表明,密码协议实现的行为安全是可控的。
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.
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.
引文
[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.XUE Rui, FENG Dengguo. The approaches and technologies for formal verification of security protocols[J]. Chinese Journal of Computers, 2006, 29(1):1-20.
[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.
[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.
[10] DOLEV D, YAO A. On the security of public key protocols[J]. IEEE Transactions on Information Theory, 1983, 29(2):198-208.
[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.
[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.
[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.
[23] 唐朝京, 鲁智勇, 冯超. 基于计算语义的安全协议验证逻辑[J]. 电子学报, 2014,42(6):1179-1185.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.
[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.
[2] 薛锐,冯登国.安全协议的形式化分析技术与方法[J].计算机学报, 2006,29(1):1-20.XUE Rui, FENG Dengguo. The approaches and technologies for formal verification of security protocols[J]. Chinese Journal of Computers, 2006, 29(1):1-20.
[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.
[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.
[10] DOLEV D, YAO A. On the security of public key protocols[J]. IEEE Transactions on Information Theory, 1983, 29(2):198-208.
[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.
[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.
[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.
[23] 唐朝京, 鲁智勇, 冯超. 基于计算语义的安全协议验证逻辑[J]. 电子学报, 2014,42(6):1179-1185.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.
[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.