Web Infrastructure Model

The origin of the Web Infrastructure Model is described in the formal review of the Verifiable Credential exchange protocols. A detailed formal description of the WIM can be found in [7]. The WIM is a Dolev-Yao (DY) style model that closely models existing web standards such as HTTP and HTML.

The central building block of the WIM is the communication model. Each entity in the model is a process that listens to one or more IP addresses and consumes events. An event has a message as well as a sender and a receiver IP address. At each processing step of the model, an event is nondeterministically selected from the “pool” of events and delivered to the appropriate process. The entity processes the event and outputs one or more events that are added to the “pool” of events. A message is a formal term over a signature Σ. The signature contains constants (such as strings and nonces) and sequence, projection, and function symbols. Examples of functions are methods for encrypting and decrypting messages or signing terms. The signature Σ can be used to show what an example message would look like for an HTTP request to “http://verifier.ex.com/response?response_code=1234”:

𝑟 := ⟨HTTPReq, 𝑛0, GET, verifier.ex.com, /response, ⟨⟨response_code, 1234⟩⟩, ⟨⟩, ⟨⟩⟩

The last two arguments are empty because the request does not contain a body or a list of headers. The equational theory defines a congruence relation ≡ that expresses the relationship between function symbols in Σ. An example is the encryption and decryption with the key 𝑛1 of the term 𝑟 with a symmetric cipher:

decs (encs (𝑟, 𝑛1), 𝑛1) ≡ 𝑟

A process has a set of IP addresses, a set of states containing terms, and a relation. The relation uses an input event and the state of the process to non-deterministically compute a set of output events

The WIM defines a special process for the attacker. The attacker process collects all received events and outputs all events that can be derived from the collected events. Note that there is a strict definition of what is derivable, e.g. the attacker cannot decrypt a symmetric cipher without knowing the key. There are two types of attackers: First, there is the web attacker who can only listen to their IP address and can only send messages from their IP, and second, there is the network attacker who can listen to all IP addresses and spoof messages with an arbitrary source IP address. Furthermore, the attacker can corrupt any honest process and thereby learn the contents of the corrupted party’s state.

The web browser is another predefined process of the WIM. A web browser models a user by non-deterministically performing user actions such as following a link or entering credentials into a form. The browser stores user credentials in its initial state per domain and only passes them to scripts running under that domain. This means that credentials are not just sent to a malicious site, as could happen in the real world in a phishing attack. The browser also models the behavior of windows, documents in windows, cookies, and web storage data. The browser can execute scripts, which are similar to DY processes and model JavaScript code. A script receives a state from the web browser and returns a new state and a command to be executed by the browser. This command can be, for example, sending a POST request to a server or following a link.

The web browser is part of a web system that formalizes the web infrastructure and web applications. In addition to web browsers, it typically includes honest web servers, honest DNS servers, and a web or network attacker. To simplify the modeling of a web server, the WIM defines a generic HTTPS server that already handles, among other things, the receiving and sending of HTTPS requests.

Problems

• The model conflates Identity and Identifier so it is hard to understand what is at risk for the users of the system. In general it seems that user concerns are entirely lacking from the entire process.
• The model is designed to deter attacks which is a backward-looking protection, not forward-looking where the new attacks will be coming from. This does not mean that protecting form existing attack is not important, just not enough.
• The model has no notion of time, so tokens never expire, e.g., id tokens.
• Users have Identifiers, but no other Attributes, Behaviors, etc.
• Attacks against the browser, including plug-ins are not addressed.

Solutions

The history-based solution of the attack model used by military planners for defense against attack. Gather all of the information from the NIST archives and determine if your solution will defend against them. That is a summation of the history-based approach to threat modeling.

There is another approach, however, capability-based threat modeling. What attacks will adversaries whom I reasonably expect to encounter mount once the system I am developing is deployed? Military planners call this the "responsive threat." There are many famous failures of history-based threat modeling: tanks vs. cavalry, bombers vs. battleships, vacuum tubes vs. electro-mechanical cipher machines, box cutters vs skyscrapers, etc. A very nice distinction. The problem with this approach is that it depends heavily on the notion of "reasonably expect," which is highly obvious, after the fact.

A third approach is risk-based modeling. In this model the assets are enumerated, including the intangible assets like the trust of your customers. Then the flow of all those assets through the system are mapped. Each flow and each storage location needs to be evaluated against a set of known attack modes. At each flow and each node a capability evaluation can be made to determine to the best of the experts knowledge, what vulnerabilities are possible and what is the probability of an attack on that vulnerability. Only then can the decision about accepting the risk or mitigating the attack be made.