[1] GORDON M J C,MELHAM T F.Introduction to HOL:a theorem proving environment for higher order logic[M].Cambridge,UK:Cambridge University Press,1993. [2] ZHOU Jiantao,SHI Meilin,YE Xinming.Formal verification techniques in workflow process modeling[J].Journal of Computer Research and Development,2005,42(1):1-9.(in Chinese)周建涛,史美林,叶新铭.工作流过程建模中的形式化验证技术[J].计算机研究与发展,2005,42(1):1-9. [3] XUE Rui,FENG Dengguo.Formal analysis technology and method of security protocol[J].Chinese Journal of Computers,2006,29(1):1-20.(in Chinese)薛锐,冯登国.安全协议的形式化分析技术与方法[J].计算机学报,2006,29(1):1-20. [4] LING Huimin,ZHANG Wenhui.Model checking:theories,techniques and applications[J].Acta Electronica Sinica,2002,30(S1):1907-1912.(in Chinese)林惠民,张文辉.模型检测:理论、方法与应用[J].电子学报,2002,30(S1):1907-1912. [5] NIPKOW T,PAULSON L,WENZEL M.Isabelle/HOL:a proof assistant for higher-order logic[M].Berlin,Germany:Springer,2002. [6] BAI Shuo,SUI Liying,CHEN Qingfeng,et al.Verification logic of security protocol[J].Journal of Software,2000,11(2):213-221.(in Chinese)白硕,隋立颖,陈庆锋,等.安全协议的验证逻辑[J].软件学报,2000,11(2):213-221. [7] CAI Xinru,WANG Yijun,XUE Zhi,et al.Analysis and verification of the vulnerability RDP[J].Cyberspace Security,2016,7(Z1):49-53.(in Chinese)蔡新儒,王轶骏,薛质,等.RDP协议的安全性分析与验证[J].网络空间安全,2016,7(Z1):49-53. [8] ZHANG Yanshuo,WANG Zehao,WANG Zhiqiang,et al.Verifiable three-party secure key exchange protocol based on eigenvalue[J].Journal on Communications,2019,40(12):149-154.(in Chinese)张艳硕,王泽豪,王志强,等.基于特征值的可验证三方安全密钥交换协议[J].通信学报,2019,40(12):149-154. [9] ZHOU Yanwei,YANG Bo,ZHANG Wenzheng.Secure and efficient roaming authentication protocol with controllable anonymity for heterogeneous wireless network[J].Journal of Software,2016,27(2):451-465.(in Chinese)周彦伟,杨波,张文政.安全高效的异构无线网络可控匿名漫游认证协议[J].软件学报,2016,27(2):451-465. [10] ZHONG Cheng,LI Xinghua,SONG Yuanyuan,et al.A lightweight anonymous authentication protocol based on shared key in wireless networks[J].Chinese Journal of Computers,2018,41(5):1157-1171.(in Chinese)钟成,李兴华,宋园园,等.无线网络中基于共享密钥的轻量级匿名认证协议[J].计算机学报,2018,41(5):1157-1171. [11] GE Weimin,ZHU Haiying,LI Juan.Performance analysis and simulation verification of TCP/NC protocol in wireless network[J].Computer Engineering,2015,41(6):71-75.(in Chinese)葛卫民,朱海颖,李娟.无线网络中TCP/NC协议性能分析与仿真验证[J].计算机工程,2015,41(6):71-75. [12] DENG Yuqiao,YANG Bo,TANG Chunming,et al.Research of ciphertext policy process-based encryption[J].Chinese Journal of Computers,2019,42(5):1063-1075.(in Chinese)邓宇乔,杨波,唐春明,等.基于密文策略的流程加密研究[J].计算机学报,2019,42(5):1063-1075. [13] ZHAO Bo,XIANG Cheng,ZHANG Huanguo.A trusted network connect protocol for resisting man-in-the-middle attack[J].Chinese Journal of Computers,2019,42(5):1137-1148.(in Chinese)赵波,向程,张焕国.一种抵御中间人攻击的可信网络连接协议[J].计算机学报,2019,42(5):1137-1148. [14] GRIOTTI M,GANDINO F,REBAUDENGO M.Mixed public and secret-key cryptography for wireless sensor networks[C]//Proceedings of the 10th International Conference on Mobile Computing and Ubiquitous Network.Washington D.C.,USA:IEEE Press,2017:1-6. [15] SHEIKHI-GARJAN M,BAHRAMIAN M,DOCHE C.Threshold verifiable multi-secret sharing based on elliptic curves and Chinese remainder theorem[J].IET Information Security,2019,13(3):278-284. [16] WANG Ding,WANG Nan,WANG Ping,et al.Preserving privacy for free:efficient and provably secure two-factor authentication scheme with user anonymity[J].Information Sciences,2015,321:162-178. [17] WANG Ding,WANG Ping.Two birds with one stone:two-factor authentication with security beyond conventional bound[J].IEEE Transactions on Dependable and Secure Computing,2018,15(4):708-722. [18] MOHAMMAD Z.Cryptanalysis and improvement of the YAK protocol with formal security proof and security verification via Scyther[J].International Journal of Communication Systems,2020,33(9):121-134. [19] LI Kun,ZHANG Xuesong.Design and formal verification of safety communication protocol in STP[J].Computer Engineering,2018,44(12):120-128.(in Chinese)李堃,张雪松.STP安全通信协议设计与形式化验证[J].计算机工程,2018,44(12):120-128. [20] NIU Leyuan,YANG Yitong,WANG Dejun,et al.Automatic analysis on authentication of SSHV2 protocol in computational model[J].Computer Engineering,2015,41(10):148-154.(in Chinese)牛乐园,杨伊彤,王德军,等.计算模型下的SSHV2协议认证性自动化分析[J].计算机工程,2015,41(10):148-154. [21] HU Chengjun,ZHENG Yuan,SHEN Changxiang.Proving secrecy property of cryptographic protocols[J].Chinese Journal of Computers,2003,26(3):367-372.(in Chinese)胡成军,郑援,沈昌祥.密码协议的秘密性证明[J].计算机学报,2003,26(3):367-372. [22] YOU Zhen,XUE Jinyun.Formal verification of algorithm program based on Isabelle theorem prover[J].Computer Engineering and Science,2009,31(10):85-89.(in Chinese)游珍,薛锦云.基于Isabelle定理证明器算法程序的形式化验证[J].计算机工程与科学,2009,31(10):85-89. [23] WANG Ji,ZHAN Naijun,FENG Xinyu,et al.Overview of formal methods[J].Journal of Software,2019,30(1):33-61.(in Chinese)王戟,詹乃军,冯新宇,等.形式化方法概貌[J].软件学报,2019,30(1):33-61. |