{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,10,5]],"date-time":"2023-10-05T03:07:58Z","timestamp":1696475278284},"reference-count":35,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2009,12,9]],"date-time":"2009-12-09T00:00:00Z","timestamp":1260316800000},"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":[[2010,4]]},"DOI":"10.1007\/s10207-009-0097-y","type":"journal-article","created":{"date-parts":[[2009,12,8]],"date-time":"2009-12-08T12:36:12Z","timestamp":1260275772000},"page":"83-97","source":"Crossref","is-referenced-by-count":5,"title":["The principle of guarantee availability for security protocol analysis"],"prefix":"10.1007","volume":"9","author":[{"given":"Giampaolo","family":"Bella","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2009,12,9]]},"reference":[{"key":"97_CR1","doi-asserted-by":"crossref","unstructured":"Abadi, M., Gordon, A.: Reasoning about cryptographic protocols in the spi calculus. In: Mazurkiewicz, A.W., Winkowski, J. (eds.) Proceedings of the 8th International Conference on Concurrency Theory (CONCUR\u201997), LNCS 1243, pp. 59\u201373. Springer (1997)","DOI":"10.1007\/3-540-63141-0_5"},{"issue":"1","key":"97_CR2","doi-asserted-by":"crossref","first-page":"6","DOI":"10.1109\/32.481513","volume":"22","author":"M. Abadi","year":"1996","unstructured":"Abadi M., Needham R.M.: Prudent engineering practice for cryptographic protocols. IEEE Trans. Softw. Eng. 22(1), 6\u201315 (1996)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"1","key":"97_CR3","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1049\/ip-ifs:20055073","volume":"153","author":"M. Abdalla","year":"2006","unstructured":"Abdalla M., Fouque P.A., Pointcheval D.: Password-based authenticated key exchange in the three-party setting. IEE Proc. Inf. Secur. 153(1), 27\u201339 (2006)","journal-title":"IEE Proc. Inf. Secur."},{"key":"97_CR4","doi-asserted-by":"crossref","unstructured":"Anderson, R., Needham, R.M.: Robustness principles for public key protocols. In: Coppersmith, D. (ed.) Proceedings of Advances in Cryptography (CRYPTO\u201995), LNCS 963, pp. 236\u2013247. Springer (1995)","DOI":"10.1007\/3-540-44750-4_19"},{"key":"97_CR5","doi-asserted-by":"crossref","unstructured":"Bella, G.: Availability of protocol goals. In: Panda, B. (ed.) Proceedings of the 18th ACM Symposium on Applied Computing (ACM SAC\u201903), pp. 312\u2013317. ACM Press (2003a)","DOI":"10.1145\/952532.952596"},{"issue":"1","key":"97_CR6","doi-asserted-by":"crossref","first-page":"87","DOI":"10.3233\/JCS-2003-11103","volume":"11","author":"G. Bella","year":"2003","unstructured":"Bella G.: Inductive verification of smartcard protocols. J. Comput. Secur. 11(1), 87\u2013132 (2003b)","journal-title":"J. Comput. Secur."},{"key":"97_CR7","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-540-68136-6","volume-title":"Formal Correctness of Security Protocols. Information Security and Cryptography","author":"G. Bella","year":"2007","unstructured":"Bella G.: Formal Correctness of Security Protocols. Information Security and Cryptography. Springer, Berlin (2007)"},{"key":"97_CR8","doi-asserted-by":"crossref","unstructured":"Bella, G., Paulson, L.C.: Kerberos Version IV: inductive analysis of the secrecy goals. In: Quisquater, J.J., Deswarte, Y., Meadows, C., Gollmann, D. (eds.) Proceedings of the 5th European Symposium on Research in Computer Security (ESORICS\u201998), LNCS 1485, pp. 361\u2013375. Springer (1998)","DOI":"10.1007\/BFb0055875"},{"issue":"2","key":"97_CR9","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1151414.1151416","volume":"9","author":"G. Bella","year":"2006","unstructured":"Bella G., Paulson L.C.: Accountability protocols: formalized and verified. ACM Trans. Inf. Syst. Secur. 9(2), 1\u201324 (2006)","journal-title":"ACM Trans. Inf. Syst. Secur."},{"issue":"1","key":"97_CR10","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1109\/JSAC.2002.806133","volume":"21","author":"G. Bella","year":"2003","unstructured":"Bella G., Massacci F., Paulson L.C.: Verifying the SET registration protocols. IEEE J. Sel. Areas Commun. 21(1), 77\u201387 (2003)","journal-title":"IEEE J. Sel. Areas Commun."},{"key":"97_CR11","doi-asserted-by":"crossref","unstructured":"Bellare, M., Rogaway, P.: Provably secure session key distribution\u2014the three party case. In: Proceedings of the 27th ACM SIGACT Symposium on Theory of Computing (STOC\u201995), pp. 57\u201366. ACM Press (1995)","DOI":"10.1145\/225058.225084"},{"key":"97_CR12","doi-asserted-by":"crossref","unstructured":"Brackin, S.: A HOL extension of GNY for automatically cryptographic protocols. In: Proceedings of the 9th IEEE Computer Security Foundations Workshop (CSFW\u201996), pp. 62\u201376. IEEE Press (1996)","DOI":"10.1109\/CSFW.1996.503691"},{"key":"97_CR13","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1098\/rspa.1989.0125","volume":"426","author":"M. Burrows","year":"1989","unstructured":"Burrows M., Abadi M., Needham R.M.: A logic of authentication. Proc. R. Soc. Lond. 426, 233\u2013271 (1989)","journal-title":"Proc. R. Soc. Lond."},{"issue":"8","key":"97_CR14","doi-asserted-by":"crossref","first-page":"533","DOI":"10.1145\/358722.358740","volume":"24","author":"D.E. Denning","year":"1981","unstructured":"Denning D.E., Sacco G.M.: Timestamps in key distribution protocols. Commun. ACM 24(8), 533\u2013536 (1981)","journal-title":"Commun. ACM"},{"issue":"29","key":"97_CR15","doi-asserted-by":"crossref","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","volume":"2","author":"D. Dolev","year":"1983","unstructured":"Dolev D., Yao A.: On the security of public-key protocols. IEEE Trans. Inf. Theory 2(29), 198\u2013208 (1983)","journal-title":"IEEE Trans. Inf. Theory"},{"key":"97_CR16","doi-asserted-by":"crossref","unstructured":"Gollmann, D.: On the verification of cryptographic protocols\u2014a tale of two committees. In: Schneider, S., Ryan, P.Y.A. (eds.) Proceedings of the Workshop on Secure Architectures and Information Flow, ENTCS 32, pp. 42\u201358. Elsevier (2000)","DOI":"10.1016\/S1571-0661(04)00094-5"},{"key":"97_CR17","unstructured":"Gong, L., Syverson. P.: Fail-stop protocols: an approach to designing secure protocols. In: Iyer, R.K., Morganti, M., Fuchs, W.K., Gligor, V. (eds.) Proceedings of the 5th International Working Conference on Dependable Computing for Critical Applications (DCCA\u201995), pp. 79\u2013100. IEEE Press (1998)"},{"key":"97_CR18","doi-asserted-by":"crossref","unstructured":"Heather, J., Schneider, S.: Towards automatic verification of authentication protocols on an unbounded network. In: Proceedings of the 13th IEEE Computer Security Foundations Workshop (CSFW\u201900), pp. 132\u2013143. IEEE Press (2000)","DOI":"10.1109\/CSFW.2000.856932"},{"key":"97_CR19","doi-asserted-by":"crossref","unstructured":"Jerdonek, R., Honeyman, P., Coffman, K., Rees, J., Wheeler, K.: Implementation of a provably secure, smartcard-based key distribution protocol. In: Quisquater, J.J., Schneier, B. (eds.) Proceedings of the 3rd Smartcard Research and Advanced Application Conference (CARDIS\u201998), pp. 229\u2013235. (1998)","DOI":"10.1007\/10721064_21"},{"key":"97_CR20","first-page":"147","volume-title":"Proceedings of the 2nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201996), LNCS 1055","author":"G. Lowe","year":"1996","unstructured":"Lowe G.: Breaking and fixing the Needham\u2013Schroeder public-key protocol using CSP and FDR. In: Margaria, T., Steffen, B. (eds) Proceedings of the 2nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201996), LNCS 1055, pp. 147\u2013166. Springer, Berlin (1996)"},{"issue":"10","key":"97_CR21","doi-asserted-by":"crossref","first-page":"659","DOI":"10.1109\/32.637148","volume":"3","author":"G. Lowe","year":"1997","unstructured":"Lowe G., Roscoe A.W.: Using CSP to detect errors in the TMN protocol. IEEE Trans. Softw. Eng. 3(10), 659\u2013669 (1997)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"97_CR22","doi-asserted-by":"crossref","unstructured":"Meadows, C.: Invariant generation techniques in cryptographic protocol analysis. In: Proceedings of the 13th IEEE Computer Security Foundations Workshop (CSFW\u201900), pp. 159\u2013169. IEEE Press (2000)","DOI":"10.1109\/CSFW.2000.856934"},{"issue":"2","key":"97_CR23","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1016\/0743-1066(95)00095-X","volume":"26","author":"C.A. Meadows","year":"1996","unstructured":"Meadows C.A.: The NRL protocol analyzer: an overview. J. Log. Program. 26(2), 113\u2013131 (1996)","journal-title":"J. Log. Program."},{"key":"97_CR24","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. Springer, LNCS Tutorial 2283 (2002)","DOI":"10.1007\/3-540-45949-9"},{"key":"97_CR25","doi-asserted-by":"crossref","unstructured":"Paulson, L.C.: Proving properties of security protocols by induction. In: Proceedings of the 10th IEEE Computer Security Foundations Workshop (CSFW\u201997), pp. 70\u201383. IEEE Press (1997)","DOI":"10.1109\/CSFW.1997.596788"},{"key":"97_CR26","doi-asserted-by":"crossref","first-page":"85","DOI":"10.3233\/JCS-1998-61-205","volume":"6","author":"L.C. Paulson","year":"1998","unstructured":"Paulson L.C.: The inductive approach to verifying cryptographic protocols. J. Comput. Secur. 6, 85\u2013128 (1998)","journal-title":"J. Comput. Secur."},{"issue":"3","key":"97_CR27","doi-asserted-by":"crossref","first-page":"332","DOI":"10.1145\/322510.322530","volume":"2","author":"L.C. Paulson","year":"1999","unstructured":"Paulson L.C.: Inductive analysis of the internet protocol TLS. ACM Trans. Comput. Syst. Secur. 2(3), 332\u2013351 (1999)","journal-title":"ACM Trans. Comput. Syst. Secur."},{"key":"97_CR28","unstructured":"Ryan, P.Y.A., Schneider, S., Goldsmith, M., Lowe, G., Roscoe, A.W.: Modelling and Analysis of Security Protocols. Addison-Wesley (2001)"},{"key":"97_CR29","doi-asserted-by":"crossref","unstructured":"Schneider, S.: Verifying authentication protocols with CSP. In: Proceedings of the 10th IEEE Computer Security Foundations Workshop (CSFW\u201997), pp. 3\u201317. IEEE Press (1997)","DOI":"10.1109\/CSFW.1997.596775"},{"key":"97_CR30","doi-asserted-by":"crossref","unstructured":"Shoup, V., Rubin, A.: Session key distribution using smartcards. In: Maurer, U. (ed.) Advances in Cryptology (Eurocrypt\u201996), LNCS 1070, pp. 321\u2013331. Springer (1996)","DOI":"10.1007\/3-540-68339-9_28"},{"key":"97_CR31","doi-asserted-by":"crossref","unstructured":"Song, B., Kim, K.: Two-pass authenticated key agreement protocol with key confirmation. In: Roy, B.K., Okamoto, E. (eds.) Proceeings of 1st International Conference in Cryptology in India, Indocrypt 2000, LNCS 1977, pp. 237\u2013249. Springer (2000)","DOI":"10.1007\/3-540-44495-5_21"},{"key":"97_CR32","doi-asserted-by":"crossref","unstructured":"Syverson, P.F.: Limitations on design principles for public key protocols. In: Proceedings of the 15th IEEE Symposium on Security and Privacy (SSP\u201996), pp. 62\u201372. IEEE Press (1996)","DOI":"10.1109\/SECPRI.1996.502670"},{"key":"97_CR33","doi-asserted-by":"crossref","first-page":"191","DOI":"10.3233\/JCS-1999-72-304","volume":"7","author":"F.J. Thayer","year":"1999","unstructured":"Thayer F.J., Herzog J.C., Guttman J.D.: Strand spaces: proving security protocols correct. J. Comput. Secur. 7, 191\u2013220 (1999)","journal-title":"J. Comput. Secur."},{"key":"97_CR34","unstructured":"URL (2009a) Isabelle download page. http:\/\/www.cl.cam.ac.uk\/Research\/HVG\/Isabelle\/download.html"},{"key":"97_CR35","unstructured":"URL (2009b) Old Isabelle releases. http:\/\/www.cl.cam.ac.uk\/Research\/HVG\/Isabelle\/download_past.html"}],"container-title":["International Journal of Information Security"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10207-009-0097-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10207-009-0097-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10207-009-0097-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T07:01:24Z","timestamp":1559113284000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10207-009-0097-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,12,9]]},"references-count":35,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2010,4]]}},"alternative-id":["97"],"URL":"https:\/\/doi.org\/10.1007\/s10207-009-0097-y","relation":{},"ISSN":["1615-5262","1615-5270"],"issn-type":[{"value":"1615-5262","type":"print"},{"value":"1615-5270","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,12,9]]}}}