Invalid certificates in modern browsers: A socio-technical analysis

The authentication of a web server is a crucial procedure in the security of web browsing. It relies on certificate validation, a process that may require the participation of the user. Thus, the security of certificate validation is socio-technical as it depends on traditional security technology as well as on social elements such as cultural values, trust and human-computer interaction. This manuscript analyzes extensively the socio-technical security of certificate validation as carried out through today's most popular browsers. First, we model processes, protocols and ceremonies that browsers run with servers and users as UML activity diagrams. We consider both classic and private browsing modes and focus on the certificate validation. We then translate each UML activity diagram to a CSP# model. The model is expanded with the LTL formalization of five socio-technical properties pivoted on user involvement with certificate validation. We automatically check whether the CSP# models are socio-technically secure against Man-in-the-Middle attacks using the PAT model checker. The findings turn out to be far from straightforward. From them, we state best-practice recommendations to browser vendors.