owned this note
owned this note
Published
Linked with GitHub
---
creation-date: 2024-06-04T00:00:00.000Z
tags: notes/paper
date-published:
link: https://eprint.iacr.org/2024/447.pdf
gists:
- id: 54511c0770dcc370b07190879e771d68
url: 'https://gist.github.com/thor314/54511c0770dcc370b07190879e771d68'
createdAt: '2024-10-03T23:07:03Z'
updatedAt: '2024-10-03T23:07:04Z'
filename: paper-Origo proving provenance of sensitive data.md
isPublic: true
hackmd:
url: https://hackmd.io/jsRFD1IORCGveQlzRBwwnA
title: paper-Origo proving provenance of sensitive data
lastSync: 2024-11-14T22:13:42.678Z
---
# paper-Origo proving provenance of sensitive data
## abstract
Transport Layer Security (TLS) is foundational for safeguarding client-server communication. However, it does not extend integrity guarantees to third-party verification of data authenticity. **If a client wants to present data obtained from a server, it cannot convince any other party that the data has not been tampered with**. **TLS oracles** ensure data authenticity beyond the client-server TLS connection, such that **clients can obtain data from a server and ensure provenance to any third party**, without server-side modifications.
Generally, a TLS oracle involves a third party, the verifier, in a TLS session to verify that the data obtained by the client is accurate. Existing protocols for TLS oracles are communication-heavy, as they rely on interactive protocols.
We present ORIGO, a TLS oracle with **constant communication**. Similar to prior work, ORIGO introduces a third party in a TLS session, and provides a protocol to ensure the authenticity of data transmitted in a TLS session, without forfeiting its confidentiality. Compared to prior work, we rely on intricate details specific to TLS 1.3, which allow us to prove correct key derivation, authentication and encryption within a Zero Knowledge Proof (ZKP). This, combined with optimizations for TLS 1.3, leads to an efficient protocol with constant communication in the online phase. Our work reduces online communication by 375× and online runtime by up to 4.6×, compared to prior work.
## introduction 1-2
### intro
- applications
- highlight 3rd party logins
- main note on methods:
- in TLS 1.3 the IV for Authenticated Encryption with Associated Data (AEAD) is derived from the traffic secret to facilitate a TLS oracle that does not demand for any communication intensive 2PC.
- a ZKP can be used to prove compliance with TLS 1.3, ensuring the same properties as achieved in previous work, under the assumption of a weaker network adversary that is unable to intercept traffic between the proxy verifier and server.
- Additionally, we provide an efficient transformation of AEAD ciphertexts to SNARK friendly commitments, enabling clients to prove disjunct statements on data obtained — without demanding re-execution of the protocol.
### related
All related papers use 2PC.
- proof systems with TLS to
- filter network traffic
- blindly obtain certificates
- prove non-reputiation
- provide offchain data to blockchains
- TLS-N (not TLS Notary) TLS-N introduces a server side extension
- Deco - without server side adaptation; with a mode where verifier acts as proxy between server and client, relying on 2PC during TLS handshake
- this paper claims to achieve without relying on 2PC (?)
- middlebox paper - clients send queries and prove traffic is compliant
- DiStefano - guarantees ring privacy with ring signatures over TLS certs
- what is "ring privacy"?
- Janus - TLS oracle tailored to TLS 1.3 verifying data provenance, relying on HVZK + {handshake, record layer} 2PC to secure against MiTM attacks
## conclusion 6-8
### implementation
- claimed 5k lines of golang code, using gnark-crypto
- integration example with paypal API and gitcoin passport
- Matt notes that they didn't open source the better part of their code base
### evaluation
- observed at most 3.5x time overhead on network traffic
- claimed E2E rurntime between 1 and 1.6s
### discussion
- main challenge discussed, minimize prover in-circuit operations
- total comms overhead around 2.4kB and 1-2 second proof generation time
- drawback: assumption that MiTM attacks (by a malicious client) are infeasible
- to instantiate the attack, the client would need to manipulate DNS resolution (trick the proxy) or intercept traffic between proxy and server
- drawback: large 100-300MB SRS, large offline preprocessing computation
- bottleneck: AES encryption remains the bottleneck in circuit compilation and proof generation. Recent work shows how to minimize AES constraints with lookup arguments.
## personal evaluation
- primary claim is a TLS 1.3 oracle with constant communication by proof of correct key derivation, authentication, and encryption with a ZKP
- concerned how they will achieve this without 2PC, sounds too good to be true
- mildly concerned about the number of typos and spelling errors in the paper
## preliminaries
- IANS: TLS 1.3, HKDF, HMAC, AEAD, zkSNARKs
- TLS 1.3 simplified as 2 layers
- handshake layer - negotiating the "Client Application Traffic Key CATK" and "Server Application Traffic Key SATK" - note that these keys should be identical in contents
- record layer - apply the traffic keys in AEAD to send application data
- AEAD, HKDF and HMAC - some bit twiddling hashes for authentication, see my note [[object-HKDF and HMAC]] for deets
- note that in AEAD, data is fragmented in 16kB maximum **records**. Most commonly AEAD used in AES-GCM. This work ignores the AD in AEAD as it is not relevant.
- SNARKs - skip
- Sec guarantees - adaptive adversary, honest server, assume client cannot MITM server<->proxy,
- properties to show
- client integrity - faulty proof not accepted
- verifier integrity - verifier cannot block or tweak client message traffic
- privacy - proxy cannot obtain knowledge about the message, beyond the header and the message size
## 4 attack on tls 1.3 on the integrity of messages
*It's difficult to actually read this section for implication. Appx C does not clarify matters. Also not sure how much this section matters, really.*
- **receiver binding** - the receiver of ciphertexts
- Carter Wegman MAC is not Collision Resistant, therefore TLS is not RB
- *tk: useless distinction in practice? I don't really understand their attack*
- **strong receiver binding** - modeled security game $\text{sr-BIND}^\mathcal A_{AEAD}$
## 5 Origo
*The actual protocol. Unfortunately, whoever wrote this section needs an english speaker.*
### overview: 3 phase protocol between server, proxy verifier, and client
- **handshake and request execution** - client-server handshake and subsequent traffic is routed through the proxy. Proxy obtains encrypted transcript of communication.
- **pre-processing** - client generates zkp-specific public values from the handshake transcript
- **proof generation & verification** - client proves integrity of data of session
- verification of authenticity of the server certificate and proof
### key derivation proof
*section is a struggle to follow, protocol not stated clearly at all*
- **what is checked**:
- verify the certificate chain
- **"non-ambiguity"** - prove a mapping of session keys against transcript data
client computes a ZKP that shows:
- mapping of TLS 1.3 keys to transcript data (zk to avoid revealing client session keys)
#### key-independence property optimization remark
Authors advertise an optimization to the cert chain verification.
Grubbs et al show that deriving HS (handshake secret) based on private input y and public key Y lead to a non-ambiguous sample of HS. (?)
The client may disclose the SHTS to the proxy without compromising the record layer keys or contents. The proxy may then use the SHTS to derive the handshake encrypting key, SHTK to decrypt handshake traffic and verify the message.
##### Key Independence Property and SHTS notes
The **Key Independence Property** in the context of TLS 1.3 ensures that the leakage of one key does not compromise the security of other keys derived within the same protocol run. Specifically, each key is derived using a Hierarchical Key Derivation Function (HKDF) with a unique context and input, ensuring that no two keys are directly related or can be used to infer one another.
The Server Handshake Traffic Secret (SHTS) is derived during the handshake phase of TLS 1.3 using the HKDF. The derivation process involves the following steps:
1. **Extract Step**: The initial secret is derived using the HKDF-Extract function, which takes in a salt and an initial key material (IKM). In the context of TLS 1.3, the pre-shared key (PSK) or the output of the Diffie-Hellman exchange is typically used as the IKM.
$$\text{Early Secret} = \text{HKDF-Extract}(\text{salt}, \text{IKM})$$
2. **Derive Handshake Secret**: The handshake secret is derived using the HKDF-Extract function again, where the salt is the early secret and the IKM is the output of the Diffie-Hellman key exchange.
$$\text{Handshake Secret} = \text{HKDF-Extract}(\text{Early Secret}, \text{DH Output})$$
3. **Expand Step**: The Server Handshake Traffic Secret (SHTS) is then derived using the HKDF-Expand function, which takes in the handshake secret, a context string (info), and the desired output length. The context string typically includes the handshake transcript up to this point.
$$\text{SHTS} = \text{HKDF-Expand}(\text{Handshake Secret}, \text{info}, \text{length})$$
#### protocol for out-of-circuit verification of certificate
1. **Derive Finished Key for Server $(fk_S)$**:
$$\text{fk}_S \leftarrow \text{HKDF.expand}(\text{SHTS}, \text{"finished"} \parallel \text{ " "})$$
This key is used to generate the HMAC for the server's finished message.
2. **Compute HMAC for Server Finished Message (SF')**:
$$\text{SF}' \leftarrow \text{HMAC}(\text{fk}_S, H_7)$$
This HMAC ($\text{SF}'$) represents the expected value of the server’s finished message, which has been used by the server to authenticate messages.
3. **Verify Server Finished Message**:
$$\text{SF}' \stackrel{?}{=} \text{SF}$$
The computed HMAC ($\text{SF}'$) is compared to the received Server Finished message ($\text{SF}$). This step verifies the integrity and authenticity of the server’s finished message. If the values match, it confirms that the handshake messages exchanged so far are authentic and have not been altered.
4. **Verify Server Certificate**:
$$\text{ok} \stackrel{?}{=} \text{verifyCertificate}()$$
Ensure that the server’s certificate is valid.
Restated in short:
$$\Pi_{\text{Auth}}(\text{SHTS}, H_7, \text{SF})$$
$$
\begin{aligned}
&1. \quad \text{fk}_S \leftarrow \text{HKDF.expand}(\text{SHTS}, \text{"finished"} \parallel \text{ " "}) \\
&2. \quad \text{SF}' \leftarrow \text{HMAC}(\text{fk}_S, H_7) \\
&3. \quad \text{SF}' \stackrel{?}{=} \text{SF} \\
&4. \quad \text{ok} \stackrel{?}{=} \text{verifyCertificate}()
\end{aligned}
$$
## second pass at understanding section 5, Origo
### 5.1 key derivation
*a pair of notes justifying revealing the SHTS value as public input to the zkp, and an optimization on proving HMAC evaluations.*
#### revealing SHTS
*mainly a note about revealing the SHTS to the proxy, and what work proxy is supposed to do, I think. I'm confused about some parts of this section.*
- Claim that verification of the server cert must be computed in the zkp circuit, and is costly. The authors propose a "shortcut" based on the key independence property of TLS 1.3 (the leakage of one key does not compromise the security of other keys).
- The authors propose to leak the SHTS to the proxy, which it may use to derive the SHTK to decrypt handshake traffic, and verify the server finished message.
- ==Does that mean the proxy relies on another party verifying the server cert? Remark not clear.==
- the proxy...can efficiently verify transcript authenticity in a local out-of-circuit computations" - ==that is, the client would not prove the server authenticity in-circuit? This contradicts the top claim.==
- authors note that transcript hashes $H_7,H_2, H_3, H_0$ are computed by the proxy
- ==what is this remark highlighting? Are the authors noting that, from $(\text{HS}; H_2, H_3, \text{SHTS})$, the proxy computes all other handshake key values in figure 5==?
- ==What is the semicolon intending to communicate? $(\text{HS}; H_2, H_3, \text{SHTS}==)$
- ==Was the intent of this remark to just describe that, from the SHTS and HS (or dHS), the proxy can compute the rest of the handshake values==?
#### HMAC optimization note
A note on optimization of TLS 1.3 key derivation wrt structure of SHA-256 HMAC, providing a way for the verifier to compute the expensive SHA256 HMAC mostly out-of-circuit to use as a public input value to the zkp. They bury the lead, but the point is that:
> the first call of the one-way compression blockcipher inside SHA256 hides inputs $(K\oplus ipad)$ or $(K\oplus opad)$ of 64 bytes and with that, hides the secret K of the prover...the output of the compressing blockcipher in SHA256 can be used as public input to reduce ZKP circuit complexity.
That, is the prover can compute $f$ and disclose it to the verifier, which computes the remaining part of the hash out-of-circuit.
HKDF.{extract,expand} both use HMAC, and there may be other calls to HMAC in TLS 1.3 key der.
Tracking their logic: `TLS_AES_128_GCM_SHA256` computes:
$$\text{HMAC}(K, m) = \text{H} \left( K' \oplus \text{opad} \ \|\ \text{H}(K' \oplus \text{ipad} \| m)\ \right)$$
looking at internal values:
- $K'\oplus opad$ and $K'\oplus ipad$ are both 64 bytes; $m$ is variable length.
- Given that the the input to each call of SHA256 is greater than 64 bytes in len, the Merkle-Damgard compression is applied in both cases.
- the first call to the compression of SHA256 hides prover secret K.
- therefore, the output of each call of $H$ can be used as a public value without leaking information about $K$.
- If 𝑚 is publicly known by the verifier, the prover can compute the grey 𝑓 and disclose it to the verifier, which computes the remaining part of the hash out of circuit.
==This section was confusingly presented, though I think I stated the main result. I would want to see their code to make sure I understand this remark correctly, as it wasn't very clear to follow their reasoning.==
#### detailed invocation of compression functions note
A note on figure 8, which shows the precise computation trace of the TLS 1.3 key der, including the optimization on HMAC described in the prior section. The proxy is denoted verifier $v$, and the client as prover $p, zk$, where zk notes computation as part of the zk circuit. Authors note that $dHS^{in}$ is the only private client input, and some other values that may be computed in or out of circuit. Authors also note that derivation of CATK requires 8 in-circuit invocations of the SHACAL-2 function $f$.
### 5.2 Formal Protocol Spec of $\Pi_{\text{ORIGO}}$
*This section is more or less a repeat of high level protocol description Origo, now with a few fancy capital letters. Figure 10 specifies the post-handshake protocol spec, and Figures 9 and 10 specify the entire protocol. The remainder of the paper should be seen as clarifying of optimizations on HMAC.*
- (handshake) Assume each message is routed through $V$, such that $V$ observes the ciphertext transcript $\hat \Gamma$ .
- (request execution) - a basic proxy flow
- $C$ sends request $\hat Q$ to $V$ who forwards it to $S$
- client may embed private data $\theta_S$ in request
- $S$ returns response $\hat R$, forwarded back to $C$
- (pre processing)
- client $C$ decrypts the record to obtain plaintext $R$.
- "The client proceeds to pre-processes the record by finding the indices of AES blocks which match the provided ctx by invoking Πpost (see Figure 9)."
- ==what?==
- if the record matches the context, $C$ outputs pre-processed transcript $\Gamma'$ , sends the preprocessed values in $\Gamma'$ to $V$, reducing the number of HMAC evaluations in the Key Derivation Circuit
- ==what does record matches the context mean?==
- the secret input is the $\text{dHS}^{in}$
- see figure 8 for detailed key exchange protocol defn.
- (proof gen and verification)
- $C$ proves key derivation via figure 8
- $C$ proves authentication tag is correct
- *how* - see below
- $C$ proves private input response $R$ encrypts to the encrypted response $\hat R$ that the Verifier forwarded.
- verifier uses $\Pi_{Auth}$ to verify the server side certificate, and check the validity of SF.
#### 5.2 glossary
Note that I am often lazy about typing mathcal for capital letters.
- $\Pi_{\text{ORIGO}}$ the zkp for Origo
- a signature scheme $\Sigma(KGen, Sig, Vf$)
- AEAD alg $\mathcal{AE}(Enc,Dec)$ over `TLS_AES_128_GCM_SHA256` and curve P-256.
- server $S$
- proxy verifier $V$
- client $C$
- Denote $\Pi_S$ the unmodified server protocol TLS 1.3
- $\Gamma$ handshake transcript between S and C
- denote encrypted values with a hat, eg $\hat X$ and decrypted without hat.
- $\hat Q$ encrypted request, response $\hat M$ ; request response pair $\angle{\hat Q,\hat M}$
- $\theta_S$ private client information, such as credentials or an API key
- $\Pi_{post}$ - protocol for "post-processing the record to identify the correct indices of AES Blocks containing the context" - ==what?==
### 5.3 Client Side Evidence Generation
*this section describes the instantiation of a merkle proof over an arbitrary hash function to the contents of a TLS transcript of at most 1024 TLS transcript record blocks.*
- section introduces how the protocol can be extended to generate commitments to plaintext TLS session transcripts via a merkle tree.
- client expands the per-record nonce into a salt tree.
- the client generates a salted merkle tree with leaves as hashes over plaintext aead blocks
- the initial nonce is the IV used to generate salt values in the TLS handshake
- the client needs to convince the verifer that the merkle root $h_0$ was derived correctly wrt the salt tree expansion and Merkle tree computaiton.
- Therefore the client computes a ZKP attesting the correct derivation of the root hash $h_0$. An algebraic hash such as MiMC can be used for the merkle tree in place of SHA-256.
- ==Why choose MiMC as opposed to more efficient algebraic snark hashes like poseidon?==
==I am confused what was meant that Origo is a simple attestation protocol, and will probably have to reread section 5 at least once more until I understand. Then I will return to this section to better understand the merklization argument given.==
## convenience reference note on TLS 1.3 full protocol description between Client and Server without optional messages
See bottom for glossary.
#### DHE shared secret setup
Setup: compute the Early Secret and derived Early Secret
$$
\begin{aligned}
&\text{ES} \leftarrow \text{HKDF.extract}(0, 0) \\
&\text{dES} \leftarrow \text{HKDF.expand}(\text{ES}, l_1, H_0)
\end{aligned}
$$
Client: compute public/private key information. Note that hello's $r_c, r_s$ not used further in this description, but are the part of the initial randomness exchange in the protocol.
$$
\begin{aligned}
&r_c \xleftarrow{\$} \{0, 1\}^{256} \\
&x \xleftarrow{\$} \mathbb{Z}_p, X \leftarrow g^x \\
&\text{ClientHello}: r_c \\
&\text{ClientKeyShare}: X
\end{aligned}
$$
Client sends public key $X$. Server compute DHE information:
$$
\begin{aligned}
&r_s \xleftarrow{\$} \{0, 1\}^{256} \\
&y \xleftarrow{\$} \mathbb{Z}_p, Y \leftarrow g^y \\
&\text{ServerHello}: r_s \\
&\text{ServerKeyShare}: Y \\
&\text{DHE} \leftarrow X^y
\end{aligned}
$$
Server sends $Y$. Client computes $\text{DHE}=Y^x$.
#### certificate verification
Both parties compute protocol values:
$$
\begin{aligned}
&\text{HS} \leftarrow \text{HKDF.extract}(\text{dES}, \text{DHE}) \\
&\text{CHTS} \leftarrow \text{HKDF.expand}(\text{HS}, l_4, H_2) \\
&\text{SHTS} \leftarrow \text{HKDF.expand}(\text{HS}, l_5, H_2) \\
&\text{dHS} \leftarrow \text{HKDF.expand}(\text{HS}, l_3, H_0) \\
& \\
&\text{CHTK} \leftarrow \text{DeriveTK}(\text{CHTS}) \\
&\text{SHTK} \leftarrow \text{DeriveTK}(\text{SHTS})
\end{aligned}
$$
- **HS (Handshake Secret)** Serves as the basis for deriving subsequent handshake traffic secrets.
- **CHTS (Client Handshake Traffic Secret)**: Derived using the HKDF-Expand function with the Handshake Secret (HS), a label ($l_4$), and a hash ($H_2$). Used to derive the Client Handshake Traffic Key (CHTK) for encrypting and authenticating handshake messages from the client.
- **SHTS (Server Handshake Traffic Secret)**: Derived using the HKDF-Expand function with the Handshake Secret (HS), a label ($l_5$), and a hash ($H_2$). Used to derive the Server Handshake Traffic Key (SHTK) for encrypting and authenticating handshake messages from the server.
- **dHS (Derived Handshake Secret)**: Derived using the HKDF-Expand function with the Handshake Secret (HS), a label ($l_3$), and a hash ($H_0$). Used in further key derivation processes in the TLS protocol.
- **CHTK (Client Handshake Traffic Key)**: Derived from the Client Handshake Traffic Secret (CHTS) using a key derivation function (DeriveTK). Encrypts and authenticates the client’s handshake messages.
- **SHTK (Server Handshake Traffic Key)**: Derived from the Server Handshake Traffic Secret (SHTS) using a key derivation function (DeriveTK). Encrypts and authenticates the server’s handshake messages.
Server sends its cert $pk_s$ to the client, computes a signature SCV ensuring the server can use its private key corresponding to the cert. $fk_S$ is the finished key for the server's MAC's. $SF$ is the authentication using the finished key.:
$$
\begin{aligned}
&\{\text{ServerCert}\} : pk_S \\
&\text{SCV} \leftarrow \text{Sign}(sk_S, l_{11} \parallel H_6) \\
&\{\text{ServerCertVfy}\} : \text{SCV} \\
&\text{fk}_S \leftarrow \text{HKDF.expand}(\text{SHTS}, l_6, \text{""}) \\
&\text{SF} \leftarrow \text{HMAC}(\text{fk}_S, H_7) \\
&\{\text{ServerFinished}\} : \text{SF}
\end{aligned}
$$
Client: abort if certificate verification fails or if the server MAC fails. Computes the client final key and MAC'd client finished message.
$$
\begin{aligned}
&\text{abort if:} \\
&\quad \text{Vfy}(pk_S, l_{11} \parallel H_6) \ne 1 \\
&\quad \text{SF} \ne \text{HMAC}(\text{fk}_S, H_7) \\
\\
&\text{fk}_C \leftarrow \text{HKDF.expand}(\text{CHTS}, l_6, \text{""}) \\
&\text{CF} \leftarrow \text{HMAC}(\text{fk}_C, H_9) \\
&\{\text{ClientFinished}\} : \text{CF}
\end{aligned}
$$
Server aborts if client authentication fails.
$$ \text{abort if } \text{CF} \ne \text{HMAC}(\text{fk}_C, H_9) $$
Then the parties compute their Resumption master secret RMS and proceed to the record layer.
$$
\begin{aligned}
&\text{RMS} \leftarrow \text{HKDF.expand}(\text{MS}, l_{10}, H_4) \\
& \text{ record layer begins here} \\
&\text{CATK} \leftarrow \text{DeriveTK}(\text{CATS}) \\
&\text{SATK} \leftarrow \text{DeriveTK}(\text{SATS})
\end{aligned}
$$
- **RMS (Resumption Master Secret)**: Derived using the HKDF-Expand function with the Master Secret (MS), a label ($l_{10}$), and a hash ($H_4$). Used for generating keys in session resumption, allowing for faster re-establishment of secure connections without a full handshake.
- **CATK/SATK (Client/Server Application Traffic Key)**:
- **Description**: Derived from the Client/Server Application Traffic Secret (C/SATS) using a key derivation function (DeriveTK).
- **Purpose**: Encrypts and authenticates the application data during the record layer phase.
#### TLS 1.3 notation glossary
- **SHTS**: Server Handshake Traffic Secret
- **SHTK**: Server Handshake Traffic Key
- **HKDF**: HMAC-based Extract-and-Expand Key Derivation Function
- **HMAC**: Hash-based Message Authentication Code
- **ES**: Early Secret
- **dES**: Derived Early Secret
- **HS**: Handshake Secret
- **CHTS**: Client Handshake Traffic Secret
- **dHS**: Derived Handshake Secret
- **fk_S**: Finished Key for Server
- **fk_C**: Finished Key for Client
- **SF**: Server Finished message
- **CF**: Client Finished message
- **DHE**: Diffie-Hellman Exchange
- **r_c**: Client Random
- **r_s**: Server Random
- **X**: Client's Diffie-Hellman public value
- **Y**: Server's Diffie-Hellman public value
- **MS**: Master Secret
- **RMS**: Resumption Master Secret
- **CATS**: Client Application Traffic Secret
- **SATK**: Server Application Traffic Key
- **SATK**: Server Application Traffic Secret
- **Vfy**: Verify function
- **SCV**: Server Certificate Verify
- **pk_S**: Public key of the Server
- **sk_S**: Secret key of the Server
- **ClientHello**: Client's initial message in the TLS handshake
- **ServerHello**: Server's response message in the TLS handshake
- **ClientKeyShare**: Client's key share for the Diffie-Hellman exchange
- **ServerKeyShare**: Server's key share for the Diffie-Hellman exchange
- **verifyCertificate**: Function to verify the server's certificate
- **DeriveTK**: Function to derive a Traffic Key from a Traffic Secret
## terms
- **TLS oracle** - ensures data authenticity beyond the client-server TLS connection, such that **clients can obtain data from a server and ensure provenance to any third party**, without server-side modifications.
## questions
## related:
- topic:: [[topic-data provenance]]
- [[protocol-Transport Layer Security (TLS)]]
- paper:: [[paper-TLS Notary]]
- topic:: [[topic-web proofs]]