Invalid certificates in modern browsers: A socio-technical analysis

1. Introduction

Although the Web has not been conceived to be a secure platform, nowadays most of the popular websites can be accessed via TLS and are authenticated via certificates. While we can reasonably assume that TLS provides confidentiality and integrity as it uses robust cryptographic schemes, we should be more careful in assuming the same for authentication. The authentication of a website depends, to various degrees, on trust. One element of trust comes either from the web-of-trust concept or from the public-key infrastructure (PKI). Either way, the authentication of a website works through the issuing of certificates. A certificate binds an identity with a public key, and contains other pieces of information that the verifier, also known as authenticator or trustor, needs to check to accept the certificate. The verifier is a software, normally the browser of the user who accesses a website. The browser verifies that the identity on the certificate corresponds to the identity on the website, and that the certificate is signed by a trusted authority. Thus an authentication that succeeds seems to depend mostly on the browser rather than on the user. But when the validation fails, browsers usually resort on the choices of users. In this case, the user is the ultimate responsible for the website’s authentication.

Invalid certificates are not rare. For example, to cut on costs, institutions often self-issue their own certificates rather than purchase them from accredited certification authorities. While the deployment of a private PKI for a large organization also bears costs, self-issuing a certificate comes at no expense. But, even if institutions purchase their certificates from a recognized authority, they may still use the certificate beyond its expiration date or abuse it to certify different domains and sub-domains that are not actually provided for the certificate. With a security take, an invalid certificate may originate from a network attacker who attempts a Man-in-the-Middle attack, namely the attacker replaces the server’s certificate with his own.

We do not intend to contribute to the long-established debate on the interpretation of the technical meaning of authentication [34] but, rather, we expect to substantiate our observation that server authentication with modern browsers goes beyond the technical certification path validation algorithm as described in the X.509 standard [22]. The validation of a certificate is in fact socio-technical to the extent in which modern browsers consider user’s choices and support the validation with novel technologies, such as the HTTP Strict Transport Security (HSTS). Thus, with certificate validation we refer to the property of the extended protocol that browsers customize with user’s involvement and additional security mechanisms.

We note that the way the certificate validation is accomplished varies considerably among browsers. This variety motivates a number of research questions. What are the differences in terms of user involvement in how modern browsers implement server authentication? Which browsers reduce the security risks for users when a certificate is invalid? Can browsers improve their security by involving the user more profitably than they do at present? This list of questions, purposely truncated to length three here, arises when server authentication, and certificate validation in particular, is assessed from a socio-technical standpoint.

Contribution. Our work complements traditional studies in human-computer interaction by advancing what seems to be the first formal analysis of browser’s certificate validation that is not only logically conditioned on the technology but also on user actions. This formal analysis was not carried out using a known approach. By contrast, it was not obvious how to represent (portions of) the functioning of a browser in order for the security analyst to quickly get confidence with its properties without reading long prose. Various graphical notations were tried out, and finally we found Unified Modelling Language (UML) activity diagrams [55] to bear the necessary flexibility. Building these diagrams is a major hallmark in our understanding of the technicalities of the browsers. However, they are only semi-formal and not directly executable; a formal model is needed for a fully automatic analysis. We therefore translate our UML diagram models to models in the Communicating Sequential Processes (CSP) process algebra [37]. The models are extended with a Linear Temporal Logic (LTL) specification of the properties of interest. Each extended model forms the input to the Process Analysis Toolkit (PAT) model checker [62], which yields the findings reported below.

This manuscript extends our earlier conference paper [12] with various contributions: (i) it considers expired and revoked certificates as causes that lead to the failure of certification path validation; (ii) it analyzes a new desktop browser, Safari, in addition to Chrome, Internet Explorer, Firefox, and the cross-platform browser Opera Mini; (iii) it considers the analysis of private browsing mode, and the interleaving of classic and private browsing; (iv) it includes a novel security property that concerns browser’s certificate validation, so that overall the manuscript considers five socio-technical properties. Finally, (v) it analyzes Safe Exam Browser (SEB), a kiosk browser conceived for Internet-based exams. Although SEB is not as popular as the other browsers considered in this manuscript, its particular purpose is to minimize the involvement of users; it is then interesting to evaluate how this feature affects certificate validation. The mix of new browsers, modes, and properties increases the 16 scenarios analyzed in the previous paper to this manuscript’s 60 scenarios. A disclaimer is in order that the proposed list of properties is not meant to be complete; however, our browser models are fairly well detailed, for example by allowing for the reception of a newly issued certificate to replace the older, expired one.

