# Evaluation and Improvement of Internet Printing Protocol Based on HCPN Model Detection Method
## 4 Security Assessment of Original Scheme  
### Security Assessment Model  
Using the advantages of CPN visual modeling, dynamic simulation, and system state-space analysis, this section introduces the improved Dolev-Yao attacker model into the original protocol model to evaluate the security of the protocol and analyze the loopholes in the protocol. According to the Dolev-Yao attack hypothesis, the attacker could intercept all the messages of the sender, and under certain circumstances (e.g., key disclosure), decrypt, tamper, and forge the message, and then transmit it to the receiver. On this basis, we further strengthened the attacker's ability to obtain the pre-shared key PSK, so an improved Dolev-Yao attacker model was established. At this point, the adversary could replace the Net entity in the original protocol model, take over the entire network, and form a security assessment model for the original protocol, as shown in Figure 10.  
First, we conducted a preliminary analysis of all current handshake messages:  
* MSG1 (CID, nc, offer) and MSG2 (SID, ns, mode) were transmitted over the network in plain text in order to complete the parameter exchange, so the security authentication function was provided by the follow-up mechanisms. * MSG3 (c1, c2, c3, c4), MSG4 (c5, c6, c7) assisted the client and the server in verifying each other's identity encrypted with TempKey. The key was obtained by ECDHE key exchange, and the generation process involved the participation of the private keys(\(\alpha\), \(\beta\) in Definitions (1) and (2)), of both communication parties. The improved Dolev-Yao attacker model did not have the ability to corrupt the client and server, obtain their private keys, nor decipher the two messages. * In MSG5(ticket), the ticket was obtained by encrypting PSK with the server's private key, which was used as a credential for subsequent session resumption and encrypted by the initial session key. The initial session key was derived from the temporary symmetric key TempKey, with a previous handshake messages. As long as the TempKey was not leaked, the security of the message could be guaranteed. * MSG7 (SFinished) and MSG8 (CFinished) were encrypted and transmitted by the subsequent handshake key. At this time, in order to ensure forward security, another round of ECDHE key exchange was performed during the subsequent handshake \begin{table}
\begin{tabular}{c c c} \hline \hline
**Category** & **Statistics** & **Name** \\ \hline Nodes & 443 & \(1,\ldots,443\) \\ Arcs & 1090 & \(1,\ldots,1090\) \\ Status & Full & Null \\ Nodes(SCC) & 443 & \(1,\ldots,443\) \\ Arcs(SCC) & 1090 & \(1,\ldots,1090\) \\ Home Markings & 1 & 443 * \\ Live Transitions & 0 & 0 \\ Dead Transitions & 1 & 443 * \\ Dead Transitions & 2 & RESET0, RESET1 \\ \hline \hline \end{tabular}  
* An asterisk represents a terminal state node.  
\end{table} 
Table 3: Model State-Space Results for the Original Protocol. key-generation process. This process involved the private keys of both parties and could be cracked. Therefore, considering the current attacker's ability, the attack behavior was aimed at the handshake message MSG6 in the subsequent session resumption phase. Figure 11 shows the model diagram of the attacking entity Adversary. In the first step, the adversary activated the attack path. It assigned the Boolean value \"true\" stored in the place Active to the variable active. The normal output path (green) of the original transition \"TransmitResumpt\" was blocked, so it entered the attack path (red). MSG6 (binder, c8) was divided into two parts and stored in the corresponding repository. This step was possible because the binder was a string of HMAC values contained in the PSK extension of the client-hello message in plain text. In the second step, it decrypted c8 to obtain the early data ed. C8 was the message encrypted by the client with the early data key EDK, and EDK was only uniquely determined by the pre-shared key PSK.