Difference between revisions of "Web Infrastructure Model"
(→Problems) |
|||
| Line 43: | Line 43: | ||
==Problems== | ==Problems== | ||
| − | * The | + | * The model has no notion of time, so tokens never expire, e.g., id tokens. |
* Users have [[Identifier]]s, but no other [[Attribute]]s, [[Behavior]]s, etc. | * Users have [[Identifier]]s, but no other [[Attribute]]s, [[Behavior]]s, etc. | ||
* Attacks against the browser, including plug-ins are not addressed. | * Attacks against the browser, including plug-ins are not addressed. | ||
Revision as of 12:18, 16 December 2023
The origin of the Web Infrastructure Model is described in the formal review of the Verifiable Credential exchange protocols.[1] 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 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.
References
- ↑ D. Fett, R. Kuesters, G. Schmitz. The Web SSO Standard OpenID Connect: In-Depth Formal Security Analysis and Security Guidelines. arXiv:1704.08539. type: article. arXiv, Apr. 27, 2017. arXiv: 1704.08539[cs]. url: http://arxiv.org/abs/1704.08539 (
