# A Formal Analysis of the Mimblewimble Cryptocurrency Protocol +
## 4 Verification of Mimblewimble
### Unlinkability and Untraceability  
As we specified in our model, each node has a pool of unconfirmed transactions in the _mempool_. This transactions are waiting for the miners in order to be included in a block. We can distinguish two security properties of the transactions. Untraceability refers to the transactions in the mempool and unlinkability to the transactions in the block. In our model, this two notions are formalized as follows. **Property 3** (Transaction Unlinkability). : _Given a valid block \(b\), it is computationally infeasible to know which input cancels which output._  
The following lemma captures the semantics of this property in MW. Moreover, the operations cut-through and CoinJoin, which were described above, also contribute to this property. **Lemma 7** (Transaction Unlinkability). : _For any valid block \(b\) and for any polynomial probabilistic time adversary \(\mathcal{A}\), the probability of \(\mathcal{A}\) in finding a balanced transaction within \(b\) is negligible._  
Proof. : Let \(b=\{i,o,tks,ko\}\) be a valid block with \(tks=(tk_{1},\ldots,tk_{t})\) the list of transaction kernels. The \(j\)-th item in \(tks\) is of the form \(tk_{j}=\{rp_{j},k_{j},\sigma_{j}\}\). The goal of the adversary \(\mathcal{A}\) is to find a tuple of the form \(\{i^{\prime},o^{\prime},k^{\prime}\}\) where the list of inputs \(i^{\prime}\) is a subset of \(i\) and the list of outputs \(o^{\prime}\) is a subset of \(o\), satisfying Definition 5 of a balanced transaction. It means that, the following equality must be true for the tuple:\[\sum_{o_{j}\in o^{\prime}}o_{j}-\sum_{c_{j}\in i^{\prime}}c_{j}=k{e^{\prime}}+ tk{o^{\prime}}.G,\]  
where \(k{e^{\prime}}\) is the transaction excess and \(tk{o^{\prime}}\) the transaction kernel offset. If we refer to the construction process in Definition 11, the transaction kernel offsets were added to generate a single aggregate offset \(k{o}\) to cover all transactions in the block. It means that we do not store the individual kernel offset \(tk{o^{\prime}}\) of the transaction in \(b\) once the transaction is aggregated to the block. The challenge is trying to solve the adversary \(\mathcal{A}\) could be seen as the subset sum problem (NP-complete) but, in this case, \(tk{o^{\prime}}\) is unrecoverable. So, although many transactions have few inputs and outputs, it is computationally infeasible, without knowing that value, to find the tuple. We can define:  
**Definition 15** (Transaction Unlinkable). : _We say block \(b\) is transaction-unlinkable, if the probability of any polynomial probabilistic time adversary \(\mathcal{A}\) in finding a balanced transaction within \(b\) is negligible._  
Then, due to Lemma 7 we conclude that in MW all blocks are transaction-unlinkable. **Property 4** (Transaction Untraceability). : _For every transaction in the mempool, it is not possible to relate the transaction to the IP address of the node which originated it._  
Regarding this property, we should refer mainly, to the broadcast of the transactions. Once the transactions are created, they are broadcasted to the network and they are included in the mempool. Each node could track the IP address from the node which received the transaction. At that point nodes could record the transactions, allowing them to build a transaction graph. We define that the broadcast of a transaction can be performed with or without confusion. Without confusion means that, once the transactions are created, they are broadcasted immediately to all the networks. However, if someone controls enough nodes on the network and discovers how the transaction moves, he could find out the IP address node from which the transaction comes from. On the other hand, we define the broadcast with confusion as a way to obscure the IP address node. **Definition 16** (Broadcast with confusion). : _Let us say node \(A\) sends a transaction to node \(B\).