The intellectual value that this manuscript gains is at least twofold: (i) it makes three best-practice recommendations to browsers upon the basis of the additional findings on the new set of browsers and modes; (ii) it finds two bugs in Safari, respectively one in Safari for OS X and one in Safari for iOS, which (we reported to Apple getting a reply that a fix would be available in the upcoming versions of the browser, and) are now filed with the vulnerability identifier CVE-2015-5859 [6,54]. It is also worth noting that, after our conference paper observed that Opera Mini fails to prompt the user in case of invalid certificate [12], a new version of the browser fixed this issue.

Socio-technical analysis. Ellison coined the concept of a ceremony extending “the concept of network protocol by including human beings as nodes in the network” [26]; therefore, a ceremony is a technical system extended with its human users and the possible interactions between the system and its users. A ceremony extends the notion of protocol to include interactions, messages, and behaviours of the social components. Similarly, the term socio-technical system refers to the system including its social components [29]. Therefore, analyzing a ceremony means to conduct a socio-technical analysis focusing on socio-technical properties. It is somewhat understood that a socio-technical property pertains to how user choices affect a traditional property of a technical system such as a security protocol; for example, we mentioned above that certificate validation is a socio-technical property. However, there seems to exist no standard approach to analyzing socio-technical properties and, in particular, to effectively modelling the user in support of that analysis. While this is subject of significant international effort, as demonstrated by the vast related work (Section 2), we base our work upon the recent ceremony concertina traversal methodology [11]. It prescribes selective focus on the layers that interpose between society and each technical system, and leverages on a previously identified layering of a ceremony [10]. In particular, layer IV is about the user expression of personas, each embodying a different attitude towards a technical system, such as a careful or a distracted one; layer III is about the interaction of the given persona with the user interface of the given technical system, normally executed on a computing device; the management of the user interface on the device, and the potential communication of the latter with another remote device are captured by the lower layers.

Following the ceremony concertina traversal methodology, our work focuses on layer III of the TLS certificate validation ceremony. In consequence, this article is, in particular, not about user studies: these traditionally assess layer IV, namely how people approach and express themselves in front of a technical system. By contrast, this article shall inspect how the particular choices of a user, namely a user persona, can affect the crucial property of certificate validation. We found out that this can be done elegantly in CSP by appealing to non-deterministic operators that allow us to account for all possible personas that can play at layer III – again, leaving aside an assessment on how and why such personas manifest themselves, which would stand on layer IV. While layer IV is the traditional playground for researchers from the Humanities, and the lower layers for researchers from Computer Science and Engineering, layer III is the meeting point for the trans-disciplinary discourse at the basis of inherently socio-technical analysis. It is therefore considered particularly challenging at present [11].

Article outline. After the related work discussed in Section 2, we position our work and detail the different aspects of certificate validation in Section 3. We introduce a description of the browsers concerned in this manuscript in Section 4, and detail their certificate validation ceremonies in Section 5 using UML activity diagrams. We then analyze five socio-technical properties on the browser’s ceremonies with the PAT model checker in Section 6. We discuss the results in Section 7 and provide three recommendations. Section 8 discusses some implications and concludes the manuscript.

2. Related work

