# A Multi-Layer Secure Sharing Framework for Aviation Big Data Based on Blockchain
## 6 Security Analysis and Formal Verification
### TLA+ Correctness Verification
#### 6.2.3 Correctness of Evaluable Model-Sharing Model  
The states of the evaluable model-sharing model are defined as shown in Table 4. All components start from the initial state. The initial state is configured with the data requester node RN's state RN_State and data provider node PN's state PN_State both set to \"Initialized\", the set of all nodes prepared for model-sharing state PN_Prepared initialized as an empty set, the blockchain BC's state BC_State set to \"Init\", the FL model's state Model_State in initialized status, and the peer-to-peer communication message set msgs initialized as an empty collection. Definition 5.7: System behavior of evaluable model-sharing model:  
The system behavior is defined by the TPNext operation, which determines permitted operations and ensures correct execution order. The formal specification is as follows:  
TPNext ==  
\(\backslash\)\(\backslash\)Epn \(\backslash\)in PN:  
\(\backslash\)/ RNBiddingPN  
\(\backslash\)/ PNRcvBiddingMsg(pn)  
\(\backslash\)/ RNRcvBidPreparedMsg(pn)  
\(\backslash\)/ RNCommitBidMsg  
\(\backslash\)/ PNTrainModel(pn)  
\(\backslash\)/ PNEvaluatePreparedMsg(pn) \begin{table}
\begin{tabular}{c c c} \hline \hline
**Entity State** & **State** & **Description** \\ \hline \multirow{5}{*}{RN\_State} & _Init_ & Data requester (RN) initialized. \\  & _Bid_ & RN in bid-publishing phase. \\  & _Waited_ & RN awaiting responses. \\  & _Obtained_ & RN in data-obtained state. \\  & _Init_ & Data provider (PN) initialized. \\  & _TrainPrepared_ & PN prepared for FL model training. \\  & _Trained_ & PN in FL training state. \\  & _EvaluatePrepared_ & PN prepared for FL model evaluation. \\  & _Evaluated_ & PN in FL evaluation state. \\  & _AggregatePrepared_ & PN prepared for FL model aggregation. \\  & _PN_Prepared_ & Set of nodes prepared for model sharing. \\  & _Init_ & Blockchain initialized. \\  & _Trained_ & Blockchain in FL training state. \\  & _Aggregated_ & Blockchain in FL aggregation state. \\  & _False_ & FL model initialized. \\  & _Trained_ & FL model trained. \\  & _Evaluated_ & FL model evaluated. \\  & _Aggregated_ & FL model aggregated. \\  & _Message_ & Peer-to-peer message set. \\ \hline \hline \end{tabular}
\end{table} 
Table 4: States of the evaluable model-sharing model. Figure 7: Model-checking results for searchable data sharing. \/ BCRcvEvaluatePreparedMsg(pn) / BCCommitEvaluatedMsg / PNRcvCommitEvaluatedMsg(pn) / PNAAggregatePreparedMsg(pn) / BCRcvAggregatePreparedMsg(pn) / BCCommitAggregated Herein, RNBiddingPN denotes that RN sends data request messages to all nodes on the blockchain; PNRcvBiddingMsg indicates that PN nodes receive the data request messages; RNRcvBidPreparedMsg represents RN receiving the complete set of PN nodes prepared to participate in model sharing; RNCommitBidMsg signifies RN submitting the message about participating model-sharing nodes; PNTrainModel shows that PN nodes receive the participation messages and subsequently initiate FL model training; PNEvaluatePreparedMsg demonstrates that PN nodes, upon completing model training, transmit model evaluation preparation messages to the blockchain; BCRcvEvaluatePreparedMsg reflects the blockchain receiving these model evaluation preparation messages from PN nodes; BCCommitEvaluatedMsg embodies the blockchain committing the model evaluation messages; PNRcvCommitEvaluatedMsg portrays PN nodes receiving the model evaluation messages from the blockchain; PNAaggregatePreparedMsg illustrates PN nodes sending model aggregation preparation messages to the blockchain after completing model evaluation; BCRcvAggregatePreparedMsg captures the blockchain receiving these model aggregation preparation messages from PN nodes; and BCCommitAggregated ultimately represents the blockchain committing the final model aggregation message.