# A Formal Analysis of the Mimblewimble Cryptocurrency Protocol +
## 4 Verification of Mimblewimble
### Unlinkability and Untraceability
We say \(B\) receives the transaction with confusion if given the IP address of node \(A\), the node \(B\) does not know if the transaction was originated by the node \(A\) or not._  
In other words, it can be said that if some malicious nodes, working together, construct a graph of the pairs \((transaction,IP address node)\), the IP address node will not convey information about what node originated the transaction. Therefore, in our model, we require Property 16 to hold before the broadcast takes place. In order to achieve this, we can establish that the node broadcasting the transaction should be far enough from the one which originated it. Moreover, CoinJoin could be performed before the broadcast. Dandelion, proposed by [PERSON] et al. [41], is a protocol for transaction broadcasting intended to resist that deanonymization attack. Dandelion is not part of the MW protocol, however this kind of protocols should be implemented by each node to lower the risk of creating the transaction graph. In Dandelion, broadcasting is performed in two phases: the \"steam\" phase and the \"fluff\" phase. In the \"steam\" phase the transaction is broadcasted randomly to one node, which then randomly sends it to another, and so on. This process finishes when the \"fluff\" phase is reached, and the transaction is broadcasted to the network using a gossip protocol. The following routines capture the semantic of the phases:subroutine steam\((tx:Transaction)\{\)  
\(c\leftarrow\{0,1\}\) (* random decision *)  
if \(c==0\) then  
\(node\leftarrow\) select_random_node\(()\)  
\(node\_steam(tx)\)  
else  
\(this\_fluff(tx)\)  
\(\}\)  
subroutine fluff\((tx:Transaction)\{\)  
\(broadcast(tx)\)  
\(\}\)  
Each node, besides having the local state, should implement these two routines. Once the transaction is created and is ready to be included in the mempool, its broadcasting start in the \"steam\" phase. When it reaches the \"fluff\" phase, it is broadcasted to the network and added in the mempool. Dandelion relies on the following three rules: all nodes obey the protocol, each node generates exactly one transaction, and all nodes on the network run Dandelion. The problem is that an adversary can violate them. For that reason, [PERSON] implements a more advanced protocol called Dandelion++ [42] which intends to prevent that [43]. However, it is believed that Dandelion++ is not good enough to guarantee the privacy of a virtual coin [44]. For instance, the flashlight attack [45] is an open problem still under investigation [46]. The scenario here is when an 'activist' want to accept donations but he cannot reveal his identity. At some point, he will deposit those payments to an exchange and his identity would be compromised. The adversary injects 'tainted coins' and could build a 'taint tree' looking through all deposits to the exchange. This way, he could link those deposits to the 'activist'. The combined use of the MW protocol with a Zerocash-style commitment-nullifier schema has been put forward in [PERSON] [47] as a countermeasure to the above attack. In the case of Zcash, every shielded transaction has a large anonymity set, namely, a set of transactions form which it is indistinguishable from. In the case of Spectrecoin (now Alias) [48], the main idea is the use, only once, of public addresses (XSPEC) to receive the payments combined with an anonymous staking protocol.