{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,13]],"date-time":"2026-02-13T10:15:40Z","timestamp":1770977740193,"version":"3.50.1"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319668444","type":"print"},{"value":"9783319668451","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-66845-1_27","type":"book-chapter","created":{"date-parts":[[2017,8,26]],"date-time":"2017-08-26T11:37:20Z","timestamp":1503747440000},"page":"407-421","source":"Crossref","is-referenced-by-count":5,"title":["Certified Password Quality"],"prefix":"10.1007","author":[{"given":"Jo\u00e3o F.","family":"Ferreira","sequence":"first","affiliation":[]},{"given":"Saul A.","family":"Johnson","sequence":"additional","affiliation":[]},{"given":"Alexandra","family":"Mendes","sequence":"additional","affiliation":[]},{"given":"Phillip J.","family":"Brooke","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,8,27]]},"reference":[{"key":"27_CR1","doi-asserted-by":"crossref","unstructured":"Appel, A.W.: Modular verification for computer security. In: IEEE 29th Computer Security Foundations Symposium (CSF), pp. 1\u20138 (2016)","DOI":"10.1109\/CSF.2016.8"},{"key":"27_CR2","doi-asserted-by":"crossref","unstructured":"Bauerei\u00df, T., Gritti, A.P., Popescu, A., Raimondi, F.: CoSMeDis: a distributed social media platform with formally verified confidentiality guarantees. In: Security and Privacy (SP) (2017)","DOI":"10.1109\/SP.2017.24"},{"key":"27_CR3","volume-title":"Interactive theorem proving and program development - Coq\u2019Art: the calculus of inductive constructions","author":"Y Bertot","year":"2013","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive theorem proving and program development - Coq\u2019Art: the calculus of inductive constructions. Springer Science & Business Media, Heidelberg (2013)"},{"key":"27_CR4","doi-asserted-by":"crossref","unstructured":"Blanchet, B., et al.: An efficient cryptographic protocol verifier based on prolog rules. In: CSFW, vol. 1, pp. 82\u201396 (2001)","DOI":"10.1109\/CSFW.2001.930138"},{"key":"27_CR5","unstructured":"Burnett, M.: Today i am releasing ten million passwords (2015). https:\/\/xato.net\/today-i-am-releasing-ten-million-passwords-b6278bbe7495 . Accessed 26 Apr 2017"},{"key":"27_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"380","DOI":"10.1007\/11681878_20","volume-title":"Theory of Cryptography","author":"R Canetti","year":"2006","unstructured":"Canetti, R., Herzog, J.: Universally composable symbolic analysis of mutual authentication and key-exchange protocols. In: Halevi, S., Rabin, T. (eds.) TCC 2006. LNCS, vol. 3876, pp. 380\u2013403. Springer, Heidelberg (2006). doi: 10.1007\/11681878_20"},{"key":"27_CR7","unstructured":"National Cyber Security Centre: Password Guidance: Simplifying Your Approach (2016). https:\/\/www.ncsc.gov.uk\/guidance\/password-guidance-simplifying-your-approach . Accessed 26 Apr 2017"},{"issue":"4","key":"27_CR8","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1145\/3051092","volume":"60","author":"T Chajed","year":"2017","unstructured":"Chajed, T., Chen, H., Chlipala, A., Kaashoek, M.F., Zeldovich, N., Ziegler, D.: Certifying a file system using crash Hoare logic: correctness in the presence of crashes. Commun. ACM 60(4), 75\u201384 (2017)","journal-title":"Commun. ACM"},{"key":"27_CR9","doi-asserted-by":"crossref","unstructured":"Chen, H., Ziegler, D., Chajed, T., Chlipala, A., Kaashoek, M.F., Zeldovich, N.: Using crash Hoare logic for certifying the FSCQ file system. In: Proceedings of the 25th Symposium on Operating Systems Principles, pp. 18\u201337. ACM (2015)","DOI":"10.1145\/2815400.2815402"},{"key":"27_CR10","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/9153.001.0001","volume-title":"Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant","author":"A Chlipala","year":"2013","unstructured":"Chlipala, A.: Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant. MIT Press, Cambridge (2013)"},{"key":"27_CR11","doi-asserted-by":"crossref","unstructured":"Dell\u2019Amico, M., Michiardi, P., Roudier, Y.: Password strength: an empirical analysis. In: INFOCOM, pp. 1\u20139, IEEE (2010)","DOI":"10.1109\/INFCOM.2010.5461951"},{"key":"27_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/BFb0028390","volume-title":"Theorem Proving in Higher Order Logics","author":"B Dutertre","year":"1997","unstructured":"Dutertre, B., Schneider, S.: Using a PVS embedding of CSP to verify authentication protocols. In: Gunter, E.L., Felty, A. (eds.) TPHOLs 1997. LNCS, vol. 1275, pp. 121\u2013136. Springer, Heidelberg (1997). doi: 10.1007\/BFb0028390"},{"key":"27_CR13","unstructured":"Finne, S., Henderson, I.F., Kowalczyk, M., Leijen, D., Marlow, S., Meijer, E., Jones, S.P., Wallace, M.: The Haskell 98 Foreign Function Interface 1.0 An Addendum to the Haskell 98 Report (2002)"},{"key":"27_CR14","volume-title":"Coding and Theory","author":"RW Hamming","year":"1980","unstructured":"Hamming, R.W.: Coding and Theory. Prentice-Hall, Englewood Cliffs (1980)"},{"issue":"2","key":"27_CR15","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1002\/j.1538-7305.1950.tb00463.x","volume":"29","author":"RW Hamming","year":"1950","unstructured":"Hamming, R.W.: Error detecting and error correcting codes. Bell Labs Tech. J. 29(2), 147\u2013160 (1950)","journal-title":"Bell Labs Tech. J."},{"key":"27_CR16","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. ACM (2010)","DOI":"10.1145\/1753326.1753384"},{"key":"27_CR17","unstructured":"Jahoda, M., Kr\u00e1tk\u00fd, R., Prpi\u010d, M., \u010capek, T., Wadeley, S., Ruseva, Y., Svoboda, M.: Red Hat Enterprise Linux 7 Security Guide (2017). https:\/\/access.redhat.com\/documentation\/en-US\/Red_Hat_Enterprise_Linux\/7\/html\/Security_Guide\/index.html . Accessed 24 Apr 2017"},{"key":"27_CR18","unstructured":"Johnson, S.: Behavior of maxclassrepeat=1 inconsistent with docs (2017). https:\/\/github.com\/linux-pam\/linux-pam\/issues\/16 . Accessed 31 Mar 2017"},{"key":"27_CR19","volume-title":"Haskell 98 Language and Libraries: The Revised Report","author":"SP Jones","year":"2003","unstructured":"Jones, S.P.: Haskell 98 Language and Libraries: The Revised Report. Cambridge University Press, Cambridge (2003)"},{"key":"27_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-319-08867-9_11","volume-title":"Computer Aided Verification","author":"S Kanav","year":"2014","unstructured":"Kanav, S., Lammich, P., Popescu, A.: A conference management system with verified document confidentiality. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 167\u2013183. Springer, Cham (2014). doi: 10.1007\/978-3-319-08867-9_11"},{"key":"27_CR21","doi-asserted-by":"crossref","unstructured":"Kelley, P.G., Komanduri, S., Mazurek, M.L., Shay, R., Vidas, T., Bauer, L., Christin, N., Cranor, L.F., Lopez, J.: Guess again (and again and again): measuring password strength by simulating password-cracking algorithms. In: Security and Privacy (SP), pp. 523\u2013537. IEEE (2012)","DOI":"10.1109\/SP.2012.38"},{"key":"27_CR22","unstructured":"Software Reliability Lab. Verified PAM Cracklib (2017). https:\/\/github.com\/sr-lab\/verified-pam-cracklib . Accessed 05 Apr 2017"},{"key":"27_CR23","unstructured":"Software Reliability Lab. Verified PAM Environment (2017). https:\/\/github.com\/sr-lab\/verified-pam-environment . Accessed 30 Mar 2017"},{"key":"27_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/978-3-540-69407-6_39","volume-title":"Logic and Theory of Algorithms","author":"P Letouzey","year":"2008","unstructured":"Letouzey, P.: Extraction in Coq: an overview. In: Beckmann, A., Dimitracopoulos, C., L\u00f6we, B. (eds.) CiE 2008. LNCS, vol. 5028, pp. 359\u2013369. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-69407-6_39"},{"key":"27_CR25","unstructured":"Morgan, A.G., Kukuk, T.: The Linux-PAM Module Writers\u2019 Guide (2010)"},{"key":"27_CR26","doi-asserted-by":"crossref","unstructured":"Samar, V.: Unified login with pluggable authentication modules (PAM). In: Proceedings of the 3rd ACM Conference on Computer and Communications Security, pp. 1\u201310 (1996)","DOI":"10.1145\/238168.238177"},{"issue":"9","key":"27_CR27","doi-asserted-by":"crossref","first-page":"741","DOI":"10.1109\/32.713329","volume":"24","author":"S Schneider","year":"1998","unstructured":"Schneider, S.: Verifying authentication protocols in CSP. IEEE Trans. Softw. Eng. 24(9), 741\u2013758 (1998)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"27_CR28","unstructured":"Shay, R., Komanduri, S., Durity, A.L., Huh, P.S., Mazurek, M.L., Segreti, S.M., Ur, B., Bauer, L., Christin, N., Cranor, L.F.: Designing password policies for strength and usability. ACM Trans. Inf. Syst. Secur. (TIS-SEC) 18(4) (2016). Article no. 13"},{"issue":"2","key":"27_CR29","doi-asserted-by":"crossref","first-page":"651","DOI":"10.1109\/TIFS.2011.2169958","volume":"7","author":"H-M Sun","year":"2012","unstructured":"Sun, H.-M., Chen, Y.-H., Lin, Y.-H.: oPass: a user authentication protocol resistant to password stealing and password reuse attacks. IEEE Trans. Inf. Forensics Secur. 7(2), 651\u2013663 (2012)","journal-title":"IEEE Trans. Inf. Forensics Secur."},{"issue":"3","key":"27_CR30","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1145\/75200.75244","volume":"14","author":"S Thompson","year":"1989","unstructured":"Thompson, S.: Functional programming: executable specifications and program transformations. ACM SIGSOFT Softw. Eng. Notes 14(3), 287\u2013290 (1989)","journal-title":"ACM SIGSOFT Softw. Eng. Notes"},{"key":"27_CR31","unstructured":"Visser, J., Oliveira, J.N.F., Barbosa, L.S., Ferreira, J.F., Mendes, A.: CAMILA revival: VDM meets Haskell. In: 1st Overture Workshop. University of Newcastle TR Series (2005)"},{"key":"27_CR32","doi-asserted-by":"crossref","unstructured":"Zhang-Kennedy, L., Chiasson, S., van Oorschot, P.: Revisiting password rules: facilitating human management of passwords. In: APWG Symposium on Electronic Crime Research (eCrime), pp. 1\u201310. IEEE (2016)","DOI":"10.1109\/ECRIME.2016.7487945"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66845-1_27","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,2]],"date-time":"2019-10-02T16:52:00Z","timestamp":1570035120000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-66845-1_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319668444","9783319668451"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66845-1_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]}}}