# A Multi-Layer Secure Sharing Framework for Aviation Big Data Based on Blockchain
## 6 Security Analysis and Formal Verification
### TLA+ Correctness Verification
#### 6.2.2 Correctness of Searchable Data-Sharing Model  
The states of the searchable data-sharing model are defined as shown in Table 3. All components start from the initial state. \begin{table}
\begin{tabular}{c c c} \hline \hline
**Entity State** & **State** & **Description** \\ \hline \multirow{3}{*}{SP\_State} & _Init_ & Data provider (SP) in ready state. \\  & _Encryption_ & SP in encryption state. \\  & _ServicePublish_ & SP in service publishing state. \\  & _Init_ & Data consumer (SC) in ready state. \\ \multirow{3}{*}{SC\_State} & _ServiceQuery_ & SC in service query state. \\  & _ServiceSubscribe_ & SC in service subscription state. \\  & _Init_ & Third-party authority (AC) in ready state. \\ \multirow{3}{*}{AC\_State} & _KeyGeneration_ & AC in key generation state. \\  & _Init_ & Blockchain in initial state. \\ \multirow{3}{*}{BC\_State} & _On-chain_ & Blockchain in on-chain state. \\  & _False_ & SP’s public key not generated. \\ \multirow{3}{*}{SPPK\_State} & _True_ & SP’s public key generated. \\  & _Untercrypted_ & SP’s private key unencrypted. \\ \multirow{3}{*}{SPSK\_State} & _Encrypted_ & SP’s private key encrypted. \\  & _False_ & SC’s public key not generated. \\ \multirow{3}{*}{SCPK\_State} & _True_ & SC’s public key generated. \\  & _False_ & SC’s private key not generated. \\ \multirow{3}{*}{SCSK\_State} & _True_ & SC’s private key generated. \\ \multirow{3}{*}{MT\_State} & _Unencrypted_ & Shared data unencrypted. \\  & _Encrypted_ & Shared data encrypted. \\ \multirow{3}{*}{KEK\_State} & _Unencrypted_ & Key-encrypting-key (KEK) unencrypted. \\  & _Encrypted_ & KEK encrypted. \\ \hline \hline \end{tabular}
\end{table} 
Table 3: States of the searchable data-sharing model. Figure 6: Verification results of optimal block deployment model. The initial state is configured with the data provider SP's state SP_State, data consumer SC's state SC_State, and third-party authority AC's state AC_State all set to \"Ready\"; the blockchain BC's state BC_State set to \"Init\"; the SP's public key state SPPK_State, SC's public key state SCPK_State, and SC's private key state SCSK_State all in \"NotGenerated\" status; and the SP's private key state SPSK_State, shared data state MT_State, and key encryption key state KEK_State for encrypting SP's private key all in \"NotEncrypted\" status. Definition 5.4: System behavior of searchable data-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 ==  
\/\ ACGenKEY  
\/\ SPEncMT  
\/\ SPEncSPSK  
\/\ SPEncKEK  
\/\ SPPublishService  
\/\ SCQueryService  
\/\ SCSubscribeService  
In the specification, ACGenKEY denotes that AC generates a public key for SP and a private key for SC; SPEncMT represents SP encrypting the shared data MT; SPEncSPSK indicates SP encrypting its own private key; SPEncKEK signifies SP encrypting the KEK; SPPublishService means SP publishing the service to the blockchain; SCQueryService refers to SC querying the service from the blockchain; and SCSubscribeService describes SC subscribing to the service from the blockchain. Definition 5.5: System specification:  
The system specification includes initial state and sequential operation execution:  
TPSpec ==  
TPInit[][TPNext]_<<SP_State,SC_State,AC_State,BC_State,SPPK_State,SPSK_State, SCPK_State,SCSK_State,MT_State,KEK_State>>  
Definition 5.6: Model invariants:  
1. Service publishing invariant: SP must be in the encrypted state with both MT and KEK encrypted before publishing service: Inv_SPPublishServiceAfterEncrypted==/\SP_State=\"Encryption\"/\MT_State = \"Encrypted\"/\KEK_State=\"Encrypted\"
2. Service query invariant:SP must have published service and SC must have generated keys before querying: Inv_SCQueryServiceAfterPublish==/\SP_State=\"ServicePublish\"/\SCPK_State=\"True\"/SCSK_State=\"True\"
3.