# A Formal Analysis of the Mimblewimble Cryptocurrency Protocol +
## 4 Verification of Mimblewimble
### Protocol Properties  
The property of _no coin inflation_ or _zero-sum_ guarantees that no new funds are produced from thin air in a valid transaction. The property can be stated as follows. **Lemma 4** (No Coin Inflation). : _Given a valid transaction \(t=\{i,o,tk,tok\}\) with transaction kernel \(tk=\{rp,ke,\sigma\}\), then the transaction excess only contains the blinding factor and the kernel offset._  
Proof. : We know the transaction \(t\) is valid, in particular, the transaction is balanced. Applying Definition 5, we know that:  
\[\sum_{o_{j}\in o}o_{j}-\sum_{c_{j}\in i}c_{j}=ke+tok.G.\]  
Using Definition 3, we start to unfold the terms in the equality:  
\[\sum_{1}^{m}r^{\prime}.G+v^{\prime}.H-\sum_{1}^{n}r.G+v.H=(\sum_{1}^{m}r^{ \prime}-\sum_{1}^{n}r-tok).G+tok.G.\]  
Applying algebraic properties on elliptic curves, we have:  
\[\sum_{1}^{m}v^{\prime}.H-\sum_{1}^{n}v.H=(\sum_{1}^{m}r^{\prime}.G-\sum_{1}^{ n}r.G)-(\sum_{1}^{m}r^{\prime}.G-\sum_{1}^{n}r.G)-tok.G+tok.G=0.\]  
Therefore,  
\[(v^{\prime}_{1}+\ldots+v^{\prime}_{m}).H-(v_{1}+\ldots+v_{n}).H=(v^{\prime}_{ 1}+\ldots+v^{\prime}_{m}-v_{1}-\ldots-v_{n}).H=0.H=0.\]  
This means that all the inputs and outputs add up to zero. In other words, they are summed to the commitment to the kernel offset plus the commitment to the excess blinding factor. Thus, we have proved that no money is created from thin air and the only ones who knew the blinding factors were the transacting parties when they created the transaction. This means the new outputs will be spendable only by them. An important feature of MW is the _cut-through_ process. The purpose of this process is to erase redundant outputs that are used as inputs within the same block. Let \(C\) be some coins that appear as an output in the block \(b\). If the same coins appear as an input within the block, then \(C\) can be removed from the list of inputs and outputs after applying the cut-through process. In this way, the only remaining data are the block headers, transaction kernels and UTXOs. After applying cut-through to a valid block \(b\) it is important to ensure that the resulting block \(b^{\prime}\) is still valid. We can say that the validity of a block should be invariant with respect to the cut-through process. **Lemma 5** (Invariant: Cut-through Block Validity). : _Let \(b\) be a block of the form \(b=\{i,o,tks,ko\}\) with \(i\) and \(o\) the list of inputs and outputs, \(tks=(tk_{1},\ldots,tk_{t})\) the list of transaction kernels and \(ko\) the block kernel offset. Let \(b^{\prime}=\{i^{\prime},o^{\prime},tks,ko\}\) be the resulting block after applying the cut-through process to \(b\) where:_  
* \(i^{\prime}=i\setminus(i\cap o)\)__
* \(o^{\prime}=o\setminus(i\cap o)\)_._  
_Hence, if \(b\) is a valid block, then \(b^{\prime}\) is valid too._  
Proof. : Let \(b\) be the block \(b=\{i,o,tks,ko\}\), with \(tks=(tk_{1},\ldots,tk_{t})\) the list of transaction kernels, where the j-th item in \(tks\) is of the form \(tk_{j}=\{rp_{j},k_{j},o_{j}\}\). Let \(r\) be \(r=i\cap o=\{r_{0},r1,\ldots,r_{n}\}\) where we assume \(r\
eq\emptyset\) because otherwise the lemma holds trivially as \(b^{\prime}=b\). Let \(b^{\prime}\) be the block \(b^{\prime}=\{i^{\prime},o^{\prime},tks,ko\}\), with \(tks=(tk_{1},\ldots,tk_{t})\), the list of transaction kernels, \(i^{\prime}=i\setminus r\) and \(o^{\prime}=o\setminus r\). We want to prove that \(b^{\prime}\) is valid. In particular, that \(b^{\prime}\) is balanced. According to Definition 10, we need to prove:  
\[\sum_{o_{j}\in o^{\prime}}o_{j}-\sum_{c_{j}\in i^{\prime}}c_{j}=ko.G+\sum_{k _{j}\in tks}ke_{j}\]  
By hypothesis, we know that \(b\) is a valid block. Applying Property 2, we know that \(b\) is balanced.