A few works have developed formal verification techniques to model and analyze web browsers [7,8,14,16,17,30]. Akhawe et al. [4] introduce a formal model of web security. They define the main components of the web, namely Non-Linear Time, Browser, Servers, and the Network as Web Concepts. They consider a spectrum of threats that span from a malicious web server to a more advanced attacker who is able to inject contents into an honest web server. Finally, they analyze two security properties, i.e., security invariants and session integrity, in five web security mechanisms. The considered mechanisms include neither TLS nor certificate validation, and the formal model assumes that the user correctly interprets the browser’s security indicators. Our work focuses on certificate validation and considers users who may not correctly understand security indicators. Groß et al. [36] propose a formal framework to model a web browser and the behaviour of a user who interacts with the browser. They validate their framework by analyzing the security of password-based user authentication. Instead of modelling an ideal browser, we analyze the actual implementation of modern browsers. It would be interesting to merge our approach with their model of web browser. Formal verification techniques have been used to analyze Human-Automation Interaction [15]. They mostly focus on cognitive aspects of users rather than on the technical aspects of the systems the users interact with. In this manuscript, we consider user choices, which do depend on human cognitive factors, but our focus is more on the technical part, namely the web browsers.

There are many studies that conduct a security analysis of certificate validation [27,28]. Georgiev et al. [33] analyze certificate validation in the context of TLS for different web applications, including shopping carts, cloud storage, and payment gateways. They show several vulnerabilities due to the customization of APIs that implement certificate validation without following any standard. Differently to our automated approach, they detect attacks by visual inspection of the source code; moreover, the analyzed applications involve no browsers. Kaminsky et al. [41] discuss different attacks against the certificate infrastructure. They point out that certificate issuers and browsers may differently interpret the field subject name in an X.509 certificate. Such a lack of standardization makes the subject name vulnerable to injection attacks. A recent update to the X.509 standard [71] aims to fix the issue. Clark and Van Oorschot [20] provide a comparative evaluation of enhancements implemented into browsers for certificate validation. They argue that it is becoming more common that attackers own valid certificates for a web site. Attackers’ attention focuses on certificate infrastructure because of its reliance on human factors. We share their view that certificate validation goes beyond the mere binding between a domain name and a public key.

Certificates may be revoked for various reasons, such as compromise of the corresponding private key or variation of the subject details. Abstracting away from those details, Liu et al. advance a comparative analysis on how modern browsers handle revocation [46]. They demonstrate that different browsers make dissimilar decisions in mapping the output of the certificate revocation statuses “unavailable” and “unknown” into yes/no decisions. Contrarily to our earlier work [12], the mapping is now explicitly represented in our models (Section 5).

Different solutions have been proposed to modify the structural flaws of the certificate infrastructure [39,50,51], but they also require dedicated modifications to the protocols that use certificates to achieve authentication. For example, the Certificate Transparency project [44] suggests an improvement to the current TLS certificate system that consists in supplemental monitoring and auditing services via certificate logs. Such improvement requires a different server implementation to accommodate a TLS extension. Structural solutions such as TLS extensions may take a long time before being implemented extensively, because both browser and server need to support the extension. In this manuscript, we also end up with a similar proposition, but it requires a modification of the browser only, with no change required on the server and on the TLS protocol.

The human aspect of certificate validation has recently been analyzed via different empirical studies and more recently also with formal methods [9]. Akhawe and Felt [5] make an empiric analysis to assess the effectiveness of browser security warnings. In particular, they measure the users’ click-through rates on certificate and malware warnings. They find that users tend to ignore warnings as they click through the Chrome certificate warnings. Such a finding led Google to redesign Chrome’s certificate warnings. Similarly, Flinn and Lumsden [31] conduct a survey to assess whether users are aware of the security risk they face online. They find that users have different interpretations of the term “secure web site” and are generally unaware that TLS provides server authentication. By contrast, our formal analysis does not pertain to user perception, but investigates the various ways in which user’s choices influence server authentication. Jøsang et al. [40] point out that web browsers can only do syntactic server authentication, as TLS cannot provide semantic server authentication. Thus, the attacker can exploit semantic attacks to trick the user. They advocate the need of a framework to determine the assurance level of server authentication. Our approach aims at analyzing how web browsers help users to avoid such server authentication attacks. Gajek et al. [32] propose a new authentication protocol that consists of a mix between the Password Authentication Key Exchange (PAKE) and TLS protocols without relying on a PKI. They formalize a user as a probabilistic machine. The user’s behaviour can recognize the so-called human-perceptible indicators like pictures and sounds. In contrast, we are not interested in the cognitive aspects, and make minimal assumptions about the user capabilities. Akhawe et al. [3] produce a taxonomy of certificate validation warnings and collect data over more 10 billion TLS connections that are not under MITM attacks. Thus, they calculate the false positive rate of showing warnings and present a number of recommendations to improve the design of browsers. Conversely, our approach considers MITM attacks.

