deg_HOL4_verification

Implementation and verification of the DEG smart contract in HOL4

Content:

1) degTypesScript.sml

Implementation of smart contract types in HOL4.

2) degScript.sml

Implementation of smart contract functions in HOL4.

3) degChainScript.sml

Framework for embedding a smart contract in an environment model and for specifying its properties in HOL4.

4) degPropertiesScript.sml

Proofs of smart contract and its functions properties.

Properties that have been proven

1. Voter authentication in SC.

2. Privacy of intermediate results.

3. The impossibility of sabotage by external violators.