{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T15:44:51Z","timestamp":1775058291572,"version":"3.50.1"},"reference-count":50,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2005,6,1]],"date-time":"2005-06-01T00:00:00Z","timestamp":1117584000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Inf Secur"],"published-print":{"date-parts":[[2005,6]]},"DOI":"10.1007\/s10207-004-0055-7","type":"journal-article","created":{"date-parts":[[2004,12,21]],"date-time":"2004-12-21T15:08:24Z","timestamp":1103641704000},"page":"181-208","source":"Crossref","is-referenced-by-count":363,"title":["OFMC: A symbolic model checker for security protocols"],"prefix":"10.1007","volume":"4","author":[{"given":"David","family":"Basin","sequence":"first","affiliation":[]},{"given":"Sebastian","family":"M\u00f6dersheim","sequence":"additional","affiliation":[]},{"given":"Luca","family":"Vigan\u00f2","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,1]]},"reference":[{"key":"55_CR1","unstructured":"Amadio R, Lugiez D (2002) On the reachability problem in cryptographic protocols. In: Proceedings of CONCUR\u201900. Lecture notes in computer science, vol 1877. Springer, Berlin Heidelberg New York, pp 380\u2013394"},{"key":"55_CR2","doi-asserted-by":"crossref","unstructured":"Armando A, Basin D, Bouallagui M, Chevalier Y, Compagna L, M\u00f6dersheim S, Rusinowitch M, Turuani M, Vigan\u00f2 L, Vigneron L (2002) The AVISS security protocol analysis tool. In: Proceedings of CAV\u201902. Lecture notes in computer science, vol 2404. Springer, Berlin Heidelberg New York, pp 349\u2013354","DOI":"10.1007\/3-540-45657-0_27"},{"key":"55_CR3","doi-asserted-by":"crossref","unstructured":"Armando A, Compagna L (2002) Automatic SAT-compilation of protocol insecurity problems via reduction to planning. In: Proceedings of FORTE 2002. Lecture notes in computer science, vol 2529. Springer, Berlin Heidelberg New York, pp 210\u2013225","DOI":"10.1007\/3-540-36135-9_14"},{"key":"55_CR4","doi-asserted-by":"crossref","unstructured":"Armando A, Compagna L, Ganty P (2003) SAT-based model-checking of security protocols using planning graph analysis. In: Proceedings of FME 2003. Lecture notes in computer science, vol 2805. Springer, Berlin Heidelberg New York, pp 875\u2013893","DOI":"10.1007\/978-3-540-45236-2_47"},{"key":"55_CR5","unstructured":"AVISPA: Automated validation of internet security protocols and applications (2003) FET Open Project IST-2001-39252. www.avispa-project.org"},{"key":"55_CR6","doi-asserted-by":"crossref","unstructured":"Baader F, Nipkow T (1998) Term rewriting and all that. Cambridge University Press, Cambridge, UK","DOI":"10.1017\/CBO9781139172752"},{"key":"55_CR7","doi-asserted-by":"crossref","unstructured":"Basin D (1999) Lazy infinite-state analysis of security protocols. In: Proceedings of CQRE\u201999. Lecture notes in computer science, vol 1740. Springer, Berlin Heidelberg New York, pp 30\u201342","DOI":"10.1007\/3-540-46701-7_3"},{"key":"55_CR8","unstructured":"Basin D, Denker G (2001) Maude versus Haskell: an experimental comparison in security protocol analysis. In: Electronic notes in computer science, vol 36. Elsevier, Amsterdam, pp 235\u2013256"},{"key":"55_CR9","doi-asserted-by":"crossref","unstructured":"Basin D, M\u00f6dersheim S, Vigan\u00f2 L (2003) An on-the-fly model-checker for security protocol analysis. In: Proceedings of ESORICS\u201903. Lecture notes in computer science, vol 2808. Springer, Berlin Heidelberg New York, pp 253\u2013270","DOI":"10.1007\/978-3-540-39650-5_15"},{"key":"55_CR10","unstructured":"Basin D, M\u00f6dersheim S, Vigan\u00f2 L (2003) Constraint differentiation: a new reduction technique for constraint-based analysis of security protocols. In: Proceedings of CCS\u201903. ACM Press, New York, pp 335\u2013344"},{"key":"55_CR11","doi-asserted-by":"crossref","unstructured":"Boreale M (2001) Symbolic trace analysis of cryptographic protocols. In: Proceedings of ICALP\u201901. Lecture notes in computer science, vol 2076. Springer, Berlin Heidelberg New York, pp 667\u2013681","DOI":"10.1007\/3-540-48224-5_55"},{"key":"55_CR12","doi-asserted-by":"crossref","unstructured":"Boreale M, Buscemi MG (2002) A framework for the analysis of security protocols. In: Proceedings of CONCUR\u201902. Lecture notes in computer science, vol 2421. Springer, Berlin Heidelberg New York, pp 483\u2013498","DOI":"10.1007\/3-540-45694-5_32"},{"key":"55_CR13","unstructured":"Boreale M, Buscemi MG (2003) On the symbolic analysis of low-level cryptographic primitives: modular exponentiation and the Diffie-Hellman protocol. In: Proceedings of FCS\u201903. TR-2003-04, Computer Science Department, University of Ottawa"},{"key":"55_CR14","unstructured":"Bouallagui M, Jain H (2003) Automatic session generation. AVISPA report, LORIA-INRIA-Lorraine"},{"key":"55_CR15","doi-asserted-by":"crossref","unstructured":"Cervesato I, Durgin NA, Lincoln PD, Mitchell JC, Scedrov A (2000) Relating strands and multiset rewriting for security protocol analysis. In: Proceedings of CSFW\u201900. IEEE Press, New York, pp 35\u201351","DOI":"10.1109\/CSFW.2000.856924"},{"key":"55_CR16","doi-asserted-by":"crossref","unstructured":"Chevalier Y, K\u00fcsters R, Rusinowitch M, Turuani M (2003) An NP decision procedure for protocol insecurity with Xor. In: Proceedings of LICS 2003. IEEE Press, New York, pp 261\u2013270","DOI":"10.1109\/LICS.2003.1210066"},{"key":"55_CR17","doi-asserted-by":"crossref","unstructured":"Chevalier Y, K\u00fcsters R, Rusinowitch M, Turuani M (2003) Deciding the security of protocols with Diffie-Hellman exponentiation and products in exponents. Lecture notes in computer science, vol 2914. In: Proceedings of FST TCS\u201903. Springer, Berlin Heidelberg New York, pp 124\u2013135","DOI":"10.1007\/978-3-540-24597-1_11"},{"key":"55_CR18","doi-asserted-by":"crossref","unstructured":"Chevalier Y, K\u00fcsters R, Rusinowitch M, Turuani M, Vigneron L (2003) Extending the Dolev\u2013Yao intruder for analyzing an unbounded number of sessions. In: Proceedings of CSL 2003. Lecture notes in computer science, vol 2803. Springer, Berlin Heidelberg New York, pp 128\u2013141","DOI":"10.1007\/978-3-540-45220-1_13"},{"key":"55_CR19","doi-asserted-by":"crossref","unstructured":"Chevalier Y, Vigneron L (2001) A tool for lazy verification of security protocols. In: Proceedings of ASE\u201901. IEEE Press, New York, pp 373\u2013376","DOI":"10.1109\/ASE.2001.989832"},{"key":"55_CR20","doi-asserted-by":"crossref","unstructured":"Chevalier Y, Vigneron L (2002) Automated unbounded verification of security protocols. In: Proceedings of CAV\u201902. Lecture notes in computer science, vol 2404. Springer, Berlin Heidelberg New York, pp 324\u2013337","DOI":"10.1007\/3-540-45657-0_24"},{"key":"55_CR21","first-page":"version","volume":"literature","author":"Clark","year":"1997","unstructured":"Clark J, Jacob J (1997) A survey of authentication protocol literature: version 1.0, 17 November 1997. www.cs.york.ac.uk\/\u223cjac\/papers\/drareview.ps.gz","journal-title":"A survey of authentication protocol"},{"key":"55_CR22","first-page":"5","volume":"4","author":"Comon","year":"2002","unstructured":"Comon H, Shmatikov V (2002) Is it possible to decide whether a cryptographic protocol is secure or not? J Telecommun Inf Technol 4:5\u201315","journal-title":"J Telecommun Inf Technol"},{"key":"55_CR23","doi-asserted-by":"crossref","unstructured":"Comon-Lundh H, Cortier V (2003) Security properties: two agents are sufficient. In: Proceedings of ESOP\u201903. Lecture notes in computer science, vol 2618. Springer, Berlin Heidelberg New York, pp 99\u2013113","DOI":"10.1007\/3-540-36575-3_8"},{"key":"55_CR24","doi-asserted-by":"crossref","unstructured":"Comon-Lundh H, Shmatikov V (2003) Intruder deductions, constraint solving and insecurity decision in presence of exclusive or. In: Proceedings of LICS 2003. IEEE Press, New York, pp 271\u2013280","DOI":"10.1109\/LICS.2003.1210067"},{"key":"55_CR25","doi-asserted-by":"crossref","unstructured":"Corin R, Etalle S (2002) An improved constraint-based system for the verification of security protocols. In: Proceedings of SAS 2002. Lecture notes in computer science, vol 2477. Springer, Berlin Heidelberg New York, pp 326\u2013341","DOI":"10.1007\/3-540-45789-5_24"},{"key":"55_CR26","unstructured":"Denker G, Millen J, Ruess H (2000) The CAPSL integrated protocol environment. Technical Report SRI-CSL-2000-02, SRI International, Menlo Park, CA"},{"key":"55_CR27","doi-asserted-by":"crossref","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","volume":"2","author":"Dolev","year":"1983","unstructured":"Dolev D, Yao A (1983) On the security of public-key protocols. IEEE Trans Inf Theory 2(29):198\u2013208","journal-title":"IEEE Trans Inf Theory"},{"key":"55_CR28","unstructured":"Donovan B, Norris P, Lowe G (1999) Analyzing a library of security protocols using Casper and FDR. In: Proceedings of the FLOC\u201999 workshop on formal methods and security protocols (FMSP\u201999)"},{"key":"55_CR29","unstructured":"Durgin N, Lincoln PD, Mitchell JC, Scedrov A (1999) Undecidability of bounded security protocols. In: Proceedings of the FLOC\u201999 workshop on formal methods and security protocols (FMSP\u201999)"},{"key":"55_CR30","doi-asserted-by":"crossref","unstructured":"Fiore M, Abadi M (2001) Computing symbolic models for verifying cryptographic protocols. In: Proceedings of CSFW\u201901. IEEE Press, New York, pp 160\u2013173","DOI":"10.1109\/CSFW.2001.930144"},{"key":"55_CR31","unstructured":"Huima A (1999) Efficient infinite-state analysis of security protocols. In: Proceedings of the FLOC\u201999 workshop on formal methods and security protocols (FMSP\u201999)"},{"key":"55_CR32","unstructured":"ITU-T Recommendation H.530: Symmetric security procedures for H.510 (mobility for H.323 multimedia systems and services) (2002)"},{"key":"55_CR33","unstructured":"ITU-T Recommendation H.530, Corrigendum 1 (2003) Corrected version of [32]"},{"key":"55_CR34","doi-asserted-by":"crossref","unstructured":"Jacquemard F, Rusinowitch M, Vigneron L (2000) Compiling and verifying security protocols. In: Proceedings of LPAR 2000. Lecture notes in computer science, vol 1955. Springer, Berlin Heidelberg New York, pp 131\u2013160","DOI":"10.1007\/3-540-44404-1_10"},{"key":"55_CR35","unstructured":"Lowe G (1996) Breaking and fixing the Needham\u2013Shroeder public-key protocol using FDR. In: Proceedings of TACAS \u201996. Lecture notes in computer science, vol 1055. Springer, Berlin Heidelberg New York, pp 147\u2013166"},{"key":"55_CR36","doi-asserted-by":"crossref","unstructured":"Lowe G (1997) A hierarchy of authentication specifications. In: Proceedings of CSFW\u201997. IEEE Press, New York, pp 31\u201343","DOI":"10.1109\/CSFW.1997.596782"},{"key":"55_CR37","doi-asserted-by":"crossref","first-page":"53","DOI":"10.3233\/JCS-1998-61-204","volume":"6","author":"Lowe","year":"1998","unstructured":"Lowe G (1998) Casper: a compiler for the analysis of security protocols. J Comput Secur 6(1):53\u201384","journal-title":"J Comput Secur"},{"key":"55_CR38","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1016\/0743-1066(95)00095-X","volume":"26","author":"Meadows","year":"1996","unstructured":"Meadows C (1996) The NRL protocol analyzer: an overview. J Logic Programm 26(2):113\u2013131","journal-title":"J Logic Programm"},{"key":"55_CR39","doi-asserted-by":"crossref","unstructured":"Meadows C (1999) Analysis of the Internet Key Exchange Protocol using the NRL protocol analyzer. In: Proceedings of the 1999 IEEE symposium on security and privacy. IEEE Press, New York, pp 216\u2013231","DOI":"10.1109\/SECPRI.1999.766916"},{"key":"55_CR40","doi-asserted-by":"crossref","unstructured":"Millen JK, Shmatikov V (2001) Constraint solving for bounded-process cryptographic protocol analysis. In: Proceedings of CCS\u201901. ACM Press, New York, pp 166\u2013175","DOI":"10.1145\/501983.502007"},{"key":"55_CR41","doi-asserted-by":"crossref","unstructured":"Millen JK, Shmatikov V (2003) Symbolic protocol analysis with products and Diffie-Hellman exponentiation. In: Proceedings of CSFW\u201903. IEEE Press, New York, pp 47\u201361","DOI":"10.1109\/CSFW.2003.1212704"},{"key":"55_CR42","unstructured":"Mitchell JC, Mitchell M, Stern U (1997) Automated analysis of cryptographic protocols using Murphi. In: Proceedings of the 1997 IEEE symposium on security and privacy. IEEE Press, New York, pp 141\u2013153"},{"key":"55_CR43","doi-asserted-by":"crossref","first-page":"85","DOI":"10.3233\/JCS-1998-61-205","volume":"6","author":"Paulson","year":"1998","unstructured":"Paulson LC (1998) The inductive approach to verifying cryptographic protocols. J Comput Secur 6(1):85\u2013128","journal-title":"J Comput Secur"},{"key":"55_CR44","unstructured":"Paulson LC (1999) Relations between secrets: the Yahalom protocol. In: Proceedings of the 7th Cambridge international workshop on security protocols. Lecture notes in computer science, vol 1796. Springer, Berlin Heidelberg New York, pp 73\u201377"},{"key":"55_CR45","doi-asserted-by":"crossref","unstructured":"Perrig A, Song D (2000) Looking for diamonds in the desert (extending automatic protocol generation to three-party authentication and key agreement protocols). In: Proceedings of CSFW\u201900. IEEE Press, New York, pp 64\u201376","DOI":"10.1109\/CSFW.2000.856926"},{"key":"55_CR46","doi-asserted-by":"crossref","unstructured":"Rusinowitch M, Turuani M (2001) Protocol insecurity with finite number of sessions is NP-complete. In: Proceedings of CSFW\u201901. IEEE Press, New York, pp 174\u2013187","DOI":"10.1109\/CSFW.2001.930145"},{"key":"55_CR47","unstructured":"Ryan P, Schneider S, Goldsmith M, Lowe G, Roscoe B (2000) Modelling and analysis of security protocols. Addison-Wesley, Reading, MA"},{"key":"55_CR48","doi-asserted-by":"crossref","first-page":"47","DOI":"10.3233\/JCS-2001-91-203","volume":"9","author":"Song","year":"2001","unstructured":"Song D, Berezin S, Perrig A (2001) Athena: a novel approach to efficient automatic security protocol analysis. J Comput Secur 9:47\u201374","journal-title":"J Comput Secur"},{"key":"55_CR49","doi-asserted-by":"crossref","first-page":"191","DOI":"10.3233\/JCS-1999-72-304","volume":"7","author":"Thayer","year":"1999","unstructured":"Thayer F\u00e1brega FJ, Herzog JC, Guttman JD (1999) Strand spaces: proving security protocols correct. J Comput Secur 7:191\u2013230","journal-title":"J Comput Secur"},{"key":"55_CR50","unstructured":"Turuani M (2003) S\u00e9curit\u00e9 des protocoles cryptographiques: d\u00e9cidabilit\u00e9 et complexit\u00e9. PhD Thesis, Universit\u00e9 Henri Poincar\u00e9, Nancy, France"}],"container-title":["International Journal of Information Security"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10207-004-0055-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10207-004-0055-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10207-004-0055-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T07:01:21Z","timestamp":1559113281000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10207-004-0055-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,6]]},"references-count":50,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2005,6]]}},"alternative-id":["55"],"URL":"https:\/\/doi.org\/10.1007\/s10207-004-0055-7","relation":{},"ISSN":["1615-5262","1615-5270"],"issn-type":[{"value":"1615-5262","type":"print"},{"value":"1615-5270","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005,6]]}}}