The security of browsers has been studied variously, for example to avoid the user’s oversight of warning messages [64], or to improve the readability of their contents [13]. These works are positioned over the cognitive aspects of human-computer interaction with the browsers. In short, our work can be positioned as follows: we see the socio-technical system consisting of a web server, a computer network, a browser, a user and possibly an intruder as a ceremony in the sense of Ellison [26]; we focus on layer III of that ceremony, referring to a layering of Bella and Coles-Kemp [10], where user personas interact with the interface of a technology.

3. Basics

This section clarifies a few technical notions and sets the terminology used throughout this article. First, it details the constituents of a web certificate and explains how their validation works or can fail. Then, it discusses the regulations that specifies the path validation of a web certificate, and observes how the standard eventually leaves the interpretation of certificate validation to browser manufacturers. In consequence, certificate validation becomes a mix of user’s choices and technical security mechanisms, from which emerges that certificate validation in modern browsers is a socio-technical process. The sequel of this section outlines a few basic concepts that are needed later.

3.4. Socio-technical aspects of certificate validation

Browsers communicate with the user in different ways, such as text warnings, pop-up windows, open or closed padlocks, and colored address bars. The main component that browsers use to interact with the user is the viewport, which is depicted in Fig. 1.

OPEN IN VIEWER

Fig. 1.

The viewport component of a browser.

The user can choose any of the options proposed in the browser’s viewport: a cautious user may close the browsing session, while a curious one may click through a warning. Users may be variously skilled and educated. They are influenced by a huge variety of local or global cultural values.

Malicious websites nowadays can use scripts to gain major control on browser’s viewport and deceive users [20] on security warnings. Although the design of browser’s security indicators has improved over the years [70], a number of studies have shown that users tend to click through a warning without paying attention [3,43,64]. These social factors make the problem of certificate validation a security problem that cannot be solved by purely technical means.

3.4.1. HTTP strict transport security (HSTS)

A few proposals have been recently advanced to minimize the participation of users in certificate validation and make security less reliant on user’s choice [38,65]. Different browsers have adopted HSTS [38], a security mechanism originally conceived to thwart TLS stripping attacks [48,49]. In a TLS stripping attack, the attacker forces the user to communicate via an HTTP connection although the web server supports HTTPS connections. HSTS-compliant browsers prevent “unsecured” HTTP connections to HSTS-compliant web servers. To do so, the web server sends the browser an HSTS header during a secured TLS session. Optionally, the HSTS header may include a list of the only certification authorities allowed to issue the web server’s certificate. Then, the browser adds an internal policy stating that the concerned web server must be accessed via HTTPS only, and with a valid certificate. Thus, once the authentication of the web server succeeded, it shall not fail in the future.

HSTS minimizes user’s participation in favour of a purely technical enforcement of security: if the certificate validation fails for browser-known HSTS-compliant web servers, then the browser shows the user an error message (not a warning) and aborts the connection. Some browsers implement an HSTS pre-loaded list of web servers precisely to make those servers browser-known and hence mitigate so called bootstrap MITM attacks: this attack exploits a vulnerability that sees a user type a URL or follow a link using HTTP rather than HTTPS to an unknown HSTS-compliant server.

Since HTTP uses an insecure channel, the first attempt to interact with the specified server is still vulnerable to MITM attacks. However, HSTS usage statistics show that only a small percentage of top web servers is HSTS-compliant [18,42]. Similarly to what they do with certification path validation, browsers implement HSTS differently from each other, as we shall see below.

4. Modern browsers

