Formal Verification of a Blockchain-Based Security Model for Personal Data Sharing Using the Dolev-Yao Model and ProVerif

Secure personal data sharing remains a critical challenge in decentralized systems due to concerns over privacy, compliance, and trust. This paper presents the formal verification of a Blockchain-Based Security Model (BSM) designed to address these challenges through a multi-layered architecture. The proposed model integrates Chaincode-as-a-Service (CCaaS) on Hyperledger Fabric to ensure modular, maintainable, and scalable execution of smart contracts. A Flask-based API serves as the secure gateway for data operations and identity management. Sensitive data is stored off-chain using InterPlanetary File System (IPFS), preserving decentralization while minimizing on-chain bloat. Access control is enforced using efficient cryptographic techniques, while Intel SGX (or simulated enclaves) safeguards secure data processing and decryption within trusted execution environments. To further enhance privacy guarantees, Zero-Knowledge Proofs (ZKPs) are optionally integrated to enable verifiable claims without disclosing raw data. For assurance of correctness and security, the BSM is formally modeled using the Dolev-Yao attacker model and verified through ProVerif, focusing on key security properties such as confidentiality, integrity, authentication, and accountability. The findings confirm that the proposed model satisfies stringent security goals and is robust against symbolic adversaries. This work contributes a verifiable and extensible framework for privacy-preserving data sharing in sectors such as healthcare, finance, and government. To the best of our knowledge, this is among the first works to formally verify a blockchain-based security model that simultaneously integrates modular chaincode execution (CCaaS), trusted hardware enclaves (Intel SGX), decentralized off-chain storage (IPFS), and optional Zero-Knowledge Proofs (ZKPs) with a unified framework for personal data sharing.