Smart Contract–Enabled P2P Energy Trading: A Formally Verified Game-Theoretic Framework

Abstract

The global energy sector is experiencing a significant revolution, propelled by the necessity to address climate change and shift towards sustainable energy sources. Particularly, the extensive implementation of distributed solar photovoltaic generation is converting traditional power grid systems into decentralized, prosumer-oriented energy grids. However, the traditional centralized energy trading frameworks cannot handle the complexity and volatility of a distributed grid, resulting in delay, costly transactions, a single point of failure, and insufficient transparency. Although blockchain (BC)-based peer-to-peer (P2P) energy trading presents an attractive solution, current models frequently neglect to ensure dependable and steady market convergence, instead concentrating mainly on transactional elements. This study proposed an innovative smart contract-based P2P renewable energy trading framework intended for decentralized grids. The proposed two-tiered framework, i.e., intra-microgrid and inter-microgrid layers, expands P2P trading from regional equilibrium to full grid connectivity. It utilizes a game-theoretic, iterative bidding approach, entirely automated by smart contracts. This method is formally proven to attain market convergence to a singular Nash equilibrium, optimizing utility for prosumers and consumers in the energy trading. Moreover, the decentralized ledger, smart contract-based market clearance, and limited disclosure of consumer/prosumer’s private data enhanced its resilience against replay, false data injection, and DoS/DDoS attacks. Additionally, the proposed energy trading market is proved monotonic and convergent formally by implementing a Promela model using the SPIN model checker.