# A Multi-Layer Secure Sharing Framework for Aviation Big Data Based on Blockchain
## 6 Security Analysis and Formal Verification
### Logical Verification  
This section conducts formal definition and logical verification analysis of the blockchain-based multi-layer aviation big data security sharing scheme using Nash equilib  
Figure 8: Model-checking results for evaluable model sharing. rium from game theory. The core of game theory lies in how rational participants select strategies to optimally respond to others' decisions in interactive environments. This analytical method aims to ensure security, privacy, and effectiveness throughout the data-sharing process. Below are relevant definitions and theorems for this model. Let \(\mathrm{P}=\{\mathrm{P}_{1},\mathrm{P}_{2},\cdots,\mathrm{P}_{\mathrm{N}}\}\) represent the set of all nodes participating in the multi-layer aviation big data security sharing, \(\chi=\{\chi_{1},\chi_{2},\cdots,\chi_{\mathrm{n}}\}\) denote the action strategy space of all participating nodes during sharing, and \(\mathrm{U}=\{\mathrm{u}_{1},\mathrm{u}_{2},\cdots,u_{\mathrm{Q}}\}\) represent the utility functions of all participating nodes under different game outcomes. The game payoff for node \(\mathrm{P}_{i}\) under strategy combination \(\{\chi_{1},\chi_{2}\cdots,\chi_{\mathrm{N}}\}\) can be expressed as \(\mathrm{u}_{i}:\chi\to V\). Lemma 1: _The utility function \(u_{i}(x),\forall x\in[0,1]\) is monotonically increasing. By definition, \(u_{i}(x)\) represents the probability that a participant can at least determine message reception/sending by others or at most obtain information with probability \(x\). Since all participants act rationally in data sharing--meaning higher \(x\) yields greater game payoff and thus higher \(u_{i}(x)\) for any \(\forall x_{1},x_{2}\in[0,1]\) where \(x_{1}\leq x_{2}\)--we have \(u_{1}(x)\leq u_{2}(x)\), proving \(u_{i}(x)\) is monotonically increasing._  
Definition 1: _Nash equilibrium. Let \(r\big{(}(\chi_{i})_{i\in\mathrm{P}}\big{)}\) denote the game outcome when participants execute strategy combination \((\chi_{i})_{i\in\mathrm{P}}\). A strategy combination \(\big{(}\chi_{i}^{*}\big{)}_{i\in\mathrm{P}}\) constitutes a Nash equilibrium if and only if no participant can unilaterally change strategy to obtain better outcomes when others' strategies are known, i.e., \(\forall i\in P\), \(r(\chi_{i},\Big{(}\chi_{j}^{*}\Big{)}_{j\in\mathrm{P}\setminus i})\leq r(\chi_ {i}^{*},\Big{(}\chi_{j}^{*}\Big{)}_{j\in\mathrm{P}\setminus i})\). As all participants are rational, none will deviate from \(\chi_{i}^{*}\). Generally, a game may yield multiple Nash equilibria._  
Definition 2: _Rational security protocol. Let \(\mu(M)=\{\mu_{1}(M_{1}),\mu_{2}(M_{2}),\cdots,\mu_{N}(M_{N})\}\) be the set of security communication protocols followed by all participants during data sharing. The communication protocol game is denoted as \(G_{\alpha,\beta,\gamma}^{S,R,A,A,A\text{viationChain}}(M)\), where \(S\) denotes sender, \(R\) receiver, \(A\) attacker, and AviationChain the sharing environment. Here, \(\alpha\) represents the minimum probability that sender \(S\) confirms correct receipt by \(R\), \(\beta\) the minimum probability that \(R\) confirms \(M\)'s origin from \(S\), and \(\gamma\) the maximum probability that \(A\) obtains \(M\). \(\mu(M)\) is rationally secure if and only if the following holds:_  
The strategy combination \(\big{(}\chi_{S}^{*},\chi_{R}^{*},\chi_{A}^{*}\big{)}\) forms a Nash equilibrium in \(G_{\alpha,\beta,\gamma}^{S,R,A,A,A\text{viationChain}}(\mathrm{M})\) producing optimal outcome \(\mathrm{r}=(\alpha,\beta,\gamma)\);  
For any Nash equilibrium in this game, \(\mathrm{u}_{i}\big{(}\chi_{S},\chi_{R},\chi_{A}\big{)}\leq\mathrm{u}_{i} \big{(}\chi_{S}^{*},\chi_{R}^{*},\chi_{A}^{*}\big{)}\). Verification:  
Per game definition, \((\alpha,\beta,\gamma)\) is the optimal outcome--no strategy change yields better results. Thus, if \(\big{(}\chi_{S}^{*},\chi_{R}^{*},\chi_{A}^{*}\big{)}\) achieves \((\alpha,\beta,\gamma)\), it constitutes a Nash equilibrium.