Exploring the Impact of Formal Verification on the Adoption of Password Security Software (PassCert)

Type: National Project Project

Duration: from 2021 Feb 01 to 2022 Jan 31

Financed by: FCT Carnegie Mellon

Prime Contractor: INESC-ID (Other)

Project Web Site: https://passcert-project.github.io/

PassCert’s short-term vision is to build an open-source, proof-of-concept PM that through the use of formal verification, is guaranteed to satisfy properties on data storage and password generation. The goal is to help non-expert users to use stronger passwords without sacrificing convenience, whilst conveying the formal guarantees in an effective way. We aim to determine whether formal verification can increase users’ confidence in PMs and thus increase their adoption. The proof-of-concept PM will result from a close collaboration between researchers from INESC-ID Lisboa, INESC TEC, and Carnegie Mellon.


  • INESC-ID (Other)
  • INESC-TEC (Other)

Principal Investigators