# Evaluation and Improvement of Internet Printing Protocol Based on HCPN Model Detection Method
## 2 Preliminary Knowledge  
### Internet Printing Protocol  
The Internet Printing Protocol (IPP) [10; 11] is a dedicated protocol for communication between client devices (computers, mobile phones, tablets, etc.) and printers (or print servers). Similar to all IP-based protocols, IPP can operate locally or over the Internet. IPP uses port 631 as a working port. The typical representative of its specific implementation is CUPS (Common UNIX Printing System, which is the printing module of the Apple macOS and many Unix-like operating system distributions). Message protection design goals have included data origin authentication, privacy, integrity, and non-repudiation [12; 13]. IPP is implemented using the Hypertext Transfer Protocol (HTTP), and it inherits all HTTP streaming and security features. For example, authorization can be transmitted through HTTP's digest authentication mechanism, generic security service application program interface (GSSAPI), or any other HTTP authentication method. Encryption is provided by the TLS protocol layer, the always-on TLS using HTTPS, or the HTTP upgrade scheme [14]. Public key certificates can be used with TLS for authentication. IPP has two schemes to realize the interaction between client and server:  
* IPP scheme [15]: convert IPP-URI to HTTP-URI;
* IPPS scheme [16]: convert IPPS-URI to HTTPS-URI. Generally speaking, the IPPS solution is superior in terms of security assurance, so this project only conducted security evaluation for this method. The TLS protocol is the cornerstone to ensure the safe operation of the IPP protocol. Most of the current browsers and web applications that use the HTTPS protocol support the version of TLS 1.2. However, with the passage of time, more and more loopholes have been exposed, including loopholes in encryption algorithms, such as by attacking the internal state of the Rivest Cipher 4 (RC4) stream cipher [17] and loopholes in the process of code implementation, such as the authors in [18] pointed out. The Heartbleed vulnerability was a technical error introduced by the OpenSSL program. When it was exploited, it caused a memory leak from the client to the server. However, we preferred to focus on the design flaws of the protocol itself, rather than discuss the internal problems of the cryptographic algorithm and the code implementation process. For example, Lucky 13 [19] used the time difference between the servers to process messages with correct padding and incorrect padding to derive plaintext information. [PERSON] [20; 21] used man-in-the-middle attacks to downgrade the secure connection of a server. To resolve the above problems, TLS1.3 has made major improvements on the basis of TLS1.2, such as only using the authenticated encryption with associated data (AEAD) algorithm on the record protocol layer and removing the static Rivest--Shamir--Adleman (RSA) and DiffieHellman (DH) key agreement at the handshake protocol layer, and removing the change password specification protocol, etc. These outstanding works have greatly improved the security of TLS1.3, but also created new problems in terms of zero round-trip time (0-RTT), fault tolerance, and forward secrecy [22]. Users hope to minimize service delays without sacrificing security. Based on this consideration, the Internet Engineering Task Force (IETF) designed the 0-RTT mechanism of TLS1.3 based on the QUIC protocol [23; 24]. The 0-RTT mechanism sped up the operation of the protocol and improved the user experience. While being widely used, its security has also attracted researchers' attention. At present, there are three methods for researching protocol formalization: the modal logic method, the theorem-proving method, and the formalization method based on model checking. The authors of [25] used the modal logic method [26] to abstract the participating objects and state relationships involved in TLS1.3, and then they analyzed the security of the 0-RTT process through logical reasoning, but the analysis results depended on the initial logic hypothesis and chosen logical framework.