diff --git a/src/SUMMARY.md b/src/SUMMARY.md
index 021237f..f71013e 100644
--- a/src/SUMMARY.md
+++ b/src/SUMMARY.md
@@ -25,10 +25,9 @@
# MPC
-- [Key Exchange](./mpc/key_exchange.md)
+- [Binary Arithmetic](./mpc/binary_arithmetic.md)
- [Finite-Field Arithmetic](./mpc/ff-arithmetic.md)
-- [Dual Execution with Asymmetric Privacy](./mpc/deap.md)
-- [Encryption](./mpc/encryption.md)
+- [Key Exchange](./mpc/key_exchange.md)
- [MAC](./mpc/mac.md)
- [Commitments](./mpc/commitments.md)
diff --git a/src/diagrams/f_deap.svg b/src/diagrams/f_deap.svg
new file mode 100644
index 0000000..1c886c7
--- /dev/null
+++ b/src/diagrams/f_deap.svg
@@ -0,0 +1,4219 @@
+
diff --git a/src/mpc/binary_arithmetic.md b/src/mpc/binary_arithmetic.md
new file mode 100644
index 0000000..bd6f6b3
--- /dev/null
+++ b/src/mpc/binary_arithmetic.md
@@ -0,0 +1,61 @@
+# Binary Arithmetic
+
+TLS includes cryptographic algorithms which are most efficiently computed over the binary field such as the SHA-256 and AES-128 block ciphers.
+
+Computing such algorithms using MPC can be quite expensive even when employing state-of-the-art protocols. To achieve practical efficiency TLSNotary leverages Dual Execution with Asymmetric Privacy (DEAP) as defined by the $\mathcal{F}_{\text{DEAP}}$ functionality presented below. This functionality is weaker than a perfectly secure functionality and thus can be efficiently realized using existing performant protocols such as garbled circuits in conjunction with a zero-knowledge protocol.
+
+## Introduction
+
+Malicious secure MPC typically comes at the expense of dramatically lower efficiency compared to the semi-honest setting. One technique, called Dual Execution [\[MF06\]](https://www.iacr.org/archive/pkc2006/39580468/39580468.pdf) [\[HKE12\]](https://www.cs.umd.edu/~jkatz/papers/SP12.pdf), achieves malicious security with a minimal 2x overhead. However, it comes with the concession that a malicious adversary may learn $k$ bits of the other's input with probability $2^{-k}$ of the leakage going undetected.
+
+We present a variant of Dual Execution with a weaker security notion in favor of performance, while still satisfying the rather niche security requirements for TLSNotary. Our variant ensures perfect privacy _for one party_, by sacrificing privacy entirely for the other. Hence the name, Dual Execution with Asymmetric Privacy (DEAP). This is a distinct notion from zero-knowledge where only one party provides private inputs. In DEAP both parties can provide private inputs until the finalization procedure.
+
+## Dual Execution with Asymmetric Privacy
+
+Figure 1 defines a functionality $\mathcal{F}_{\text{DEAP}}$ which runs between parties $P_A$ and $P_B$, and an adversary $\mathcal{A}$. The functionality provides an interface akin to a virtual machine, including persistent memory and the ability to execute arbitrary boolean functions.
+
+
+
+For $P_A$ the functionality provides perfect security with aborts, while $P_B$ receives significantly weaker guarantees.
+
+The adversary is assumed to only corrupt one of the parties, and upon doing so is granted a number of affordances. Despite these affordances, $\mathcal{F}_{\text{DEAP}}$ maintains some key properties.
+
+### Privacy
+
+The functionality provides perfect privacy for the inputs of $P_A$ in the presence of a corrupted $P_B$. Upon corrupting $P_B$ the adversary can at most provide inconsistent inputs in the **Input** procedure. However, $\mathcal{A}$ can not learn any information about $P_A$ inputs as the functionality enforces consistency during the **Finalize** routine prior to performing an equality check on output values.
+
+If $P_A$ is corrupted the inputs of $P_B$ are vulnerable to selective failure attacks by $\mathcal{A}$ prior to calling **Finalize**. The adversary may sample information about inputs provided by $P_B$ during the **Call** procedure using an arbitrary predicate $\text{P}$ at risk of causing an abort. In other words, for every **Call** invocation, $\mathcal{A}$ may sample $k$ input bits provided by $P_B$ with probability $2^{-k}$ of this leakage going undetected.
+
+### Correctness
+
+A key security notion to consider is that of _correctness_, which, loosely speaking, is whether upon receiving a function $f$ in the **Call** routine the functionality correctly computes $f$ and not some alternate function $f'$.
+
+The functionality provides correctness to $P_A$ in the presence of a corrupted $P_B$. As mentioned earlier, the adversary may only replace the inputs of $P_B$ which is of no consequence regarding correctness.
+
+$P_B$ does not enjoy the same notion of correctness if $P_A$ is corrupted. Rather, the adversary is permitted to provide an _arbitrary_ alternate function $f'$ in the **Call** procedure in addition to flipping output values in invocations of **Output**. It is in the **Finalize** procedure that $P_B$ can detect corruptions introduced by $\mathcal{A}$.
+
+### Finalization
+
+The **Finalize** procedure reveals all inputs provided by $P_B$ to $P_A$ and ensures that the adversary $\mathcal{A}$ can not learn any information of $P_A$ inputs by providing inconsistent inputs used in **Call**.
+
+For example, if $P_B$ is corrupted and the adversary causes the input vectors $\bold{\mathbb{x}}_1$ and $\bold{\mathbb{x}}_2$ in **Call** to be inconsistent by exploiting the **Input** procedure, $\mathcal{A}$ could learn if $f(\bold{\mathbb{x}}_1) = f(\bold{\mathbb{x}}_2)$ in Step 4 of **Finalize**. Aborting beforehand if the inputs are inconsistent mitigates this possibility.
+
+As mentioned [earlier](#correctness), $P_B$ is not provided any correctness guarantees in the presence of a corrupted $P_A$ prior to finalization. In leau of that, $P_B$ learns if any _output values_ are inconsistent via an equality check in Step 4. This significantly constrains the adversary while choosing alternate functions in **Call**. To illustrate this consider the following:
+
+Suppose an honest $P_B$ expects to compute the function $f(x, y)$ where $x$ and $y$ are inputs provided by $P_A$ and $P_B$ respectively. Recall that an adversary corrupting $P_A$ may provide inconsistent input values $x_1$ and $x_2$ and an alternate function $f'$:
+
+$$z_1 = f'(x_1, y)$$
+$$z_2 = f(x_2, y)$$
+
+In the extreme case, $\mathcal{A}$ may choose $f'$ such that it simply outputs $y$ and thus learning the input of $P_B$ directly. Indeed this is allowed, however such a corruption will be detected in Step 4 of **Finalize** which notifies $P_B$ if $z_1 \neq z_2$. Given that $\mathcal{A}$ must choose $x_1$, $x_2$ and $f'$ prior to learning the output, for the adversary to avoid detection they must satisfy all constraints on $y$ a priori. Put simply, the adversary may guess $k$ bits of $y$ with probability $2^{-k}$ of it going undetected.
+
+To summarize the above, the finalization procedure ensures a probabilistic leakage bound on the inputs of $P_B$ and also enforces correctness albeit with potentially inconsistent inputs from $P_A$.
+
+## Usage in TLSNotary
+
+TLSNotary uses $\mathcal{F}_{\text{DEAP}}$ such that the `Prover` and `Verifier` are $P_A$ and $P_B$ respectively. This ensures that a corrupted `Verifier` can not extract any private information of the `Prover` nor can it affect the correctness of any of the computations which could lead to malicious state updates in an application. Conversely, a corrupted `Prover` can not prematurely learn the inputs of the `Verifier` nor break correctness in any meaningful way without detection.
diff --git a/src/mpc/deap.md b/src/mpc/deap.md
index e0b24ba..76312fd 100644
--- a/src/mpc/deap.md
+++ b/src/mpc/deap.md
@@ -1,136 +1 @@
# Dual Execution with Asymmetric Privacy
-
-TLSNotary uses the `DEAP` protocol described below to ensure malicious security of the overall protocol.
-
-When using DEAP in TLSNotary, the `User` plays the role of Alice and has full privacy and the `Notary` plays the role of Bob and reveals all of his private inputs after the TLS session with the server is over. The Notary's private input is his TLS session key share.
-
-The parties run the `Setup` and `Execution` steps of `DEAP` but they defer the `Equality Check`.
-Since during the `Equality Check` all of the `Notary`'s secrets are revealed to User, it must be deferred until after the TLS session with the server is over, otherwise the User would learn the full TLS session keys and be able to forge the TLS transcript.
-
-## Introduction
-
-Malicious secure 2-party computation with garbled circuits typically comes at the expense of dramatically lower efficiency compared to execution in the semi-honest model. One technique, called Dual Execution [\[MF06\]](https://www.iacr.org/archive/pkc2006/39580468/39580468.pdf) [\[HKE12\]](https://www.cs.umd.edu/~jkatz/papers/SP12.pdf), achieves malicious security with a minimal 2x overhead. However, it comes with the concession that a malicious adversary may learn $k$ bits of the other's input with probability $2^{-k}$.
-
-We present a variant of Dual Execution which provides different trade-offs. Our variant ensures complete privacy _for one party_, by sacrificing privacy entirely for the other. Hence the name, Dual Execution with Asymmetric Privacy (DEAP). During the execution phase of the protocol both parties have private inputs. The party with complete privacy learns the authentic output prior to the final stage of the protocol. In the final stage, prior to the equality check, one party reveals their private input. This allows a series of consistency checks to be performed which guarantees that the equality check can not cause leakage.
-
-Similarly to standard DualEx, our variant ensures output correctness and detects leakage (of the revealing parties input) with probability $1 - 2^{-k}$ where $k$ is the number of bits leaked.
-
-## Preliminary
-
-The protocol takes place between Alice and Bob who want to compute $f(x, y)$ where $x$ and $y$ are Alice and Bob's inputs respectively. The privacy of Alice's input is ensured, while Bob's input will be revealed in the final steps of the protocol.
-
-### Premature Leakage
-
-Firstly, our protocol assumes a small amount of premature leakage of Bob's input is tolerable. By premature, we mean prior to the phase where Bob is expected to reveal his input.
-
-If Alice is malicious, she has the opportunity to prematurely leak $k$ bits of Bob's input with $2^{-k}$ probability of it going undetected.
-
-### Aborts
-
-We assume that it is acceptable for either party to cause the protocol to abort at any time, with the condition that no information of Alice's inputs are leaked from doing so.
-
-### Committed Oblivious Transfer
-
-In the last phase of our protocol Bob must open all oblivious transfers he sent to Alice. To achieve this, we require a very relaxed flavor of committed oblivious transfer. For more detail on these relaxations see section 2 of [Zero-Knowledge Using Garbled Circuits \[JKO13\]](https://eprint.iacr.org/2013/073.pdf).
-
-### Notation
-
-* $x$ and $y$ are Alice and Bob's inputs, respectively.
-* $[X]_A$ denotes an encoding of $x$ chosen by Alice.
-* $[x]$ and $[y]$ are Alice and Bob's encoded _active_ inputs, respectively, ie $\mathsf{Encode}(x, [X]) = [x]$.
-* $\mathsf{com}_x$ denotes a binding commitment to $x$
-* $G$ denotes a garbled circuit for computing $f(x, y) = v$, where:
- * $\mathsf{Gb}([X], [Y]) = G$
- * $\mathsf{Ev}(G, [x], [y]) = [v]$.
-* $d$ denotes output decoding information where $\mathsf{De}(d, [v]) = v$
-* $\Delta$ denotes the global offset of a garbled circuit where $\forall i: [x]^{1}_i = [x]^{0}_i \oplus \Delta$
-* $\mathsf{PRG}$ denotes a secure pseudo-random generator
-* $\mathsf{H}$ denotes a secure hash function
-
-## Protocol
-
-The protocol can be thought of as three distinct phases: The setup phase, execution, and equality-check.
-
-### Setup
-
-1. Alice creates a garbled circuit $G_A$ with corresponding input labels $([X]_A, [Y]_A)$, and output label commitment $\mathsf{com}_{[V]_A}$.
-2. Bob creates a garbled circuit $G_B$ with corresponding input labels $([X]_B, [Y]_B)$.
-3. For committed OT, Bob picks a seed $\rho$ and uses it to generate all random-tape for his OTs with $\mathsf{PRG}(\rho)$. Bob sends $\mathsf{com}_{\rho}$ to Alice.
-4. Alice retrieves her active input labels $[x]_B$ from Bob using OT.
-5. Bob retrieves his active input labels $[y]_A$ from Alice using OT.
-6. Alice sends $G_A$, $[x]_A$, $d_A$ and $\mathsf{com}_{[V]_A}$ to Bob.
-7. Bob sends $G_B$ and $[y]_B$ to Alice.
-
-### Execution
-
-Both Alice and Bob can execute this phase of the protocol in parallel as described below:
-
-#### Alice
-
-8. Evaluates $G_B$ using $[x]_B$ and $[y]_B$ to acquire $[v]_B$.
-9. Defines $\mathsf{check}_A = [v]_B$.
-10. Computes a commitment $\mathsf{Com}(\mathsf{check}_A, r) = \mathsf{com}_{\mathsf{check}_A}$ where $r$ is a key only known to Alice. She sends this commitment to Bob.
-11. Waits to receive $[v]_A$ from Bob[^1].
-12. Checks that $[v]_A$ is authentic, aborting if not, then decodes $[v]_A$ to $v^A$ using $d_A$.
-
-At this stage, a malicious Bob has learned nothing and Alice has obtained the output $v^A$ which she knows to be authentic.
-
-#### Bob
-
-13. Evaluates $G_A$ using $[x]_A$ and $[y]_A$ to acquire $[v]_A$. He checks $[v]_A$ against the commitment $\mathsf{com}_{[V]_A}$ which Alice sent earlier, aborting if it is invalid.
-14. Decodes $[v]_A$ to $v^A$ using $d_A$ which he received earlier. He defines $\mathsf{check}_B = [v^A]_B$ and stores it for the equality check later.
-15. Sends $[v]_A$ to Alice[^1].
-16. Receives $\mathsf{com}_{\mathsf{check}_A}$ from Alice and stores it for the equality check later.
-
-Bob, even if malicious, has learned nothing except the purported output $v^A$ and is not convinced it is correct. In the next phase Alice will attempt to convince Bob that it is.
-
-Alice, if honest, has learned the correct output $v$ thanks to the authenticity property of garbled circuits. Alice, if malicious, has potentially learned Bob's entire input $y$.
-
-[^1]: This is a significant deviation from standard DualEx protocols such as [\[HKE12\]](https://www.cs.umd.edu/~jkatz/papers/SP12.pdf). Typically the output labels are _not_ returned to the Generator, instead, output authenticity is established during a secure equality check at the end. See the [section below](#malicious-alice) for more detail.
-
-### Equality Check
-
-17. Bob opens his garbled circuit and OT by sending $\Delta_B$, $y$ and $\rho$ to Alice.
-18. Alice, can now derive the _purported_ input labels to Bob's garbled circuit $([X]^{\\*}_B, [Y]^{\\*}_B)$.
-19. Alice uses $\rho$ to open all of Bob's OTs for $[x]_B$ and verifies that they were performed honestly. Otherwise she aborts.
-20. Alice verifies that $G_B$ was garbled honestly by checking $\mathsf{Gb}([X]^{\\*}_B, [Y]^{\\*}_B) == G_B$. Otherwise she aborts.
-21. Alice now opens $\mathsf{com}_{\mathsf{check}_A}$ by sending $\mathsf{check}_A$ and $r$ to Bob.
-22. Bob verifies $\mathsf{com}_{\mathsf{check}_A}$ then asserts $\mathsf{check}_A == \mathsf{check}_B$, aborting otherwise.
-
-Bob is now convinced that $v^A$ is correct, ie $f(x, y) = v^A$. Bob is also assured that Alice only learned up to k bits of his input prior to revealing, with a probability of $2^{-k}$ of it being undetected.
-
-## Analysis
-
-### Malicious Alice
-
-[On the Leakage of Corrupted Garbled Circuits \[DPB18\]](https://eprint.iacr.org/2018/743.pdf) is recommended reading on this topic.
-
-During the first execution, Alice has some degrees of freedom in how she garbles $G_A$. According to \[DPB18\], when using a modern garbling scheme such as \[ZRE15\], these corruptions can be analyzed as two distinct classes: detectable and undetectable.
-
-Recall that our scheme assumes Bob's input is an ephemeral secret which can be revealed at the end. For this reason, we are entirely unconcerned about the detectable variety. Simply providing Bob with the output labels commitment $\mathsf{com}_{[V]_A}$ is sufficient to detect these types of corruptions. In this context, our primary concern is regarding the _correctness_ of the output of $G_A$.
-
-\[DPB18\] shows that any undetectable corruption made to $G_A$ is constrained to the arbitrary insertion or removal of NOT gates in the circuit, such that $G_A$ computes $f_A$ instead of $f$. Note that any corruption of $d_A$ has an equivalent effect. \[DPB18\] also shows that Alice's ability to exploit this is constrained by the topology of the circuit.
-
-Recall that in the final stage of our protocol Bob checks that the output of $G_A$ matches the output of $G_B$, or more specifically:
-
-$$f_A(x_1, y_1) == f_B(x_2, y_2)$$
-
-For the moment we'll assume Bob garbles honestly and provides the same inputs for both evaluations.
-
-$$f_A(x_1, y) == f(x_2, y)$$
-
-In the scenario where Bob reveals the output of $f_A(x_1, y)$ prior to Alice committing to $x_2$ there is a trivial _adaptive attack_ available to Alice. As an extreme example, assume Alice could choose $f_A$ such that $f_A(x_1, y) = y$. For most practical functions this is not possible to garble without detection, but for the sake of illustration we humor the possibility. In this case she could simply compute $x_2$ where $f(x_2, y) = y$ in order to pass the equality check.
-
-To address this, Alice is forced to choose $f_A$, $x_1$ and $x_2$ prior to Bob revealing the output. In this case it is obvious that any _valid_ combination of $(f_A, x_1, x_2)$ must satisfy all constraints on $y$. Thus, for any non-trivial $f$, choosing a valid combination would be equivalent to guessing $y$ correctly. In which case, any attack would be detected by the equality check with probability $1 - 2^{-k}$ where k is the number of guessed bits of $y$. This result is acceptable within our model as [explained earlier](#premature-leakage).
-
-### Malicious Bob
-
-[Zero-Knowledge Using Garbled Circuits \[JKO13\]](https://eprint.iacr.org/2013/073.pdf) is recommended reading on this topic.
-
-The last stage of our variant is functionally equivalent to the protocol described in \[JKO13\]. After Alice evaluates $G_B$ and commits to $[v]_B$, Bob opens his garbled circuit and all OTs entirely. Following this, Alice performs a series of consistency checks to detect any malicious behavior. These consistency checks do _not_ depend on any of Alice's inputs, so any attempted selective failure attack by Bob would be futile.
-
-Bob's only options are to behave honestly, or cause Alice to abort without leaking any information.
-
-### Malicious Alice & Bob
-
-They deserve whatever they get.
diff --git a/src/mpc/encryption.md b/src/mpc/encryption.md
deleted file mode 100644
index 163ae1a..0000000
--- a/src/mpc/encryption.md
+++ /dev/null
@@ -1,74 +0,0 @@
-# Encryption
-
-Here we will explain our protocol for 2PC encryption using a block cipher in counter-mode.
-
-Our documentation on [Dual Execution with Asymmetric Privacy](deap.md) is recommended prior reading for this section.
-
-## Preliminary
-
-### Ephemeral Keyshare
-
-It is important to recognise that the Notary's keyshare is an _ephemeral secret_. It is only private for the duration of the User's TLS session, after which the User is free to learn it without affecting the security of the protocol.
-
-It is this fact which allows us to achieve malicious security for relatively low cost. More details on this [here](../mpc/deap.md).
-
-### Premature Leakage
-
-A small amount of undetected premature keyshare leakage is quite tolerable. For example, if the Notary leaks 3 bits of their keyshare, it gives the User no meaningful advantage in any attack, as she could have simply guessed the bits correctly with $2^{-3} = 12.5\%$ probability and mounted the same attack. Assuming a sufficiently long cipher key is used, eg. 128 bits, this is not a concern.
-
-The equality check at the end of our protocol ensures that premature leakage is detected with a probability of $1 - 2^{-k}$ where k is the number of leaked bits. The Notary is virtually guaranteed to detect significant leakage and can abort prior to notarization.
-
-### Plaintext Leakage
-
-Our protocol assures _no leakage_ of the plaintext to the Notary during both encryption and decryption. The Notary reveals their keyshare at the end of the protocol, which allows the Notary to open their garbled circuits and oblivious transfers completely to the User. The User can then perform a series of consistency checks to ensure that the Notary behaved honestly. Because these consistency checks do not depend on any inputs of the User, aborting does not reveal any sensitive information (in contrast to standard DualEx which does).
-
-### Integrity
-
-During the entirety of the TLS session the User performs the role of the garbled circuit generator, thus ensuring that a malicious Notary can not corrupt or otherwise compromise the integrity of messages sent to/from the Server.
-
-### Notation
-
-* $p$ is one block of plaintext
-* $c$ is the corresponding block of ciphertext, ie $c = \mathsf{Enc}(k, ctr) \oplus p$
-* $k$ is the cipher key
-* $ctr$ is the counter block
-* $k_U$ and $k_N$ denote the User and Notary cipher keyshares, respectively, where $k = k_U \oplus k_N$
-* $z$ is a mask randomly selected by the User
-* $ectr$ is the encrypted counter-block, ie $ectr = \mathsf{Enc}(k, ctr)$
-* $\mathsf{Enc}$ denotes the block cipher used by the TLS session
-* $\mathsf{com}_x$ denotes a binding commitment to the value $x$
-* $[x]_A$ denotes a garbled encoding of $x$ chosen by party $A$
-
-## Encryption Protocol
-
-The encryption protocol uses [DEAP](../mpc/deap.md) without any special variations. The User and Notary directly compute the ciphertext for each block of a message the User wishes to send to the Server:
-
-$$f(k_U, k_N, ctr, p) = \mathsf{Enc}(k_U \oplus k_N, ctr) \oplus p = c$$
-
-The User creates a commitment to the plaintext active labels for the Notary's circuit $\mathsf{Com}([p]_N, r) = \mathsf{com}_{[p]_N}$ where $r$ is a random key known only to the User. The User sends this commitment to the Notary to be used in the authdecode protocol later. It's critical that the User commits to $[p]_N$ prior to the Notary revealing $\Delta$ in the final phase of DEAP. This ensures that if $\mathsf{com}_{[p]_N}$ is a commitment to valid labels, then it must be a valid commitment to the plaintext $p$. This is because learning the complementary wire label for any bit of $p$ prior to learning $\Delta$ is virtually impossible.
-
-## Decryption Protocol
-
-The protocol for decryption is very similar but has some key differences to encryption.
-
-For decryption, [DEAP](../mpc/deap.md) is used for every block of the ciphertext to compute the _masked encrypted counter-block_:
-
-$$f(k_U, k_N, ctr, z) = \mathsf{Enc}(k_U \oplus k_N, ctr) \oplus z = ectr_z$$
-
-This mask $z$, chosen by the User, hides $ectr$ from the Notary and thus the plaintext too. Conversely, the User can simply remove this mask in order to compute the plaintext $p = c \oplus ectr_z \oplus z$.
-
-Following this, the User can retrieve the wire labels $[p]_N$ from the Notary using OT.
-
-Similarly to the procedure for encryption, the User creates a commitment $\mathsf{Com}([p]_N, r) = \mathsf{com}_{[p]_N}$ where $r$ is a random key known only to the User. The User sends this commitment to the Notary to be used in the authdecode protocol later.
-
-### Proving the validity of $[p]_N$
-
-In addition to computing the masked encrypted counter-block, the User must also prove that the labels $[p]_N$ they chose afterwards actually correspond to the ciphertext $c$ sent by the Server.
-
-This is can be done efficiently in one execution using the zero-knowledge protocol described in [[JKO13]](https://eprint.iacr.org/2013/073.pdf) the same as we do in the final phase of DEAP.
-
-The Notary garbles a circuit $G_N$ which computes:
-
-$$p \oplus ectr = c$$
-
-Notice that the User and Notary will already have computed $ectr$ when they computed $ectr_z$ earlier. Conveniently, the Notary can re-use the garbled labels $[ectr]_N$ as input labels for this circuit. For more details on the reuse of garbled labels see [[AMR17]](https://eprint.iacr.org/2017/062.pdf).
\ No newline at end of file
diff --git a/src/protocol/mpc-tls/encryption.md b/src/protocol/mpc-tls/encryption.md
index 5d2ae33..1204f8a 100644
--- a/src/protocol/mpc-tls/encryption.md
+++ b/src/protocol/mpc-tls/encryption.md
@@ -4,7 +4,7 @@ This section explains how the `Prover` and `Verifier` use MPC to encrypt data se
## Encryption
-To encrypt the plaintext, both parties input their TLS key shares as private inputs to the [MPC](../../mpc/deap.md) protocol, along with some other public data. Additionally, the `Prover` inputs her plaintext as a private input.
+To encrypt the plaintext, both parties input their TLS key shares as private inputs to the [MPC](../../mpc/binary_arithmetic.md) protocol, along with some other public data. Additionally, the `Prover` inputs her plaintext as a private input.
@@ -16,10 +16,9 @@ The `Prover` then dispatches the ciphertext and the MAC to the server.
Once the `Prover` receives the ciphertext and its associated MAC from the server, the parties first authenticate the ciphertext by validating the MAC. They do this by running the [MPC](../../mpc/mac.md) protocol to compute the authentic MAC for the ciphertext. They then verify if the authentic MAC matches the MAC received from the server.
-Next, the parties decrypt the ciphertext by providing their key shares as private inputs to the [MPC](../../mpc/deap.md) protocol, along with the ciphertext and some other public data.
+Next, the parties decrypt the ciphertext by providing their key shares as private inputs to the [MPC](../../mpc/binary_arithmetic.md) protocol, along with the ciphertext and some other public data.
The resulting plaintext is revealed ONLY to the `Prover`.
-Please note, the actual low-level implementation details of decryption are more nuanced than what we have described here. For more information, please consult [Low-level Decryption details](../../mpc/encryption.md).
diff --git a/typst/f_deap.typst b/typst/f_deap.typst
new file mode 100644
index 0000000..5409b48
--- /dev/null
+++ b/typst/f_deap.typst
@@ -0,0 +1,70 @@
+#set text(font: "New Computer Modern")
+#set page(width: 600pt, height: 500pt, margin: 10pt)
+#set align(center + horizon)
+
+#let func(x) = $cal(F)_#x$;
+#let deap = func("DEAP");
+#let PA = $P_A$;
+#let PB = $P_B$;
+#let A = $cal(A)$;
+#let mem = $upright(bold(M))$;
+#let call = $upright(bold(C))$;
+#let keys = $"keys"(#mem)$;
+
+#figure(
+ block(
+ stroke: 1pt,
+ inset: 20pt,
+ [
+ *Functionality* #deap
+ #set align(left)
+ The functionality runs with parties #PA, #PB, and an adversary #A. It maintains a map $#mem: cal(K) -> ({0,1}, {0,1})$,
+ of which entries can only be assigned once, and stores sets $cal(X), cal(Z) subset.eq cal(K)$.
+
+ *Input:* On receiving $("Input", "id", x)$ from either #PA or #PB, and $("Input", "id")$ from the other party,
+ where $x in {0, 1}$ and $"id" in cal(K) \\ #keys$: \
+ #enum(
+ indent: 20pt,
+ [If the party providing $x$ is corrupt then receive $x' in {0,1}$
+ from #A then set $#mem ["id"] <- (x, x')$.
+
+ Else if #PA is corrupt and #PB provided $x$ then receive $f: {0,1} -> {0,1}$
+ from #A then set $#mem ["id"] <- (f(x), x)$.
+
+ Otherwise, set $#mem ["id"] <- (x, x)$.],
+ [If #PB provided $x$ then store $cal(X) <- cal(X) union {id}$.]
+ )
+
+ *Call:* On receiving $("Call", f, bold("id")_"x", bold("id")_"y")$ from #PA and #PB, where $f: {0,1}^m -> {0,1}^n$,
+ $forall i in [1, m], "id"_(x,i) in #keys$ and $forall i in [1, n], "id"_(y,i) in cal(K) \\ #keys$:
+ #enum(
+ indent: 20pt,
+ [Retrieve $(bold(x)_1, bold(x)_2) <- (#mem ["id"])_("id" in bold("id")_x)$.],
+ [If #PA is corrupt then receive $f'$ and predicate $upright(P): {0,1}^m -> {0,1}$ from #A,
+ then compute $(bold(y)_1, bold(y)_2) = (f'(bold(x)_1), f(bold(x)_2))$ and abort if $upright(P)(bold(x)_1) = 0$.\
+
+ Otherwise, compute $(bold(y)_1, bold(y)_2) = (f(bold(x)_1), f(bold(x)_2))$.
+ ],
+ [For all $i in [1, n]$ set $#mem ["id"_(y,i)] <- (y_(1,i), y_(2,i))$.]
+ )
+
+ *Output:* On receiving $("Output", "id")$ from #PA and #PB where $"id" in #keys$:
+ #enum(
+ indent: 20pt,
+ [Retrieve $(z, \_) <- #mem ["id"]$ and store $cal(Z) <- cal(Z) union {"id"}$.],
+ [If #PA is corrupt then receive $e in {0,1}$ from #A, otherwise set $e = 0$.],
+ [Send $z xor e$ to #PA and #PB.]
+ )
+
+ *Finalize:* On receiving $("Finalize")$ from #PA and #PB ignore all
+ subsequent commands then finally:
+ #enum(
+ indent: 20pt,
+ [Set $bold(id)_x eq "vec"(cal(X))$ and retrieve $(bold(x)_1, bold(x)_2) <- (#mem ["id"])_("id" in bold("id")_x)$.],
+ [Send $(bold("id")_x, bold(x)_1)$ to #PA and then abort if $bold(x)_1 eq.not bold(x)_2$.],
+ [Set $bold(id)_z eq "vec"(cal(Z))$ and retrieve $(bold(z)_1, bold(z)_2) <- (#mem ["id"])_("id" in bold("id")_z)$.],
+ [Send $"true"$ to #PB if $bold(z)_1 = bold(z)_2$ otherwise send $"false"$.],
+ )
+ ]
+ )
+)
