A privacy-preserving framework for smart contracts based on stochastic model checking

Abstract

In the process of using smart contracts, users need to provide privacy data such as personal account information to the contract for transactions. However, as the number of users continues to increase, privacy data leakage has become more and more serious. Also, the current model checking methods do not involve verifying the privacy data in smart contracts. For these reasons, we introduce a privacy-preserving framework based on stochastic model checking called VeriPrivData. It formally expresses privacy data by data sensitivity. The smart contract is defined as the Commitments tuple with data sensitivity. Then the Commitments tuple is used to model as DTMC (Discrete Time Markov Chains). We extend PCTL (Probabilistic Computation Tree Logic) to ds-PCTL (Probabilistic Computation Tree Logic with data sensitivity) for describing the privacy requirements. Finally, we verify whether DTMC satisfies the ds-PCTL formula. In this paper, the VeriPrivData framework uses the stochastic model checking tool PRISM, and experiments are carried out. Experimental results show that this method can effectively avoid illegal disclosure of privacy data and enhance the protection of privacy data in the contract.