{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,13]],"date-time":"2026-02-13T10:16:11Z","timestamp":1770977771574,"version":"3.50.1"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783031077265","type":"print"},{"value":"9783031077272","type":"electronic"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"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":[[2022]]},"DOI":"10.1007\/978-3-031-07727-2_15","type":"book-chapter","created":{"date-parts":[[2022,6,1]],"date-time":"2022-06-01T01:12:12Z","timestamp":1654045932000},"page":"271-288","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Verified Password Generation from\u00a0Password Composition Policies"],"prefix":"10.1007","author":[{"given":"Miguel","family":"Grilo","sequence":"first","affiliation":[]},{"given":"Jo\u00e3o","family":"Campos","sequence":"additional","affiliation":[]},{"given":"Jo\u00e3o F.","family":"Ferreira","sequence":"additional","affiliation":[]},{"given":"Jos\u00e9 Bacelar","family":"Almeida","sequence":"additional","affiliation":[]},{"given":"Alexandra","family":"Mendes","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,6,1]]},"reference":[{"key":"15_CR1","doi-asserted-by":"crossref","unstructured":"Alkaldi, N., Renaud, K.: Why do people adopt, or reject, smartphone password managers? In: 1st European Workshop on Usable Security-EuroUSEC 2016 (2016)","DOI":"10.14722\/eurousec.2016.23011"},{"key":"15_CR2","doi-asserted-by":"crossref","unstructured":"Almeida, J.B., et al.: Jasmin: high-assurance and high-speed cryptography. In: Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, pp. 1807\u20131823 (2017)","DOI":"10.1145\/3133956.3134078"},{"key":"15_CR3","doi-asserted-by":"crossref","unstructured":"Almeida, J.B., et al.: The last mile: high-assurance and high-speed cryptographic implementations. In: 2020 IEEE Symposium on Security and Privacy (SP) (2020)","DOI":"10.1109\/SP40000.2020.00028"},{"key":"15_CR4","doi-asserted-by":"crossref","unstructured":"Almeida, J.B., et al.: Machine-checked proofs for cryptographic standards: indifferentiability of sponge and secure high-assurance implementations of SHA-3. In: Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security (2019)","DOI":"10.1145\/3319535.3363211"},{"key":"15_CR5","unstructured":"Apple. Customizing Password AutoFill Rules (2021). https:\/\/developer.apple.com\/documentation\/security\/password_autofill\/customizing_password_autofill_rules. Accessed 31 July 2021"},{"key":"15_CR6","unstructured":"Apple. Web sites won\u2019t accept Safari generated strong passwords due to dashes or other criteria (2021). https:\/\/discussions.apple.com\/thread\/251341081. Accessed 26 Oct 2021"},{"key":"15_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/978-3-319-10082-1_6","volume-title":"Foundations of Security Analysis and Design VII","author":"G Barthe","year":"2014","unstructured":"Barthe, G., Dupressoir, F., Gr\u00e9goire, B., Kunz, C., Schmidt, B., Strub, P.-Y.: EasyCrypt: a tutorial. In: Aldini, A., Lopez, J., Martinelli, F. (eds.) FOSAD 2012-2013. LNCS, vol. 8604, pp. 146\u2013166. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-10082-1_6"},{"key":"15_CR8","unstructured":"Bellare, M., Rogaway, P.: Code-based game-playing proofs and the security of triple encryption. IACR Cryptology ePrint Archive 2004\/331 (2004)"},{"key":"15_CR9","unstructured":"Bond, B., et al.: Vale: verifying high-performance cryptographic assembly code. In: 26th USENIX Security Symposium, pp. 917\u2013934 (2017)"},{"key":"15_CR10","unstructured":"Carreira, C., Ferreira, J.F., Mendes, A.: Towards improving the usability of password managers. In: INFORUM (2021)"},{"key":"15_CR11","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. In: First Workshop on Applicable Formal Methods (Co-Located with Formal Methods 2021) (2021)","DOI":"10.4204\/EPTCS.349.6"},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"Chiasson, S., van Oorschot, P.C., Biddle, R.: A usability study and critique of two password managers. In: USENIX Security Symposium, vol. 15, pp. 1\u201316 (2006)","DOI":"10.1145\/1280680.1280682"},{"key":"15_CR13","unstructured":"EA. Password Does Not Meet Requirements (2021). https:\/\/web.archive.org\/web\/20210817105229\/answers.ea.com\/t5\/EA-General-Questions\/quot-Password-Does-Not-Meet-Requirements-quot\/td-p\/5744758. Accessed 26 Oct 2021"},{"key":"15_CR14","doi-asserted-by":"crossref","unstructured":"Erbsen, A., Philipoom, J., Gross, J., Sloan, R., Chlipala, A.: Simple high-level code for cryptographic arithmetic - with proofs, without compromises. In: 2019 IEEE Symposium on Security and Privacy, SP 2019, pp. 1202\u20131219. IEEE (2019)","DOI":"10.1109\/SP.2019.00005"},{"key":"15_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"407","DOI":"10.1007\/978-3-319-66845-1_27","volume-title":"Integrated Formal Methods","author":"JF Ferreira","year":"2017","unstructured":"Ferreira, J.F., Johnson, S.A., Mendes, A., Brooke, P.J.: Certified password quality. In: Polikarpova, N., Schneider, S. (eds.) IFM 2017. LNCS, vol. 10510, pp. 407\u2013421. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66845-1_27"},{"key":"15_CR16","doi-asserted-by":"crossref","unstructured":"Florencio, D., Herley, C.: A large-scale study of web password habits. In: Proceedings of the 16th International Conference on World Wide Web, pp. 657\u2013666 (2007)","DOI":"10.1145\/1242572.1242661"},{"key":"15_CR17","unstructured":"Grilo, M., Ferreira, J.F., Almeida, J.B.: Towards formal verification of password generation algorithms used in password managers. arXiv preprint arXiv:2106.03626 (2021)"},{"key":"15_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"426","DOI":"10.1007\/978-3-319-40253-6_26","volume-title":"Information Security and Privacy","author":"M Horsch","year":"2016","unstructured":"Horsch, M., Schlipf, M., Braun, J., Buchmann, J.: Password requirements markup language. In: Liu, J.K., Steinfeld, R. (eds.) ACISP 2016. LNCS, vol. 9722, pp. 426\u2013439. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40253-6_26"},{"key":"15_CR19","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: Proceedings of the 15th ACM Asia Conference on Computer and Communications Security, pp. 101\u2013115 (2020)","DOI":"10.1145\/3320269.3384762"},{"key":"15_CR20","unstructured":"Oesch, S., Ruoti, S.: That was then, this is now: a security evaluation of password generation, storage, and autofill in browser-based password managers. In: USENIX Security Symposium (2020)"},{"key":"15_CR21","unstructured":"Pearman, S., Zhang, S.A., Bauer, L., Christin, N., Cranor, L.F.: Why people (don\u2019t) use password managers effectively. In: Fifteenth Symposium on Usable Privacy and Security (SOUPS 2019), pp. 319\u2013338. USENIX Association, Santa Clara (2019)"},{"key":"15_CR22","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: 2020 IEEE International Symposium on Software Reliability Engineering Workshops (ISSREW), pp. 237\u2013242. IEEE (2020)","DOI":"10.1109\/ISSREW51248.2020.00079"},{"issue":"4","key":"15_CR23","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2891411","volume":"18","author":"R Shay","year":"2016","unstructured":"Shay, R., et al.: Designing password policies for strength and usability. ACM Trans. Inf. Syst. Secur. (TISSEC) 18(4), 1\u201334 (2016)","journal-title":"ACM Trans. Inf. Syst. Secur. (TISSEC)"},{"key":"15_CR24","unstructured":"Shoup, V.: Sequences of games: a tool for taming complexity in security proofs. IACR Cryptology ePrint Archive 2004\/332 (2004)"},{"key":"15_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/978-3-319-24192-0_4","volume-title":"Technology and Practice of Passwords","author":"F Stajano","year":"2015","unstructured":"Stajano, F., Spencer, M., Jenkinson, G., Stafford-Fraser, Q.: Password-manager friendly (PMF): semantic annotations to improve the effectiveness of password managers. In: Mj\u00f8lsnes, S.F. (ed.) PASSWORDS 2014. LNCS, vol. 9393, pp. 61\u201373. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-24192-0_4"},{"key":"15_CR26","unstructured":"TechNet. Can\u2019t create local user \u201cPassword does not meet password policy requirements\u201d - but it does (2021). https:\/\/web.archive.org\/web\/20211026082725\/. https:\/\/social.technet.microsoft.com\/Forums\/en-US\/12b06881-ea1a-403d-aafb-99bbe7d4d1b0\/cant-create-local-user-quotpassword-does-not-meet-password-policy-requirementsquot-but-it?forum=win10itprosecurity. Accessed 26 Oct 2021"},{"key":"15_CR27","doi-asserted-by":"crossref","unstructured":"Zinzindohou\u00e9, J.-K., Bhargavan, K., Protzenko, J., Beurdouche, B.: HACL*: a verified modern cryptographic library. In: Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS 2017, pp. 1789\u20131806. Association for Computing Machinery, New York (2017). ISBN: 9781450349468","DOI":"10.1145\/3133956.3134043"},{"key":"15_CR28","doi-asserted-by":"crossref","unstructured":"Zuo, C., Lin, Z., Zhang, Y.: Why does your data leak? Uncovering the data leakage in cloud from mobile apps. In: 2019 IEEE Symposium on Security and Privacy (SP). IEEE (2019)","DOI":"10.1109\/SP.2019.00009"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-07727-2_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,26]],"date-time":"2024-09-26T06:00:33Z","timestamp":1727330433000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-07727-2_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031077265","9783031077272"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-07727-2_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"1 June 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"IFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Integrated Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Lugano","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Switzerland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 June 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 June 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ifm2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.ifmconference.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-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":"46","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":"14","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":"2","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":"30% - 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":"4","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":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Also includes: 1 abstract of an invited talk, 2 invited papers, 7 extended abstracts of presentations accepted at PhD symposium","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}