{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,30]],"date-time":"2025-05-30T23:40:09Z","timestamp":1748648409470,"version":"3.41.0"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319255262"},{"type":"electronic","value":"9783319255279"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-25527-9_7","type":"book-chapter","created":{"date-parts":[[2015,10,7]],"date-time":"2015-10-07T11:08:43Z","timestamp":1444216123000},"page":"66-85","source":"Crossref","is-referenced-by-count":12,"title":["Alice and Bob: Reconciling Formal Models and Implementation"],"prefix":"10.1007","author":[{"given":"Omar","family":"Almousa","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":[[2015,11,20]]},"reference":[{"issue":"1\u20132","key":"7_CR1","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1016\/j.tcs.2006.08.032","volume":"367","author":"M Abadi","year":"2006","unstructured":"Abadi, M., Cortier, V.: Deciding knowledge in security protocols under equational theories. Theoret. Comput. Sci. 367(1\u20132), 2\u201332 (2006)","journal-title":"Theoret. Comput. Sci."},{"key":"7_CR2","doi-asserted-by":"crossref","unstructured":"Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: POPL, pp. 104\u2013115. ACM (2001)","DOI":"10.1145\/373243.360213"},{"key":"7_CR3","unstructured":"Almousa, O., M\u00f6dersheim, S., Modesti, P., Vigan\u00f2, L.: Typing and Compositionality for Security Protocols: A Generalization to the Geometric Fragment. In: ESORICS 2015, 2015, to appear, http:\/\/compute.dtu.dk\/~samo"},{"key":"7_CR4","unstructured":"Almousa, O., M\u00f6dersheim, S., Vigan\u00f2, L.: Alice and Bob: reconciling formal models and implementation (Extended Version). Technical report 2014-10, DTU Compute (2015). http:\/\/www.imm.dtu.dk\/~samo\/"},{"key":"7_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/978-3-642-28756-5_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Armando","year":"2012","unstructured":"Armando, A., et al.: The AVANTSSAR platform for the automated validation of trust and security of service-oriented architectures. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 267\u2013282. Springer, Heidelberg (2012)"},{"key":"7_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1007\/978-3-642-28891-3_34","volume-title":"NASA Formal Methods","author":"C Hri\u0163cu","year":"2012","unstructured":"Hri\u0163cu, C., Busenius, A., Backes, M.: On the development and formalization of an extensible code generator for real life security protocols. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol. 7226, pp. 371\u2013387. Springer, Heidelberg (2012)"},{"key":"7_CR7","doi-asserted-by":"crossref","unstructured":"Basin, D., Keller, M., Radomirovi\u0107, S., Sasse, R.: Alice and Bob meet equational theories. In: Festschrift for Jos\u00e9 Meseguer on his 65th Birthday (2015)","DOI":"10.1007\/978-3-319-23165-5_7"},{"key":"7_CR8","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2133375.2133378","volume":"15","author":"K Bhargavan","year":"2012","unstructured":"Bhargavan, K., Fournet, C., Corin, R., Z\u0103linescu, E.: Verified cryptographic implementations for TLS. ACM Trans. Inf. Syst. Secur. 15, 1 (2012). Article 3","journal-title":"ACM Trans. Inf. Syst. Secur."},{"key":"7_CR9","doi-asserted-by":"crossref","unstructured":"Bhargavan, K., Fournet, C., Gordon, A.D., Tse, S.: Verified interoperable implementations of security protocols. In: CSF 19, pp. 139\u2013152. IEEE (2006)","DOI":"10.1007\/11841197_6"},{"key":"7_CR10","doi-asserted-by":"crossref","unstructured":"Blanchet, B.: An efficient cryptographic protocol verifier based on Prolog rules. In: CSF, pp. 82\u201396. IEEE (2001)","DOI":"10.1109\/CSFW.2001.930138"},{"issue":"3","key":"7_CR11","doi-asserted-by":"publisher","first-page":"347","DOI":"10.3233\/JCS-2005-13302","volume":"13","author":"C Bodei","year":"2005","unstructured":"Bodei, C., Buchholtz, M., Degano, P., Nielson, F., Riis Nielson, H.: Static validation of security protocols. J. Comput. Secur. 13(3), 347\u2013390 (2005)","journal-title":"J. Comput. Secur."},{"issue":"3","key":"7_CR12","doi-asserted-by":"publisher","first-page":"484","DOI":"10.1016\/j.tcs.2007.09.005","volume":"389","author":"S Briais","year":"2007","unstructured":"Briais, S., Nestmann, U.: A formal semantics for protocol narrations. Theoret. Comput. Sci. 389(3), 484\u2013511 (2007)","journal-title":"Theoret. Comput. Sci."},{"issue":"1","key":"7_CR13","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1016\/j.tcs.2006.08.041","volume":"367","author":"C Caleiro","year":"2006","unstructured":"Caleiro, C., Vigan\u00f2, L., Basin, D.: On the semantics of Alice&Bob specifications of security protocols. Theoret. Comput. Sci. 367(1), 88\u2013122 (2006)","journal-title":"Theoret. Comput. Sci."},{"issue":"3","key":"7_CR14","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1016\/j.ipl.2009.11.004","volume":"110","author":"Y Chevalier","year":"2010","unstructured":"Chevalier, Y., Rusinowitch, M.: Compiling and securing cryptographic protocols. Inf. Process. Lett. 110(3), 116\u2013122 (2010)","journal-title":"Inf. Process. Lett."},{"key":"7_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/11495628_4","volume-title":"Scenarios: Models, Transformations and Tools","author":"CJF Cremers","year":"2005","unstructured":"Cremers, C.J.F., Mauw, S.: Operational semantics of security protocols. In: Leue, S., Syst\u00e4, T.J. (eds.) Scenarios: Models, Transformations and Tools. LNCS, vol. 3466, pp. 66\u201389. Springer, Heidelberg (2005)"},{"key":"7_CR16","doi-asserted-by":"crossref","unstructured":"Dierks, T., Rescorla, E.: RFC 5246: The Transport Layer Security (TLS) Protocol, Version 1.2 (2008)","DOI":"10.17487\/rfc5246"},{"key":"7_CR17","unstructured":"FutureID Project: Deliverable D42.6: Specification of execution environment (2014). www.futureid.eu"},{"key":"7_CR18","unstructured":"FutureID Project: Deliverable D42.8: APS Files for Selected Authentication Protocols (2015). www.futureid.eu"},{"key":"7_CR19","unstructured":"German Federal Office for Information Security (BSI): Advanced Security Mechanism for Machine Readable Travel Documents (2008). www.bsi.bund.de\/EN\/Publications\/TechnicalGuidelines\/TR03110\/BSITR03110"},{"key":"7_CR20","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/3-540-44404-1_10","volume-title":"Logic for Programming and Automated Reasoning","author":"F Jacquemard","year":"2000","unstructured":"Jacquemard, F., Rusinowitch, M., Vigneron, L.: Compiling and verifying security protocols. In: Parigot, M., Voronkov, A. (eds.) LPAR 2000. LNCS (LNAI), vol. 1955, pp. 131\u2013160. Springer, Heidelberg (2000)"},{"key":"7_CR21","doi-asserted-by":"crossref","unstructured":"K\u00fcsters, R., Truderung, T.: Using ProVerif to analyze protocols with Diffie-Hellman exponentiation. In: CSF, pp. 157\u2013171. IEEE (2009)","DOI":"10.1109\/CSF.2009.17"},{"key":"7_CR22","doi-asserted-by":"crossref","unstructured":"Lowe, G.: Casper: a compiler for the analysis of security protocols. In: CSFW, pp. 18\u201330. IEEE (1997)","DOI":"10.1109\/CSFW.1997.596779"},{"key":"7_CR23","unstructured":"Millen, J.: CAPSL: common authentication protocol specification language. Technical report, Technical Report MP 97B48, The MITRE Corporation (1997)"},{"key":"7_CR24","doi-asserted-by":"crossref","unstructured":"M\u00f6dersheim, S.: Algebraic properties in Alice and Bob notation. In: ARES 2009, pp. 433\u2013440. IEEE (2009)","DOI":"10.1109\/ARES.2009.95"},{"key":"7_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/978-3-642-29420-4_14","volume-title":"Formal Aspects of Security and Trust","author":"S M\u00f6dersheim","year":"2012","unstructured":"M\u00f6dersheim, S.: Diffie-Hellman without difficulty. In: Barthe, G., Datta, A., Etalle, S. (eds.) FAST 2011. LNCS, vol. 7140, pp. 214\u2013229. Springer, Heidelberg (2012)"},{"key":"7_CR26","doi-asserted-by":"crossref","unstructured":"M\u00f6dersheim, S., Katsoris, G.: A sound abstraction of the parsing problem. In: CSF, pp. 259\u2013273. IEEE (2014)","DOI":"10.1109\/CSF.2014.26"},{"key":"7_CR27","doi-asserted-by":"crossref","unstructured":"Modesti, P.: Efficient Java code generation of security protocols specified in AnB\/AnBx. In: STM (2014)","DOI":"10.1007\/978-3-319-11851-2_17"},{"issue":"1","key":"7_CR28","doi-asserted-by":"publisher","first-page":"191","DOI":"10.3233\/JCS-1999-72-304","volume":"7","author":"FJ Thayer","year":"1999","unstructured":"Thayer, F.J., Herzog, J.C., Guttman, J.D.: Strand spaces: proving security protocols correct. J. Comput. Secur. 7(1), 191\u2013230 (1999)","journal-title":"J. Comput. Secur."},{"key":"7_CR29","series-title":"IFIP On-Line Library in Computer Science","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/11397427_3","volume-title":"Certification and Security in Inter-Organizational E-Service","author":"B Tobler","year":"2005","unstructured":"Tobler, B., Hutchison, A.C.: Generating network security protocol implementations from formal specifications. In: Nardelli, E., Talamo, M. (eds.) Certification and Security in Inter-Organizational E-Service. IFIP, vol. 177, pp. 33\u201354. Springer, Heidelberg (2005)"}],"container-title":["Lecture Notes in Computer Science","Programming Languages with Applications to Biology and Security"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-25527-9_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,30]],"date-time":"2025-05-30T22:58:59Z","timestamp":1748645939000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-25527-9_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319255262","9783319255279"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-25527-9_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}