# A Multi-Layer Secure Sharing Framework for Aviation Big Data Based on Blockchain
## 6 Security Analysis and Formal Verification
### TLA+ Correctness Verification
#### 6.2.1 Correctness of Optimal Block Deployment Model  
The states of the optimal block deployment model are defined as shown in Table 2. All components start from the initial state. Figure 5: The specific process of model training and contribution assessment. The initial state is set with the aircraft node state AN_State as \"SBR\", the master node state MN_State as SBR, and empty sets for the block optimization candidate node set as AN_OptimizePrepared, block pruning candidate node set as AN_PrunePrepared, and peer-to-peer message collection set as msgs. Definition 5.1: System behavior of the optimal block deployment model: The system behavior is defined by the \"TPNext\" operation, which determines what operations are allowed to occur in the system and ensures they are executed in the correct order. The formal description of the optimal block deployment model's system behavior is defined as:  
TPNext ==  
\(\backslash\)/ \(\backslash\)E an \(\backslash\)in AN :  
ANPrepareOptimize(an)  
\(\backslash\)/ MNRcvOptimizePrepared(an)  
\(\backslash\)/MNCommitOptimize  
\(\backslash\)/ ANRvCommitOptimizeMsg(an)  
\(\backslash\)/ ANPreparePrune(an)  
\(\backslash\)/ MNRcvPrunePrepared(an)  
\(\backslash\)/ MNCommitPrune  
\(\backslash\)/ ANRvCommitPrunedMsg(an)  
where ANPrepareOptimize and MNRcvOptimizePrepared represent all nodes sending block optimization preparation messages to the master node and the master node receiving these messages, respectively. MNCommitOptimize and ANRvCommitOptimizeMsg represent the master node committing block optimization deployment and other nodes receiving the optimization deployment messages, respectively. ANPreparePrune and MNRcvPrunePrepared represent all nodes sending block pruning preparation messages to the master node and the master node receiving these messages, respectively. MNCommitPrune and ANRvCommitPrunedMsg represent the master node committing block pruning and other nodes receiving the pruning messages, respectively. Definition 5.2: System specification of optimal block deployment model: The behavioral specification of the system includes the initial state and sequential execution of each operation, formally described as \begin{table}
\begin{tabular}{c c c} \hline \hline
**Entity State** & **State** & **Description** \\ \hline AN\_State & SBR & Node in “Storage-by-Request” phase. \\  & OptimizePrepared & Node prepared for block optimization. \\  & SOD & Node in “Storage-on-Demand” phase. \\  & PrunePrepared & Node prepared for block pruning. \\  & DPS & Node in block pruning phase. \\  & SBR & Master node in “Storage-by-Request” phase. \\ MN\_State & & Master node in \\  & SOD & “Storage-on-Demand” phase. \\  & DPS & Master node in block pruning phase. \\ AN\_OptimizePrepared & AN & Candidate node set for block optimization. \\ AN\_PrunePrepared & AN & Candidate node set for block pruning. \\  & & Peer-to-peer communication message \\ msgs & Message & set. \\ \hline \hline \end{tabular}
\end{table} 
Table 2: States of the optimal block deployment model. TPSpec ==  
TPInit[][TPNext]_<<AN_State,MN_State,AN_OptimizePrepared,AN_PrunePrepared,msgs>>  
Definition 5.3: Invariants of optimal block deployment model:  
(1) Before the master node commits block optimization deployment, it must receive block optimization preparation messages from all other nodes, and the master node state must be in the Block On-Demand Storage phase. The formal description is  
Inv_MNCommitOptimizeAfterPrepared==/\MN_State=\"SBR\"/\AN_OptimizePrepared=AN  
(2) Before the master node commits block pruning, it must receive block pruning preparation messages from all other nodes, and the master node state must be in the Block Optimized Storage phase. The formal description is  
Inv_MNCommitPruneAfterPrepared==/\MN_State=\"SOD\"/\AN_PrunePrepared=AN  
The TLA+ model checker was used to verify the formal specification of the optimal block deployment model. The verification results are shown in Figure 6. All invariant checks were passed, and no deadlocks were found in the entire state space.