密码协议代码执行的安全验证分析综述
|
摘要
密码协议安全验证分析是信息安全重点研究之一.常用的密码协议安全分析(例如,形式化分析、计算模型分析、计算可靠的形式化分析)只能从理论上验证或证明密码协议的安全,无法确保密码协议代码实际执行的安全.只有当密码协议在代码执行时被验证或证明安全,才能保障密码协议在实现中是安全的.因此,代码级的密码协议安全验证分析是值得关注的方向.文中分别从自动模型提取、代码自动生成、操作语义及程序精化4个方面,综述代码级的密码协议安全验证分析,并对当前代码级的密码协议安全验证分析领域中的最新成果进行详细比较、分析、总结和评论.文中以常用程序语言(C、Java、F#等)编写的密码协议为例,重点阐述密码协议代码执行的安全验证分析,并展望代码级的密码协议安全验证分析的研究方向.
Security verification analysis of cryptographic protocols is one of the most important fields of researching the information security in network.Although common ways to analyze the security of cryptographic protocols(such as formal analysis,computational model analysis,and computational sound formal analysis)can theoretically verify or prove whether cryptographic protocols are secure,they can't guarantee that cryptographic protocols are secure in the process of implementation on real code.However,if cryptographic protocols are verified or proved to be secure during the process of implementation on real code,it can be insured that cryptographic protocols are implemented safely.Therefore,it is worthwhile to focus on the field of researching security verification analysis of cryptographic protocols implemented on real code.In this paper,first of all,we summarize the research status of security verification analysis of cryptographic protocols at home and abroad.Furthermore,we summarize the research status of security verification analysis of cryptographic protocols implemented on real code,and there are four branches:automated model extraction,automated code generation,operational semantics and program refinement.Meanwhile,we compare,analyze,summarize and comment the latest achievements in the research of security verification analysis of cryptographic protocols implemented on real code.Inthis paper,taking common programming languages as examples(such as C,Java,F#,and so on),we carry out the discussion and focus on four kinds of security analysis.Based on classical abstract theories,automated model extraction analyzes the security of a cryptographic protocol by applying an abstract mapping,which maps the properties of a cryptographic protocol from concrete program state space onto a corresponding abstract model.Automated code generation,based on the specifications of a cryptographic protocol,generates the codes automatically and analyzes the security of a cryptographic protocol with these codes.The security analysis of cryptographic protocols implementation on real code which is based on operational semantics analyzes the security of the properties of a cryptographic protocol,such as the sequence of the traces,the match of messages during the process of the implementation of a cryptographic protocol and so on.The program refinement security analysis analyzes the security of a cryptographic protocol by applying the relation of the program refinement.At the end of this paper,we prospect the research direction of security verification analysis of cryptographic protocols implemented on real code in six parts:Model checking techniques(such as program refinement,program verification and so on)are applied to analyze and verify cryptographic protocol implementation on real code;Based on Dolev-Yao model,the security of cryptographic protocols is automatically analyzed and verified on real code;Programming languages(C/C++,Java,F#and so on)are applied to build models or frames(F7,CoSP,Spi2 Java,etc.)in the process of security verification analysis of cryptographic protocols;Security verification analysis of cryptographic protocol implementation on real code is based on semantic security;Computational sound formal analysis is applied to analyze and verify the security of cryptographic protocols implementation on real code;Concurrency security verification analysis of cryptographic protocols implemented on real code is developed.
Security verification analysis of cryptographic protocols is one of the most important fields of researching the information security in network.Although common ways to analyze the security of cryptographic protocols(such as formal analysis,computational model analysis,and computational sound formal analysis)can theoretically verify or prove whether cryptographic protocols are secure,they can't guarantee that cryptographic protocols are secure in the process of implementation on real code.However,if cryptographic protocols are verified or proved to be secure during the process of implementation on real code,it can be insured that cryptographic protocols are implemented safely.Therefore,it is worthwhile to focus on the field of researching security verification analysis of cryptographic protocols implemented on real code.In this paper,first of all,we summarize the research status of security verification analysis of cryptographic protocols at home and abroad.Furthermore,we summarize the research status of security verification analysis of cryptographic protocols implemented on real code,and there are four branches:automated model extraction,automated code generation,operational semantics and program refinement.Meanwhile,we compare,analyze,summarize and comment the latest achievements in the research of security verification analysis of cryptographic protocols implemented on real code.Inthis paper,taking common programming languages as examples(such as C,Java,F#,and so on),we carry out the discussion and focus on four kinds of security analysis.Based on classical abstract theories,automated model extraction analyzes the security of a cryptographic protocol by applying an abstract mapping,which maps the properties of a cryptographic protocol from concrete program state space onto a corresponding abstract model.Automated code generation,based on the specifications of a cryptographic protocol,generates the codes automatically and analyzes the security of a cryptographic protocol with these codes.The security analysis of cryptographic protocols implementation on real code which is based on operational semantics analyzes the security of the properties of a cryptographic protocol,such as the sequence of the traces,the match of messages during the process of the implementation of a cryptographic protocol and so on.The program refinement security analysis analyzes the security of a cryptographic protocol by applying the relation of the program refinement.At the end of this paper,we prospect the research direction of security verification analysis of cryptographic protocols implemented on real code in six parts:Model checking techniques(such as program refinement,program verification and so on)are applied to analyze and verify cryptographic protocol implementation on real code;Based on Dolev-Yao model,the security of cryptographic protocols is automatically analyzed and verified on real code;Programming languages(C/C++,Java,F#and so on)are applied to build models or frames(F7,CoSP,Spi2 Java,etc.)in the process of security verification analysis of cryptographic protocols;Security verification analysis of cryptographic protocol implementation on real code is based on semantic security;Computational sound formal analysis is applied to analyze and verify the security of cryptographic protocols implementation on real code;Concurrency security verification analysis of cryptographic protocols implemented on real code is developed.
引文
[1]Zhang Huan-Guo,Han Wen-Bao,Lai Xue-Jia,et al.Survey on cyberspace security.Science China Information Sciences,2016,46(2):125-164(in Chinese)(张焕国,韩文报,来学嘉等.网络空间安全综述.中国科学:信息科学,2016,46(2):125-164)
[2]Zhang Rui,Xie Rui,Lin Dong-Dai.The vast cloud security architecture.Science China Information Sciences,2015,45(6):796-816(in Chinese)(章睿,薛锐,林东岱.海云安全体系架构.中国科学:信息科学,2015,45(6):796-816)
[3]Feng Deng-Guo,Zhang Min,Li Hao.Big data security and privacy protection.Chinese Journal of Computers,2014,37(1):246-258(in Chinese)(冯登国,张敏,李昊.大数据安全与隐私保护.计算机学报,2014,37(1):246-258)
[4]Cheng Ke-Fei,Weng Jian.Data security and privacy protection in cloud computing environment.Journal of Hangzhou Normal University(Natural Science),2014,13(6):561-571(in Chinese)(陈克非,翁健.云计算环境下数据安全与隐私保护.杭州师范大学学报(自然科学版),2014,13(6):561-571)
[5]Cao Zhen-Fu.New development of cryptography.Journal of Sichuan University(Engineering Science Edition),2015,47(1):1-12(in Chinese)(曹珍富.密码学的新发展.四川大学学报(工程科学版),2015,47(1):1-12)
[6]Lei Xin-Feng,Song Shu-Min,Liu Wei-Bing,Xue Rui.Asurvey on computationally sound formal analysis of cryptographic protocols.Chinese Journal of Computers,2014,37(5):993-1016(in Chinese)(雷新锋,宋书民,刘伟兵,薛锐.计算可靠的密码协议形式化分析综述.计算机学报,2014,37(5):993-1016)
[7]Bhargavan K,Fournet C,Gordon A D,Tse S.Verified interoperable implementations of security protocols.ACMTransactions on Programming Languages and Systems,2008,31(1):1-61
[8]O’Shea N.Verification and Validation of Security Protocol Implementations[Ph.D.dissertation].School of Informatics,University of Edinburgh,UK,2010
[9]Cremers C,Mauw S.Operational Semantics and Verification of Security Protocols.Berlin Heidelberg:Springer-Verlag,2012
[10]Abadi M,Lamport L.The existence of refinement mapping.Theoretical Computer Science,1992,82:253-284
[11]Wei Fu-Shan,Zhang Zhen-Feng,Ma Chuan-Gui.A framework for gateway oriented password authenticated key exchange in the standard mode.Chinese Journal of Computers,2012,35(9):1833-1843(in Chinese)(魏福山,张振峰,马传贵.标准模型下网关口令认证密钥交换协议的通用框架.计算机学报,2012,35(9):1833-1843)
[12]Miao Yin-Bin,Ma Jian-Feng,Liu Zhi-Quan,et al.Verifiable search over encrypted data with variable keyword-field.Journal of Xidian University(Natural Science),2017,44(1):57-63(in Chinese)(苗银宾,马建峰,刘志全等.关键字域可变的可验证密文检索.西安电子科技大学学报(自然科学版),2017,44(1):57-63)
[13]Tang Chao-Jing,Lu Zhi-Yong,Feng Chao.A verification logic for security protocols based on computational semantics.Acta Electronic Sinica,2014,42(6):1179-1185(in Chinese)(唐朝京,鲁智勇,冯超.基于计算语义的安全协议验证逻辑.电子学报,2014,42(6):1179-1185)
[14]Tian Yuan,Wang Ying,Jin Feng,Jin Yue.Non-malleability and emulation bases approach to cryptographic protocol analysis.Chinese Journal of Computers,2009,32(4):618-634(in Chinese)(田园,王颖,金锋,金月.基于刚性与相似性概念的密码协议分析方法.计算机学报,2009,32(4):618-634)
[15]Neddham R M,Schroeder M D.Using encryption for authentication in large networks of computers.Communications of the ACM,1978,21(12):993-999
[16]Dolev D,Yao A C.On the security of public key protocols//Proceedings of the 22nd Symposium on Foundation of Computer Science.Oakland,USA,1981:350-357
[17]Burrows M,Abadi M,Needham R.A logic of authentication.Palo Alto,USA:Digital Equipment Corp.(DEC),Systems Research Center:39,1989
[18]Blu M,Micali S.How to generate cryptographically strong sequences of pseudo random bits//Proceedings of the 23rd Annual Symposium on Foundations of Computer Science.Los Alamitos,USA,1982:112-117
[19]Yao A C.Theory and application of trapdoor functions//Proceedings of the 23rd IEEE Symposium on Foundations of Computer Science.California,USA,1982:80-91
[20]Goldwasser S,Micali S.Probabilistic encryption.Journal of Computer and System Sciences,1984,28(2):270-299
[21]Abadi M,Rogaway P.Reconciling two views of cryptography:The computational soundness of formal encryption.Journal of Cryptology,2002,15(2):103-127
[22]Micciancio D,Warinschi B.Completeness theorems for the abadi-rogaway logic of encrypted expressions.Journal of Computer Security,2004,12(1):99-129
[23]Blanchet B.Computationally sound mechanized proofs of correspondence assertions//Proceedings of the 20th IEEEComputer Security Foundations Symposium.Venice,Italy,2007:97-111
[24]Cortier V,Warinshi B.Computationally sound,automated proofs for security protocol analysis.Logical Methods in Computer Science,2007,3(3):396-458
[25]Backes M,Pfitzman B,Waidner A.A composable cryptographic library with nested operations//Proceedings of the10th ACM Conference of Computer and Communications Security.New York,UK,2003:122-136
[26]Cousot P,Cousot P.Abstract interpretation frameworks.Journal of Logic and Computation,1992,2(4):511-547
[27]Clarke E M,Grumberg O,Long D E.Model checking and abstraction.ACM Transactions on Programming Languages and System,1994,16(5):1512-1542
[28]Goubault-Larrecq J,Parrennes F.Cryptographic protocol analysis on real C code//Proceedings of the International Conference on Verification,Model Checking,and Abstract Interpretation.Paris,France,2005:363-379
[29]Menezes A J,van Oorschot P C,Vanstone S A.Handbook of Applied Cryptography.Florida,USA:CRC Press,1996
[30]Ganesh V,Dill D L.A decision procedure for bit-vectors and arrays//Proceedings of the 19th International Conference on Computer Aided Verification.Berlin,Germany,2007:519-531
[31]Wagner D,Foster J S,Brewer E A,Aiken A.A first step towards automated detection of buffer overrun vulnerabilities//Proceedings of the Network&Distributed Systems Security.San Diego,USA,2000:3-17
[32]Chaki S,Datta A.ASPIER:An automated framework for verifying security protocol implementations//Proceedings of the 22nd IEEE Computer Security Foundations Symposium.Los Alamitos,USA,2009:3-12
[33]Cohen E,Dahlweid M,Hillebrand M,et al.VCC:A practical system for verifying concurrent C//Proceedings of the Theorem Proving in Higher Order Logics,International Conference.Munich,Germany,2009:23-42
[34]Chaki S,Ivers J,Sharygina N,Wallnau K.The ComFoRTreasoning framework//Proceedings of the 17th International Conference on Computer Aided Verification.Scotland,UK,2005:164-169
[35]Dupressoir F,Gordon A D,Jürjens J,Naumann D A.Guiding ageneral-purpose C verifier to prove cryptographic protocols.Journal of Computer Security,2014,22(5):823-866
[36]Necula G C,McPeak S,Rahul S P,Weimer W.CIL:Intermediate language and tools for analysis and transformation of C programs//Proceedings of the 11th International Conference on Compiler Construction.London,UK,2002:213-228
[37]Aizatulin M,Gordon A D,Jürjens J.Extracting and verifying cryptographic models from C protocol code by symbolic execution//Proceedings of the ACM Conference on Computer and Communications Security.Chicago,USA,2011:17-21
[38]Blanchet B,et al.An efficient cryptographic protocol verifier based on Prolog rules//Proceedings of the 14th IEEE Computer Security Foundations Workshop.Cape Breton,Canada,2002:82-96
[39]Aizatulin M,Gordon A D,Jürjens J.Computational verification of C protocol implementations by symbolic execution//Proceedings of the ACM Conference on Computer and Communications Security.Raleigh,North Carolina,USA,2012:16-18
[40]Blanchet B.A computationally sound mechanized prover for security protocols.IEEE Transactions on Dependable and Secure Computing,2007,5(4):193-207
[41]Bhargavan K,Corin R.Cryptographically verified implementations for TLS//Proceedings of the ACM Conference on Computer and Communications Security.Alexandria,USA,2008:27-31
[42]Vanspauwen G,Jacobs B.Verifying protocol implementations by augmenting existing cryptographic libraries with specifications//Proceedings of the Formal Methods-20th International Symposium.Oslo,Norway,2015:53-68
[43]Beurdouche B,Bhargavan K,Delignat-Lavaud A,et al.Amessy state of the union:Taming the composite state machines of TLS//Proceedings of the IEEE Symposium on Security and Privacy.Oakland,USA,2015:535-552
[44]Pullicino K.Jif:Language-based information-flow security in java.https://arxiv.org/pdf/1412.8639,2014
[45]Askarov A,Sabelfeld A.Security-typed languages for implementation of cryptographic protocols:A case study//Proceedings of the European Symposium on Research in Computer Security.Milan,Italy,2005:197-221
[46]Fortune S,Merritt M.Poker Protocols//Proceedings of the Advances in Cryptology.California,USA,1984:454-464
[47]Jürjens J.Using interface specifications for verifying cryptoprotocol implementations//Proceedings of the Foundations of Interface Technologies.Budapest,Hungary,2008:1-15
[48]Bush W R,Pincus J D,Sielaff D J.A static analyzer for finding dynamic programming errors.Software-Practice and Experience,2000,30(7):775-802
[49]Scott Oaks.Java Security.2nd Revised Edition.New York,USA:O′Reilly Media,2001
[50]Jürjens J.Security analysis of crypto-based java programs using automated theorem provers//Proceedings of the 21st IEEE/ACM International Conference on Automated Software Engineering.Tokyo,Japan,2006:167-176
[51]Jürjens J.Automated security verification for crypto protocol implementations.Verifying the Jessie Project Electronic Notes in Theoretical Computer Science,2009,250(1):123-136
[52]Jia L,Sen S,Garg D,Datta A.A logic of programs with interface-confined code//Proceedings of the 28th Computer Security Foundations Symposium.Verona,Italy,2015:512-525
[53]Jia L,Sen S,Garg D,Datta A.System M:A program logic for code sandboxing and identification.arxiv.org/abs/1501.05673,2015
[54]Datta A,Derek A,Mitchell J C,Pavlovic D.A derivation system and compositional logic for security protocols.Journal of Computer Security,2005,13:423-482
[55]Bhargavan K,Fournet C,Corin R,Zlinescu E.Verified cryptographic implementations for TLS.ACM Transactions on Information and System Security,Special Issue on Computer and Communications Security,2012,15(1):1-32
[56]Backes M,Maffei M,Unruh D.Computationally sound verification of source code//Proceedings of the ACM Conference on Computer and Communications Security.Chicago,USA,2010:387-398
[57]Bengtson J,Bhargavan K,et al.Refinement types for secure implementations//Proceedings of the 21st IEEE Security Foundations Symposium.Pennsylvania,USA,2008:17-32
[58]Backes M,Hofheinz D,Unruh D.CoSP:A general framework for computational soundness proofs//Proceedings of the ACMConference on Computer and Communications Security.Chicago,USA,2009:66-78
[59]Backes M,Mohammadi E,Ruffing T.Computational soundness results for ProVerif bridging the gap from trace properties to uniformity//Proceedings of the 3rd Conference on Principles of Security and Trust.Grenoble,France,2014:42-62
[60]Milner R.Communicating and Mobile Systems:Theπ-Calculus.Cabridge:Cabridge University Press,1999
[61]Backes M,Mohammadi E,Ruffing T.Computational soundness for interactive primitives//Proceedings of the European Symposium on Research in Computer Security.Vienna,Austria,2015:125-145
[62]Bengtson J,Bhargavan K,Fournet C,Gordon A D.Modular verification of security protocol code by typing//Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming.Madrid,Spain,2010:17-23
[63]Milner R,Harper R,MacQueen D,Tofte M.The Definition of Standard ML(Revised).Massachusetts,USA:MIT Press,1997
[64]Bangerter E,Camenisch J,Krenn S,et al.Automatic generation of sound zero-knowledge protocols//Proceedings of the European Cryptology Conference Poster Session.Cologne,Germany,2009:471
[65]Meiklejohn S,Erway C C,Küp9üA,et al.ZKPDL:Alanguage-based system for efficient zero-knowledge proofs and electronic cash//Proceedings of the 19th USENIXConference on Security.Washington,USA,2010:193-206
[66]Backes M,Busenius A,Hritcu C.On the Development and Formalization of an Extensible Code Generator for Real Life Security Protocols.Berlin Heidelberg,Germany:Springer,2012,7226:371-387
[67]Kiyomoto S,Ota H,Tanaka T.A security protocol compiler generating C source codes//Proceedings of the International Conference on Information Security and Assurance.Busan,Korea,2008:20-25
[68]Dembinski P,Budkowski S.Specification Language Estelle.Springer International,1998,124(7):9-10
[69]Kohler E,Kaashoek M F,Montgomery D R.A readable TCP in the prolac protocol language.ACM SIGCOMMComputer Communication Review,2000,29(4):3-13
[70]Sidhu D,Chung A,Blumer T P.A Formal Description Technique for Protocol Engineering[Ph.D.dissertation].University of Maryland,College Park,Maryland,USA,1990
[71]Almeida J B,Barbosa M,Bangerter E.Full proof cryptography:Verifiable compilation of efficient zero-knowledge protocols//Proceedings of the ACM Conference on Computer and Communications Security.Raleigh,USA,2012:488-500
[72]Almeida J B,Bangerter E,Barbosa M,et al.A certifying compiler for zero-knowledge proofs of knowledge based onΣ-protocols//Proceedings of the European Symposium on Research in Computer Security.Athens,Greece,2010:151-167
[73]Paulson L.Isabelle:A Generic Theorem Prover.Berlin,Germany:Springer-Verlag,1994
[74]Fournet C,Kohlweiss M,Danezis G,Luo Zhengqin.ZQL:A compiler for privacy-preserving data processing//Proceedings of the 22nd USENIX Security Symposium.Washington,USA,2013:14-16
[75]Song D,Perrig A,Phan D.AGVI-Automatic generation,verification,and implementation of security protocols//Proceedings of the Computer Aided Verification.Paris,France,2102:241-245
[76]Hubbers E,Oostdijk M,Poll E.Implementing a formally verifiable security protocol in java card//Proceedings of the1st International Conference on Security in Pervasive Computing.Boppard,Germany,2013:213-226
[77]Schellhorn G,Banach R.A concept-driven construction of the Mondex protocol using three refinements//Proceedings of the Abstract State Machines,B and Z,First International Conference.London,UK,2008:57-70
[78]Leavens G T,Baker A L,Ruby C.Preliminary design of JML:A behavioral interface specification language for java.ACM SIGSOFT Software Engineering Notes,2006,31(3):1-38
[79]Pozza D,Sisto R,Durante L.Spi2Java:Automatic cryptographic protocol java code generation from spi calculus//Proceedings of the 18th International Conference on Advanced Information Networking and Application.Fukuoka,Japan,2004:400-405
[80]Avalle M,Pironti A,Sisto R,Pozza D.The JavaSPI framework for security protocol implementation//Proceedings of the 6th International Conference on Availability,Reliability and Security.Vienna,Austria,2011:746-751
[81]Grandy H,Bischof M,Stenzel K,et al.Verification of Mondex electronic purses with KIV:From a security protocol to verified code//Proceedings of the 15th International Symposium on Formal Methods.Turku,Finland,2008:165-180
[82]Pironti A,Sisto R.Provably correct java implementations of spi Calculus security protocols specifications.Computers&Security,2010,29:302-314
[83]Pironti A,Pozza D,Sisto R.Formally-based semi-automatic implementation of an open security protocol.Journal of Systems and Software,2012,85(1):835-849
[84]Pironti A.Sound Automatic Implementation Generation and Monitoring of Security Protocol Implementations from Verified Formal Specifications[Ph.D.dissertation].Politecnico di Torino,Torino,Italy,2010
[85]Hahnle R,Heisel M,Reif W,Stephan W.An interactive verification system based on dynamic logic//Proceedings of the International Conference on Automated Deduction.Oxford,England,1986:306-315
[86]Busenius A.Expi2Java:An Extensible Code Generator for Security Protocols[Ph.D.dissertation].Saarland University,Saarland,2008
[87]Cremers C J F.The scyther tool:Verification,falsification and analysis of security protocols//Proceedings of the Computer Aided Verification,20th International Conference.Princeton,USA,2008:414-418
[88]Chomsky N.Three models for the description of language.IRE Transactions on Information Theory,1956,2(3):113-124
[89]Meier S,Schmidt B,Cremers C,Basin D.The TAMARINprover for the symbolic analysis of security protocols//Proceedings of the Computer Aided Verification.Saint Petersburg,Russia,2013:696-701
[90]Schmidt B,Meier S,Cremers C,Basin D.Automated analysis of Diffie-Hellman protocols and advanced security properties//Proceedings of the Computer Security Foundations Symposium.Cambridge,USA,2012:78-94
[91]Cremers C,Horva M,Scott S,van der Merwe T.Automated analysis and verification of TLS 1.3:0-RTT,resumption and delayed authentication//Proceedings of the 2016IEEESymposium on Security and Privacy.San Jose,USA,2016:470-485
[92]Schmidt B,Sasse R,Cremers C,Basin D.Automated verification of group key agreement protocols//Proceedings of the 2014IEEE Symposium on Security and Privacy.California,USA,2014:179-194
[93]Meier S,Cremers C J F,Basin D A,Strong invariants for the efficient construction of machine-checked protocol security proofs//Proceedings of the 23rd IEEE Computer Security Foundations Symposium.Edinburgh,UK,2010:231-245
[94]Armando A,Arsac W,Avanesov T,et al.The AVA-NTSSAR platform for the automated validation of trust and security of service-oriented architectures//Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems.Tallinn,Estonia,2012:267-282
[95]Wang Ting,Chen Tie-Ming,Liu Yang.Refinement checking based on simulation relations.Journal of Software,2016,27(3):580-592(in Chinese)(王婷,陈铁明,刘杨.基于模拟关系的精化检测方法.软件学报,2016,27(3):580-592)
[96]Liang Hong-Jing.Refinement Verification of Concurrent Programs and Its Applications[Ph.D.dissertation].University of Science and Technology of China,Hefei,2014(in Chinese)(梁红瑾.并发程序精化验证及其应用[博士学位论文].中国科技大学,合肥,2014)
[97]Avalle M,Pironti A,Sisto R.Formal verification of security protocol implementations:A survey.Formal Aspects of Computing,2014,26(1):99-123
[98]Gibson-Robinson T,Armstrong P,Boulgakov A,Roscoe A W.FDR3:A modern refinement checker for CSP//Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems.Grenoble,France,2014:187-201
[99]Sun J,Liu Y,Dong J S,Pang J.PAT:Towards flexible verification under fairness//Proceedings of the 21st International Conference on Computer Aided Verification.Grenoble,France,2009:709-714
[100]Hoare C A R.Communicating sequential processes.Communications of the ACM,1978,21(8):666-677
[101]Roscoe A W.CSP and determinism in security modelling//Proceedings of the IEEE Symposium on Security and Privacy.Oakland,USA,1995:114-127
[102]Lowe G.Casper:A compiler for the analysis of security protocols.Journal of Computer Security,1998,6(2):18-30
[103]Roscoe A W,Hopkins D.SVA:A tool for analysing shared-variable programs.Proceedings of AVoCS,2007,4(1):14-25
[104]Gibson-Robinson T,Armstrong P,Boulgakov A,Roscoe A W.FDR3:A parallel refinement checker for CSP.International Journal on Software Tools for Technology Transfer,2016,18(2):149-167
[105]Liu Yang,Sun Jun,Dong Jin-Song.PAT 3:An extensible architecture for building multi-domain model checkers//Proceedings of the 22nd IEEE International Symposium on Software Reliability Engineering.Hiroshima,Japan.2011:190-199
[106]Neis G,Hur C-K.Pilsner:A compositionally verified compiler for a higher-order imperative language.ACMSIGPLAN Notices,2015,50(9):166-178
[107]Laud P,Randmets J.A domain-specific language for lowlevel secure multiparty computation protocols//Proceedings of the ACM Conference on Computer and Communications Security.Denver,Colorado,USA,2015:12-16
[108]Bieber P,Cuppens N B.Formal development of authentication protocols//Proceedings of the 6th Refinement Workshop.London,UK,1994:5-7
[109]Morgan C.The Shadow Knows:Refinement and security in sequential programs.Science of Computer Programming,2009,74:629-653
[110]Barthe G,Fournet C,Grégoire B.Probabilistic relational verification for cryptographic implementations//Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages.San Diego,USA,2014:22-24
[111]Sprenger C,Basin D.Refining key establishment//Proceedings of the IEEE 25th Computer Security Foundations Symposium.Cambridge,USA,2012:230-246
[112]Sprenger C,Basin D.Developing security protocols by refinement//Proceedings of the ACM Conference on Computer and Communications Security.Chicago,USA,2010:361-374
[113]Narendra Kumar N V,Shyamasundar R K.POSTER:Dynamic labelling for analyzing security protocols//Proceedings of the ACM Conference on Computer and Communications Security.Denver,USA,2015:12-16
[114]McIver A K.Program refinement,perfect secrecy and information flow.Engineering Trustworthy Software Systems,2016,9506:80-102
[115]Costanzo D,Shao Zhong,Gu Ronghui.End-to-end verification of information-flow security for C and assembly programs//Proceedings of the ACM SIGPLAN Symposium on Programming Language Design&Implementation.Santa Barbara,USA,2016:13-17
[116]Shmatikov V,Mitchell J C.Finite-state analysis of two contract signing protocols.Theoretical Computer Science,2002,283:419-450
[117]Yao A C-C,Yung Moti,Zhao Yunlei.Concurrent knowledge extraction in public-key models.Journal of Cryptology,2016,29(1):156-219
(1)TamarinManual,http://tamarin-prover.github.io/manual
[2]Zhang Rui,Xie Rui,Lin Dong-Dai.The vast cloud security architecture.Science China Information Sciences,2015,45(6):796-816(in Chinese)(章睿,薛锐,林东岱.海云安全体系架构.中国科学:信息科学,2015,45(6):796-816)
[3]Feng Deng-Guo,Zhang Min,Li Hao.Big data security and privacy protection.Chinese Journal of Computers,2014,37(1):246-258(in Chinese)(冯登国,张敏,李昊.大数据安全与隐私保护.计算机学报,2014,37(1):246-258)
[4]Cheng Ke-Fei,Weng Jian.Data security and privacy protection in cloud computing environment.Journal of Hangzhou Normal University(Natural Science),2014,13(6):561-571(in Chinese)(陈克非,翁健.云计算环境下数据安全与隐私保护.杭州师范大学学报(自然科学版),2014,13(6):561-571)
[5]Cao Zhen-Fu.New development of cryptography.Journal of Sichuan University(Engineering Science Edition),2015,47(1):1-12(in Chinese)(曹珍富.密码学的新发展.四川大学学报(工程科学版),2015,47(1):1-12)
[6]Lei Xin-Feng,Song Shu-Min,Liu Wei-Bing,Xue Rui.Asurvey on computationally sound formal analysis of cryptographic protocols.Chinese Journal of Computers,2014,37(5):993-1016(in Chinese)(雷新锋,宋书民,刘伟兵,薛锐.计算可靠的密码协议形式化分析综述.计算机学报,2014,37(5):993-1016)
[7]Bhargavan K,Fournet C,Gordon A D,Tse S.Verified interoperable implementations of security protocols.ACMTransactions on Programming Languages and Systems,2008,31(1):1-61
[8]O’Shea N.Verification and Validation of Security Protocol Implementations[Ph.D.dissertation].School of Informatics,University of Edinburgh,UK,2010
[9]Cremers C,Mauw S.Operational Semantics and Verification of Security Protocols.Berlin Heidelberg:Springer-Verlag,2012
[10]Abadi M,Lamport L.The existence of refinement mapping.Theoretical Computer Science,1992,82:253-284
[11]Wei Fu-Shan,Zhang Zhen-Feng,Ma Chuan-Gui.A framework for gateway oriented password authenticated key exchange in the standard mode.Chinese Journal of Computers,2012,35(9):1833-1843(in Chinese)(魏福山,张振峰,马传贵.标准模型下网关口令认证密钥交换协议的通用框架.计算机学报,2012,35(9):1833-1843)
[12]Miao Yin-Bin,Ma Jian-Feng,Liu Zhi-Quan,et al.Verifiable search over encrypted data with variable keyword-field.Journal of Xidian University(Natural Science),2017,44(1):57-63(in Chinese)(苗银宾,马建峰,刘志全等.关键字域可变的可验证密文检索.西安电子科技大学学报(自然科学版),2017,44(1):57-63)
[13]Tang Chao-Jing,Lu Zhi-Yong,Feng Chao.A verification logic for security protocols based on computational semantics.Acta Electronic Sinica,2014,42(6):1179-1185(in Chinese)(唐朝京,鲁智勇,冯超.基于计算语义的安全协议验证逻辑.电子学报,2014,42(6):1179-1185)
[14]Tian Yuan,Wang Ying,Jin Feng,Jin Yue.Non-malleability and emulation bases approach to cryptographic protocol analysis.Chinese Journal of Computers,2009,32(4):618-634(in Chinese)(田园,王颖,金锋,金月.基于刚性与相似性概念的密码协议分析方法.计算机学报,2009,32(4):618-634)
[15]Neddham R M,Schroeder M D.Using encryption for authentication in large networks of computers.Communications of the ACM,1978,21(12):993-999
[16]Dolev D,Yao A C.On the security of public key protocols//Proceedings of the 22nd Symposium on Foundation of Computer Science.Oakland,USA,1981:350-357
[17]Burrows M,Abadi M,Needham R.A logic of authentication.Palo Alto,USA:Digital Equipment Corp.(DEC),Systems Research Center:39,1989
[18]Blu M,Micali S.How to generate cryptographically strong sequences of pseudo random bits//Proceedings of the 23rd Annual Symposium on Foundations of Computer Science.Los Alamitos,USA,1982:112-117
[19]Yao A C.Theory and application of trapdoor functions//Proceedings of the 23rd IEEE Symposium on Foundations of Computer Science.California,USA,1982:80-91
[20]Goldwasser S,Micali S.Probabilistic encryption.Journal of Computer and System Sciences,1984,28(2):270-299
[21]Abadi M,Rogaway P.Reconciling two views of cryptography:The computational soundness of formal encryption.Journal of Cryptology,2002,15(2):103-127
[22]Micciancio D,Warinschi B.Completeness theorems for the abadi-rogaway logic of encrypted expressions.Journal of Computer Security,2004,12(1):99-129
[23]Blanchet B.Computationally sound mechanized proofs of correspondence assertions//Proceedings of the 20th IEEEComputer Security Foundations Symposium.Venice,Italy,2007:97-111
[24]Cortier V,Warinshi B.Computationally sound,automated proofs for security protocol analysis.Logical Methods in Computer Science,2007,3(3):396-458
[25]Backes M,Pfitzman B,Waidner A.A composable cryptographic library with nested operations//Proceedings of the10th ACM Conference of Computer and Communications Security.New York,UK,2003:122-136
[26]Cousot P,Cousot P.Abstract interpretation frameworks.Journal of Logic and Computation,1992,2(4):511-547
[27]Clarke E M,Grumberg O,Long D E.Model checking and abstraction.ACM Transactions on Programming Languages and System,1994,16(5):1512-1542
[28]Goubault-Larrecq J,Parrennes F.Cryptographic protocol analysis on real C code//Proceedings of the International Conference on Verification,Model Checking,and Abstract Interpretation.Paris,France,2005:363-379
[29]Menezes A J,van Oorschot P C,Vanstone S A.Handbook of Applied Cryptography.Florida,USA:CRC Press,1996
[30]Ganesh V,Dill D L.A decision procedure for bit-vectors and arrays//Proceedings of the 19th International Conference on Computer Aided Verification.Berlin,Germany,2007:519-531
[31]Wagner D,Foster J S,Brewer E A,Aiken A.A first step towards automated detection of buffer overrun vulnerabilities//Proceedings of the Network&Distributed Systems Security.San Diego,USA,2000:3-17
[32]Chaki S,Datta A.ASPIER:An automated framework for verifying security protocol implementations//Proceedings of the 22nd IEEE Computer Security Foundations Symposium.Los Alamitos,USA,2009:3-12
[33]Cohen E,Dahlweid M,Hillebrand M,et al.VCC:A practical system for verifying concurrent C//Proceedings of the Theorem Proving in Higher Order Logics,International Conference.Munich,Germany,2009:23-42
[34]Chaki S,Ivers J,Sharygina N,Wallnau K.The ComFoRTreasoning framework//Proceedings of the 17th International Conference on Computer Aided Verification.Scotland,UK,2005:164-169
[35]Dupressoir F,Gordon A D,Jürjens J,Naumann D A.Guiding ageneral-purpose C verifier to prove cryptographic protocols.Journal of Computer Security,2014,22(5):823-866
[36]Necula G C,McPeak S,Rahul S P,Weimer W.CIL:Intermediate language and tools for analysis and transformation of C programs//Proceedings of the 11th International Conference on Compiler Construction.London,UK,2002:213-228
[37]Aizatulin M,Gordon A D,Jürjens J.Extracting and verifying cryptographic models from C protocol code by symbolic execution//Proceedings of the ACM Conference on Computer and Communications Security.Chicago,USA,2011:17-21
[38]Blanchet B,et al.An efficient cryptographic protocol verifier based on Prolog rules//Proceedings of the 14th IEEE Computer Security Foundations Workshop.Cape Breton,Canada,2002:82-96
[39]Aizatulin M,Gordon A D,Jürjens J.Computational verification of C protocol implementations by symbolic execution//Proceedings of the ACM Conference on Computer and Communications Security.Raleigh,North Carolina,USA,2012:16-18
[40]Blanchet B.A computationally sound mechanized prover for security protocols.IEEE Transactions on Dependable and Secure Computing,2007,5(4):193-207
[41]Bhargavan K,Corin R.Cryptographically verified implementations for TLS//Proceedings of the ACM Conference on Computer and Communications Security.Alexandria,USA,2008:27-31
[42]Vanspauwen G,Jacobs B.Verifying protocol implementations by augmenting existing cryptographic libraries with specifications//Proceedings of the Formal Methods-20th International Symposium.Oslo,Norway,2015:53-68
[43]Beurdouche B,Bhargavan K,Delignat-Lavaud A,et al.Amessy state of the union:Taming the composite state machines of TLS//Proceedings of the IEEE Symposium on Security and Privacy.Oakland,USA,2015:535-552
[44]Pullicino K.Jif:Language-based information-flow security in java.https://arxiv.org/pdf/1412.8639,2014
[45]Askarov A,Sabelfeld A.Security-typed languages for implementation of cryptographic protocols:A case study//Proceedings of the European Symposium on Research in Computer Security.Milan,Italy,2005:197-221
[46]Fortune S,Merritt M.Poker Protocols//Proceedings of the Advances in Cryptology.California,USA,1984:454-464
[47]Jürjens J.Using interface specifications for verifying cryptoprotocol implementations//Proceedings of the Foundations of Interface Technologies.Budapest,Hungary,2008:1-15
[48]Bush W R,Pincus J D,Sielaff D J.A static analyzer for finding dynamic programming errors.Software-Practice and Experience,2000,30(7):775-802
[49]Scott Oaks.Java Security.2nd Revised Edition.New York,USA:O′Reilly Media,2001
[50]Jürjens J.Security analysis of crypto-based java programs using automated theorem provers//Proceedings of the 21st IEEE/ACM International Conference on Automated Software Engineering.Tokyo,Japan,2006:167-176
[51]Jürjens J.Automated security verification for crypto protocol implementations.Verifying the Jessie Project Electronic Notes in Theoretical Computer Science,2009,250(1):123-136
[52]Jia L,Sen S,Garg D,Datta A.A logic of programs with interface-confined code//Proceedings of the 28th Computer Security Foundations Symposium.Verona,Italy,2015:512-525
[53]Jia L,Sen S,Garg D,Datta A.System M:A program logic for code sandboxing and identification.arxiv.org/abs/1501.05673,2015
[54]Datta A,Derek A,Mitchell J C,Pavlovic D.A derivation system and compositional logic for security protocols.Journal of Computer Security,2005,13:423-482
[55]Bhargavan K,Fournet C,Corin R,Zlinescu E.Verified cryptographic implementations for TLS.ACM Transactions on Information and System Security,Special Issue on Computer and Communications Security,2012,15(1):1-32
[56]Backes M,Maffei M,Unruh D.Computationally sound verification of source code//Proceedings of the ACM Conference on Computer and Communications Security.Chicago,USA,2010:387-398
[57]Bengtson J,Bhargavan K,et al.Refinement types for secure implementations//Proceedings of the 21st IEEE Security Foundations Symposium.Pennsylvania,USA,2008:17-32
[58]Backes M,Hofheinz D,Unruh D.CoSP:A general framework for computational soundness proofs//Proceedings of the ACMConference on Computer and Communications Security.Chicago,USA,2009:66-78
[59]Backes M,Mohammadi E,Ruffing T.Computational soundness results for ProVerif bridging the gap from trace properties to uniformity//Proceedings of the 3rd Conference on Principles of Security and Trust.Grenoble,France,2014:42-62
[60]Milner R.Communicating and Mobile Systems:Theπ-Calculus.Cabridge:Cabridge University Press,1999
[61]Backes M,Mohammadi E,Ruffing T.Computational soundness for interactive primitives//Proceedings of the European Symposium on Research in Computer Security.Vienna,Austria,2015:125-145
[62]Bengtson J,Bhargavan K,Fournet C,Gordon A D.Modular verification of security protocol code by typing//Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming.Madrid,Spain,2010:17-23
[63]Milner R,Harper R,MacQueen D,Tofte M.The Definition of Standard ML(Revised).Massachusetts,USA:MIT Press,1997
[64]Bangerter E,Camenisch J,Krenn S,et al.Automatic generation of sound zero-knowledge protocols//Proceedings of the European Cryptology Conference Poster Session.Cologne,Germany,2009:471
[65]Meiklejohn S,Erway C C,Küp9üA,et al.ZKPDL:Alanguage-based system for efficient zero-knowledge proofs and electronic cash//Proceedings of the 19th USENIXConference on Security.Washington,USA,2010:193-206
[66]Backes M,Busenius A,Hritcu C.On the Development and Formalization of an Extensible Code Generator for Real Life Security Protocols.Berlin Heidelberg,Germany:Springer,2012,7226:371-387
[67]Kiyomoto S,Ota H,Tanaka T.A security protocol compiler generating C source codes//Proceedings of the International Conference on Information Security and Assurance.Busan,Korea,2008:20-25
[68]Dembinski P,Budkowski S.Specification Language Estelle.Springer International,1998,124(7):9-10
[69]Kohler E,Kaashoek M F,Montgomery D R.A readable TCP in the prolac protocol language.ACM SIGCOMMComputer Communication Review,2000,29(4):3-13
[70]Sidhu D,Chung A,Blumer T P.A Formal Description Technique for Protocol Engineering[Ph.D.dissertation].University of Maryland,College Park,Maryland,USA,1990
[71]Almeida J B,Barbosa M,Bangerter E.Full proof cryptography:Verifiable compilation of efficient zero-knowledge protocols//Proceedings of the ACM Conference on Computer and Communications Security.Raleigh,USA,2012:488-500
[72]Almeida J B,Bangerter E,Barbosa M,et al.A certifying compiler for zero-knowledge proofs of knowledge based onΣ-protocols//Proceedings of the European Symposium on Research in Computer Security.Athens,Greece,2010:151-167
[73]Paulson L.Isabelle:A Generic Theorem Prover.Berlin,Germany:Springer-Verlag,1994
[74]Fournet C,Kohlweiss M,Danezis G,Luo Zhengqin.ZQL:A compiler for privacy-preserving data processing//Proceedings of the 22nd USENIX Security Symposium.Washington,USA,2013:14-16
[75]Song D,Perrig A,Phan D.AGVI-Automatic generation,verification,and implementation of security protocols//Proceedings of the Computer Aided Verification.Paris,France,2102:241-245
[76]Hubbers E,Oostdijk M,Poll E.Implementing a formally verifiable security protocol in java card//Proceedings of the1st International Conference on Security in Pervasive Computing.Boppard,Germany,2013:213-226
[77]Schellhorn G,Banach R.A concept-driven construction of the Mondex protocol using three refinements//Proceedings of the Abstract State Machines,B and Z,First International Conference.London,UK,2008:57-70
[78]Leavens G T,Baker A L,Ruby C.Preliminary design of JML:A behavioral interface specification language for java.ACM SIGSOFT Software Engineering Notes,2006,31(3):1-38
[79]Pozza D,Sisto R,Durante L.Spi2Java:Automatic cryptographic protocol java code generation from spi calculus//Proceedings of the 18th International Conference on Advanced Information Networking and Application.Fukuoka,Japan,2004:400-405
[80]Avalle M,Pironti A,Sisto R,Pozza D.The JavaSPI framework for security protocol implementation//Proceedings of the 6th International Conference on Availability,Reliability and Security.Vienna,Austria,2011:746-751
[81]Grandy H,Bischof M,Stenzel K,et al.Verification of Mondex electronic purses with KIV:From a security protocol to verified code//Proceedings of the 15th International Symposium on Formal Methods.Turku,Finland,2008:165-180
[82]Pironti A,Sisto R.Provably correct java implementations of spi Calculus security protocols specifications.Computers&Security,2010,29:302-314
[83]Pironti A,Pozza D,Sisto R.Formally-based semi-automatic implementation of an open security protocol.Journal of Systems and Software,2012,85(1):835-849
[84]Pironti A.Sound Automatic Implementation Generation and Monitoring of Security Protocol Implementations from Verified Formal Specifications[Ph.D.dissertation].Politecnico di Torino,Torino,Italy,2010
[85]Hahnle R,Heisel M,Reif W,Stephan W.An interactive verification system based on dynamic logic//Proceedings of the International Conference on Automated Deduction.Oxford,England,1986:306-315
[86]Busenius A.Expi2Java:An Extensible Code Generator for Security Protocols[Ph.D.dissertation].Saarland University,Saarland,2008
[87]Cremers C J F.The scyther tool:Verification,falsification and analysis of security protocols//Proceedings of the Computer Aided Verification,20th International Conference.Princeton,USA,2008:414-418
[88]Chomsky N.Three models for the description of language.IRE Transactions on Information Theory,1956,2(3):113-124
[89]Meier S,Schmidt B,Cremers C,Basin D.The TAMARINprover for the symbolic analysis of security protocols//Proceedings of the Computer Aided Verification.Saint Petersburg,Russia,2013:696-701
[90]Schmidt B,Meier S,Cremers C,Basin D.Automated analysis of Diffie-Hellman protocols and advanced security properties//Proceedings of the Computer Security Foundations Symposium.Cambridge,USA,2012:78-94
[91]Cremers C,Horva M,Scott S,van der Merwe T.Automated analysis and verification of TLS 1.3:0-RTT,resumption and delayed authentication//Proceedings of the 2016IEEESymposium on Security and Privacy.San Jose,USA,2016:470-485
[92]Schmidt B,Sasse R,Cremers C,Basin D.Automated verification of group key agreement protocols//Proceedings of the 2014IEEE Symposium on Security and Privacy.California,USA,2014:179-194
[93]Meier S,Cremers C J F,Basin D A,Strong invariants for the efficient construction of machine-checked protocol security proofs//Proceedings of the 23rd IEEE Computer Security Foundations Symposium.Edinburgh,UK,2010:231-245
[94]Armando A,Arsac W,Avanesov T,et al.The AVA-NTSSAR platform for the automated validation of trust and security of service-oriented architectures//Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems.Tallinn,Estonia,2012:267-282
[95]Wang Ting,Chen Tie-Ming,Liu Yang.Refinement checking based on simulation relations.Journal of Software,2016,27(3):580-592(in Chinese)(王婷,陈铁明,刘杨.基于模拟关系的精化检测方法.软件学报,2016,27(3):580-592)
[96]Liang Hong-Jing.Refinement Verification of Concurrent Programs and Its Applications[Ph.D.dissertation].University of Science and Technology of China,Hefei,2014(in Chinese)(梁红瑾.并发程序精化验证及其应用[博士学位论文].中国科技大学,合肥,2014)
[97]Avalle M,Pironti A,Sisto R.Formal verification of security protocol implementations:A survey.Formal Aspects of Computing,2014,26(1):99-123
[98]Gibson-Robinson T,Armstrong P,Boulgakov A,Roscoe A W.FDR3:A modern refinement checker for CSP//Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems.Grenoble,France,2014:187-201
[99]Sun J,Liu Y,Dong J S,Pang J.PAT:Towards flexible verification under fairness//Proceedings of the 21st International Conference on Computer Aided Verification.Grenoble,France,2009:709-714
[100]Hoare C A R.Communicating sequential processes.Communications of the ACM,1978,21(8):666-677
[101]Roscoe A W.CSP and determinism in security modelling//Proceedings of the IEEE Symposium on Security and Privacy.Oakland,USA,1995:114-127
[102]Lowe G.Casper:A compiler for the analysis of security protocols.Journal of Computer Security,1998,6(2):18-30
[103]Roscoe A W,Hopkins D.SVA:A tool for analysing shared-variable programs.Proceedings of AVoCS,2007,4(1):14-25
[104]Gibson-Robinson T,Armstrong P,Boulgakov A,Roscoe A W.FDR3:A parallel refinement checker for CSP.International Journal on Software Tools for Technology Transfer,2016,18(2):149-167
[105]Liu Yang,Sun Jun,Dong Jin-Song.PAT 3:An extensible architecture for building multi-domain model checkers//Proceedings of the 22nd IEEE International Symposium on Software Reliability Engineering.Hiroshima,Japan.2011:190-199
[106]Neis G,Hur C-K.Pilsner:A compositionally verified compiler for a higher-order imperative language.ACMSIGPLAN Notices,2015,50(9):166-178
[107]Laud P,Randmets J.A domain-specific language for lowlevel secure multiparty computation protocols//Proceedings of the ACM Conference on Computer and Communications Security.Denver,Colorado,USA,2015:12-16
[108]Bieber P,Cuppens N B.Formal development of authentication protocols//Proceedings of the 6th Refinement Workshop.London,UK,1994:5-7
[109]Morgan C.The Shadow Knows:Refinement and security in sequential programs.Science of Computer Programming,2009,74:629-653
[110]Barthe G,Fournet C,Grégoire B.Probabilistic relational verification for cryptographic implementations//Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages.San Diego,USA,2014:22-24
[111]Sprenger C,Basin D.Refining key establishment//Proceedings of the IEEE 25th Computer Security Foundations Symposium.Cambridge,USA,2012:230-246
[112]Sprenger C,Basin D.Developing security protocols by refinement//Proceedings of the ACM Conference on Computer and Communications Security.Chicago,USA,2010:361-374
[113]Narendra Kumar N V,Shyamasundar R K.POSTER:Dynamic labelling for analyzing security protocols//Proceedings of the ACM Conference on Computer and Communications Security.Denver,USA,2015:12-16
[114]McIver A K.Program refinement,perfect secrecy and information flow.Engineering Trustworthy Software Systems,2016,9506:80-102
[115]Costanzo D,Shao Zhong,Gu Ronghui.End-to-end verification of information-flow security for C and assembly programs//Proceedings of the ACM SIGPLAN Symposium on Programming Language Design&Implementation.Santa Barbara,USA,2016:13-17
[116]Shmatikov V,Mitchell J C.Finite-state analysis of two contract signing protocols.Theoretical Computer Science,2002,283:419-450
[117]Yao A C-C,Yung Moti,Zhao Yunlei.Concurrent knowledge extraction in public-key models.Journal of Cryptology,2016,29(1):156-219
(1)TamarinManual,http://tamarin-prover.github.io/manual