This manuscript considers the most popular browsers available nowadays. According to StatCounter [61], the most used browsers are Firefox, Chrome, Internet Explorer, and Safari. Additionally, we consider two more browsers: Opera Mini and Safe Exam Browser (SEB) [60]. Opera Mini is the most popular platform-independent browser [56] and is available on many mobile devices. Its analysis is motivated because nowadays more and more users prefer to browse the Web with touchscreen mobile devices, and in particular Opera Mini dramatically reduces the amount of data transferred. In doing so, we aim to evaluate how such restrictions affect certificate validation. SEB is the state-of-the-art browser to carry out online exams securely, in which authentication is a critical security property [25]. By analyzing SEB socio-technically, we mean to evaluate how certificate validation is affected by a kiosk browser intended to minimize the interaction with its users. We remark that not all browser specifications are available, hence many of our modelling choices are derived empirically, as noted below.

Firefox. The inception of Mozilla Firefox originates from Netscape Navigator. According to StatCounter [61], it is the third most popular browser over desktop, mobile, tablet, and console devices. Among the browsers we consider, Firefox seems to be the most complete: it supports HSTS, distinguishes two different certificate stores, and allows users to store server certificates either permanently or temporarily. Since Firefox is open source, we studied it by looking at its official documentation and source code. In this manuscript we consider Firefox version 36.0.4.

Chrome. Although Google Chrome is the youngest browser we consider, it is the most popular. It was the first browser to support HSTS policies, and adopts different certificate stores depending on the operating system underlying the browser. Chrome is based on the Chromium open source code with minor differences. We analyzed Chrome inspecting the Chromium source code and using empirical tests. This work considers Chrome version 41.0.

Internet Explorer. Microsoft Internet Explorer was the most popular browser for years, and has been overtaken by Chrome only recently. Currently, it does not support HSTS, which is however planned to be implemented soon [53]. Internet Explorer is available only for Windows operating systems, and uses their certificate stores. Since Internet Explorer is closed source, we relied on empirical tests, also supported by network analyzers. The version of Internet Explorer analyzed is 11.0.16.

Safari. Safari is the browser developed by Apple and is popular on the company devices. It supports HSTS and, similarly to Firefox, distinguishes two different certificate stores allowing users to store server certificates. Safari is available only on Apple’s operating systems and is closed source. We thus analyzed it empirically and assisted by network analyzers. We studied Safari 8.0.3.

Opera Mini. Opera Mini is used by more than 244 million people per month and is particularly popular in emerging countries, according to the company data [56]. It aims at being the most lightweight browser for any Java-capable device. To do so, the browser uses Opera proxy servers and compression technologies to reduce traffic and speed up page display. Thus, although communications to the proxy server are encrypted, there is no end-to-end TLS encryption between the browser and the web server. We analyzed the (closed-source) browser empirically, using a Java emulator with network analyzers. In this work we consider version 7.6.4.

Safe Exam Browser. The last browser considered in this manuscript is SEB, which is developed at ETH Zurich. The goal of SEB is to impede fraud in online exams by preventing access to unwanted resources and utilities of the operating systems. In practice, it turns the device into a kiosk for exams by removing any other components of a browser but the viewport. Due to the stringent security requirements imposed by the risk of cheating at exams, SEB is an interesting case study for our browser analysis. Since SEB is open source, we studied it by looking at its official documentation and source code, analyzing the version 2.0 of the browser.

5. Modelling certificate validation

As seen in Section 3, the certificate validation is not an algorithm, since it may involve users. Therefore, we refer to it as a ceremony, namely as a heterogeneous protocol where users and machines are the communicating processes.

The certificate validation ceremony includes a user, the browser, and the web server. In this section, we provide a formalization of the ceremony for each browser. However, finding the right formalism for the socio-technical analysis is not easy. The standard notation to describe security protocols is the Alice-and-Bob notation [47]. Although this notation provides a simple and clear description, it comes with some limitations: it cannot express fork, join, and branching, which are essential, for example, to model multiple user’s choices in the certificate validation. Flowcharts offer a graphical description and look suitable to describe browsers and algorithms in general, but are less appropriate for the description of protocols: we have the three roles of browser, user, and server, and we need to detail the messages that the roles exchange. Message sequence charts extend flowcharts to the domain of protocols, emphasizing the interaction among the roles. Still, they have the same limitation of the Alice-and-Bob notation.

