{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,12]],"date-time":"2026-02-12T15:09:45Z","timestamp":1770908985453,"version":"3.50.1"},"publisher-location":"Cham","reference-count":37,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032104434","type":"print"},{"value":"9783032104441","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,11,12]],"date-time":"2025-11-12T00:00:00Z","timestamp":1762905600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,11,12]],"date-time":"2025-11-12T00:00:00Z","timestamp":1762905600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-10444-1_12","type":"book-chapter","created":{"date-parts":[[2025,11,11]],"date-time":"2025-11-11T06:58:55Z","timestamp":1762844335000},"page":"185-202","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Are Users More Willing to\u00a0Use Formally Verified Password Managers?"],"prefix":"10.1007","author":[{"given":"Carolina","family":"Carreira","sequence":"first","affiliation":[]},{"given":"Jo\u00e3o F.","family":"Ferreira","sequence":"additional","affiliation":[]},{"given":"Alexandra","family":"Mendes","sequence":"additional","affiliation":[]},{"given":"Nicolas","family":"Christin","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,11,12]]},"reference":[{"key":"12_CR1","unstructured":"Akhawe, D., Felt, A.P.: Alice in warningland: a large-scale field study of browser security warning effectiveness. In: 22nd USENIX Security, pp. 257\u2013272 (2013)"},{"key":"12_CR2","unstructured":"Bitwarden: Bitwarden (2023). https:\/\/bitwarden.com Accessed 10 Jun 2025"},{"key":"12_CR3","doi-asserted-by":"crossref","unstructured":"Carreira, C.: Studying users\u2019 willingness to use a formally verified password manager. In: International Conference on Integrated Formal Methods, pp. 343\u2013346. Springer (2022)","DOI":"10.1007\/978-3-031-07727-2_19"},{"key":"12_CR4","unstructured":"Carreira, C., Ferreira, J.F., Mendes, A.: Towards improving the usability of password managers. INFORUM (2021)"},{"key":"12_CR5","doi-asserted-by":"crossref","unstructured":"Carreira, C., Ferreira, J.F., Mendes, A., Christin, N.: Exploring usable security to improve the impact of formal verification: a research agenda. First Workshop on Applicable Formal Methods (co-located with Formal Methods 2021) (2021)","DOI":"10.4204\/EPTCS.349.6"},{"key":"12_CR6","unstructured":"Chiasson, S., van Oorschot, P.C., Biddle, R.: A usability study and critique of two password managers. In: USENIX Security Symposium (2006)"},{"key":"12_CR7","doi-asserted-by":"crossref","unstructured":"Chudnov, A., et\u00a0al.: Continuous formal verification of Amazon S2N. In: International Conference on Computer Aided Verification, pp. 430\u2013446. Springer (2018)","DOI":"10.1007\/978-3-319-96142-2_26"},{"key":"12_CR8","doi-asserted-by":"crossref","unstructured":"Cummings, R., Kaptchuk, G., Redmiles, E.M.: I need a better description: an investigation into user expectations for differential privacy. In: ACM SIGSAC (2021)","DOI":"10.1145\/3460120.3485252"},{"key":"12_CR9","doi-asserted-by":"crossref","unstructured":"Emami-Naeini, P., Agarwal, Y., Cranor, L.F., Hibshi, H.: Ask the experts: what should be on an IoT privacy and security label? In: SP. IEEE (2020)","DOI":"10.1109\/SP40000.2020.00043"},{"key":"12_CR10","unstructured":"ENISA: European union agency for cibersecurity authentication methods (2025). https:\/\/www.enisa.europa.eu\/topics\/cyber-hygiene Accessed 10 Jun 2025"},{"key":"12_CR11","doi-asserted-by":"crossref","unstructured":"Felt, A.P., et al.: Improving SSL warnings: comprehension and adherence. In: CHI (2015)","DOI":"10.1145\/2702123.2702442"},{"key":"12_CR12","doi-asserted-by":"crossref","unstructured":"Ferreira, J.F., Johnson, S., Mendes, A., Brooke, P.: Certified password quality: a case study using coq and Linux pluggable authentication modules. In: 13th International Conference on Integrated Formal Methods (2017)","DOI":"10.1007\/978-3-319-66845-1_27"},{"key":"12_CR13","doi-asserted-by":"crossref","unstructured":"Garavel, H., Beek, M.H.t., Pol, J.v.d.: The 2020 expert survey on formal methods. In: Formal Methods for Industrial Critical Systems: 25th International Conference, pp. 3\u201369. Springer (2020)","DOI":"10.1007\/978-3-030-58298-2_1"},{"key":"12_CR14","doi-asserted-by":"crossref","unstructured":"Grilo, M., Campos, J., Ferreira, J.F., Mendes, A., Almeida, J.B.: Verified password generation from password composition policies. In: 17th International Conference on Integrated Formal Methods (2022)","DOI":"10.1007\/978-3-031-07727-2_15"},{"key":"12_CR15","unstructured":"Harley, A.: Usability testing of icons (2016). www.nngroup.com\/articles\/icon-testing\/ Accessed 10 Jun 2025"},{"key":"12_CR16","unstructured":"Hartnett, K.: Hacker-proof code (2020) . https:\/\/www.quantamagazine.org\/formal-verification-creates-hacker-proof-code-20160920\/ Accessed 10 Jun 2025"},{"key":"12_CR17","doi-asserted-by":"crossref","unstructured":"Inglesant, P.G., Sasse, M.A.: The true cost of unusable password policies: password use in the wild. In: Proceedings of the SIGCHI conference on human factors in computing systems, pp. 383\u2013392 (2010)","DOI":"10.1145\/1753326.1753384"},{"key":"12_CR18","unstructured":"Ion, I., Reeder, R., Consolvo, S.: ...No one can hack my mind: comparing expert and non-expert security practices. In: Eleventh Symposium On Usable Privacy and Security (SOUPS 2015), pp. 327\u2013346 (2015)"},{"key":"12_CR19","unstructured":"Jangid, M.K., Chen, G., Zhang, Y., Lin, Z.: Towards formal verification of state continuity for enclave programs. In: USENIX Security Symposium (2021)"},{"key":"12_CR20","doi-asserted-by":"crossref","unstructured":"Johnson, S., Ferreira, J.F., Mendes, A., Cordry, J.: Skeptic: automatic, justified and privacy-preserving password composition policy selection. In: 15th ACM Asia Conference on Computer and Communications Security (2020)","DOI":"10.1145\/3320269.3384762"},{"key":"12_CR21","doi-asserted-by":"crossref","unstructured":"Kelley, P.G., Bresee, J., Cranor, L.F., Reeder, R.W.: A \u201cnutrition label\u201d for privacy. In: SOUPS, pp. 1\u201312 (2009)","DOI":"10.1145\/1572532.1572538"},{"issue":"1","key":"12_CR22","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1145\/2578855.2535841","volume":"49","author":"R Kumar","year":"2014","unstructured":"Kumar, R., Myreen, M.O., Norrish, M., Owens, S.: CakeML: a verified implementation of ML. ACM SIGPLAN Notices 49(1), 179\u2013191 (2014)","journal-title":"ACM SIGPLAN Notices"},{"key":"12_CR23","unstructured":"Lazar, J., Feng, J.H., Hochheiser, H.: Research methods in human-computer interaction. Morgan Kaufmann (2017)"},{"key":"12_CR24","doi-asserted-by":"crossref","unstructured":"Leroy, X.: Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In: ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 42\u201354 (2006)","DOI":"10.1145\/1111037.1111042"},{"issue":"7","key":"12_CR25","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107\u2013115 (2009)","journal-title":"Commun. ACM"},{"key":"12_CR26","doi-asserted-by":"crossref","unstructured":"Li, Y., Chen, D., Li, T., Agarwal, Y., Cranor, L.F., Hong, J.I.: Understanding IOS privacy nutrition labels: an exploratory large-scale analysis of app store data. In: CHI (2022)","DOI":"10.1145\/3491101.3519739"},{"key":"12_CR27","unstructured":"Mai, A., Pfeffer, K., Gusenbauer, M., Weippl, E., Krombholz, K.: User mental models of cryptocurrency systems-a grounded theory approach. In: Sixteenth Symposium on Usable Privacy and Security (SOUPS 2020), pp. 341\u2013358 (2020)"},{"key":"12_CR28","unstructured":"Nelson, L., Van\u00a0Geffen, J., Torlak, E., Wang, X.: Specification and verification in the field: Applying formal methods to BPF just-in-time compilers in the Linux kernel. In: OSDI \u201920, pp. 41\u201361 (2020)"},{"key":"12_CR29","unstructured":"Pearman, S., Zhang, S.A., Bauer, L., Christin, N., Cranor, L.F.: Why people (don\u2019t) use password managers effectively. In: SOUPS (2019)"},{"key":"12_CR30","doi-asserted-by":"crossref","unstructured":"Pearman, S., Thomas, J., et al.: Let\u2019s go in for a closer look: observing passwords in their natural habitat. In: ACM SIGSAC (2017)","DOI":"10.1145\/3133956.3133973"},{"key":"12_CR31","doi-asserted-by":"crossref","unstructured":"Pereira, D., Ferreira, J.F., Mendes, A.: Evaluating the accuracy of password strength meters using off-the-shelf guessing attacks. In: ISSREW. IEEE (2020)","DOI":"10.1109\/ISSREW51248.2020.00079"},{"key":"12_CR32","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1016\/j.procs.2017.11.013","volume":"121","author":"W Presthus","year":"2017","unstructured":"Presthus, W., O\u2019Malley, N.O.: Motivations and barriers for end-user adoption of bitcoin as digital currency. Procedia Comput. Sci. 121, 89\u201397 (2017). https:\/\/doi.org\/10.1016\/j.procs.2017.11.013","journal-title":"Procedia Comput. Sci."},{"key":"12_CR33","doi-asserted-by":"crossref","unstructured":"Ray, H., Wolf, F., Kuber, R., Aviv, A.J.: Why older adults (don\u2019t) use password managers. In: USENIX Security Symposium (2021)","DOI":"10.2478\/popets-2021-0016"},{"key":"12_CR34","unstructured":"Redmiles, E.M., Acar, Y., Fahl, S., Mazurek, M.L.: A summary of survey methodology best practices for security and privacy researchers. Technical report (2017)"},{"key":"12_CR35","unstructured":"Rubens, P.: How playing computer games can make the world safer (2015). https:\/\/www.bbc.com\/news\/business-33519194 Accessed 10 Jun 2025"},{"issue":"9","key":"12_CR36","doi-asserted-by":"publisher","first-page":"1278","DOI":"10.1109\/PROC.1975.9939","volume":"63","author":"JH Saltzer","year":"1975","unstructured":"Saltzer, J.H., Schroeder, M.D.: The protection of information in computer systems. Proc. IEEE 63(9), 1278\u20131308 (1975)","journal-title":"Proc. IEEE"},{"key":"12_CR37","unstructured":"Stobert, E., Biddle, R.: The password life cycle: user behaviour in managing passwords. In: SOUPS 2014 (2014)"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-10444-1_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,12]],"date-time":"2026-02-12T14:06:57Z","timestamp":1770905217000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-10444-1_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,12]]},"ISBN":["9783032104434","9783032104441"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-10444-1_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,11,12]]},"assertion":[{"value":"12 November 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SEFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Software Engineering and Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Toledo","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Spain","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 November 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14 November 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sefm2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/sefm-conference.github.io\/2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}