1. Introduction
In recent years, the security issues of Building Automation Systems [
1] have become a hot research topic, among which the EIBsec protocol is used as the KNX data protection [
2] protocol in building automation systems. KNX/EIB [
3] bus technology can realize the control of heating, ventilation, air conditioning, lighting, and shading systems, so it is widely used in BAS. However, while it offers convenience, there are also many security risks between devices connected by the bus. In particular, when communicating between devices, due to the incomplete security mechanism of the protocol, user identity information is leaked and communication data are intercepted. Additionally, fire alarm systems, system intrusion and access control systems must resist not only random interference, but also deliberate attacks by third parties who want to disrupt their actions, like supply chain attacks, third-party plugin vulnerability attacks, Phishing, etc., so they have higher security requirements. For example, the BACnet/IP [
4,
5] protocol, which is also widely used in BAS, has authentication defects. The sender and receiver obtain the session key through the key server in this protocol, but there is no storage and management of historical keys. Therefore, there are forward and backward security flaws. In addition, in the LonTalk [
6] protocol, the sender and receiver authenticate their identities through pre-shared keys, but the two parties do not conduct key negotiation in advance, and there is a risk of authentication defects and key leakage.
As an extension of the KNX/EIB protocol, EIBsec employs the advanced AES [
7,
8] symmetric encryption algorithm for secure data transmission across the bus. This enables various devices to communicate and collaborate effectively. Consequently, the EIBsec protocol finds extensive use in smart home devices and industrial control equipment for building automation.
For instance, iconic landmarks like the Oriental Pearl Tower in Shanghai rely on the EIBsec protocol to orchestrate the nightly display of synchronized colorful lights. Similarly, numerous shopping malls and renowned hotels depend on the EIBsec protocol to ensure the normal operation and data security [
9,
10] of ventilation systems, lighting systems, elevators, and other equipment. These Internet of Things (IoT) devices gather environmental information through sensors [
11], converting them into digital data to uniformly transmit the information to the Internet of Things gateway [
12,
13], and transmit it to the EIBsec system for processing. The processed data are then sent back to the sensors [
14], allowing them to adjust IoT devices based on the feedback. Simultaneously, the results are transmitted to managers through the Internet, facilitating the redesign or improvement of IoT devices using the collected data. Moreover, some businesses need to collect substantial user data through industrial control systems, including sensitive personal information such as images, videos, and audio recordings. There are some security issues involved in the above-mentioned transmission process. To address these issues, the EIBsec protocol should initially desensitize sensitive information when collecting and responding to data in the end device. There are three entities in the above process, terminal sensor, IoT gateway and EIBsec system. The data generated during this process are managed uniformly by data security engineers. Residential users should only have access rights; data administrators should have access, add and modify permissions; and system administrators should have access, modify, add and delete permissions.
Furthermore, this process should rigorously verify device information integrated into the EIBsec system. Additionally, identity verification of device administrators in the cloud environment is essential. In actual applications, the security requirements are far greater than these. But in the actual environment, does the EIBsec protocol meet this series of security requirements? Administrators have repeatedly claimed that the EIBsec system is absolutely secure. However, in recent years, network attackers use diverse attack methods, such as Apache Log4j2 (CVE-2021-4101) remote code execution vulnerability exploitation, Shiro deserialization vulnerability exploitation (CVE-2019-12422), social engineering phishing, etc., which have caused a series of security problems, such as system host compromise, system permissions and data loss, and sensitive data exposure to occur frequently. These are enough to cause us to pay attention to the security of the underlying protocol of the system.
Therefore, this article focuses on the EIBsec protocol as its research subject. Using the CPN Tools [
15] modeling tool combined with the Dolev–Yao attacker model, we analyze the message interaction process of the protocol, evaluate the security attributes of the protocol, identify potential security vulnerabilities [
16], and ultimately put forth an improved plan. This plan aims to mitigate security risks and enhance the system’s security attributes. The contributions of this article are as follows:
The structure of this article is as follows: In
Section 2, we discuss related work and introduce the basic knowledge of the protocol.
Section 3 uses the CPN Tools tool to model and analyze the EIBsec protocol and verifies the consistency between the CPN model and the original protocol based on the state space report. In
Section 4, we introduce the security assessment model to conduct security assessment and discover the security vulnerabilities of the protocol. In
Section 5, we provide an improvement method for the security vulnerabilities in the protocol and conduct CPN modeling based on the improved scheme. The same security assessment model is introduced into the improved CPN model to verify the security of the new scheme. In
Section 6, the performance and security of the new scheme are mainly analyzed and compared.
Section 7 summarizes the full paper and looks forward to future work.
We found that the new scheme can resist tampering attacks and replay attacks through modeling evaluation. By comparing the original scheme and the new scheme in
Section 7, we found that the new scheme has higher security.
2. Related Work
The security of data transmission in building automation systems is extremely important for individual users or for a business unit. Scholars in the field of information security have proposed various solutions for the secure transmission of data in building automation systems in communication protocols. The authors of [
21] proposed a dual-factor authentication scheme, claiming that it can provide forward encryption and resist sensor capture attacks, user tracking attacks, and DOS attacks. This scheme is logically safe, but the author did not use formal analysis tools for modeling and analysis. Moreover, this scheme requires a large amount of capital costs when invested in actual production environments, and the implementation risk factors are high. The authors of [
22] propose a secure EIB protocol called SEIB, which uses 32-bit CRC verification to monitor unauthorized access and a 128-bit counter to prevent replay attacks. However, SEIB still has many security risks, such as unprotected communication tunnels and the use of weak encryption algorithms, which can easily crack the content. literature [
23,
24] use the KNX/EIB-based network simulation framework OMNeT++ [
25] to build a model for the EIBsec protocol to test the performance of the protocol, but do not analyze the security of the protocol, nor establish a visual security assessment model. The authors of [
26] pointed out the application characteristics of the EIBsec protocol in KNX/TP networks, but did not analyze the security flaws of the protocol.
In summary, there is currently no reliable solution to verify and improve the EIBsec protocol, and there is also a lack of a formal protocol modeling analysis method. Additionally, an attacker model is needed to perform security testing on the original protocol and the improved protocol. This article uses formal analysis methods to analyze the interaction process of the original protocol and uses the Dolev–Yao attacker model to conduct a security assessment of the original protocol. It is found that the protocol has a risk of man-in-the-middle attacks leading to the theft of session keys and user data. In view of the security flaws in the protocol, this paper proposes a new improvement scheme and conducts modeling analysis and security assessment of the improved new protocol. This article conducts formal modeling, analysis, and evaluation of the protocol based on CPN theory. Security testing is conducted by extracting key parts of the protocol to discover security flaws. After a security assessment, it was found that the protocol has replay attacks and tampering attack vulnerabilities initiated by man-in-the-middle attackers. This article will propose an improved scheme to solve the security vulnerabilities [
2,
23] of this protocol. In order to verify the effectiveness of the proposed scheme, a security evaluation of the new method was conducted. Finally, the security of the original scheme and the improved scheme was compared.
Compared with existing security research, the scheme proposed in this article has the advantage of formal verification. A new formal model-checking method was used to analyze the security of the protocol while ensuring consistency with the original model. In order to study the security vulnerabilities of this protocol, an attacker model is introduced. We also propose targeted improvement methods for the discovered security vulnerabilities, and conduct subsequent security verification of the new solution.
2.1. Tools Comparison
This article mainly focuses on the security mechanisms in the protocol, verifies the security of the EIBsec protocol, and identifies security vulnerabilities in the protocol. Therefore, it is assumed that the communication is reliable. Then, formal modeling tools are used to model and analyze the protocol. The current mainstream formal modeling tools include Scyther [
27], Tamarin [
28], ProVerif [
29], and CPN Tools [
20].
The Scyther tool can only verify the confidentiality of the protocol, and it is not very effective at verifying other properties such as availability and integrity. In addition, the ability of Scyther in protocol verification is relatively weak, and for complex protocols or protocols that require more sophisticated analysis techniques, it cannot fully cover all security vulnerabilities. Tamarin only supports a limited range of protocol models; for example, it does not support non-deterministic state transitions, complex data structures, and computations, among others. Therefore, some complex protocols may not receive full verification in Tamarin, and the models generated by Tamarin may become very large, requiring a significant amount of memory and computational resources. ProVerif is a highly abstract tool that is typically used to verify small-scale protocols. As the protocol becomes more complex, it may not be able to handle all cases correctly. The verification time of ProVerif is influenced by the size and complexity of the protocol, so verifying large-scale protocols may take a long time.
CPN Tools is a tool for modeling, simulating, and analyzing Colored Petri Nets. It supports various models, including static and dynamic models, and can be easily modified and extended. It has an intuitive user interface that helps users create, edit, and analyze CPN models. Users can directly edit Petri nets through the graphical interface, or use advanced features to define Petri nets. It supports multiple analysis techniques, including simulation analysis, performance analysis, model checking, and state space analysis, making it convenient for users to perform comprehensive analyses of models. It enables hierarchical modeling and analysis of complex protocols for the verification of security mechanisms. Users can define the necessary data types through the ML language to detect the protocol’s confidentiality, integrity, and availability and identify potential vulnerabilities. However, CPN Tools uses a specialized Petri net drawing language (ML), so users need to have a certain Petri net foundation to use the tool for modeling and analysis. Therefore, the learning curve is steep and may require some time and effort to learn and become proficient with the tool.
Compared to the three automated protocol security verification tools mentioned above, CPN Tools has several advantages in the manual analysis of protocols. Additionally, the high degree of freedom in the CPN modeling process is also one of its strengths. The state space is entirely controlled by the modeler, and different modeling and analysis methods can be implemented for different protocols. This is why CPN Tools are usually more effective than automated protocol verification tools in protocol verification. Therefore, this paper uses the CPN Tools to simulate the protocol.
3. Modeling for EIBsec Protocol
The EIBsec protocol is an extension of the KNX/EIB protocol, which provides protection for management communications and process data communications and is mainly used to protect data from malicious attacks during transmission. This protocol contains three communication entities during the communication process, namely: Entity A, Entity B, and ACU. In the EIBsec protocol, identity authentication is divided into two stages: the first stage is for the distribution of session keys, and the second stage is for identity authentication between entities. The protocol uses the AES-128 symmetric encryption algorithm to encrypt request and response messages in the key distribution phase and identity authentication phase. This article mainly studies the security flaws existing in the session establishment process, models and analyzes the protocol, and evaluates the security mechanism of the protocol. The flow chart and description of the symbols required in the modeling process are shown in
Table 1.
The message flow diagram of the protocol is shown in
Figure 5:
Phase 1: Key Distribution
Step 1: Entity A sends a session key request message to the corresponding key distribution server ACU, which includes random numbers N1, NA, and AddrA of Entity A, as well as the request address AddrB of Entity A.
Step 2: After receiving the session key request message, the corresponding ACU sends an initialization connection message to entity B based on the request content, which includes the address AddrA of entity A and the random number NB.
Step 3: Entity B responds to ACU with an encrypted message based on the connection request content, which contains a random number N2 and is encrypted using Entity B’s key KB.
Step 4: After receiving the response message from entity B, ACU decrypts the response message and then responds to entity A and entity B with a message containing the session key. The message responding to entity A contains the session key KSB_AB and Random number NB of entity B, Using KA to encrypt messages containing KSB_AB and NB. The message responding to entity B contains the session key KSB_AB and Random number NA of entity A, Using KA to encrypt messages containing KSB_AB and NA. After this step is completed, it indicates that ACU has completed key distribution, followed by entity A and entity B for identity authentication.
Phase 2: Identity Authentication
Step 5: Entity A and entity B use KA and KB to decrypt the key response message and obtain the session key KSB_AB. At the same time, entity A obtains the random number NB and entity B obtains the random number NA. Entity A initiates an identity authentication connection request to entity B. The request contains a new random number N3, using the session key KSB_AB to encrypt the request message, and then sends the encrypted message A_Auth_Connect_Request to entity B.
Step 6: After receiving the request message A_Auth_Connect_Request, entity B uses the session key to decrypt and obtain the random number N3. At the same time, the random number N3’ (N3−1) is calculated according to the agreed calculation rules. Then, we use KSB_AB to encrypt N3’ and the new random number N4 and send the encrypted message A_Auth_Connect_Reply to entity A.
Step 7: After receiving the A_Auth_Connect_Reply message from entity B, entity A decrypts and obtains the random number N4. Entity A uses the agreed calculation rules to recover N3 (N3’ +1) and Compares N3 and N3’(N3’ = N3 of original EntityA), if expectations are met, subsequent certification will be carried out. At the same time, Calculating N4’ (N4−1) and encrypting messages containing the random number N4’ using the session key KSB_AB to form an A_Auth_Connect_Response message, it responds to entity B; entity B decrypts the message, obtains N4’, then restores N4 (N4’ + 1), and compares recovered N4 and N4’ (N4’ = N4 of original Etity B). If the expectations are met, the session between entity A and entity B is successfully established.
3.3. CPN Formal Modeling for EIBsec Protocol
Figure 6 is a top-level CPN model built based on the message flow of the EIBsec protocol. This model generally describes the process of key distribution and identity authentication in the protocol. The top-level model consists of Entity A, which which initiates the request; ACU, which is responsible for key distribution, and Entity B. The entire interaction process of the protocol is visually simulated; the double matrix represents the existence of underlying substitution transitions, which respectively represent Entity A, ACU, and Entity B. A single matrix in an alternative transition represents a transition that is used to encrypt, decrypt, and calculate messages during a session, The ellipse represents a place which is used to store messages during the session construction process. The line segment with an arrow represents the message delivery direction. Its main function is to pass the message to the corresponding entity for processing. Overall, the top-level model contains a total of three transitions and eight message locations.
Figure 7 shows the internal CPN model of entity A’s substitution transition. Firstly, Entity A sends a session key request nnaa message to the key distribution server ACU through the message store place S1. The message nnaa is composed of random numbers NA, N1, addra, and addrb. Place S5 receives the MSGA message sent by the key server ACU. The MSGA message is encrypted by ka, decrypted at the transition DmsgA to obtain the session key kab, and stored in the kab place. Transition Auth combines the session key kab and the random number N3 into an AUTH1 identity authentication request message, sends it to the S6 message storage place, and sends it to entity B through the S6 place.
The S7 place receives the identity authentication AUTH2 message from entity B. AUTH2 is composed of the composite random number nn and the session key kab. The composite random number nn is split through the transition Denn to obtain N3’ calculated by entity B, and temporarily store N3’ in the N3’ place. Next, verification and calculation of N3’ is carried out through transition verification to obtain the restored N3. Comparing N3’ and N3 in transition comparison. If the expectations are met, the identity of entity B is verified and the random number N4 is output. The random number comes from entity B. Subsequently, the identity authentication of entity A is performed, and the random number n4 is subtracted by one through the transition convertN4 to obtain N4’.Transition encry uses the session key kab to encrypt the message containing the random number N4’ to obtain the identity authentication message AUTH3, and sends AUTH3 to entity B through place S8 to verify the identity of entity A.
Figure 8 shows the internal CPN model of the key distribution server ACU substitution transition. After receiving the request message from entity A through the S1 place, AUC splits the message NNAA according to the splitting principle and learns the entity object that entity A wants to establish a session connection. Subsequently, the ACU combines the request message (addra, NB) through the transition AICR. This message is composed of addra and the random number NB, and NB is generated by the ACU.
Place S3 receives the response message KN from entity B, which is a combination of kb and N2. At this time, ACU obtains the keys ka and kb generated by entity A and entity B, respectively. Finally, MSGA and MSGB are sent to Entity A and Entity B, respectively, through output places S4 and S5. Both messages contain the session key kab and carry random numbers NB and NA, respectively. At the same time, the messages are encrypted and transmitted using the keys ka and kb generated by each.
Figure 9 describes the internal CPN model of the substitution transition entity B. After receiving the request message sent by the ACU through S2, entity B learns the entity object that wants to establish a session connection. Entity B receives the MSGB message through S4, the transition DMSGB to use the key kb to decrypt, and it obtains the session key kab and the random number N2 generated by itself. If N2 is met as expected, it means that the session key is obtained by the expected key server distribution.
After entity B obtains the session key, it performs mutual identity authentication between entities. S6 receives the message encrypted by the session key and contains the random number n3. The transition auth uses the session key kab to decrypt the message. After the transition n3’ obtains n3, it calculates n3’ according to the action(n3-1) function. Transition N3N4 combines n3’ and n4, and the combined message nn is encrypted using the session key kab through transition AUTH2 to obtain the AUTH2 message. At the same time, it is sent to entity A by S7. S8 receives the AUTH3 message, DeAUTH3 uses the session key to decrypt it, obtaining n4’ and storing it in the n4’ place, and transition verify verifies and calculates n4. The transition compare compares n4 and n4’. If they are equal, it proves that the identity of entity A is legal. Otherwise, the session establishment process ends, and the identity of entity A is not trustworthy.
5. New Scheme of EIBsec Protocol
After passing the EIBsec protocol modeling evaluation in
Section 4, it is found that there is no spoofing attack in the protocol itself. However, since the message is transmitted in plain text when sending the request and there is no time limit on the request and response of the message, there are tampering attacks and replay attack vulnerabilities in the original protocol. The improvement plan given in this article is: when entity A sends a request, it uses the parameters in the request message as the input of the hash function to calculate a hash value recorded as hash1, and sends the hash value together with the plaintext request message to the key distribution Server ACU. When ACU receives the request message, it uses the same hash function, uses the parameters in the request message to enter the hash function, and then calculates a new hash value recorded as hash2. Hash2 is compared with hash1 in the request message. In addition, considering the operation delay of transition in the model and the maximum time for normal message transmission, we added a timestamp based on the original protocol, which is in line with the idea of our design plan. In the CPN model, the timestamp is carried out at each stage of the message interaction process between entity A, ACU, and entity B, and a time upper limit threshold is set.
If the attacker tampers with the message, the generated hash value is different from hash1 in the original message, then the hash comparison fails in the ACU, the key request message is discarded, and the session establishment is interrupted. If the attacker simply intercepts the message and then replays it, the process will generate more time overhead, and the timestamp will exceed the upper time threshold. This chapter will conduct CPN modeling of the new scheme and use the same security assessment model to verify the effectiveness of the new scheme.
5.1. Protocol Improvement Scheme
Figure 12 is the message flow chart of the improvement scheme. The entire message flow process in the new scheme is also divided into two stages: distribution of session keys and identity authentication between communicating entities.
The message interaction process of the improved new scheme protocol is as follows:
Phase One: Key Distribution
Step 1: Entity A initiates a session key request message to the corresponding key distribution server ACU. The message contains the random number N1, NA, AddrA, and the address AddrB of the entity object that entity A wants to establish a session connection. At the same time, the data in the request message are used as a parameter to calculate a hash value recorded as hash1, the hash1 value is carried in the request message, and a timestamp is added when sending the message.
Step 2: After the corresponding ACU receives the session key request message, it obtains hash1 from the request message and uses the same method to calculate a new hash value recorded as hash2. Hash1 is compared with hash2. If the hash values are the same, the operation is followed up; otherwise, entity A’s request is rejected. At the same time, ACU sets the timestamp threshold to determine whether the time spent by entity A in sending the request message has timed out.
Step 3: After entity B receives the instruction from ACU, it obtains the request parameters, uses the parameters in the request message to calculate a hash value, and then compares it with the hash value in the instruction. If the hash values are the same, it sends an encrypted message to ACU. Otherwise, the instruction from the ACU is discarded. At the same time, the timestamp threshold is set, and it is verified whether the timestamp times out and include the timestamp when sending messages to the ACU.
Step 4: After receiving the message sent by entity B, ACU decrypts the message, and then responds to entity A and entity B each with a message containing the session key. The message responding to entity A contains the session key KSB_AB, entity B’s random number NB, and timestamp. KA is used to encrypt the message containing KSB_AB and NB. The message responding to entity B contains the session key KSB_AB, entity A’s random number NA, and timestamp. KB is used to encrypt the message containing KSB_AB and NA. After this step is completed, it means that ACU completes key distribution, and then entity A and entity B perform identity authentication.
Phase 2: Identity Authentication
Step 5: Entity A and Entity B use KA and KB, respectively, to decrypt the key response message from the ACU and obtain the session key KSB_AB. At the same time, entity A obtains the random number NB, and entity B obtains the random number NA. Entity A and Entity B verify the time threshold. Entity A initiates an identity authentication connection request to entity B. The request contains a new random number N3, uses the session key KSB_AB to encrypt the request message, timestamps it, and then sends it to entity B.
Step 6: Entity B receives the request message, uses the session key to decrypt it, and obtains the random number N3 and timestamp information. At the same time, the random number N3’ is calculated through the action() function, and the timestamp is verified. Then, N3’ is combined with the new random number N4 to form an A_Auth_Connect_Reply message, which is encrypted using KSB_AB, timestamp information is added, and the encrypted message with the timestamp is sent to entity A.
Step 7: After receiving the response message from entity B, entity A decrypts and obtains random numbers N3’ and N4. Entity A uses the action() function to restore N3 (N3’ + 1) and compares it with the N3 carried when requesting from entity A. If the two are equal, subsequent authentication will be performed. At the same time, N4’ is calculated, and the message containing N4’ is encrypted using the session key KSB_AB, and the timestamp information is carried together to form an A_Auth_Connect_Response message, which is responded to Entity B. After entity B receives the message, it decrypts the message and obtains N4’, then restores N4 according to the agreed calculation rules, compares N4 and N4’ (N4 = N4’) and verifies whether the timestamp exceeds the set time threshold. If it meets As expected, the session between Entity A and Entity B is successfully established.
5.2. New Scheme Model of EIBsec Protocol
The improved EIBsec protocol also consists of three parts: entity A, ACU, and entity B. The new scheme adds hash verification and timestamp judgment into the original protocol to strengthen the security mechanism of the protocol. In this section, we use the CPN Tools tool to model and analyze the new scheme. In
Section 5.3, we use the same security assessment model to verify the security of our new and improved scheme. The new scheme CPN model is mainly divided into the top-level model and bottom-level model. The top-level model is consistent with the top-level model of the original protocol, so this section only shows the underlying CPN model. The underlying model describes the key distribution and identity authentication process of the protocol message flow in the new scheme in more detail.
The first CPN mathematical model expression of the modified original protocol:
colset AddrA = string; colset AddrB = string; closet T = int; colset HASH = string;
val prdelay = 3; val trdelay = 6;
Place set P = AddrA, NA, AddrB, N1, config, S1, Initial time, hash;
Transition set T = ASR, mes, Hnnaat;
Directed arc set A = AddrA→ASR; NA→ASR; AddrB→ASR;N1→ASR;
Initial time→ASR; HASH→ASR; ASR→config; config→mes;
mes→hnnaat; hnnaat→Hnnaat; Hnnaat→S1
AddrB→ASR:(AddrB,ASR); N1→ASR:(N1,ASR); t→ASR:(t,ASR);
hash1→ASR:(hash1,ASR); ASR→config:(ASR,config);
config→mes:(config, mes); mes→hnnaat:(mes, hnnaat);
hnnaat→Hnnaat:(hnnaat, Hnnaat); Hnnaat→S1: (Hnnaat, S1);
N1:WHIT; config; NNAA;
S1:NNAA; T:int; HASH:STRING; prdelay, trdelay:VAL;
addrb→ASR:addrb; N1→ ASR:N1; t→ASR:t; hash1→ASR:hash1;
ASR→config:addra, NA, addrb, N1, t + prdelay + trdelay, hash1;
config→mes:config; mes→hnnaat:cmes;
hnnaat→Hnnaat:hnnaat; Hnnaat→S1:Hnnaat;
hash1:hash1; config, hnnaat, S1:NULL;
Figure 13 shows the underlying CPN model of the improved entity A. In the original protocol, we introduced timestamp and hash. The initial time of the timestamp is 0, and the hash value hash1 is obtained through the hash function. In practical applications, SHA-1 and MD5 can be selected to calculate hash values using the hash function. Place S1 sends message hNNaat to ACU. The message hNNaat is composed of (hash1, N1, NA, addra, addrb, t). Among them, hash1 is used to ensure the integrity of the message, and timestamp is used to ensure the freshness of the message. Place S5 receives the message {k = ka, m = msga} from the ACU, and uses [t <= 9] at the transition Msga to verify whether the timestamp has timed out. If the timestamp has not timed out, it means that the message has not been tampered with or repeated. The distribution of session key kab is completed. Place S6 sends a message ((kab, n3), t) to entity B. The session key kab encrypts the content to be sent and the random number n3 and adds a new timestamp to the encrypted message. Place S7 receives the message {k = kab, n = nn} from entity B, decrypts it at transition DeAUTH2, and verifies whether the message has timed out through the preset timestamp threshold of [t <= 45] at transition Denn. Message ((kab, n4’), t) is sent to entity B through place S8. n4’ = n4-1 in the message is calculated through the action(n4-1) function in the transition convertN4, using the session key kab, the message content and random number N4’ are encrypted, and a new timestamp is added to the encrypted message. In the new scheme, each message will carry a timestamp.
Figure 14 depicts the underlying CPN model of the improved ACU. ACU receives the hNNaat message through the input place S1, decomposes it at the transition DeASR, and obtains the request message parameters. Using (N1, NA, addra, addrb) as the input of the hash function to recalculate the hash value at the transition CalculateHash and storing the calculation result in hash2, the hash value is calculated at the transition compareHash. If hash1 is not equal to hash2, it means that the message has been tampered with. At this time, the key distribution server ACU discards the request message packet and interrupts the session establishment. On the contrary, place S2 will send the message (hash1, NB, addra, t) to entity B. Place S3 receives the response message (N2, kb, t) from entity B, and ACU verifies whether the timestamp message times out at the transition DeAICRes. Subsequently, the key distribution server ACU sends messages msGA and msGB to entity A and entity B, respectively. Both messages contain the session key communicated by entity A and entity B and the random number of the other party, and the message package carries a timestamp.
Figure 15 describes the underlying CPN model of the improved entity B. The input place S2 receives the message (hash1, NB, addra, t), verifies the timestamp information at the transition DNA1, transition CalculateHash to recalculate the hash, and stores the calculation result in the variable hash3. Transition CompareHASH compares hash1 and hash3 and output place S3 to send a message ((kb, N2), t) to ACU. The input place S4 receives the {m = msgb, k = kb, t1 = t} message, verifies the timestamp information at the transition DMSGB, and entity B obtains the session key kab in the message msgb. Place S6 receives the identity authentication request message ((kab, n3), t) from entity A. Using the session key kab previously distributed by ACU in the transition DeAuth, it decrypts the authentication message and verifies the timestamp. Place S7 sends {k = kab, n = nn} message to entity A. In the message, nn = (n3’, n4, t + prdelay + trdelay), n3’ = action(n3-1), and kab is used to Encrypt the message. Finally, it is sent with a timestamp to entity A. Place S8 receives the message ((kab, n4’), t), verifies whether the timestamp has timed out according to the upper time threshold [t <= 54] at transition DeAUTH3, and decrypts it to obtain n4’. At the transition verify, n4 is restored according to n4 = action(n4’ + 1). At the transition compareN4, according to [n4 = n4’], it is judged whether the random number has been tampered with. If they are equal, it means that the session between Entity A and Entity B has been successfully established.