# A Formal Analysis of the Mimblewimble Cryptocurrency Protocol +
## 3 Idealized Model of Mimblewimble-Based Blockchain
### Blocks and Chains  
Genesis block _Gen_ is a special block since it is the first ever block recorded in the chain. Transactions can be merged into a _block_. We can see a block as a big transaction with aggregated inputs, outputs and transaction kernels. **Definition 9** (Block). : _A Block \(b\) is either the genesis block Gen, or a tuple of type:_  
\[\textit{Block}\stackrel{{\text{def}}}{{=}}\{i:I^{*},o:O^{*},\ \textit{tks}:\textit{TxKernel}^{*},ko:\textit{KOffset},\}\]  
_where:_  
* \(i=(c_{1},\dots,c_{n})\) _and_ \(o=(o_{1},\dots,o_{m})\) _are the lists of inputs and outputs of the transactions._
* \(\textit{tks}=(\textit{tk}_{1},\dots,\textit{tk}_{t})\) _is the list of_ \(t\) _transaction kernels._
* \(\textit{ko}\in\mathbb{F}_{n}\) _is the block kernel offset which covers all the transactions of the block._  
We can say a block is balanced if each aggregated transaction is balanced. **Definition 10** (Balanced Block). : _Let \(b\) be a block of the form \(b=\{i,o,\textit{tks},ko\}\) with \(\textit{tks}=(\textit{tk}_{1},\dots,\textit{tk}_{t})\) the list of transaction kernels and where the j-th item in tks is of the form \(\textit{tk}_{j}=\{\textit{rp}_{j},\textit{k}_{j},\sigma_{j}\}\). We say the block \(b\) is balanced if the following holds:_  
\[\sum_{o_{j}\in o}o_{j}-\sum_{c_{j}\in i}c_{j}=\textit{ko}.G+\sum_{\textit{k} _{j}\in\textit{tk}_{S}}\textit{k}_{\textit{ej}}.\]  
We assume the genesis block _Gen_ is valid. We define the notion of block validity as follows:  
**Property 2** (Valid Block). : _A block \(b\) is valid (valid_\(\_\)_block\((b)\)) if \(b\) is the genesis block Gen or it satisfies:_  
* _The block is balanced._
* _For every transaction kernel, the range proofs of all the outputs are valid and the kernel signature_ \(\sigma\) _is valid for the transaction excess._  
Blocks can be constructed by aggregating transactions as follows:  
**Definition 11** (Block Aggregation). : _Given a valid transaction \(t_{0}\) and a valid block \(b\) as follows:_  
\[t_{0}=\{i_{0},o_{0},\textit{tk}_{0},\textit{tk}_{0}\}\ \textit{and}\ b=\{i,o, \textit{tks},ko\}\]a new block can be constructed as:_  
\[b^{\prime}=\{i_{0}\ ||\ i,o_{0}\ ||\ o,tk_{0}\ ||\ tks,tko_{0}+ko,\}\]  
_where \(||\) is the list concatenation operator and \(+\) is the scalar sum._  
Block aggregation preserves the validity of blocks; that is, block validity is invariant w.r.t. block aggregation. **Lemma 2** (Invariant: Block Validity). : _Given a valid transaction \(t_{0}\) and a valid block \(b\) as in Definition 11. Let \(b^{\prime}\) be the result of aggregating \(t_{0}\) into \(b\). Then, \(b^{\prime}\) is valid._  
Proof. : Let \(t_{0}\) be the transaction \(t_{0}=\{i_{0},o_{0},tk_{0},tk_{0}\}\) with \(tk_{0}=\{rp_{0},ke_{0},o_{0}\}\). Let \(b\) be the block \(b=\{i,o,tks,ko\}\), with \(tks=(tk_{1},\ldots,tk_{t})\), the list of transaction kernels. Applying Definition 11, we have that the resulting \(b^{\prime}\) is of the form:  
\[b^{\prime}=\{i^{\prime},o^{\prime},tks^{\prime},ko^{\prime}\}\]  
with \(i^{\prime}=i_{0}\ ||\ i,\ o^{\prime}=o_{0}\ ||\ o,\ tks^{\prime}=(tk_{0},tk_{1}, \ldots,tk_{t}),\ ko^{\prime}=tk_{0}+ko\). According to Definition 10, we need to prove the following equality holds for the block \(b^{\prime}\):  
\[\sum_{o_{j}\in o^{\prime}}o_{j}-\sum_{c_{j}\in i^{\prime}}c_{j}=ko^{\prime}.G +\sum_{k\epsilon_{j}\in tks^{\prime}}ke_{j}\]  
Each term can be written as follows:  
\[(\sum_{o_{j}\in o_{0}}o_{j}+\sum_{o_{j}\in o}o_{j})-(\sum_{c_{j}\in i_{0}}c_{j }+\sum_{c_{j}\in i}c_{j})=(tk_{0}+ko).G+k\epsilon_{0}+\sum_{k\epsilon_{j}\in tks }ke_{j}.\]  
Rearranging the equality and using algebraic properties on elliptic curves, we have:  
\[(\sum_{o_{j}\in o_{0}}o_{j}-\sum_{c_{j}\in i_{0}}c_{j})+(\sum_{o_{j}\in o}o_{ j}-\sum_{c_{j}\in i}c_{j})=(ke_{0}+tko_{0}.G)+(ko.G+\sum_{k\epsilon_{j}\in tks }ke_{j}).\]  
Now, we apply the hypothesis concerning the validity of \(t_{0}\) and \(b\).