{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,7,18]],"date-time":"2024-07-18T05:58:25Z","timestamp":1721282305856},"reference-count":65,"publisher":"Association for Computing Machinery (ACM)","issue":"3","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Priv. Secur."],"published-print":{"date-parts":[[2020,8,31]]},"abstract":"Over the last few years, there has been an almost exponential increase in the number of mobile applications that deal with sensitive data, such as applications for e-commerce or health. When dealing with sensitive data, classical authentication solutions based on username-password pairs are not enough, and multi-factor authentication solutions that combine two or more authentication factors of different categories are required instead. Even if several solutions are currently used, their security analyses have been performed informally or semiformally at best, and without a reference model and a precise definition of the multi-factor authentication property. This makes a comparison among the different solutions both complex and potentially misleading. In this article, we first present the design of two reference models for native applications based on the requirements of two real-world use-case scenarios. Common features between them are the use of one-time password approaches and the support of a single sign-on experience. Then, we provide a formal specification of our threat model and the security goals, and discuss the automated security analysis that we performed. Our formal analysis validates the security goals of the two reference models we propose and provides an important building block for the formal analysis of different multi-factor authentication solutions.<\/jats:p>","DOI":"10.1145\/3386685","type":"journal-article","created":{"date-parts":[[2020,6,7]],"date-time":"2020-06-07T00:46:20Z","timestamp":1591490780000},"page":"1-37","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Formal Analysis of Mobile Multi-Factor Authentication with Single Sign-On Login"],"prefix":"10.1145","volume":"23","author":[{"given":"Giada","family":"Sciarretta","sequence":"first","affiliation":[{"name":"Security 8 Trust, FBK, Trento, Italia"}]},{"given":"Roberto","family":"Carbone","sequence":"additional","affiliation":[{"name":"Security 8 Trust, FBK, Trento, Italia"}]},{"given":"Silvio","family":"Ranise","sequence":"additional","affiliation":[{"name":"Security 8 Trust, FBK, Trento, Italia"}]},{"ORCID":"http:\/\/orcid.org\/0000-0001-9916-271X","authenticated-orcid":false,"given":"Luca","family":"Vigan\u00f2","sequence":"additional","affiliation":[{"name":"Department of Informatics, King\u2019s College London, London, United Kingdom"}]}],"member":"320","published-online":{"date-parts":[[2020,6,6]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"Android. 2017. Handling Android App Links. Retrieved from https:\/\/developer.android.com\/training\/app-links\/index.html. Android. 2017. Handling Android App Links. Retrieved from https:\/\/developer.android.com\/training\/app-links\/index.html."},{"key":"e_1_2_1_2_1","unstructured":"Android. 2019. Android Security 8 Privacy 2018 Year in Review. Retrieved from https:\/\/source.android.com\/security\/reports\/Google_Android_Security_2018_Report_Final.pdf. Android. 2019. Android Security 8 Privacy 2018 Year in Review. Retrieved from https:\/\/source.android.com\/security\/reports\/Google_Android_Security_2018_Report_Final.pdf."},{"key":"e_1_2_1_3_1","volume-title":"Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'12)","author":"Armando A.","unstructured":"A. Armando , W. Arsac , T. Avanesov , M. Barletta , A. Calvi , A. Cappai , R. Carbone , Y. Chevalier , L. Compagna , J. Cu\u00e9llar , G. Erzse , S. Frau , M. Minea , S. M\u00f6dersheim , D. von Oheimb , G. Pellegrino , S.E. Ponta , M. Rocchetto , M. Rusinowitch , M. Torabi Dashti , M. Turuani , and L. Vigan\u00f2 . 2012. The AVANTSSAR platform for the automated validation of trust and security of service-oriented architectures . In Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'12) . Springer, 267--282. https:\/\/doi.org\/10.1007\/978-3-642-28756-5_19 10.1007\/978-3-642-28756-5_19 A. Armando, W. Arsac, T. Avanesov, M. Barletta, A. Calvi, A. Cappai, R. Carbone, Y. Chevalier, L. Compagna, J. Cu\u00e9llar, G. Erzse, S. Frau, M. Minea, S. M\u00f6dersheim, D. von Oheimb, G. Pellegrino, S.E. Ponta, M. Rocchetto, M. Rusinowitch, M. Torabi Dashti, M. Turuani, and L. Vigan\u00f2. 2012. The AVANTSSAR platform for the automated validation of trust and security of service-oriented architectures. In Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'12). Springer, 267--282. https:\/\/doi.org\/10.1007\/978-3-642-28756-5_19"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-015-0385-y"},{"key":"e_1_2_1_5_1","volume-title":"Proceedings of the 6th ACM Workshop on Formal Methods in Security Engineering (FMSE\u201908)","author":"Armando A.","unstructured":"A. Armando , R. Carbone , L. Compagna , J. Cu\u00e9llar , and L. Tobarra . 2008. Formal analysis of SAML 2.0 web browser single sign-on: Breaking the SAML-based single sign-on for Google apps . In Proceedings of the 6th ACM Workshop on Formal Methods in Security Engineering (FMSE\u201908) . 1--10. https:\/\/doi.org\/10.1145\/1456396.1456397 10.1145\/1456396.1456397 A. Armando, R. Carbone, L. Compagna, J. Cu\u00e9llar, and L. Tobarra. 2008. Formal analysis of SAML 2.0 web browser single sign-on: Breaking the SAML-based single sign-on for Google apps. In Proceedings of the 6th ACM Workshop on Formal Methods in Security Engineering (FMSE\u201908). 1--10. https:\/\/doi.org\/10.1145\/1456396.1456397"},{"key":"e_1_2_1_6_1","volume-title":"Proceedings of 7th International Conference on Network and System Security (NSS\u201913)","author":"Armando A.","unstructured":"A. Armando , R. Carbone , and L. L. Zanetti . 2013. Formal modeling and automatic security analysis of two-factor and two-channel authentication protocols . In Proceedings of 7th International Conference on Network and System Security (NSS\u201913) . 728--734. https:\/\/doi.org\/10.1007\/978-3-642-38631-2_63 10.1007\/978-3-642-38631-2_63 A. Armando, R. Carbone, and L. L. Zanetti. 2013. Formal modeling and automatic security analysis of two-factor and two-channel authentication protocols. In Proceedings of 7th International Conference on Network and System Security (NSS\u201913). 728--734. https:\/\/doi.org\/10.1007\/978-3-642-38631-2_63"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10207-007-0041-y"},{"key":"e_1_2_1_8_1","unstructured":"AVANTSSAR Project. 2008. Deliverable D2.3 (update) ASLan++ specification and tutorial. Retrieved from http:\/\/www.avantssar.eu\/pdf\/deliverables\/avantssar-d2-3_update.pdf. Also available at https:\/\/stfbk.github.io\/complementary\/TOPS2020. AVANTSSAR Project. 2008. Deliverable D2.3 (update) ASLan++ specification and tutorial. Retrieved from http:\/\/www.avantssar.eu\/pdf\/deliverables\/avantssar-d2-3_update.pdf. Also available at https:\/\/stfbk.github.io\/complementary\/TOPS2020."},{"key":"e_1_2_1_9_1","volume-title":"Proceedings of 25th IEEE Computer Security Foundations Symposium (CSF\u201912)","author":"Bansal C.","year":"2012","unstructured":"C. Bansal , K. Bhargavan , and S. Maffeis . 2012. Discovering concrete attacks on website authorization by formal analysis . In Proceedings of 25th IEEE Computer Security Foundations Symposium (CSF\u201912) . 247--262. https:\/\/doi.org\/10.1109\/CSF. 2012 .27 10.1109\/CSF.2012.27 C. Bansal, K. Bhargavan, and S. Maffeis. 2012. Discovering concrete attacks on website authorization by formal analysis. In Proceedings of 25th IEEE Computer Security Foundations Symposium (CSF\u201912). 247--262. https:\/\/doi.org\/10.1109\/CSF.2012.27"},{"key":"#cr-split#-e_1_2_1_10_1.1","doi-asserted-by":"crossref","unstructured":"D. A. Basin C. Cremers and C. A. Meadows. 2018. Model checking security protocols. In Handbook of Model Checking. 727--762. DOI:https:\/\/doi.org\/10.1007\/978-3-319-10575-8_22 10.1007\/978-3-319-10575-8_22","DOI":"10.1007\/978-3-319-10575-8_22"},{"key":"#cr-split#-e_1_2_1_10_1.2","doi-asserted-by":"crossref","unstructured":"D. A. Basin C. Cremers and C. A. Meadows. 2018. Model checking security protocols. In Handbook of Model Checking. 727--762. DOI:https:\/\/doi.org\/10.1007\/978-3-319-10575-8_22","DOI":"10.1007\/978-3-319-10575-8_22"},{"key":"e_1_2_1_11_1","unstructured":"BBA. 2017. An app-etite for banking. Retrieved from https:\/\/www.bba.org.uk\/wp-content\/uploads\/2017\/06\/WWBN-IV.pdf. BBA. 2017. An app-etite for banking. Retrieved from https:\/\/www.bba.org.uk\/wp-content\/uploads\/2017\/06\/WWBN-IV.pdf."},{"key":"e_1_2_1_12_1","unstructured":"B. Blanchet B. Smyth V. Cheval and M. Sylvestre. 2018. ProVerif 2.00: Automatic Cryptographic Protocol Verifier User Manual and Tutorial. Retrieved from https:\/\/prosecco.gforge.inria.fr\/personal\/bblanche\/proverif\/manual.pdf. B. Blanchet B. Smyth V. Cheval and M. Sylvestre. 2018. ProVerif 2.00: Automatic Cryptographic Protocol Verifier User Manual and Tutorial. Retrieved from https:\/\/prosecco.gforge.inria.fr\/personal\/bblanche\/proverif\/manual.pdf."},{"key":"e_1_2_1_13_1","volume-title":"Proceedings of the ACM Conference on Computer and Communications Security (CCS\u201914)","author":"Chen E.","unstructured":"E. Chen , Y. Pei , S. Chen , Y. Tian , R. Kotcher , and P. Tague . 2014. OAuth demystified for mobile application developers . In Proceedings of the ACM Conference on Computer and Communications Security (CCS\u201914) . https:\/\/doi.org\/10.1145\/2660267.2660323 10.1145\/2660267.2660323 E. Chen, Y. Pei, S. Chen, Y. Tian, R. Kotcher, and P. Tague. 2014. OAuth demystified for mobile application developers. In Proceedings of the ACM Conference on Computer and Communications Security (CCS\u201914). https:\/\/doi.org\/10.1145\/2660267.2660323"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.1983.1056650"},{"key":"e_1_2_1_15_1","unstructured":"European Banking Authority. 2014. Final guidelines on the security of Internet payments. European Banking Authority. 2014. Final guidelines on the security of Internet payments."},{"key":"e_1_2_1_16_1","volume-title":"Regulation EU 2016\/679 on the protection of natural persons with regard to the processing of personal data and on the free movement of such data, and repealing Directive 95\/46\/EC (GDPR).","author":"European Commission","year":"2016","unstructured":"European Commission . 2016 . Regulation EU 2016\/679 on the protection of natural persons with regard to the processing of personal data and on the free movement of such data, and repealing Directive 95\/46\/EC (GDPR). European Commission. 2016. Regulation EU 2016\/679 on the protection of natural persons with regard to the processing of personal data and on the free movement of such data, and repealing Directive 95\/46\/EC (GDPR)."},{"key":"e_1_2_1_17_1","unstructured":"European Parliament. 2014. Regulation 910\/2014 of the European Parliament and of the Council of 23 July 2014 on electronic identification and trust services for electronic transactions in the internal market and repealing Directive 1999\/93\/EC. Retrieved from http:\/\/eur-lex.europa.eu\/legal-content\/EN\/TXT\/PDF\/?uri=CELEX:32014R09108from=EN. European Parliament. 2014. Regulation 910\/2014 of the European Parliament and of the Council of 23 July 2014 on electronic identification and trust services for electronic transactions in the internal market and repealing Directive 1999\/93\/EC. Retrieved from http:\/\/eur-lex.europa.eu\/legal-content\/EN\/TXT\/PDF\/?uri=CELEX:32014R09108from=EN."},{"key":"e_1_2_1_18_1","unstructured":"Facebook. 2015. Getting started with the Facebook SDK for Android. Retrieved from https:\/\/developers.facebook.com\/docs\/android\/getting-started\/facebook-sdk-for-android\/. Facebook. 2015. Getting started with the Facebook SDK for Android. Retrieved from https:\/\/developers.facebook.com\/docs\/android\/getting-started\/facebook-sdk-for-android\/."},{"key":"#cr-split#-e_1_2_1_19_1.1","doi-asserted-by":"crossref","unstructured":"S. Fahl M. Harbach M. Oltrogge T. Muders and M. Smith. 2013. Hey you get off of my clipboard-On how usability trumps security in Android password managers. In Financial Cryptography and Data Security. 144--161. DOI:https:\/\/doi.org\/10.1007\/978-3-642-39884-1_12 10.1007\/978-3-642-39884-1_12","DOI":"10.1007\/978-3-642-39884-1_12"},{"key":"#cr-split#-e_1_2_1_19_1.2","doi-asserted-by":"crossref","unstructured":"S. Fahl M. Harbach M. Oltrogge T. Muders and M. Smith. 2013. Hey you get off of my clipboard-On how usability trumps security in Android password managers. In Financial Cryptography and Data Security. 144--161. DOI:https:\/\/doi.org\/10.1007\/978-3-642-39884-1_12","DOI":"10.1007\/978-3-642-39884-1_12"},{"key":"e_1_2_1_20_1","volume-title":"Proceedings of the 35th IEEE Symposium on Security and Privacy (S8P\u201914)","author":"Fett D.","unstructured":"D. Fett , R. K\u00fcsters , and G. Schmitz . 2014. An expressive model for the web infrastructure: Definition and application to the BrowserID SSO system . In Proceedings of the 35th IEEE Symposium on Security and Privacy (S8P\u201914) . IEEE Computer Society, 673--688. D. Fett, R. K\u00fcsters, and G. Schmitz. 2014. An expressive model for the web infrastructure: Definition and application to the BrowserID SSO system. In Proceedings of the 35th IEEE Symposium on Security and Privacy (S8P\u201914). IEEE Computer Society, 673--688."},{"key":"e_1_2_1_21_1","volume-title":"Proceedings of the 23rd ACM SIGSAC Conference on Computer and Communications Security (CCS\u201916)","author":"Fett D.","unstructured":"D. Fett , R. K\u00fcsters , and G. Schmitz . 2016. A comprehensive formal security analysis of OAuth 2.0 . In Proceedings of the 23rd ACM SIGSAC Conference on Computer and Communications Security (CCS\u201916) . ACM, 1204--1215. https:\/\/doi.org\/10.1145\/2976749.2978385 10.1145\/2976749.2978385 D. Fett, R. K\u00fcsters, and G. Schmitz. 2016. A comprehensive formal security analysis of OAuth 2.0. In Proceedings of the 23rd ACM SIGSAC Conference on Computer and Communications Security (CCS\u201916). ACM, 1204--1215. https:\/\/doi.org\/10.1145\/2976749.2978385"},{"key":"e_1_2_1_22_1","volume-title":"Proceedings of the 30th Computer Security Foundations Symposium (CSF\u201917)","author":"Fett D.","year":"2017","unstructured":"D. Fett , R. K\u00fcsters , and G. Schmitz . 2017. The web SSO standard OpenID connect: In-depth formal security analysis and security guidelines . In Proceedings of the 30th Computer Security Foundations Symposium (CSF\u201917) . IEEE Computer Society. https:\/\/doi.org\/10.1109\/CSF. 2017 .20 10.1109\/CSF.2017.20 D. Fett, R. K\u00fcsters, and G. Schmitz. 2017. The web SSO standard OpenID connect: In-depth formal security analysis and security guidelines. In Proceedings of the 30th Computer Security Foundations Symposium (CSF\u201917). IEEE Computer Society. https:\/\/doi.org\/10.1109\/CSF.2017.20"},{"key":"e_1_2_1_23_1","unstructured":"Google. 2019. Google Authenticator. Retrieved from https:\/\/support.google.com\/accounts\/answer\/1066447?hl=en. Google. 2019. Google Authenticator. Retrieved from https:\/\/support.google.com\/accounts\/answer\/1066447?hl=en."},{"key":"#cr-split#-e_1_2_1_24_1.1","doi-asserted-by":"crossref","unstructured":"P. A. Grassi J. L. Fenton E. M. Newton R. A. Perlner A. R. Regenscheid W. E. Burr and J. P. Richer. 2017. Digital Identity Guidelines. National Institute of Standards and Technology. DOI:https:\/\/doi.org\/10.6028\/NIST.SP.800-63b 10.6028\/NIST.SP.800-63b","DOI":"10.6028\/NIST.SP.800-63b"},{"key":"#cr-split#-e_1_2_1_24_1.2","doi-asserted-by":"crossref","unstructured":"P. A. Grassi J. L. Fenton E. M. Newton R. A. Perlner A. R. Regenscheid W. E. Burr and J. P. Richer. 2017. Digital Identity Guidelines. National Institute of Standards and Technology. DOI:https:\/\/doi.org\/10.6028\/NIST.SP.800-63b","DOI":"10.6028\/NIST.SP.800-63b"},{"key":"e_1_2_1_25_1","unstructured":"D. He M. Naveed C. A. Gunter and K. Nahrstedt. 2014. Security Concerns in Android mHealth App. Retrieved from https:\/\/www.ncbi.nlm.nih.gov\/pmc\/articles\/PMC4419898\/. D. He M. Naveed C. A. Gunter and K. Nahrstedt. 2014. Security Concerns in Android mHealth App. Retrieved from https:\/\/www.ncbi.nlm.nih.gov\/pmc\/articles\/PMC4419898\/."},{"key":"e_1_2_1_26_1","volume-title":"HOTP: An HMAC-Based One-Time Password Algorithm.","author":"IETF.","year":"2005","unstructured":"IETF. 2005 . HOTP: An HMAC-Based One-Time Password Algorithm. Retrieved from https:\/\/tools.ietf.org\/html\/rfc4226. IETF. 2005. HOTP: An HMAC-Based One-Time Password Algorithm. Retrieved from https:\/\/tools.ietf.org\/html\/rfc4226."},{"key":"e_1_2_1_27_1","volume-title":"OCRA: OATH Challenge-Response Algorithms.","author":"IETF.","year":"2010","unstructured":"IETF. 2010 . OCRA: OATH Challenge-Response Algorithms. Retrieved from https:\/\/tools.ietf.org\/id\/draft-mraihi-mutual-oath-hotp-variants-11.html. IETF. 2010. OCRA: OATH Challenge-Response Algorithms. Retrieved from https:\/\/tools.ietf.org\/id\/draft-mraihi-mutual-oath-hotp-variants-11.html."},{"key":"e_1_2_1_28_1","volume-title":"TOTP: Time-Based One-Time Password Algorithm.","author":"IETF.","year":"2011","unstructured":"IETF. 2011 . TOTP: Time-Based One-Time Password Algorithm. Retrieved from https:\/\/tools.ietf.org\/html\/rfc6238. IETF. 2011. TOTP: Time-Based One-Time Password Algorithm. Retrieved from https:\/\/tools.ietf.org\/html\/rfc6238."},{"key":"e_1_2_1_29_1","unstructured":"IETF. 2012. The OAuth 2.0 Authorization Framework. Retrieved from http:\/\/tools.ietf.org\/html\/rfc6749. IETF. 2012. The OAuth 2.0 Authorization Framework. Retrieved from http:\/\/tools.ietf.org\/html\/rfc6749."},{"key":"e_1_2_1_30_1","unstructured":"IETF. 2015. Proof Key for Code Exchange by OAuth Public Clients. Retrieved from https:\/\/tools.ietf.org\/html\/rfc7636. IETF. 2015. Proof Key for Code Exchange by OAuth Public Clients. Retrieved from https:\/\/tools.ietf.org\/html\/rfc7636."},{"key":"e_1_2_1_31_1","unstructured":"Internet-Draft. 2019. OAuth 2.0 Security Best Current Practice. Retrieved from https:\/\/tools.ietf.org\/html\/draft-ietf-oauth-security-topics-13. Internet-Draft. 2019. OAuth 2.0 Security Best Current Practice. Retrieved from https:\/\/tools.ietf.org\/html\/draft-ietf-oauth-security-topics-13."},{"key":"e_1_2_1_32_1","unstructured":"iOS. 2017. Universal Links for Developers. Retrieved from https:\/\/developer.apple.com\/ios\/universal-links\/. iOS. 2017. Universal Links for Developers. Retrieved from https:\/\/developer.apple.com\/ios\/universal-links\/."},{"key":"e_1_2_1_33_1","volume-title":"31st IEEE Computer Security Foundations Symposium (CSF\u201918)","author":"Jacomme C.","year":"2018","unstructured":"C. Jacomme and S. Kremer . 2018. An extensive formal analysis of multi-factor authentication protocols . In 31st IEEE Computer Security Foundations Symposium (CSF\u201918) . 1--15. DOI:https:\/\/doi.org\/10.1109\/CSF. 2018 .00008 10.1109\/CSF.2018.00008 C. Jacomme and S. Kremer. 2018. An extensive formal analysis of multi-factor authentication protocols. In 31st IEEE Computer Security Foundations Symposium (CSF\u201918). 1--15. DOI:https:\/\/doi.org\/10.1109\/CSF.2018.00008"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/358790.358797"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.5555\/794197.795075"},{"key":"e_1_2_1_36_1","volume-title":"Proceedings. 696--701","author":"Meier S.","unstructured":"S. Meier , B. Schmidt , C. Cremers , and D. A. Basin . 2013. The TAMARIN prover for the symbolic analysis of security protocols. In Computer Aided Verification - 25th International Conference (CAV\u201913) , Proceedings. 696--701 . DOI:https:\/\/doi.org\/10.1007\/978-3-642-39799-8_48 10.1007\/978-3-642-39799-8_48 S. Meier, B. Schmidt, C. Cremers, and D. A. Basin. 2013. The TAMARIN prover for the symbolic analysis of security protocols. In Computer Aided Verification - 25th International Conference (CAV\u201913), Proceedings. 696--701. DOI:https:\/\/doi.org\/10.1007\/978-3-642-39799-8_48"},{"key":"e_1_2_1_37_1","unstructured":"Ministero dell\u2019Interno. 2019. Carta di Identit\u00e0 Elettronica. Retrieved from https:\/\/www.cartaidentita.interno.gov.it\/. Ministero dell\u2019Interno. 2019. Carta di Identit\u00e0 Elettronica. Retrieved from https:\/\/www.cartaidentita.interno.gov.it\/."},{"key":"e_1_2_1_38_1","volume-title":"Proceedings of the 14th European Symposium on Research in Computer Security (ESORICS\u201909)","author":"M\u00f6dersheim S.","unstructured":"S. M\u00f6dersheim and L. Vigan\u00f2 . 2009. Secure pseudonymous channels . In Proceedings of the 14th European Symposium on Research in Computer Security (ESORICS\u201909) . 337--354. https:\/\/doi.org\/10.1007\/978-3-642-04444-1_21 10.1007\/978-3-642-04444-1_21 S. M\u00f6dersheim and L. Vigan\u00f2. 2009. Secure pseudonymous channels. In Proceedings of the 14th European Symposium on Research in Computer Security (ESORICS\u201909). 337--354. https:\/\/doi.org\/10.1007\/978-3-642-04444-1_21"},{"key":"e_1_2_1_39_1","unstructured":"OASIS. 2005. SAML V2.0 technical overview. Retrieved from https:\/\/docs.oasis-open.org\/security\/saml\/v2.0\/saml-core-2.0-os.pdf. OASIS. 2005. SAML V2.0 technical overview. Retrieved from https:\/\/docs.oasis-open.org\/security\/saml\/v2.0\/saml-core-2.0-os.pdf."},{"key":"e_1_2_1_40_1","unstructured":"OAuth Working Group. 2016. OAuth 2.0 for Native Apps. Retrieved from https:\/\/tools.ietf.org\/html\/rfc8252. OAuth Working Group. 2016. OAuth 2.0 for Native Apps. Retrieved from https:\/\/tools.ietf.org\/html\/rfc8252."},{"key":"e_1_2_1_41_1","unstructured":"OIDF. 2014. OpenID Connect Core 1.0. Retrieved from http:\/\/openid.net\/specs\/openid-connect-core-1_0.html. OIDF. 2014. OpenID Connect Core 1.0. Retrieved from http:\/\/openid.net\/specs\/openid-connect-core-1_0.html."},{"key":"e_1_2_1_42_1","volume-title":"11th EAI International Conference on Pervasive Computing Technologies for Healthcare","author":"Osmani V.","unstructured":"V. Osmani , S. Forti , O. Mayora , and D. Conforti . 2017. Challenges and opportunities in evolving TreC personal health record platform . In 11th EAI International Conference on Pervasive Computing Technologies for Healthcare V. Osmani, S. Forti, O. Mayora, and D. Conforti. 2017. Challenges and opportunities in evolving TreC personal health record platform. In 11th EAI International Conference on Pervasive Computing Technologies for Healthcare"},{"key":"e_1_2_1_43_1","volume-title":"Proceedings of the IEEE International Conference on Communication Systems and Network Technologies (CSNT\u201911)","author":"Pai S.","year":"2011","unstructured":"S. Pai , Y. Sharma , S. Kumar , R. M. Pai , and S. Singh . 2011. Formal verification of OAuth 2.0 using Alloy framework . In Proceedings of the IEEE International Conference on Communication Systems and Network Technologies (CSNT\u201911) . 655--659. DOI:https:\/\/doi.org\/10.1109\/CSNT. 2011 .141 10.1109\/CSNT.2011.141 S. Pai, Y. Sharma, S. Kumar, R. M. Pai, and S. Singh. 2011. Formal verification of OAuth 2.0 using Alloy framework. In Proceedings of the IEEE International Conference on Communication Systems and Network Technologies (CSNT\u201911). 655--659. DOI:https:\/\/doi.org\/10.1109\/CSNT.2011.141"},{"key":"#cr-split#-e_1_2_1_44_1.1","doi-asserted-by":"crossref","unstructured":"O. Pereira F. Rochet and C. Wiedling. 2017. Formal analysis of the FIDO 1.x protocol. In Foundations and Practice of Security - 10th International Symposium (FPS'17). 68--82. DOI:https:\/\/doi.org\/10.1007\/978-3-319-75650-9_5 10.1007\/978-3-319-75650-9_5","DOI":"10.1007\/978-3-319-75650-9_5"},{"key":"#cr-split#-e_1_2_1_44_1.2","doi-asserted-by":"crossref","unstructured":"O. Pereira F. Rochet and C. Wiedling. 2017. Formal analysis of the FIDO 1.x protocol. In Foundations and Practice of Security - 10th International Symposium (FPS'17). 68--82. DOI:https:\/\/doi.org\/10.1007\/978-3-319-75650-9_5","DOI":"10.1007\/978-3-319-75650-9_5"},{"key":"e_1_2_1_45_1","unstructured":"M. Pohl. 2017. 325 000 mobile health apps available in 2017 -- Android now the leading mHealth platform. Retrieved from https:\/\/research2guidance.com\/325000-mobile-health-apps-available-in-2017\/. M. Pohl. 2017. 325 000 mobile health apps available in 2017 -- Android now the leading mHealth platform. Retrieved from https:\/\/research2guidance.com\/325000-mobile-health-apps-available-in-2017\/."},{"key":"#cr-split#-e_1_2_1_46_1.1","doi-asserted-by":"crossref","unstructured":"G. Sciarretta R. Carbone S. Ranise and A. Armando. 2017. Anatomy of the Facebook solution for mobile single sign-on: Security assessment and improvements.Journal of Computers 8 Security 71 (2017) 71--86. DOI:https:\/\/doi.org\/10.1016\/j.cose.2017.04.011 10.1016\/j.cose.2017.04.011","DOI":"10.1016\/j.cose.2017.04.011"},{"key":"#cr-split#-e_1_2_1_46_1.2","doi-asserted-by":"crossref","unstructured":"G. Sciarretta R. Carbone S. Ranise and A. Armando. 2017. Anatomy of the Facebook solution for mobile single sign-on: Security assessment and improvements.Journal of Computers 8 Security 71 (2017) 71--86. DOI:https:\/\/doi.org\/10.1016\/j.cose.2017.04.011","DOI":"10.1016\/j.cose.2017.04.011"},{"key":"#cr-split#-e_1_2_1_47_1.1","doi-asserted-by":"crossref","unstructured":"G. Sciarretta R. Carbone S. Ranise and L. Vigan\u00f2. 2018. Design formal specification and analysis of multi-factor authentication solutions with a single sign-on experience. In Principles of Security and Trust (POST'18) L. Bauer and R. K\u00fcsters (Eds.). Springer International Publishing 188--213. DOI:https:\/\/doi.org\/10.1007\/978-3-319-89722-6_8 10.1007\/978-3-319-89722-6_8","DOI":"10.1007\/978-3-319-89722-6_8"},{"key":"#cr-split#-e_1_2_1_47_1.2","doi-asserted-by":"crossref","unstructured":"G. Sciarretta R. Carbone S. Ranise and L. Vigan\u00f2. 2018. Design formal specification and analysis of multi-factor authentication solutions with a single sign-on experience. In Principles of Security and Trust (POST'18) L. Bauer and R. K\u00fcsters (Eds.). Springer International Publishing 188--213. DOI:https:\/\/doi.org\/10.1007\/978-3-319-89722-6_8","DOI":"10.1007\/978-3-319-89722-6_8"},{"key":"e_1_2_1_48_1","volume-title":"IEEE International Conference on Mobile Services (MS\u201914)","author":"Shehab M.","year":"2014","unstructured":"M. Shehab and F. Mohsen . 2014. Towards enhancing the security of OAuth implementations in smart phones . In IEEE International Conference on Mobile Services (MS\u201914) . 39--46. DOI:https:\/\/doi.org\/10.1109\/MobServ. 2014 .15 10.1109\/MobServ.2014.15 M. Shehab and F. Mohsen. 2014. Towards enhancing the security of OAuth implementations in smart phones. In IEEE International Conference on Mobile Services (MS\u201914). 39--46. DOI:https:\/\/doi.org\/10.1109\/MobServ.2014.15"},{"key":"#cr-split#-e_1_2_1_49_1.1","doi-asserted-by":"crossref","unstructured":"F. Sinigaglia R. Carbone G. Costa and N. Zannone. 2020. A survey on multi-factor authentication for online banking in the wild. Comput. Security (2020) 101745. DOI:https:\/\/doi.org\/10.1016\/j.cose.2020.101745 10.1016\/j.cose.2020.101745","DOI":"10.1016\/j.cose.2020.101745"},{"key":"#cr-split#-e_1_2_1_49_1.2","doi-asserted-by":"crossref","unstructured":"F. Sinigaglia R. Carbone G. Costa and N. Zannone. 2020. A survey on multi-factor authentication for online banking in the wild. Comput. Security (2020) 101745. DOI:https:\/\/doi.org\/10.1016\/j.cose.2020.101745","DOI":"10.1016\/j.cose.2020.101745"},{"key":"e_1_2_1_50_1","volume-title":"Proceedings of the 23nd Annual Network and Distributed System Security Symposium (NDSS'16)","author":"Sudhodanan A.","unstructured":"A. Sudhodanan , A. Armando , R. Carbone , and L. Compagna . 2016. Attack patterns for black-box security testing of multi-party web applications . In Proceedings of the 23nd Annual Network and Distributed System Security Symposium (NDSS'16) . A. Sudhodanan, A. Armando, R. Carbone, and L. Compagna. 2016. Attack patterns for black-box security testing of multi-party web applications. In Proceedings of the 23nd Annual Network and Distributed System Security Symposium (NDSS'16)."},{"key":"e_1_2_1_51_1","volume-title":"Proceedings of the ACM Conference on Computer and Communications Security (CCS\u201912)","author":"Sun S.","unstructured":"S. Sun and K. Beznosov . 2012. The devil is in the (implementation) details: An empirical analysis of OAuth SSO systems . In Proceedings of the ACM Conference on Computer and Communications Security (CCS\u201912) . DOI:https:\/\/doi.org\/10.1145\/2382196.2382238 10.1145\/2382196.2382238 S. Sun and K. Beznosov. 2012. The devil is in the (implementation) details: An empirical analysis of OAuth SSO systems. In Proceedings of the ACM Conference on Computer and Communications Security (CCS\u201912). DOI:https:\/\/doi.org\/10.1145\/2382196.2382238"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2013.75"},{"key":"e_1_2_1_53_1","volume-title":"Proceedings of the 9th International Symposium on Formal Methods for Components and Objects (FMCO\u201910)","author":"von Oheimb D.","unstructured":"D. von Oheimb and S. M\u00f6dersheim . 2010. ASLan++ \u2014 A formal security specification language for distributed systems . In Proceedings of the 9th International Symposium on Formal Methods for Components and Objects (FMCO\u201910) , revised papers (LNCS 6957). Springer, 1--22. DOI:https:\/\/doi.org\/10.1007\/978-3-642-25271-6_1 10.1007\/978-3-642-25271-6_1 D. von Oheimb and S. M\u00f6dersheim. 2010. ASLan++ \u2014 A formal security specification language for distributed systems. In Proceedings of the 9th International Symposium on Formal Methods for Components and Objects (FMCO\u201910), revised papers (LNCS 6957). Springer, 1--22. DOI:https:\/\/doi.org\/10.1007\/978-3-642-25271-6_1"},{"key":"e_1_2_1_54_1","volume-title":"Proceedings of the IEEE Symposium on Security and Privacy (S8P\u201912)","author":"Wang R.","year":"2012","unstructured":"R. Wang , S. Chen , and X. Wang . 2012. Signing me onto your accounts through Facebook and Google: A traffic-guided security study of commercially deployed single-sign-on web services . In Proceedings of the IEEE Symposium on Security and Privacy (S8P\u201912) . 365--379. DOI:https:\/\/doi.org\/10.1109\/SP. 2012 .30 10.1109\/SP.2012.30 R. Wang, S. Chen, and X. Wang. 2012. Signing me onto your accounts through Facebook and Google: A traffic-guided security study of commercially deployed single-sign-on web services. In Proceedings of the IEEE Symposium on Security and Privacy (S8P\u201912). 365--379. DOI:https:\/\/doi.org\/10.1109\/SP.2012.30"},{"key":"e_1_2_1_55_1","volume-title":"Proceedings of 16th IEEE International Symposium on High Assurance Systems Engineering (HASE\u201915)","author":"Yan H.","year":"2015","unstructured":"H. Yan , H. Fang , C. Kuka , and H. Zhu . 2015. Verification for OAuth using ASLan++ . In Proceedings of 16th IEEE International Symposium on High Assurance Systems Engineering (HASE\u201915) . 76--84. DOI:https:\/\/doi.org\/10.1109\/HASE. 2015 .20 10.1109\/HASE.2015.20 H. Yan, H. Fang, C. Kuka, and H. Zhu. 2015. Verification for OAuth using ASLan++. In Proceedings of 16th IEEE International Symposium on High Assurance Systems Engineering (HASE\u201915). 76--84. DOI:https:\/\/doi.org\/10.1109\/HASE.2015.20"},{"key":"e_1_2_1_56_1","unstructured":"R. Yang W. C. Lau and T. Liu. 2016. Signing into one billion mobile app accounts effortlessly with OAuth2.0. In Black Hat Europe. R. Yang W. C. Lau and T. Liu. 2016. Signing into one billion mobile app accounts effortlessly with OAuth2.0. In Black Hat Europe."},{"key":"e_1_2_1_57_1","volume-title":"Proceedings of the 20th ICECCS. 90--99","author":"Ye Q.","year":"2015","unstructured":"Q. Ye , G. Bai , K. Wang , and J. S. Dong . 2015. Formal analysis of a single sign-on protocol implementation for Android . In Proceedings of the 20th ICECCS. 90--99 . DOI:https:\/\/doi.org\/10.1109\/ICECCS. 2015 .20 10.1109\/ICECCS.2015.20 Q. Ye, G. Bai, K. Wang, and J. S. Dong. 2015. Formal analysis of a single sign-on protocol implementation for Android. In Proceedings of the 20th ICECCS. 90--99. DOI:https:\/\/doi.org\/10.1109\/ICECCS.2015.20"},{"key":"e_1_2_1_58_1","unstructured":"Yubico. 2019. YubiKey NEO. Retrieved from https:\/\/www.yubico.com\/products\/yubikey-hardware\/yubikey-neo. Yubico. 2019. YubiKey NEO. Retrieved from https:\/\/www.yubico.com\/products\/yubikey-hardware\/yubikey-neo."}],"container-title":["ACM Transactions on Privacy and Security"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3386685","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T08:01:44Z","timestamp":1672560104000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3386685"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,6,6]]},"references-count":65,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2020,8,31]]}},"alternative-id":["10.1145\/3386685"],"URL":"https:\/\/doi.org\/10.1145\/3386685","relation":{},"ISSN":["2471-2566","2471-2574"],"issn-type":[{"value":"2471-2566","type":"print"},{"value":"2471-2574","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,6,6]]},"assertion":[{"value":"2019-08-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2020-03-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2020-06-06","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}