{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,15]],"date-time":"2026-07-15T16:46:49Z","timestamp":1784134009502,"version":"3.55.0"},"reference-count":89,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2014,1]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Automated formal verification of security protocols has been mostly focused on analyzing high-level abstract models which, however, are significantly different from real protocol implementations written in programming languages. Recently, some researchers have started investigating techniques that bring automated formal proofs closer to real implementations. This paper surveys these attempts, focusing on approaches that target the application code that implements protocol logic, rather than the libraries that implement cryptography. According to these approaches, libraries are assumed to correctly implement some models. The aim is to derive formal proofs that, under this assumption, give assurance about the application code that implements the protocol logic. The two main approaches of model extraction and code generation are presented, along with the main techniques adopted for each approach.<\/jats:p>","DOI":"10.1007\/s00165-012-0269-9","type":"journal-article","created":{"date-parts":[[2012,12,3]],"date-time":"2012-12-03T18:19:57Z","timestamp":1354558797000},"page":"99-123","source":"Crossref","is-referenced-by-count":53,"title":["Formal verification of security protocol implementations: a survey"],"prefix":"10.1145","volume":"26","author":[{"given":"Matteo","family":"Avalle","sequence":"first","affiliation":[{"name":"Dipartimento di Automatica e Informatica, Politecnico di Torino, Corso Duca degli Abruzzi, 24, 10129, Torino, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Alfredo","family":"Pironti","sequence":"additional","affiliation":[{"name":"Prosecco, INRIA, Paris-Rocquencourt, 23, Avenue d\u2019Italie, 75013, Paris, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Riccardo","family":"Sisto","sequence":"additional","affiliation":[{"name":"Dipartimento di Automatica e Informatica, Politecnico di Torino, Corso Duca degli Abruzzi, 24, 10129, Torino, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Almeida J Bangerter E Barbosa M Krenn S Sadeghi A-R Schneider T (2010) A certifying compiler for zero-knowledge proofs of knowledge based on \u03c3-protocols. In: 15th European symposium on research in computer security (ESORICS) pp 151\u2013167","DOI":"10.1007\/978-3-642-15497-3_10"},{"issue":"1","key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/j.jlap.2007.06.002","article-title":"Automated verification of selected equivalences for security protocols","volume":"75","author":"Abadi M","year":"2008","journal-title":"J Logic Algebr Progr"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Mart\u00edn Abadi C\u00e9dric Fournet (2001) Mobile values new names and secure communication. In: 28th ACM SIGPLAN-SIGACT symposium on principles of programming languages (POPL) pp 104\u2013115","DOI":"10.1145\/373243.360213"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Abadi M Gordon AD (1998) A calculus for cryptographic protocols: The spi calculus. Technical report Digital System Research Center Report 149","DOI":"10.1145\/266420.266432"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Aizatulin M Gordon AD J\u00fcrjens J (2011) Extracting and verifying cryptographic models from C protocol code by symbolic execution. In: 18th ACM conference on computer and communications security (CCS) pp 331\u2013340","DOI":"10.1145\/2046707.2046745"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Aizatulin M Gordon AD J\u00fcrjens J (2012) Computational verification of C protocol implementations by symbolic execution. In: 19th ACM conference on computer and communications security (CCS) (To appear)","DOI":"10.1145\/2382196.2382271"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.481513"},{"issue":"2","key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","first-page":"8","DOI":"10.1145\/2240276.2240279","article-title":"On protection by layout randomization","volume":"15","author":"Abadi M","year":"2012","journal-title":"ACM Trans Inf Syst Secur"},{"key":"e_1_2_1_2_9_2","unstructured":"AlFardan NJ Paterson K (2012) Plaintext-recovery attacks against datagram TLS. In: Network and distributed system security symposium (NDSS)"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"publisher","DOI":"10.4018\/jsse.2011100103"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Albrecht MR Paterson KG Watson GJ (2009) Plaintext recovery attacks against SSH. In: 30th IEEE symposium on security and privacy pp 16\u201326","DOI":"10.1109\/SP.2009.5"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00145-001-0014-7"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Askarov A Sabelfeld A (2005) Security-typed languages for implementation of cryptographic protocols: a case study. In: 10th European symposium on research in computer security (ESORICS) pp 197\u2013221","DOI":"10.1007\/11555827_12"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/1890028.1890031"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Backes M Busenius A Hritcu C (2012) On the development and formalization of an extensible code generator for real life security protocols. In: NASA Formal Methods Symposium (NFM) pp 371\u2013387","DOI":"10.1007\/978-3-642-28891-3_34"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Bertot Y Cast\u00e9ran P (2004) Interactive theorem proving and program development. Coq\u2019Art: the calculus of inductive constructions. Texts in theoretical computer science. Springer Berlin","DOI":"10.1007\/978-3-662-07964-5"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Bhargavan K Corin R Fournet C Z\u0103linescu E (2008) Cryptographically verified implementations for TLS. In: 15th ACM conference on computer and communications security (CCS) pp 459\u2013468","DOI":"10.1145\/1455770.1455828"},{"key":"e_1_2_1_2_18_2","unstructured":"Bangerter E Camenisch J Krenn S Sadeghi A-R Schneider T (2008) Automatic generation of sound zero-knowledge protocols. Technical report Cryptology ePrint Archive Report 2008\/471"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"Bhargavan K Corin R Deni\u00e9lou P-M Fournet C Leifer JJ (2009) Cryptographic protocol synthesis and verification for multiparty sessions. In: 22nd IEEE symposium on computer security foundations (CSF) pp 124\u2013140","DOI":"10.1109\/CSF.2009.26"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Bhargavan K Fournet C Gordon AD (2006) Verified reference implementations of WS-security protocols. In: 3rd International Workshop on Web Services and Formal Methods (WS-FM) pp 88\u2013106","DOI":"10.1007\/11841197_6"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Bhargavan K Fournet C Guts N (2010) Typechecking higher-order security libraries. In: 8th Asian conference on programming languages and systems (APLAS) pp 47\u201362","DOI":"10.1007\/978-3-642-17164-2_5"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"Bhargavan K Fournet C Gordon AD Swamy N (2008) Verified implementations of the information card federated identity-management protocol. In: ACM symposium on information computer and communications security (ASIA CCS) pp 123\u2013135","DOI":"10.1145\/1368310.1368330"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/1452044.1452049"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.cose.2009.09.003"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/bxq042"},{"key":"e_1_2_1_2_26_2","unstructured":"Bangerter E Krenn S Sadeghi A-R Schneider T (2010) YACZK: yet another compiler for zero-knowledge. USENIX Security Symposium Posters"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Blanchet B (2001) An efficient cryptographic protocol verifier based on prolog rules. In: 14th IEEE computer security foundations workshop (CSFW) pp 82\u201396","DOI":"10.1109\/CSFW.2001.930138"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"Backes M Maffei M Unruh D (2010) Computationally sound verification of source code. In: 17th ACM conference on computer and communications security (CCS) pp 387\u2013398","DOI":"10.1145\/1866307.1866351"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"Blanchet B Pointcheval D (2006) Automated security proofs with sequences of games. In: 26th international conference on advances in cryptology (CRYPTO) pp 537\u2013554","DOI":"10.1007\/11818175_32"},{"key":"e_1_2_1_2_30_2","unstructured":"Bierman G Parkinson M Pitts A (2003) MJ: an imperative core calculus for Java and Java with effects. Technical report Cambridge University Computer Laboratory Report 563"},{"key":"e_1_2_1_2_31_2","unstructured":"Busenius A (2011) Mechanized formalization of a transformation from an extensible spi calculus to Java. Master\u2019s thesis Saarland University (Germany). Available at http:\/\/www.infsec.cs.uni-sb.de\/~hritcu\/students\/busenius\/masters_thesis.pdf"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"crossref","unstructured":"Carlsen U (1994) Cryptographic protocol flaws: know your enemy. In: 7th computer security foundations workshop (CSFW) pp 192\u2013200","DOI":"10.1109\/CSFW.1994.315934"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"crossref","unstructured":"Cad\u00e9 D Blanchet B (2012) From computationally-proved protocol specifications to implementations. In: 7th international conference on availability reliability and security (ARES) pp 65\u201374","DOI":"10.1109\/ARES.2012.63"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"crossref","unstructured":"Chaki S Datta A (2009) ASPIER: an automated framework for verifying security protocol implementations. In: 22nd IEEE symposium on computer security foundations (CSF) pp 172\u2013185","DOI":"10.1109\/CSF.2009.20"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/186025.186051"},{"key":"e_1_2_1_2_36_2","unstructured":"Choi J-Y Jeon C-W Kim I-G (2005) Automatic generation of the C# code for security protocols verified with Casper\/FDR. In: 19th international conference on advanced information networking and applications (AINA) pp 507\u2013510"},{"issue":"1","key":"e_1_2_1_2_37_2","first-page":"225","article-title":"A survey of symbolic methods in computational analysis of cryptographic systems","volume":"46","author":"Cortier V","year":"2011","journal-title":"J Autom Secur"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"crossref","unstructured":"Dupressoir F Gordon AD J\u00fcrjens J Naumann DA (2011) Guiding a general-purpose C verifier to prove cryptographic protocols. In: 24th IEEE symposium on computer security foundations (CSF) pp 3\u201317","DOI":"10.1109\/CSF.2011.8"},{"key":"e_1_2_1_2_39_2","doi-asserted-by":"crossref","unstructured":"Dierks T Rescorla E (2008) The transport layer security (TLS) protocol version 1.2. RFC 5246","DOI":"10.17487\/rfc5246"},{"key":"e_1_2_1_2_40_2","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.1983.1056650"},{"key":"e_1_2_1_2_41_2","doi-asserted-by":"crossref","unstructured":"Fournet C Kohlweiss M Strub P-Y (2011) Modular code-based cryptographic verification. In: 18th ACM conference on computer and communications security (CCS) pp 341\u2013350","DOI":"10.1145\/2046707.2046746"},{"key":"e_1_2_1_2_42_2","doi-asserted-by":"crossref","unstructured":"Grandy H Bischof M Stenzel K Schellhorn G Reif W (2008) Verification of Mondex electronic purses with KIV: From a security protocol to verified code. In: 15th international symposium on formal methods (FM) pp 165\u2013180","DOI":"10.1007\/978-3-540-68237-0_13"},{"key":"e_1_2_1_2_43_2","doi-asserted-by":"crossref","unstructured":"Goubault-Larrecq J Parrennes F (2005) Cryptographic protocol analysis on real C code. In: 6th international conference on verification model checking and abstract interpretation (VMCAI) pp 363\u2013379","DOI":"10.1007\/978-3-540-30579-8_24"},{"key":"e_1_2_1_2_44_2","unstructured":"Goubault-Larrecq J Parrennes F (2009) Cryptographic protocol analysis on real C code. Technical report Laboratoire Sp\u00e9cification et V\u00e9rification Report LSV-09-18"},{"key":"e_1_2_1_2_45_2","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(84)90070-9"},{"key":"e_1_2_1_2_46_2","doi-asserted-by":"crossref","unstructured":"Graf S Sa\u00efdi H (1997) Construction of abstract state graphs with PVS. In: 9th international conference on computer aided verification (CAV) pp 72\u201383","DOI":"10.1007\/3-540-63166-6_10"},{"key":"e_1_2_1_2_47_2","doi-asserted-by":"crossref","unstructured":"Gritzalis S Spinellis D (1997) Cryptographic protocols over open distributed systems: a taxonomy of flaws and related protocol analysis tools. In: 16th international conference on computer safety reliability and security (SAFECOMP) pp 123\u2013137","DOI":"10.1007\/978-1-4471-0997-6_10"},{"key":"e_1_2_1_2_48_2","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2001-91-202"},{"key":"e_1_2_1_2_49_2","doi-asserted-by":"crossref","unstructured":"Hubbers E Oostdijk M Poll E (2003) Implementing a formally verifiable security protocol in Java Card. In: 1st international conference on security in pervasive computing (SPC) pp 213\u2013226","DOI":"10.1007\/978-3-540-39881-3_19"},{"key":"e_1_2_1_2_50_2","unstructured":"MasterCard International Inc. The Mondex protocol. http:\/\/www.mondexusa.com"},{"issue":"1","key":"e_1_2_1_2_51_2","first-page":"135","article-title":"Secrecy-preserving refinement","volume":"2021","author":"J\u00fcrjens J","year":"2001","journal-title":"Form Methods Increasing Softw Product"},{"key":"e_1_2_1_2_52_2","doi-asserted-by":"crossref","unstructured":"J\u00fcrjens J (2005) Verification of low-level crypto-protocol implementations using automated theorem proving. In: 2nd ACM\/IEEE international conference on formal methods and models for co-design (MEMOCODE) pp 89\u201398","DOI":"10.1109\/MEMCOD.2005.1487898"},{"key":"e_1_2_1_2_53_2","unstructured":"J\u00fcrjens J (2008) Using interface specifications for verifying crypto-protocol implementations. In: Workshop on foundations of interface technologies (FIT)"},{"key":"e_1_2_1_2_54_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.08.009"},{"key":"e_1_2_1_2_55_2","doi-asserted-by":"crossref","unstructured":"J\u00fcrjens J Yu Y Bauer A (2008) Tools for traceable security verification. In: BCS international academic conference on visions of computer science (VoCS) pp 367\u2013390","DOI":"10.14236\/ewic\/VOCS2008.31"},{"key":"e_1_2_1_2_56_2","doi-asserted-by":"crossref","unstructured":"Kiyomoto S Ota H Tanaka T (2008) A security protocol compiler generating C source codes. In: 2nd international conference on information security and assurance (ISA) pp 20\u201325","DOI":"10.1109\/ISA.2008.13"},{"issue":"1","key":"e_1_2_1_2_57_2","doi-asserted-by":"crossref","first-page":"583","DOI":"10.1016\/j.entcs.2005.11.074","article-title":"On the relationship between web services security and traditional protocols","volume":"155","author":"Kleiner E","year":"2006","journal-title":"Electro Notes Theor Comput Sci"},{"key":"e_1_2_1_2_58_2","doi-asserted-by":"crossref","unstructured":"Kuesters R Truderung T Graf J (2012) A framework for the cryptographic verification of Java-like programs. In: 25th IEEE symposium on computer security foundations (CSF) pp 192\u2013212","DOI":"10.1109\/CSF.2012.9"},{"key":"e_1_2_1_2_59_2","doi-asserted-by":"publisher","DOI":"10.1145\/1127878.1127884"},{"key":"e_1_2_1_2_60_2","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(95)00144-2"},{"key":"e_1_2_1_2_61_2","doi-asserted-by":"crossref","unstructured":"Lowe G (1996) Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In: 2nd international workshop on tools and algorithms for construction and analysis of systems (TACAS) pp 147\u2013166","DOI":"10.1007\/3-540-61042-1_43"},{"key":"e_1_2_1_2_62_2","unstructured":"Meiklejohn S Erway CC K\u00fcp\u00e7\u00fc A Hinkle T Lysyanskaya A (2010) ZKPDL: a language-based system for efficient zero-knowledge proofs and electronic cash. In: 19th USENIX conference on security pp 193\u2013206"},{"key":"e_1_2_1_2_63_2","unstructured":"Mitchell JC Shmatikov V Stern U (1998) Finite-state analysis of SSL 3.0. In: 7th USENIX security symposium (SSYM) pp 201\u2013216"},{"key":"e_1_2_1_2_64_2","doi-asserted-by":"publisher","DOI":"10.1145\/359657.359659"},{"key":"e_1_2_1_2_65_2","unstructured":"Ogata K Futatsugi K (2005) Equational approach to formal analysis of TLS. In: 25th IEEE international conference on distributed computing systems (ICDCS) pp 795\u2013804"},{"key":"e_1_2_1_2_66_2","doi-asserted-by":"publisher","DOI":"10.1145\/24592.24594"},{"key":"e_1_2_1_2_67_2","unstructured":"O\u2019Shea N (2008) Using Elyjah to analyse Java implementations of cryptographic protocols. In: Joint workshop on foundations of computer security automated reasoning for security protocol analysis and issues in the theory of security (FCS-ARSPA-WITS) pp 221\u2013226"},{"key":"e_1_2_1_2_68_2","unstructured":"O\u2019Shea N (2010) Verification and validation of security protocol implementations. PhD thesis School of Informatics University of Edinburgh (UK). Available at http:\/\/hdl.handle.net\/1842\/4753."},{"key":"e_1_2_1_2_69_2","doi-asserted-by":"publisher","DOI":"10.1145\/322510.322530"},{"key":"e_1_2_1_2_70_2","unstructured":"Pironti A (2010) Sound automatic implementation generation and monitoring of security protocol implementations from verified formal specifications. PhD thesis Politecnico di Torino (Italy). Available at http:\/\/alfredo.pironti.eu\/research\/sites\/default\/files\/Pironti_Dissertation.pdf"},{"key":"e_1_2_1_2_71_2","doi-asserted-by":"crossref","unstructured":"Pironti A J\u00fcrjens J (2010) Formally-based black-box monitoring of security protocols. In: International symposium on engineering secure software and systems (ESSoS) pp 79\u201395","DOI":"10.1007\/978-3-642-11747-3_7"},{"key":"e_1_2_1_2_72_2","doi-asserted-by":"crossref","unstructured":"Polikarpova N Moskal M (2012) Verifying implementations of security protocols by refinement. In: Verified software: theories tools experiments (VSTTE) pp 50\u201365","DOI":"10.1007\/978-3-642-27705-4_5"},{"key":"e_1_2_1_2_73_2","doi-asserted-by":"crossref","unstructured":"Pironti A Pozza D Sisto R (2011) Automated formal methods for security protocol engineering. In: IGI global cyber security standards practices and industrial applications: systems and methodologies pp 138\u2013166","DOI":"10.4018\/978-1-60960-851-4.ch008"},{"issue":"1","key":"e_1_2_1_2_74_2","doi-asserted-by":"crossref","first-page":"835","DOI":"10.1016\/j.jss.2011.10.052","article-title":"Formally-based semi-automatic implementation of an open security protocol","volume":"85","author":"Pironti A","year":"2012","journal-title":"J Syst Soft"},{"key":"e_1_2_1_2_75_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.cose.2009.08.001"},{"key":"e_1_2_1_2_76_2","unstructured":"Pironti A Sisto R (2012) Safe abstractions of data encodings in formal security protocol models. Form Asp Comput (To appear)"},{"key":"e_1_2_1_2_77_2","doi-asserted-by":"crossref","unstructured":"Pozza D Sisto R Durante L (2004) Spi2java: automatic cryptographic protocol Java code generation from spi calculus. In: 18th international conference on advanced information networking and applications (AINA) pp 400\u2013405","DOI":"10.1109\/AINA.2004.1283943"},{"key":"e_1_2_1_2_78_2","unstructured":"Rizzo J Duong T (2010) Practical padding oracle attacks. In: 4th USENIX offensive technologies (WOOT) pp 1\u20138"},{"key":"e_1_2_1_2_79_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.11.013"},{"key":"e_1_2_1_2_80_2","doi-asserted-by":"crossref","unstructured":"Song DX Perrig A Phan D (2001) AGVI\u2014automatic generation verification and implementation of security protocols. In: 13th international conference on computer aided verification (CAV) pp 241\u2013245","DOI":"10.1007\/3-540-44585-4_21"},{"key":"e_1_2_1_2_81_2","unstructured":"Shamir A Rivest R Adleman L (1978) Mental poker. Technical report Massachussets Institute of Technology"},{"key":"e_1_2_1_2_82_2","doi-asserted-by":"crossref","unstructured":"Stenzel K (2004) A formally verified calculus for full Java Card. In: 10th international conference on algebraic methodology and software technology (AMAST) pp 33\u201336","DOI":"10.1007\/978-3-540-27815-3_37"},{"key":"e_1_2_1_2_83_2","unstructured":"Tobarra L Cazorla D Cuartero F D\u00edaz G (2006) Formal verification of TLS handshake and extensions for wireless networks. In: IADIS international conference on applied computing pp 57\u201364"},{"key":"e_1_2_1_2_84_2","doi-asserted-by":"crossref","unstructured":"Tobler B Hutchison A (2004) Generating network security protocol implementations from formal specifications. In: 2nd international workshop on certification and security in inter-organizational e-services (CSES) pp 33\u201354","DOI":"10.1007\/11397427_3"},{"key":"e_1_2_1_2_85_2","doi-asserted-by":"crossref","unstructured":"Vaudenay S (2002) Security flaws induced by CBC padding\u2014applications to SSL IPSEC WTLS . . . . In: International conference on the theory and applications of cryptographic techniques\u2014advances in cryptology (EUROCRYPT) pp 534\u2013546","DOI":"10.1007\/3-540-46035-7_35"},{"issue":"1","key":"e_1_2_1_2_86_2","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1016\/j.entcs.2005.11.052","article-title":"Automated security protocol analysis with the AVISPA tool","volume":"155","author":"Vigan\u00f2 L","year":"2006","journal-title":"Electr Notes Theor Comput Sci"},{"key":"e_1_2_1_2_87_2","unstructured":"Wagner D Schneier B (1996) Analysis of the SSL 3.0 protocol. In: 2nd USENIX Workshop on Electronic Commerce (WOEC) pp 29\u201340"},{"key":"e_1_2_1_2_88_2","unstructured":"Xiaodong SD David W Xuqing T (2001) Timing analysis of keystrokes and timing attacks on SSH. In: 10th conference on USENIX security symposium (SSYM) pp 25\u201325"},{"key":"e_1_2_1_2_89_2","doi-asserted-by":"crossref","unstructured":"Yao AC (1982) Theory and application of trapdoor functions. In: 23rd annual symposium on foundations of computer science (FOCS) pp 80\u201391","DOI":"10.1109\/SFCS.1982.45"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-012-0269-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-012-0269-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-012-0269-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T16:02:50Z","timestamp":1641484970000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-012-0269-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,1]]},"references-count":89,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2014,1]]}},"alternative-id":["10.1007\/s00165-012-0269-9"],"URL":"https:\/\/doi.org\/10.1007\/s00165-012-0269-9","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,1]]}}}