{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,30]],"date-time":"2022-03-30T18:15:12Z","timestamp":1648664112524},"reference-count":65,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2007,9,4]],"date-time":"2007-09-04T00:00:00Z","timestamp":1188864000000},"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":[[2008,1]]},"DOI":"10.1007\/s10207-007-0043-9","type":"journal-article","created":{"date-parts":[[2007,9,3]],"date-time":"2007-09-03T04:19:56Z","timestamp":1188793196000},"page":"55-84","source":"Crossref","is-referenced-by-count":3,"title":["A symbolic framework for multi-faceted security protocol analysis"],"prefix":"10.1007","volume":"7","author":[{"given":"Andrea","family":"Bracciali","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gianluigi","family":"Ferrari","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Emilio","family":"Tuosto","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2007,9,4]]},"reference":[{"key":"43_CR1","doi-asserted-by":"crossref","unstructured":"Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: POPL \u201901. Proceedings of the 28th ACM SIGPLAN-SIGACT on Principles of Programming Languages, ACM SIGPLAN Notices. ACM Press (2001)","DOI":"10.1145\/360204.360213"},{"issue":"1","key":"43_CR2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1006\/inco.1998.2740","volume":"148","author":"M. Abadi","year":"1999","unstructured":"Abadi M. and Gordon A. (1999). A calculus for cryptographic protocols: the Spi calculus. Inform. Comput. 148(1): 1\u201370","journal-title":"Inform. Comput."},{"key":"43_CR3","first-page":"380","volume-title":"International Conference in Concurrency Theory. Lecture Notes in Computer Science, vol. 1877","author":"R. Amadio","year":"2000","unstructured":"Amadio R. and Lugiez D. (2000). On the reachability problem in cryptographic protocols. In: Palamidessi, C (eds) International Conference in Concurrency Theory. Lecture Notes in Computer Science, vol. 1877, pp 380\u2013394. Springer, Heidelberg"},{"issue":"1","key":"43_CR4","doi-asserted-by":"crossref","first-page":"695","DOI":"10.1016\/S0304-3975(02)00090-7","volume":"290","author":"R. Amadio","year":"2003","unstructured":"Amadio R., Lugiez D. and Vanack\u00e8re V. (2003). On the symbolic reduction of processes with cryptographic functions. Theor. Comput. Sci. 290(1): 695\u2013740","journal-title":"Theor. Comput. Sci."},{"key":"43_CR5","first-page":"15","volume-title":"Advances in Computing Science\u2014ASIAN\u201999. Lecture Notes in Computer Science vol. 1742","author":"R. Amadio","year":"1999","unstructured":"Amadio R. and Prasad S. (1999). The game of the name in cryptographic tables. In: Thiagarajan, P.S. and Yap, R. (eds) Advances in Computing Science\u2014ASIAN\u201999. Lecture Notes in Computer Science vol. 1742., pp 15\u201326. Springer, Heidelberg"},{"key":"43_CR6","unstructured":"Asokan, N.: Fairness in electronic commerce. PhD thesis, University of Waterloo (1998)"},{"key":"43_CR7","unstructured":"Baldi, G.: Security protocols verification by means of symbolic model checking Ms.Thesis, University of Pisa. Available at [8]"},{"key":"43_CR8","unstructured":"Baldi, G., Bracciali, A., Ferrari, G., Tuosto, E.: ASPASyA: Automated tool for security protocols analysis based on a symbolic approach. http:\/\/www.cs.le.ac.uk\/people\/et52\/aspasya\/aspasya.html"},{"key":"43_CR9","first-page":"23","volume-title":"International Workshop on Security Issues with Petri Nets and other Computational Models. Electronic Notes in Theoretical Computer Science vol. 121","author":"G. Baldi","year":"2005","unstructured":"Baldi G., Bracciali A., Ferrari G. and Tuosto E. (2005). A Coordination-based Methodology for Security Protocol Verification. In: Busi, N., Gorrieri, R., and Martinelli, F. (eds) International Workshop on Security Issues with Petri Nets and other Computational Models. Electronic Notes in Theoretical Computer Science vol. 121, pp 23\u201346. Elsevier, Amsterdam"},{"key":"43_CR10","doi-asserted-by":"crossref","unstructured":"Basin, D., M\u00f6dersheim, S., Vigan\u00f2, L.: Constraint differentiation: a new reduction technique for constraint-based analysis of security protocols. In CCS \u201903: Proceedings of the 10th ACM Conference on Computer and communications security. pp. 335\u2013344. ACM Press (2003)","DOI":"10.1145\/948109.948154"},{"key":"43_CR11","unstructured":"Bodei, C., Buchholtz, M., Degano, P., Nielson, F., Riis Nielson, H.: Control flow analysis can find new flaws too. In: Workshop on Issues on the Theory of Security (WITS\u201904). Electronic Notes in Theoretical Computer Science. Elsevier, Amsterdam, (2004)"},{"key":"43_CR12","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1006\/inco.2000.3020","volume":"168","author":"C. Bodei","year":"2001","unstructured":"Bodei C., Degano P., Nielson F. and Nielson H. (2001). Static analysis for the \u03c0-calculus with applications to security. Inform. Comput. 168: 68\u201392","journal-title":"Inform. Comput."},{"key":"43_CR13","volume-title":"Colloquium on Automata, Languages and Programming. Lecture Notes in Computer Science, vol. 2076.","author":"M. Boreale","year":"2001","unstructured":"Boreale M. (2001). Symbolic trace analysis of cryptographic protocols. In: Orejas, F., Spirakis, P. and van Leeuwen, J. (eds) Colloquium on Automata, Languages and Programming. Lecture Notes in Computer Science, vol. 2076., pp. Springer, Heidelberg"},{"key":"43_CR14","unstructured":"Boreale M., Buscemi M (2002) A Framework for the Analysis of Security Protocols. In: Brim L., Jan\u010dar P., K\u0159etinsk\u00fd M., Ku\u010dera A. (eds.) International Conference in Concurrency Theory. Lecture Notes in Computer Science, vol. 2421, Springer, Heidelberg, pp 483\u2013498"},{"issue":"1-3","key":"43_CR15","doi-asserted-by":"crossref","first-page":"393","DOI":"10.1016\/j.tcs.2005.03.044","volume":"338","author":"M. Boreale","year":"2005","unstructured":"Boreale M. and Buscemi M. (2005). A method for symbolic analysis of security protocols. Theor. Comput. Sci. 338(1-3): 393\u2013425","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"43_CR16","doi-asserted-by":"crossref","first-page":"34","DOI":"10.1006\/inco.1996.0032","volume":"126","author":"M. Boreale","year":"1996","unstructured":"Boreale M. and De Nicola R. (1996). A Symbolic Semantics for the \u03c0-calculus. Inform. Comput. 126(1): 34\u201352","journal-title":"Inform. Comput."},{"key":"43_CR17","first-page":"161","volume-title":"International Conference in Concurrency Theory. Lecture Notes in Computer Science, vol. 3170","author":"J. Borgstr\u00f6m","year":"2004","unstructured":"Borgstr\u00f6m J., Briais S. and Nestmann U. (2004). Symbolic Bisimulation in the Spi Calculus. In: Gardner, P. and Yoshida, N. (eds) International Conference in Concurrency Theory. Lecture Notes in Computer Science, vol. 3170, pp 161\u2013176. Springer, Heidelberg"},{"key":"43_CR18","unstructured":"Bracciali, A.: Behavioural patterns and software composition. PhD thesis, Dipartimento di Informatica, Universit\u00e0 di Pisa, (2003)"},{"key":"43_CR19","unstructured":"Bracciali, A., Brogi, A., Ferrari, G., Tuosto, E.: Security and Dynamic Compositions of Open Systems. In: Arabnia H. (ed.) Conference on Parallel and Distributed Processing Techniques and Applications, vol. 3, pp. 1372\u20131377. CSREA Press, (2002)"},{"issue":"1","key":"43_CR20","doi-asserted-by":"crossref","first-page":"18","DOI":"10.1145\/77648.77649","volume":"8","author":"M. Burrows","year":"1990","unstructured":"Burrows M., Abadi M. and Needham R. (1990). A logic of authentication. ACM Trans. Comput. Syst. 8(1): 18\u201336","journal-title":"ACM Trans. Comput. Syst."},{"key":"43_CR21","unstructured":"Chevalier, Y., K\u00fcsters, R., Rusinowitch, M., Turuani, M.: Deciding the security of protocols with Diffie-Hellman exponentiation and products in exponents. of Lecture Notes in Computer Science, vol. 2914, pp. 124\u2013135. Springer, Heidelberg, (2003)"},{"key":"43_CR22","doi-asserted-by":"crossref","unstructured":"Chevalier, Y., K\u00fcsters, R., Rusinowitch, M., Turuani, M.: An NP decision procedure for protocol insecurity with XOR. In: Annual Symposium on Logic in Computer Science. pp. 261\u2013270. IEEE Computer Society (2003)","DOI":"10.1109\/LICS.2003.1210066"},{"key":"43_CR23","unstructured":"Clark, J., Jacob, J.: A survey of authentication protocols 1.0. Technical Report, University of York (1997)"},{"issue":"5","key":"43_CR24","doi-asserted-by":"crossref","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"E. Clarke","year":"1994","unstructured":"Clarke E., Grumberg O. and Long D. (1994). Model checking and abstraction. ACM Trans. Programm. Languages Syst. 16(5): 1512\u20131542","journal-title":"ACM Trans. Programm. Languages Syst."},{"key":"43_CR25","doi-asserted-by":"crossref","unstructured":"Clarke, E., Jha, S., Marrero, W.: Using state space exploration and a natural deduction style message derivation engine to verify security protocols. In: IFIP Working Conference on Programming Concepts and Methods (PROCOMET), (1998)","DOI":"10.1007\/978-0-387-35358-6_10"},{"key":"43_CR26","first-page":"682","volume-title":"Colloquium on Automata, Languages and Programming. Lecture Notes in Computer Science, vol. 2076","author":"H. Comon","year":"2001","unstructured":"Comon H., Cortier V. and Mitchell J. (2001). Tree automata with one memory, set constraints, and ping-pong protocols. In: Orejas, F., Spirakis, P., and van Leeuwen, J. (eds) Colloquium on Automata, Languages and Programming. Lecture Notes in Computer Science, vol. 2076., pp 682\u2013693. Springer, Heidelberg"},{"key":"43_CR27","unstructured":"Crazzolara, F.: Language, semantics, and methods for security protocols. PhD thesis, BRICS, May 2003"},{"key":"43_CR28","doi-asserted-by":"crossref","unstructured":"Crazzolara F., Winskel G.. Events in security protocols. In: Proceedings of the 8th ACM conference on Computer and Communications Security. pp. 96\u2013105. ACM Press (2001)","DOI":"10.1145\/501983.501998"},{"issue":"2","key":"43_CR29","doi-asserted-by":"crossref","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","volume":"29","author":"D. Dolev","year":"1983","unstructured":"Dolev D. and Yao A. (1983). On the security of public key protocols. IEEE Trans. Inform. Theory. 29(2): 198\u2013208","journal-title":"IEEE Trans. Inform. Theory."},{"key":"43_CR30","unstructured":"Durgin, N., Lincoln, P., Mitchell, J., Scedrov, A.: Undecidability of bounded security protocols. In: Heintze N., Clarke E. (eds.) Workshop on Formal Methods and Security Protocols, Part of the Federated Logic Conference (1999)"},{"key":"43_CR31","doi-asserted-by":"crossref","unstructured":"Fabrega, J., Herzog, J., Guttman, J.: Strand spaces: Why is a security protocol correct? In: RSP: 19th IEEE Computer Society Symposium on Research in Security and Privacy (1998)","DOI":"10.21236\/ADA459060"},{"issue":"2,3","key":"43_CR32","first-page":"181","volume":"7","author":"J. Fabrega","year":"1999","unstructured":"Fabrega J., Herzog J. and Guttman J. (1999). Strand spaces: Proving security protocols correct. J. Comput. Secur. 7(2,3): 181\u2013230","journal-title":"J. Comput. Secur."},{"key":"43_CR33","doi-asserted-by":"crossref","unstructured":"Focardi, R., Gorrieri, R.: A Classification of security properties. J. Comput. Secur. 3(1), 1995","DOI":"10.3233\/JCS-1994\/1995-3103"},{"issue":"9","key":"43_CR34","first-page":"550","volume":"23","author":"R. Focardi","year":"1997","unstructured":"Focardi R. and Gorrieri R. (1997). The Compositional Security Checker: A tool for the verification of information flow security properties. IEEE Comput. Soc. 23(9): 550\u2013571","journal-title":"IEEE Comput. Soc."},{"key":"43_CR35","unstructured":"Freier, A., Karlton, P., Kocher, P.: The SSL protocol version 3.0 (1996) http:\/\/home.netscape.com\/eng\/ssl3"},{"issue":"4","key":"43_CR36","doi-asserted-by":"crossref","first-page":"451","DOI":"10.3233\/JCS-2003-11402","volume":"11","author":"A.D. Gordon","year":"2004","unstructured":"Gordon A.D. and Jeffrey A. (2004). Authenticity by typing for security protocols. J. Comput. Secur. 11(4): 451\u2013519","journal-title":"J. Comput. Secur."},{"issue":"2","key":"43_CR37","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1016\/0304-3975(94)00172-F","volume":"138","author":"M. Hennessy","year":"1995","unstructured":"Hennessy M. and Lin H. (1995). Symbolic Bisimulations. Theor. Comput. Sci. 138(2): 353\u2013389","journal-title":"Theor. Comput. Sci."},{"key":"43_CR38","unstructured":"Huima, A.: Efficient finite-state analysis of security protocols. In: Formal methods and security protocols. FLOC Workshop. INRIA (1999)"},{"key":"43_CR39","unstructured":"Kehne, A., Sch\u00f6nw\u00e4lder, J., Langend\u00f6rfer, H.: Multiple authentications with a nonce-based protocol using generalized timestamps. In: Proc. ICCC \u201992 (1992)"},{"key":"43_CR40","doi-asserted-by":"crossref","unstructured":"Kohl, J., Neuman, B.: The kerberos network authentication service (version 5). Internet Request for Comment RFC-1510 (1993)","DOI":"10.17487\/rfc1510"},{"issue":"17","key":"43_CR41","doi-asserted-by":"crossref","first-page":"1606","DOI":"10.1016\/S0140-3664(02)00049-X","volume":"25","author":"S. Kremer","year":"2002","unstructured":"Kremer S., Markowitch O. and Zhou J (2002). An intensive survey of non-repudiation protocols. Computer Commun. 25(17): 1606\u20131621","journal-title":"Computer Commun."},{"key":"43_CR42","doi-asserted-by":"crossref","unstructured":"Lowe, G.: Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In: Tools and Algorithms for the Construction and Analysis of Systems. vol. 1055, pp. 147\u2013166. Springer, Heidelberg, (1996)","DOI":"10.1007\/3-540-61042-1_43"},{"key":"43_CR43","doi-asserted-by":"crossref","unstructured":"Lowe, G.: Some New Attacks upon Security Protocols. In: Proceedings of 9th IEEE Computer Security Foundations Workshop. IEEE Computer Society, (1996)","DOI":"10.1109\/CSFW.1996.503701"},{"key":"43_CR44","doi-asserted-by":"crossref","unstructured":"Lowe, G.: A hierarchy of authentication specifications. In: Computer Security Foundation Workshop. IEEE Computer Society (1997)","DOI":"10.1109\/CSFW.1997.596782"},{"issue":"1","key":"43_CR45","doi-asserted-by":"crossref","first-page":"1057","DOI":"10.1016\/S0304-3975(02)00596-0","volume":"209","author":"F. Martinelli","year":"2003","unstructured":"Martinelli F. (2003). Analysis of security protocols as open systems. Theor. Comput. Sci. 209(1): 1057\u20131106","journal-title":"Theor. Comput. Sci."},{"key":"43_CR46","unstructured":"Menzies, A., van Oorschot, P., Vanstone, S.: Handbook of Applied Cryptography. CRC Press (1997)"},{"key":"43_CR47","unstructured":"Millen, J.K.: A necessarily parallel attack. In: Heintze N., Clarke E. (eds.) Workshop on Formal Methods and Security Protocols, Part of the Federated Logic Conference (1999)"},{"key":"43_CR48","doi-asserted-by":"crossref","first-page":"329","DOI":"10.1016\/S0020-0190(03)00211-4","volume":"86","author":"J.K. Millen","year":"2003","unstructured":"Millen J.K. (2003). On the freedom of decryption. Inform. Process. Lett. 86: 329\u2013333","journal-title":"Inform. Process. Lett."},{"key":"43_CR49","doi-asserted-by":"crossref","unstructured":"Millen, J.K., Shmatikov, V.: Constraint solving for bounded- process cryptographic protocol analysis. In: ACM Conference on Computer and Communications Security. pp. 166\u2013175 (2001)","DOI":"10.1145\/501983.502007"},{"key":"43_CR50","unstructured":"Mitchell J., Mitchell M., Stern U.. Automated analysis of cryptographic protocols using mur\u03d5. In: Computer Security Foundation Workshop. pp. 141\u2013151. IEEE Computer Society (1997)"},{"key":"43_CR51","unstructured":"Mitchell, J., Shmatikov, V., Stern, U.: Finite-state analysis of SSL 3.0. In: Proceedings of the 7th USENIX Security Symposium (SECURITY-98). pp. 201\u2013216. Usenix Association (1998)"},{"issue":"12","key":"43_CR52","doi-asserted-by":"crossref","first-page":"993","DOI":"10.1145\/359657.359659","volume":"21","author":"R. Needham","year":"1978","unstructured":"Needham R. and Schroeder M. (1978). Using encryption for authentication in large networks of computers. Commun. ACM. 21(12): 993\u2013999","journal-title":"Commun. ACM."},{"key":"43_CR53","doi-asserted-by":"crossref","unstructured":"Paulson, L.: Proving properties of security protocols by induction. In: Computer Security Foundation Workshop. IEEE Computer Society (1997)","DOI":"10.1109\/CSFW.1997.596788"},{"key":"43_CR54","unstructured":"Paulson, L.: The inductive approach to verifying cryptographic protocols. Technical report; no. 443. 4006797499. University of Cambridge, Computer Laboratory (1998)"},{"key":"43_CR55","unstructured":"Shmatikov, V.: Decidable analysis of cryptographic protocols with products and modular exponentiation, of Lecture Notes in Computer Science. vol. 2986, pp. 355\u2013369. Springer, Heidelberg, (2004)"},{"key":"43_CR56","unstructured":"Shmatikov, V., Mitchell, J.: Analysis of a fair exchange protocol. In: Symposium on Network and Distributed Systems Security (NDSS 2000). pp. 119\u2013128. Internet Society (2000)"},{"issue":"2","key":"43_CR57","first-page":"419","volume":"283","author":"V. Shmatikov","year":"2002","unstructured":"Shmatikov V. and Mitchell J. (2002). Finite-state analysis of two contract signing protocols. Theor. Comput. Sci. Special issue on Theoretical Foundations of Security Analysis and Design 283(2): 419\u2013450","journal-title":"Theor. Comput. Sci. Special issue on Theoretical Foundations of Security Analysis and Design"},{"issue":"1,2","key":"43_CR58","doi-asserted-by":"crossref","first-page":"47","DOI":"10.3233\/JCS-2001-91-203","volume":"9","author":"D. Song","year":"2001","unstructured":"Song D., Berezin S. and Perrig A. (2001). Athena, a novel approach to efficient automatic security protocol analysis. Comput. Secur. 9(1,2): 47\u201374","journal-title":"Comput. Secur."},{"key":"43_CR59","unstructured":"Stinson, D.: Cryptography: Theory and practice. CRC Press (1995)"},{"key":"43_CR60","unstructured":"Thayer, J., Herzog, J., Guttman, J.: Honest ideals on strand spaces. In: Computer Security Foundation Workshop. IEEE Computer Society (1998)"},{"key":"43_CR61","unstructured":"Tuosto, E.: Non-functional aspects of wide area network programming. PhD thesis, Dipartimento di Informatica, Universit\u00e0 di Pisa (2003)"},{"key":"43_CR62","unstructured":"Vanack\u00e9re V. The TRUST protocol analyser. Automatic and efficient verification of cryptographic protocols. In: VERIFY02 (2002)"},{"key":"43_CR63","doi-asserted-by":"crossref","unstructured":"Woo, T., Lam, S.: A semantic model for authentication protocols. In: RSP: IEEE Computer Society Symposium on Research in Security and Privacy (1993)","DOI":"10.1109\/RISP.1993.287633"},{"key":"43_CR64","unstructured":"Zhou, J.: Non-repudiation. PhD thesis, University of London, (1996)"},{"issue":"1","key":"43_CR65","doi-asserted-by":"crossref","first-page":"154","DOI":"10.1016\/j.tcs.2005.03.006","volume":"340","author":"R. Zunino","year":"2005","unstructured":"Zunino R. and Degano P. (2005). Weakening the perfect encryption assumption in Dolev\u2013Yao adversaries. Theor. Comput. Sci. 340(1): 154\u2013178","journal-title":"Theor. Comput. Sci."}],"container-title":["International Journal of Information Security"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10207-007-0043-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10207-007-0043-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10207-007-0043-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T07:01:23Z","timestamp":1559113283000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10207-007-0043-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,9,4]]},"references-count":65,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2008,1]]}},"alternative-id":["43"],"URL":"https:\/\/doi.org\/10.1007\/s10207-007-0043-9","relation":{},"ISSN":["1615-5262","1615-5270"],"issn-type":[{"value":"1615-5262","type":"print"},{"value":"1615-5270","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,9,4]]}}}