Thus, we choose the semi-formal and graphical description of UML Activity Diagram [55], but we are aware that also Workflow Description Languages such as BPMN would have suited well. An UML activity diagram is a graphical scheme that defines the activities needed to meet a given functionality. UML activity diagrams are made of shapes that model choices, interactions, and concurrency. A description of the main UML activity diagram’s shapes is given in Appendix A. The contribution of activity diagrams is threefold. First, they give an intuitive representation of a protocol session, highlighting the mechanisms used on each role. Second, they can represent parallel actions (fork/join) and multiple choices (branching). Third, they can be easily translated in a fully formal language, thanks to their semi-formal semantics [1]. In short, the activity diagrams provide invaluable help to our understanding of the various entanglements of modern browsers, and we can now comment a posteriori that we would not have managed the formal models for the browsers without an intermediate graphical notation.

We translate UML activity diagrams to CSP# [62], a modelling language that enriches the high-level operators of CSP (e.g., choices, interleaving, hiding, etc.) with low-level programming constructs (e.g., arrays, while, etc.). The CSP# code is then fed to an automatic tool that checks whether the input model guarantees a set of properties. The code is given in Appendix B.

5.1. UML activity diagrams for certificate validation

We build nine activity diagrams that model the certificate validation ceremonies for the browsers both in classic and private browsing. Although we consider six browsers, we do not model the private browsing of Internet Explorer and Opera Mini because they are identical to the corresponding classic browsing modes, and we do not model the classic browsing for SEB since it supports only private browsing.

OPEN IN VIEWER

Fig. 2.

Activity diagram for certificate validation in Firefox.

OPEN IN VIEWER

Fig. 3.

Activity diagram for certificate validation in Firefox in private browsing.

The UML activity diagrams modelling Firefox in classic and private browsing are respectively in Fig. 2 and in Fig. 3. The remaining seven activity diagrams can be found in Appendix A.

The activity diagrams include the functionalities limited to describe how each browser achieves certificate validation. Each activity diagram has four columns, each representing a communicating role. From left to right we have the user, the browser user interface, the browser engine, and the server. Each role begins with a filled dot that points to their first activity. We assume that the browser bootstraps with the start web page, which is displayed in the browser user interface. Next, the browser user interface can load a web page because the user types a URL or clicks on an active link in the currently displayed web page. A label close to a thick arrow defines the object exchanged between activities. Activities may need to get access to datastores, which are represented as object nodes.

6. Formal analysis of certificate validation

We use model checking to formally analyze certificate validation. We provide a systematic method to translate the UML activity diagrams to a formalization in CSP# that is amenable to automatic validation by means of PAT. Then, we define a threat model and specify the socio-technical properties that concern certificate validation in LTL.

It must be noted that the idea of using LTL model checking for validating web protocols is not a novelty: notably it has been vastly explored within a successful EU project [67]. Our work explores how a generic model checker can be tailored to the same task.

7. Findings

We studied our five properties on the six browsers by checking the satisfiability of our formulas on the CSP# models of the certificate validation. As said above, we considered Firefox, Chrome, and Safari in three different modes: classical browsing, private browsing, and their interleaving. In total, the analysis covered 60 different scenarios due to the mix of browsers, modes, and properties.

Interpreting the output of the tool required some effort, and Table 2 summarizes the findings. At first glance, the browsers that verify the highest number of properties are Chrome and SEB, then come Internet Explorer and Firefox, and lastly Safari and Opera Mini, but this conclusion should be gauged through the details that the table conveys.

It was possible to encode most of the scenarios without incurring state explosion: PAT terminates the validation of each scenario in just a few seconds over an Intel i7 processor with 8 GB RAM. However, we needed to assume no expired certificates to avoid non-termination in five scenarios that turn out to ensure the properties: Applying HSTS User Security on classic browsing of Firefox, and Applying HSTS Bootstrap on classic browsing of Safari, Firefox, and the respective interleaving. This does not seem limitative because expired certificates would only cause CertificateIsValid to fail, which in turn may also fail due to a subject mismatch or to an unknown certificate issuer.

