Difference between revisions of "Web Infrastructure Model"

Revision as of 22:47, 15 December 2023

the basics of the Web Infrastructure Model and is based on the description of the WIM in [5]. 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