Certified Password Quality

A Case Study Using Coq and Linux Pluggable Authentication Modules
  • João F. FerreiraEmail author
  • Saul A. Johnson
  • Alexandra Mendes
  • Phillip J. Brooke
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10510)


We propose the use of modern proof assistants to specify, implement, and verify password quality checkers. We use the proof assistant Coq, focusing on Linux PAM, a widely-used implementation of pluggable authentication modules for Linux. We show how password quality policies can be expressed in Coq and how to use Coq’s code extraction features to automatically encode these policies as PAM modules that can readily be used by any Linux system.

We implemented the default password quality policy shared by two widely-used PAM modules: pam_cracklib and pam_pwquality. We then compared our implementation with the original modules by running them against a random sample of 100,000 leaked passwords obtained from a publicly available database. In doing this, we demonstrated a potentially serious bug in the original modules. The bug was reported to the maintainers of Linux PAM and is now fixed.


Password quality Password policy Verification Security Authentication Coq Proof assistant Theorem prover Linux PAM 


  1. 1.
    Appel, A.W.: Modular verification for computer security. In: IEEE 29th Computer Security Foundations Symposium (CSF), pp. 1–8 (2016)Google Scholar
  2. 2.
    Bauereiß, 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)Google Scholar
  3. 3.
    Bertot, Y., Castéran, P.: Interactive theorem proving and program development - Coq’Art: the calculus of inductive constructions. Springer Science & Business Media, Heidelberg (2013)zbMATHGoogle Scholar
  4. 4.
    Blanchet, B., et al.: An efficient cryptographic protocol verifier based on prolog rules. In: CSFW, vol. 1, pp. 82–96 (2001)Google Scholar
  5. 5.
    Burnett, M.: Today i am releasing ten million passwords (2015). Accessed 26 Apr 2017
  6. 6.
    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–403. Springer, Heidelberg (2006). doi: 10.1007/11681878_20 CrossRefGoogle Scholar
  7. 7.
    National Cyber Security Centre: Password Guidance: Simplifying Your Approach (2016). Accessed 26 Apr 2017
  8. 8.
    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–84 (2017)CrossRefGoogle Scholar
  9. 9.
    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–37. ACM (2015)Google Scholar
  10. 10.
    Chlipala, A.: Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant. MIT Press, Cambridge (2013)zbMATHGoogle Scholar
  11. 11.
    Dell’Amico, M., Michiardi, P., Roudier, Y.: Password strength: an empirical analysis. In: INFOCOM, pp. 1–9, IEEE (2010)Google Scholar
  12. 12.
    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–136. Springer, Heidelberg (1997). doi: 10.1007/BFb0028390 CrossRefGoogle Scholar
  13. 13.
    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)Google Scholar
  14. 14.
    Hamming, R.W.: Coding and Theory. Prentice-Hall, Englewood Cliffs (1980)zbMATHGoogle Scholar
  15. 15.
    Hamming, R.W.: Error detecting and error correcting codes. Bell Labs Tech. J. 29(2), 147–160 (1950)MathSciNetCrossRefGoogle Scholar
  16. 16.
    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)Google Scholar
  17. 17.
    Jahoda, M., Krátký, R., Prpič, M., Čapek, T., Wadeley, S., Ruseva, Y., Svoboda, M.: Red Hat Enterprise Linux 7 Security Guide (2017). Accessed 24 Apr 2017
  18. 18.
    Johnson, S.: Behavior of maxclassrepeat=1 inconsistent with docs (2017). Accessed 31 Mar 2017
  19. 19.
    Jones, S.P.: Haskell 98 Language and Libraries: The Revised Report. Cambridge University Press, Cambridge (2003)zbMATHGoogle Scholar
  20. 20.
    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–183. Springer, Cham (2014). doi: 10.1007/978-3-319-08867-9_11 Google Scholar
  21. 21.
    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–537. IEEE (2012)Google Scholar
  22. 22.
    Software Reliability Lab. Verified PAM Cracklib (2017). Accessed 05 Apr 2017
  23. 23.
    Software Reliability Lab. Verified PAM Environment (2017). Accessed 30 Mar 2017
  24. 24.
    Letouzey, P.: Extraction in Coq: an overview. In: Beckmann, A., Dimitracopoulos, C., Löwe, B. (eds.) CiE 2008. LNCS, vol. 5028, pp. 359–369. Springer, Heidelberg (2008). doi: 10.1007/978-3-540-69407-6_39 CrossRefGoogle Scholar
  25. 25.
    Morgan, A.G., Kukuk, T.: The Linux-PAM Module Writers’ Guide (2010)Google Scholar
  26. 26.
    Samar, V.: Unified login with pluggable authentication modules (PAM). In: Proceedings of the 3rd ACM Conference on Computer and Communications Security, pp. 1–10 (1996)Google Scholar
  27. 27.
    Schneider, S.: Verifying authentication protocols in CSP. IEEE Trans. Softw. Eng. 24(9), 741–758 (1998)CrossRefGoogle Scholar
  28. 28.
    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. 13Google Scholar
  29. 29.
    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–663 (2012)CrossRefGoogle Scholar
  30. 30.
    Thompson, S.: Functional programming: executable specifications and program transformations. ACM SIGSOFT Softw. Eng. Notes 14(3), 287–290 (1989)CrossRefGoogle Scholar
  31. 31.
    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)Google Scholar
  32. 32.
    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–10. IEEE (2016)Google Scholar

Copyright information

© Springer International Publishing AG 2017

Authors and Affiliations

  • João F. Ferreira
    • 1
    • 2
    Email author
  • Saul A. Johnson
    • 1
  • Alexandra Mendes
    • 1
  • Phillip J. Brooke
    • 1
  1. 1.School of ComputingTeesside UniversityMiddlesbroughUK
  2. 2.HASLab/INESC TECUniversidade do MinhoBragaPortugal

Personalised recommendations