Also, as expected, if a property fails in one of the modes (i.e., classic or private), then it fails also on their interleaving. However a more interesting result is that a session in one mode may influence a later session in a different mode. This is the case with Safari for Applying HSTS Bootstrap. In the remainder, we comment on each property in detail.

Warning users. The first property is found valid over Chrome, Internet Explorer, and SEB. It is also valid in Firefox in private browsing. By contrast, the model checker shows traces that falsify the property over the other modes for Firefox, Safari, and Opera Mini. With Firefox and Safari the traces are similar. They report a sequence of two TLS sessions both with a MITM attack. In the first session, the browser connects to the corrupted server and warns the user, who chooses to store the certificate of the attacker anyway. In the second session, the user tries to get access to the same server, but this time the browser has the attacker’s server certificate stored, and completes the session without warning the user. This is due to the drawbacks of storing server certificates, which Firefox and Safari allow their users to do. Notably, Firefox in private browsing forbids the user to store server certificates, hence the property turns out to be valid. The trace that falsifies the property with Opera Mini is rather trivial because the browser does not involve the user at all. Opera Mini in fact shows a padlock when the certificate is valid, but even if the certificate is invalid, the browser completes the TLS session anyway, without informing the user.

Storing server certificate. The second property turns out to be the most tricky to be interpreted. It is found that all browsers verify the property except Firefox and Safari, since the latter are the only browsers that allow a user to store server certificates. This is because the property is a logical implication whose precondition is trivially falsified by the browsers that do no store server certificate. The property does not hold on Firefox in classic browsing and on Safari in all modes, even though the precondition is not falsified. The user can in fact replace a server certificate as many times as she wishes to, while the browser does not inform the user that a server certificate was already stored. In support of this, the tool exhibits the following counterexample. In one session, the user engages with an honest server that transmits a self-issued certificate; the browser warns the user about the invalid certificate, but she chooses to store the certificate, thus the browser successfully concludes the TLS session. In a subsequent session, the user wants to connect again with the same server, but this time the attacker interposes himself between the communication and sends a self-issued certificate pretending to be the honest server; the browser warns the user about this second invalid certificate, regardless the fact that another certificate was already stored for the same server; the user decides to store also this certificate and the browser concludes the TLS session.

Applying HSTS user security. The third property is valid in classic browsing on Chrome and on SEB. PAT does not terminate in the full model of classic browsing on Firefox unless assuming no expired certificates. In that case, the property is valid. The property does not hold in private browsing because Firefox and Chrome prefer to remove HSTS policies stored during private browsing sessions to protect user’s privacy. In fact an examination of the stored HSTS policies would reveal which HSTS-compliant websites the user visited in private browsing. Surprisingly, the property is not valid on Safari in any mode. The model checker shows a trace as follows: in the first session the attacker interposes himself in the communication, and the user chooses to store the attacker’s certificate. In a subsequent session, the browser communicates with the honest server, from which it receives the HSTS header. Then, in a new session, the attacker interposes himself again on the communication, and the browser does not abort but concludes with no warnings. This is because a user’s approved certificate bypasses the HSTS policy in Safari as the browser prioritizes user’s approved certificates over HSTS policies.2

Applying HSTS bootstrap. The fourth property is checked over the browsers that support HSTS. PAT does not terminate in the full models for Firefox and on classic browsing for Safari. The property can be proved valid only assuming no expired certificates. It is valid on Chrome but not on private browsing of Safari, which does not consider the HSTS pre-loaded list.3

Learning from server certificate history. Finally, the fifth property holds only on SEB, in which the precondition ( F INISH TLS ∧ ¬ CertificateIsValid ) is always falsified since SEB aborts the session when the certificate is invalid. However, the property is not valid in the other browsers. This denounces the stateless philosophy whereby browsers do not record warnings they issued in the past, hence browsers cannot leverage upon them at present.