Let us assume that Alice and Bob are playing a game. Alice first commits her value chosen from $\{0,1\}$ via Pedersen commitment scheme and sends the commitment to Bob. Then Bob sends his value chosen from $\{0,1\}$ to Alice. Finally, Alice opens this commitment to Bob. If Alice's value is equal to Bob's, then Alice wins. Otherwise, Bob wins. We assume that there is no abortion during the procedure.
A malicious Alice may try to open the commitment to the same value as Bob. But the intuition is that Pedersen commitment scheme is computational binding, and thus Alice cannot equivocate the committed value.
However, I am wondering whether we could provide a formal security proof via reduction. I.e., whether we could use malicious Alice to break the binding property of the commitment scheme. If we cannot do this, I am wondering how to formally show that the protocol is secure.