Formalizing security properties in blockchain protocols

Abstract: In this report we have used the logic L to write a formal specification of security properties in blockchain protocols for managing Electronic Health Records. The protocols have been adapted from previous research, and then formalized with regards to the properties data privacy and data integrity. We used the logic L to define a logical model M. M was then used to write formulas which formalize security properties in the blockchain protocols. The protocols handle encryption key exchange, agent authentication, permission handling and read/write operations to blockchain storage. It remains to be proven that the adapted protocols have the properties defined by our formal specification.