# A Formal Analysis of the Mimblewimble Cryptocurrency Protocol +
## 4 Verification of Mimblewimble
### Security Properties of Pedersen Commitments
#### 4.3.1 Pedersen Commitments Are Computational Binding  
This property relies on the discrete logarithm assumption. In provable security, security is proved to hold against any probabilistic time adversary by showing an efficient way to break the cryptography protocol implies a way to break the underlying mathematical problem which is supposed to be hard (security reduction). The adversary is modeled as a procedure. **Definition 13** (Computational Binding Commitment). : _Let \(\zeta(Setup,Com)\) be a [PERSON] commitment scheme as in Definition 2. Let \(\mathcal{A}_{Binding}\) be a polynomial probabilistic time adversary against the binding property running in the context of the game \(\mathcal{G}_{Binding}\) as in Figure 1. We say that the [PERSON] commitment scheme \(\zeta\) is computational binding if the success probability of \(\mathcal{A}_{Binding}\) winning game \(G_{Binding}\) is negligible._  
In game \(G_{Binding}\), firstly the scheme is set up by choosing two generator points, \(G\) and \(H\), over the elliptic curve \(\mathcal{C}\) of prime order \(n\). All these parameters are public. Secondly, the adversary \(\mathcal{A}_{Binding}\) performs the attack attempting to find out two different transactional values \(v_{1}\) and \(v_{2}\) that commit to the same commitment. Once the adversary finishes the attack, two pair of different opening values are returned. The adversary succeeds if both pairs commit to the same value and \(v_{1}\
eq v_{2}\). As we mentioned before, the computational binding property is based on a security reduction. In terms of Pedersen commitment, it means that if the adversary \(\mathcal{A}_{Binding}\) could perform the attack in the context of game \(G_{Binding}\) and could win with non-negligible probability, an adversary \(\mathcal{I}_{Dlog}\) attacking a game against the discrete logarithm problem on the group \(\mathcal{C}\) could use \(\mathcal{A}_{Binding}\) to win the game with non-negligible probability. Recall that MW uses Pedersen commitment with elliptic curves (Definition 2). The discrete logarithm problem on this context means: given a point \(y\) over the elliptic curve \(\mathcal{C}\) with generator \(G\), it is hard to find \(x\) such that \(y=x.G\). The following lemma captures the semantics of that security reduction. **Lemma 6** (Computational Binding). : _Let \(\zeta(Setup,Com)\) be a [PERSON] commitment scheme as in Definition 2. Let \(\mathcal{A}_{Binding}\) be an adversary against the computational binding commitment (Definition 13) in the commitment scheme \(\zeta\)._  
_Let us assume that \(\mathcal{A}_{Binding}\) succeeds in finding two distinct pair of opening values that commit to the same commitment with \(\epsilon\) probability. Therefore, there exists an inversor \(\mathcal{I}_{Dlog}\) which can find out the discrete logarithm to the base \(G\) of a randomly chosen element \(y\) on the elliptic curve \(\mathcal{C}\) with \(\epsilon^{\prime}\) probability using the adversary \(\mathcal{A}_{Binding}\)._  
_Hence, if \(e^{\prime}\) is negligible then \(e\) is negligible too._  
In these cases, the contraposition is proved: if \(\epsilon\) is non-negligible, then \(e^{\prime}\) is non-negligible too. The goal of the proof is to show how to transform the efficient adversary \(\mathcal{A}_{Binding}\) that is able to break the computational binding commitment into an algorithm that efficiently solves the discrete logarithm assumption. The inversor \(\mathcal{I}_{Dlog}\) will provide a simulation context in which the adversary \(\mathcal{A}_{Binding}\) will perform its attack. The attack of the inversor \(\mathcal{I}_{Dlog}\) will be successful if \(\mathcal{A}_{Binding}\) is successful and the simulation does not fail. According to game \(G_{Binding}\), when the adversary \(\mathcal{A}\) succeeds we have two identical commitments \(Com(v_{1},r_{1})=Com(v_{2},r_{2})\) and \(v_{1}\
eq v_{2}\) such that (Definition 2):  
Figure 1: Game Binding Commitment.