{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T00:50:29Z","timestamp":1743036629665,"version":"3.40.3"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030916305"},{"type":"electronic","value":"9783030916312"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-91631-2_5","type":"book-chapter","created":{"date-parts":[[2021,11,18]],"date-time":"2021-11-18T21:02:24Z","timestamp":1637269344000},"page":"98-111","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Security Protocols as Choreographies"],"prefix":"10.1007","author":[{"given":"Alessandro","family":"Bruni","sequence":"first","affiliation":[]},{"given":"Marco","family":"Carbone","sequence":"additional","affiliation":[]},{"given":"Rosario","family":"Giustolisi","sequence":"additional","affiliation":[]},{"given":"Sebastian","family":"M\u00f6dersheim","sequence":"additional","affiliation":[]},{"given":"Carsten","family":"Sch\u00fcrmann","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,11,19]]},"reference":[{"key":"5_CR1","unstructured":"Tamarin code (2021). https:\/\/www.dropbox.com\/sh\/lonxu6vmj3iilmu\/AAAErB3ATSNg59MFGxBcp74Ha?dl=0"},{"key":"5_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/978-3-642-13869-0_16","volume-title":"Trust and Trustworthy Computing","author":"K Ables","year":"2010","unstructured":"Ables, K., Ryan, M.D.: Escrowed data and the digital envelope. In: Acquisti, A., Smith, S.W., Sadeghi, A.-R. (eds.) Trust 2010. LNCS, vol. 6101, pp. 246\u2013256. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-13869-0_16"},{"key":"5_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/978-3-319-25527-9_7","volume-title":"Programming Languages with Applications to Biology and Security","author":"O Almousa","year":"2015","unstructured":"Almousa, O., M\u00f6dersheim, S., Vigan\u00f2, L.: Alice and bob: reconciling formal models and implementation. In: Bodei, C., Ferrari, G.-L., Priami, C. (eds.) Programming Languages with Applications to Biology and Security. LNCS, vol. 9465, pp. 66\u201385. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-25527-9_7"},{"issue":"5","key":"5_CR4","doi-asserted-by":"publisher","first-page":"743","DOI":"10.3233\/JCS-140501","volume":"22","author":"M Arapinis","year":"2014","unstructured":"Arapinis, M., Phillips, J., Ritter, E., Ryan, M.D.: Statverif: verification of stateful processes. J. Comput. Secur. 22(5), 743\u2013821 (2014). https:\/\/doi.org\/10.3233\/JCS-140501","journal-title":"J. Comput. Secur."},{"issue":"3","key":"5_CR5","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/s10207-004-0055-7","volume":"4","author":"DA Basin","year":"2005","unstructured":"Basin, D.A., M\u00f6dersheim, S., Vigan\u00f2, L.: OFMC: a symbolic model checker for security protocols. Int. J. Inf. Sec. 4(3), 181\u2013208 (2005). https:\/\/doi.org\/10.1007\/s10207-004-0055-7","journal-title":"Int. J. Inf. Sec."},{"key":"5_CR6","doi-asserted-by":"publisher","unstructured":"Bhargavan, K., Corin, R., Deni\u00e9lou, P., Fournet, C., Leifer, J.J.: Cryptographic protocol synthesis and verification for multiparty sessions. In: Proceedings of the 22nd IEEE Computer Security Foundations Symposium, CSF 2009, Port Jefferson, New York, USA, 8\u201310 July 2009, pp. 124\u2013140. IEEE Computer Society (2009). https:\/\/doi.org\/10.1109\/CSF.2009.26","DOI":"10.1109\/CSF.2009.26"},{"key":"5_CR7","unstructured":"Br\u00f8ndum, C.: Languages and Translators for Stateful Protocols. Tech. rep., DTU, MSc. Thesis (2020). https:\/\/findit.dtu.dk\/en\/catalog\/2525864377"},{"key":"5_CR8","doi-asserted-by":"publisher","first-page":"417","DOI":"10.1007\/978-3-319-69659-1_23","volume-title":"Information Security Conference","author":"A Bruni","year":"2017","unstructured":"Bruni, A., Giustolisi, R., Schuermann, C.: Automated analysis of accountability. In: Nguyen, P., Zhou, J. (eds.) Information Security Conference, vol. 10599, pp. 417\u2013434. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-319-69659-1_23"},{"key":"5_CR9","doi-asserted-by":"publisher","unstructured":"Bruni, A., M\u00f6dersheim, S., Nielson, F., Nielson, H.R.: Set-pi: Set membership p-calculus. In: Fournet, C., Hicks, M.W., Vigan\u00f2, L. (eds.) IEEE 28th Computer Security Foundations Symposium, CSF 2015, Verona, Italy, 13\u201317 July 2015, pp. 185\u2013198. IEEE Computer Society (2015). https:\/\/doi.org\/10.1109\/CSF.2015.20","DOI":"10.1109\/CSF.2015.20"},{"key":"5_CR10","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1016\/j.jisa.2016.05.004","volume":"30","author":"M Bugliesi","year":"2016","unstructured":"Bugliesi, M., Calzavara, S., M\u00f6dersheim, S., Modesti, P.: Security protocol specification and verification with anbx. J. Inf. Secur. Appl. 30, 46\u201363 (2016). https:\/\/doi.org\/10.1016\/j.jisa.2016.05.004","journal-title":"J. Inf. Secur. Appl."},{"key":"5_CR11","doi-asserted-by":"publisher","unstructured":"Carbone, M., Guttman, J.D.: Choreographies with secure boxes and compromised principals. In: Bonchi, F., Grohmann, D., Spoletini, P., Tuosto, E. (eds.) Proceedings 2nd Interaction and Concurrency Experience: Structured Interactions, ICE 2009, Bologna, Italy, 31st August 2009. EPTCS, vol. 12, pp. 1\u201315 (2009). https:\/\/doi.org\/10.4204\/EPTCS.12.1","DOI":"10.4204\/EPTCS.12.1"},{"key":"5_CR12","doi-asserted-by":"publisher","unstructured":"Carbone, M., Guttman, J.D.: Execution models for choreographies and cryptoprotocols. In: Beresford, A.R., Gay, S.J. (eds.) Proceedings Second International Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software, PLACES 2009, New York, UK, 22nd March 2009. EPTCS, vol. 17, pp. 31\u201341 (2009). https:\/\/doi.org\/10.4204\/EPTCS.17.3","DOI":"10.4204\/EPTCS.17.3"},{"key":"5_CR13","doi-asserted-by":"publisher","unstructured":"Carbone, M., Honda, K., Yoshida, N.: Structured communication-centered programming for web services. ACM Trans. Program. Lang. Syst. 34(2), 8:1\u20138:78 (2012). https:\/\/doi.org\/10.1145\/2220365.2220367","DOI":"10.1145\/2220365.2220367"},{"key":"5_CR14","doi-asserted-by":"publisher","unstructured":"Carbone, M., Montesi, F.: Deadlock-freedom-by-design: multiparty asynchronous global programming. In: Giacobazzi, R., Cousot, R. (eds.) The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201913, Rome, Italy, 23\u201325 January 2013. pp. 263\u2013274. ACM (2013). https:\/\/doi.org\/10.1145\/2429069.2429101","DOI":"10.1145\/2429069.2429101"},{"key":"5_CR15","doi-asserted-by":"publisher","unstructured":"Cheval, V., Cortier, V., Turuani, M.: A little more conversation, a little less action, a lot more satisfaction: Global states in proverif. In: 31st IEEE Computer Security Foundations Symposium, CSF 2018, Oxford, United Kingdom, 9\u201312 July 2018, pp. 344\u2013358. IEEE Computer Society (2018). https:\/\/doi.org\/10.1109\/CSF.2018.00032","DOI":"10.1109\/CSF.2018.00032"},{"key":"5_CR16","doi-asserted-by":"crossref","unstructured":"Cortier, V., Galindo, D., K\u00fcsters, R., M\u00fcller, J., Truderung, T.: SoK: verifiability notions for e-voting protocols. In: IEEE Symposium on Security and Privacy, pp. 779\u2013798 (2016)","DOI":"10.1109\/SP.2016.52"},{"key":"5_CR17","doi-asserted-by":"publisher","unstructured":"Delaune, S., Kremer, S., Ryan, M.D., Steel, G.: Formal analysis of protocols based on TPM state registers. In: Proceedings of the 24th IEEE Computer Security Foundations Symposium, CSF 2011, Cernay-la-Ville, France, 27\u201329 June, 2011, pp. 66\u201380. IEEE Computer Society (2011). https:\/\/doi.org\/10.1109\/CSF.2011.12","DOI":"10.1109\/CSF.2011.12"},{"key":"5_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"523","DOI":"10.1007\/978-3-540-71209-1_41","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"SF Doghmi","year":"2007","unstructured":"Doghmi, S.F., Guttman, J.D., Thayer, F.J.: Searching for shapes in cryptographic protocols. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 523\u2013537. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71209-1_41"},{"issue":"2","key":"5_CR19","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","volume":"29","author":"D Dolev","year":"1983","unstructured":"Dolev, D., Yao, A.C.: On the security of public key protocols. IEEE Trans. Inf. Theory 29(2), 198\u2013208 (1983)","journal-title":"IEEE Trans. Inf. Theory"},{"key":"5_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/978-3-030-60347-2_5","volume-title":"Electronic Voting","author":"R Giustolisi","year":"2020","unstructured":"Giustolisi, R., Bruni, A., et al.: Privacy-preserving dispute resolution in the improved bingo voting. In: Krimmer, R. (ed.) E-Vote-ID 2020. LNCS, vol. 12455, pp. 67\u201383. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-60347-2_5"},{"key":"5_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-642-04444-1_11","volume-title":"Computer Security \u2013 ESORICS 2009","author":"N Guts","year":"2009","unstructured":"Guts, N., Fournet, C., Zappa Nardelli, F.: Reliable evidence: auditability by typing. In: Backes, M., Ning, P. (eds.) ESORICS 2009. LNCS, vol. 5789, pp. 168\u2013183. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-04444-1_11"},{"key":"5_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/978-3-319-27152-1_13","volume-title":"Security Standardisation Research","author":"JD Guttman","year":"2015","unstructured":"Guttman, J.D., Liskov, M.D., Ramsdell, J.D., Rowe, P.D.: Formal support for standardizing protocols with state. In: Chen, L., Matsuo, S. (eds.) SSR 2015. LNCS, vol. 9497, pp. 246\u2013265. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-27152-1_13"},{"key":"5_CR23","doi-asserted-by":"publisher","unstructured":"Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. J. ACM 63(1), 9:1\u20139:67 (2016). https:\/\/doi.org\/10.1145\/2827695","DOI":"10.1145\/2827695"},{"key":"5_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/978-3-642-04444-1_10","volume-title":"Computer Security \u2013 ESORICS 2009","author":"R Jagadeesan","year":"2009","unstructured":"Jagadeesan, R., Jeffrey, A., Pitcher, C., Riely, J.: Towards a theory of accountability and audit. In: Backes, M., Ning, P. (eds.) ESORICS 2009. LNCS, vol. 5789, pp. 152\u2013167. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-04444-1_10"},{"key":"5_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/978-3-642-15497-3_24","volume-title":"Computer Security \u2013 ESORICS 2010","author":"S Kremer","year":"2010","unstructured":"Kremer, S., Ryan, M., Smyth, B.: Election verifiability in electronic voting protocols. In: Gritzalis, D., Preneel, B., Theoharidou, M. (eds.) ESORICS 2010. LNCS, vol. 6345, pp. 389\u2013404. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15497-3_24"},{"key":"5_CR26","doi-asserted-by":"crossref","unstructured":"K\u00fcsters, R., Truderung, T., Vogt, A.: Accountability: definition and relationship to verifiability. In: CCS, pp. 526\u2013535. ACM (2010)","DOI":"10.1145\/1866307.1866366"},{"key":"5_CR27","doi-asserted-by":"crossref","unstructured":"Lowe, G.: Casper: a compiler for the analysis of security protocols. J. Comput. Secur. 6(1\u20132), 53\u201384 (1998). http:\/\/content.iospress.com\/articles\/journal-of-computer-security\/jcs106","DOI":"10.3233\/JCS-1998-61-204"},{"key":"5_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"696","DOI":"10.1007\/978-3-642-39799-8_48","volume-title":"Computer Aided Verification","author":"S Meier","year":"2013","unstructured":"Meier, S., Schmidt, B., Cremers, C., Basin, D.: The TAMARIN prover for the symbolic analysis of security protocols. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 696\u2013701. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_48"},{"issue":"1","key":"5_CR29","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(92)90008-4","volume":"100","author":"R Milner","year":"1992","unstructured":"Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes I and II. Inf. Comput. 100(1), 1\u201377 (1992)","journal-title":"Inf. Comput."},{"key":"5_CR30","doi-asserted-by":"publisher","unstructured":"M\u00f6dersheim, S.: Algebraic properties in alice and bob notation. In: Proceedings of the The Forth International Conference on Availability, Reliability and Security, ARES 2009, 16\u201319 March 2009, Fukuoka, Japan, pp. 433\u2013440. IEEE Computer Society (2009). https:\/\/doi.org\/10.1109\/ARES.2009.95","DOI":"10.1109\/ARES.2009.95"},{"key":"5_CR31","doi-asserted-by":"publisher","unstructured":"M\u00f6dersheim, S.: Abstraction by set-membership: verifying security protocols and web services with databases. In: Al-Shaer, E., Keromytis, A.D., Shmatikov, V. (eds.) Proceedings of the 17th ACM Conference on Computer and Communications Security, CCS 2010, Chicago, Illinois, USA, 4\u20138 October 2010, pp. 351\u2013360. ACM (2010). https:\/\/doi.org\/10.1145\/1866307.1866348","DOI":"10.1145\/1866307.1866348"},{"key":"5_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-662-49635-0_12","volume-title":"Principles of Security and Trust","author":"S M\u00f6dersheim","year":"2016","unstructured":"M\u00f6dersheim, S., Bruni, A.: AIF-$$\\omega $$: set-based protocol abstraction with countable families. In: Piessens, F., Vigan\u00f2, L. (eds.) POST 2016. LNCS, vol. 9635, pp. 233\u2013253. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49635-0_12"},{"key":"5_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-642-04444-1_21","volume-title":"Computer Security \u2013 ESORICS 2009","author":"S M\u00f6dersheim","year":"2009","unstructured":"M\u00f6dersheim, S., Vigan\u00f2, L.: Secure pseudonymous channels. In: Backes, M., Ning, P. (eds.) ESORICS 2009. LNCS, vol. 5789, pp. 337\u2013354. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-04444-1_21"},{"key":"5_CR34","unstructured":"W3C WS-CDL Working Group: Web services choreography description language version 1.0 (2004). http:\/\/www.w3.org\/TR\/ws-cdl-10\/"}],"container-title":["Lecture Notes in Computer Science","Protocols, Strands, and Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-91631-2_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,5,9]],"date-time":"2022-05-09T13:05:54Z","timestamp":1652101554000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-91631-2_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030916305","9783030916312"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-91631-2_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"19 November 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}