# TDLearning: Trusted Distributed Collaborative Learning Based on Blockchain Smart Contracts
## 4 Formal Security Analysis of Smart Contracts
### Design and Analysis of Authority Layer and Validation Layer  
#### 4.3.1 Formal Modelling  
The Authority layer model is the bottom implementation of the authority-management substitution transition, which models the role-authority-management function. As shown in Figure 8, the model contains a total of 17 places and 10 transitions, with five of the port places connected to the top-layer CPN model. The places _UInfo_ and _VInfo_ denote the collaborators and model verifiers to be authorised, respectively, and _C_list_ and _V_list_ are the lists of collaborators and model verifiers that have been authorised, respectively. Collaborator permissions are modelled as a quadruplet (UAdd, URole, UStatus and UInfo) with the collaborating node's Ethernet address, node role, node-identity status and node information overview, respectively. The model verifier authority is modelled as a five-tuple (UAdd, URole, UStatus, UInfo and V_Credit), with the first four items of authority information being the same as the collaborator and the fifth item being the model-verifier credibility value. Therefore, we will introduce the places and transitions of the Authority layer in terms of the model-verifier authority-management process, without going into the rest of the content. The change _Init_V_ models the collaborative node information-initialisation behaviour, modifying the node-identity status from pending review to legal, and _V_Auth_ models the smart contract assignment of node role-authority behaviour, modifying the node role from pending assignment to model verifier. The places _V_Nodes_ and _Co_Verifier_ denote model verifiers before and after the role-authority assignment, respectively. The place _v_times_ denotes the number of times the smart contract presets role-authority assignment to limit the supervisor's authority assignment behaviour. The transition _V_As_ adds model verifiers that have been assigned collaborative node role authority to the list _V_list_ and also records the corresponding authority information to the place _v_node_. When a model verifier behaves suspiciously, the _Su_ can restrict its role authority through the AMC. The transitions _Cancel_V_ and _Deau_V_ model the behaviour of the AMC restricting the authority of a model verifier, and the places _cancel_v_ and _V_Malicious_ denote a malicious model verifier with its corresponding suspicious behaviour, respectively.  
Figure 7: The top layer of CPN model.  
The Validation layer is the bottom implementation of the Authorisation Validation Institution, which models the role-authority-validation function in smart contracts. As shown in Figure 9, the transition _Validation_C_ models the collaborator-authority-validation behaviour, which is achieved by determining whether a collaborator belongs to the list of legitimate collaborators. The place of _require_1_ indicates the collaborator request, and the place of _right_1_ indicates the result of the smart contract authority-restriction function, which returns \"access\" if it passes the authority verification; otherwise, it returns \"no acces\". The transitions _Validation_C_ and _Validation_U_ together represent the authority-validation behaviour, where _Validation_C_ determines whether the model verifier requesting an on-chain operation belongs to the list of legitimate verifiers, _Validation_U_ determines whether the corresponding model verifier meets the credibility threshold requirements and the places _require_2_ and _right_2_ represent the results returned by the model-verifier on-chain operation request and the smart contract authority-restriction function, respectively.