{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,11]],"date-time":"2026-03-11T01:43:10Z","timestamp":1773193390029,"version":"3.50.1"},"publisher-location":"Cham","reference-count":42,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030255398","type":"print"},{"value":"9783030255404","type":"electronic"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-25540-4_12","type":"book-chapter","created":{"date-parts":[[2019,7,12]],"date-time":"2019-07-12T11:02:35Z","timestamp":1562929355000},"page":"219-237","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Automated Synthesis of Secure Platform Mappings"],"prefix":"10.1007","author":[{"given":"Eunsuk","family":"Kang","sequence":"first","affiliation":[]},{"given":"St\u00e9phane","family":"Lafortune","sequence":"additional","affiliation":[]},{"given":"Stavros","family":"Tripakis","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,7,12]]},"reference":[{"key":"12_CR1","doi-asserted-by":"crossref","unstructured":"Akhawe, D., Barth, A., Lam, P.E., Mitchell, J.C., Song, D.: Towards a formal foundation of web security. In: CSF, pp. 290\u2013304 (2010)","DOI":"10.1109\/CSF.2010.27"},{"issue":"4","key":"12_CR2","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1016\/0020-0190(85)90056-0","volume":"21","author":"B Alpern","year":"1985","unstructured":"Alpern, B., Schneider, F.B.: Defining liveness. Inf. Process. Lett. 21(4), 181\u2013185 (1985)","journal-title":"Inf. Process. Lett."},{"key":"12_CR3","doi-asserted-by":"crossref","unstructured":"Alur, R., et al.: Syntax-guided synthesis. In: FMCAD, pp. 1\u20138 (2013)","DOI":"10.1109\/FMCAD.2013.6679385"},{"issue":"6","key":"12_CR4","doi-asserted-by":"publisher","first-page":"593","DOI":"10.1007\/BF00291051","volume":"25","author":"R-J Back","year":"1988","unstructured":"Back, R.-J.: A calculus of refinements for program derivations. Acta Inf. 25(6), 593\u2013624 (1988)","journal-title":"Acta Inf."},{"key":"12_CR5","doi-asserted-by":"crossref","unstructured":"Bansal, C., Bhargavan, K., Maffeis, S.: Discovering concrete attacks on website authorization by formal analysis. In: CSF, pp. 247\u2013262 (2012)","DOI":"10.1109\/CSF.2012.27"},{"key":"12_CR6","doi-asserted-by":"crossref","unstructured":"Ben-David, S., Chechik, M., Uchitel, S.: Merging partial behaviour models with different vocabularies. In: CONCUR, pp. 91\u2013105 (2013)","DOI":"10.1007\/978-3-642-40184-8_8"},{"key":"12_CR7","doi-asserted-by":"crossref","unstructured":"Bhargavan, K., Corin, R., Deni\u00e9lou, P.-M., Fournet, C., Leifer, J.J.: Cryptographic protocol synthesis and verification for multiparty sessions. In: CSF, pp. 124\u2013140 (2009)","DOI":"10.1109\/CSF.2009.26"},{"key":"12_CR8","doi-asserted-by":"crossref","unstructured":"Brunet, G., Chechik, M., Easterbrook, S., Nejati, S., Niu, N., Sabetzadeh, M.: A manifesto for model merging. In: Proceedings of the 2006 International Workshop on Global Integrated Model Management, pp. 5\u201312 (2006)","DOI":"10.1145\/1138304.1138307"},{"key":"12_CR9","unstructured":"Chari, S., Jutla, C.S., Roy, A.: Universally Composable Security Analysis of OAuth v2.0. IACR Cryptology ePrint Archive, 2011, 526 (2011)"},{"key":"12_CR10","doi-asserted-by":"crossref","unstructured":"Chen, E.Y., Pei, Y., Chen, S., Tian, Y., Kotcher, R., Tague, P.: OAuth Demystified for Mobile Application Developers. In: CCS, pp. 892\u2013903 (2014)","DOI":"10.1145\/2660267.2660323"},{"key":"12_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). \n                      https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"12_CR12","doi-asserted-by":"crossref","unstructured":"Dutertre, B.: Yices 2.2. In: CAV, pp. 737\u2013744 (2014)","DOI":"10.1007\/978-3-319-08867-9_49"},{"key":"12_CR13","doi-asserted-by":"crossref","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible sat-solver. In: SAT, pp. 502\u2013518 (2003)","DOI":"10.1007\/978-3-540-24605-3_37"},{"key":"12_CR14","doi-asserted-by":"crossref","unstructured":"Fett, D., K\u00fcsters, R., Schmitz, G.: An expressive model for the web infrastructure: definition and application to the browser ID SSO system. In: 2014 IEEE Symposium on Security and Privacy, SP 2014, Berkeley, 18\u201321 May 2014, pp. 673\u2013688 (2014)","DOI":"10.1109\/SP.2014.49"},{"key":"12_CR15","unstructured":"OAuth Working Group. OAuth Security Advisory: 2009.1 \u201cSession Fixation\u201d. \n                      https:\/\/oauth.net\/advisories\/2009-1\n                      \n                     (2009)"},{"key":"12_CR16","unstructured":"OAuth Working Group. OAuth Security Advisory: 2014.1 \u201cCovert Redirect\u201d. \n                      https:\/\/oauth.net\/advisories\/2014-1-covert-redirect\n                      \n                     (2014)"},{"key":"12_CR17","unstructured":"Hanmer. E.: OAuth 2.0 and the Road to Hell. \n                      https:\/\/hueniverse.com\/2012\/07\/26\/oauth-2-0-and-the-road-to-hell\n                      \n                     (2012)"},{"key":"12_CR18","doi-asserted-by":"crossref","unstructured":"Hawkins, P., Aiken, A., Fisher, K., Rinard, M.C., Sagiv, M.: Data representation synthesis. In: PLDI, pp. 38\u201349 (2011)","DOI":"10.1145\/1993316.1993504"},{"key":"12_CR19","doi-asserted-by":"crossref","unstructured":"Hawkins, P., Aiken, A., Fisher, K., Rinard, M.C., Sagiv, M.: Concurrent data representation synthesis. In: PLDI, pp. 417\u2013428 (2012)","DOI":"10.1145\/2345156.2254114"},{"key":"12_CR20","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/BF00289507","volume":"1","author":"CAR Hoare","year":"1972","unstructured":"Hoare, C.A.R.: Proof of correctness of data representations. Acta Inf. 1, 271\u2013281 (1972)","journal-title":"Acta Inf."},{"issue":"8","key":"12_CR21","doi-asserted-by":"publisher","first-page":"666","DOI":"10.1145\/359576.359585","volume":"21","author":"CAR Hoare","year":"1978","unstructured":"Hoare, C.A.R.: Communicating sequential processes. Commun. ACM 21(8), 666\u2013677 (1978)","journal-title":"Commun. ACM"},{"key":"12_CR22","doi-asserted-by":"crossref","unstructured":"Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. In: POPL, pp. 273\u2013284 (2008)","DOI":"10.1145\/1328897.1328472"},{"key":"12_CR23","unstructured":"Internet Engineering Task Force. The OAuth 1.0 Protocol. \n                      https:\/\/tools.ietf.org\/html\/rfc5849\n                      \n                     (2010)"},{"key":"12_CR24","unstructured":"Internet Engineering Task Force. OAuth Authorization Framework. \n                      http:\/\/tools.ietf.org\/html\/rfc6749\n                      \n                     (2014)"},{"key":"12_CR25","volume-title":"Software Abstractions: Logic, Language, and Analysis","author":"D Jackson","year":"2006","unstructured":"Jackson, D.: Software Abstractions: Logic, Language, and Analysis. MIT Press, Cambridge (2006)"},{"key":"12_CR26","doi-asserted-by":"crossref","unstructured":"Jha, S., Gulwani, S., Seshia, S.A., Tiwari, A.: Oracle-guided component-based program synthesis. In: ICSE, pp. 215\u2013224 (2010)","DOI":"10.1145\/1806799.1806833"},{"key":"12_CR27","unstructured":"Kang, E., Lafortune, S., Tripakis, S.: Synthesis of property-preserving mappings. CoRR, abs\/1705.03618 (2017)"},{"key":"12_CR28","doi-asserted-by":"crossref","unstructured":"Kang, E., Milicevic, A., Jackson, D.: Multi-representational security analysis. In: FSE (2016)","DOI":"10.1145\/2950290.2950356"},{"issue":"2","key":"12_CR29","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1109\/TSE.1977.229904","volume":"3","author":"L Lamport","year":"1977","unstructured":"Lamport, L.: Proving the correctness of multiprocess programs. IEEE Trans. Software Eng. 3(2), 125\u2013143 (1977)","journal-title":"IEEE Trans. Software Eng."},{"issue":"10","key":"12_CR30","doi-asserted-by":"publisher","first-page":"613","DOI":"10.1145\/362375.362389","volume":"16","author":"BW Lampson","year":"1973","unstructured":"Lampson, B.W.: A note on the confinement problem. Commun. ACM 16(10), 613\u2013615 (1973)","journal-title":"Commun. ACM"},{"key":"12_CR31","doi-asserted-by":"crossref","unstructured":"Maoz, S., Ringert, J.O., Rumpe, B.: Synthesis of component and connector models from crosscutting structural views. In: ESEC\/FSE, pp. 444\u2013454 (2013)","DOI":"10.1145\/2491411.2491414"},{"key":"12_CR32","doi-asserted-by":"crossref","unstructured":"Nejati, S., Sabetzadeh, M., Chechik, M., Easterbrook, S.M., Zave, P.: Matching and merging of statecharts specifications. In: ICSE, pp. 54\u201364 (2007)","DOI":"10.1109\/ICSE.2007.50"},{"key":"12_CR33","doi-asserted-by":"crossref","unstructured":"Pai, S., Sharma, Y., Kumar, S., Pai, R.M., Singh, S.: Formal verification of OAuth 2.0 using Alloy framework. In: Communication Systems and Network Technologies (CSNT), pp. 655\u2013659. IEEE (2011)","DOI":"10.1109\/CSNT.2011.141"},{"key":"12_CR34","doi-asserted-by":"crossref","unstructured":"Pottinger, R., Bernstein, P.A.: Merging models based on given correspondences. In: VLDB, pp. 826\u2013873 (2003)","DOI":"10.1016\/B978-012722442-8\/50081-1"},{"issue":"6","key":"12_CR35","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1109\/54.970421","volume":"18","author":"AL Sangiovanni-Vincentelli","year":"2001","unstructured":"Sangiovanni-Vincentelli, A.L., Martin, G.: Platform-based design and software design methodology for embedded systems. IEEE Design Test Comput. 18(6), 23\u201333 (2001)","journal-title":"IEEE Design Test Comput."},{"key":"12_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1007\/978-3-642-10672-9_3","volume-title":"Programming Languages and Systems","author":"A Solar-Lezama","year":"2009","unstructured":"Solar-Lezama, A.: The sketching approach to program synthesis. In: Hu, Z. (ed.) APLAS 2009. LNCS, vol. 5904, pp. 4\u201313. Springer, Heidelberg (2009). \n                      https:\/\/doi.org\/10.1007\/978-3-642-10672-9_3"},{"key":"12_CR37","doi-asserted-by":"crossref","unstructured":"Solar-Lezama, A., Rabbah, R., Bod\u00edk, R., Ebcio\u011flu, K.: Programming by sketching for bit-streaming programs. In: Proceedings of the 2005 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2005, pp. 281\u2013294. ACM (2005)","DOI":"10.1145\/1065010.1065045"},{"key":"12_CR38","doi-asserted-by":"crossref","unstructured":"Solar-Lezama, A., Tancau, L., Bod\u00edk, R., Seshia, S.A., Saraswat, V.A.: Combinatorial sketching for finite programs. In: ASPLOS, pp. 404\u2013415 (2006)","DOI":"10.1145\/1168918.1168907"},{"key":"12_CR39","doi-asserted-by":"crossref","unstructured":"Sun, S.-T., Beznosov, K.: The devil is in the (implementation) details: an empirical analysis of OAuth SSO systems. In: CCS, pp. 378\u2013390 (2012)","DOI":"10.1145\/2382196.2382238"},{"key":"12_CR40","doi-asserted-by":"crossref","unstructured":"Uchitel, S., Chechik, M.: Merging partial behavioural models. In: SIGSOFT FSE, pp. 43\u201352 (2004)","DOI":"10.1145\/1041685.1029904"},{"key":"12_CR41","doi-asserted-by":"crossref","unstructured":"Wang, R., Chen, S., Wang, X.: Signing me onto your accounts through facebook and google: a traffic-guided security study of commercially deployed single-sign-on web services. In: IEEE Symposium on Security and Privacy, pp. 365\u2013379 (2012)","DOI":"10.1109\/SP.2012.30"},{"issue":"12","key":"12_CR42","doi-asserted-by":"publisher","first-page":"2273","DOI":"10.3923\/itj.2013.2273.2285","volume":"12","author":"X Xu","year":"2013","unstructured":"Xu, X., Niu, L., Meng, B.: Automatic verification of security properties of OAuth 2.0 protocol with cryptoverif in computational model. Inf. Technol. J. 12(12), 2273 (2013)","journal-title":"Inf. Technol. J."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-25540-4_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,12]],"date-time":"2019-07-12T11:04:11Z","timestamp":1562929451000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-25540-4_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030255398","9783030255404"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-25540-4_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"12 July 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"New York City, NY","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 July 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 July 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav0","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2019\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"258","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"67","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"26% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"9","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}