Virtual private networks (VPNs) are widely used to create a secure communication mode between multiple parties over an insecure channel. A common use case for VPNs is secure access to company networks. Therefore, bugs in VPN software are often severe. The Internet Key Exchange protocol (IKE) is a protocol in the Internet Protocol Security (IPsec) protocol suite used in VPNs. There are two version of IKE, IPsec-IKEv1 and the newer IPsec-IKEv2, with IPsec-IKEv1 still widely used in practice. While IPsec-IKEv2 has been investigated in the context of automata learning, no such work exists for IPsec-IKEv1. This paper closes the gap for the IPsec-IKEv1 protocol and shows the steps taken to learn a digital twin of an IPsec server using automata learning. We present and contrast two learned models of an IPsec server. Using learning, we also found security issues in encryption libraries.
the system to gain knowledge about it. In this way, not only a model is created, but also a stateful testing approach for black-box systems. The learned model represents a digital twin of the system under learning, which can then be used for other model-based techniques, like model-based test-case generation or model checking.
In this paper, we investigate the applicability of automata learning for mining security-critical components of a VPN. For this, we learn the behavioral model of the Internet Key Exchange protocol (IKE) protocol which is part of the Internet Protocol Security (IPsec) protocol suite. IKE is used to share authenticated key material between the involved parties. For learning, we use a VPN client to query the VPN server instantiation. This allows us to create a digital twin of the security-critical part of a VPN server without knowing its internals (black-box). The work is part of LearnTwins, a research project on learning digital twins1.
The paper is organized as follows. Sect. 2 provides details about the used modeling-formalism, the learning algorithm, and the system-under-learning. Section 3 provides a comparison with related work. In Sect. 4, we present our learning setup for mining a digital twin of a VPN. In Sect. 5 we present our learned models and, finally, in Sect. 6 we draw our conclusions.
Mealy machines are a modeling formalism for reactive systems such as communication protocols. They are finite-state machines in which each transition is labeled with an input and the corresponding output action. We consider Mealy machines to describe deterministic behavior. More formally, a Mealy machine is defined as a 6-tuple = {, 0, , , , }, where is a finite set of states, 0 ∈ is the initial state, is a finite set called input alphabet, is a ifnite set called output alphabet, is the state-transition function : × → that maps a state and an element of the input alphabet to another state in and is the output function : × → that maps a state-input pair to an output in .
Automata learning algorithms generate a model that describes the behavior of the system under learning (SUL). We diferentiate between active and passive automata learning. Passive learning creates a behavioral model based on a given data set, e.g., log files, while active learning directly queries the SUL. For learning a digital twin, we prefer active learning since active algorithms can query unusual or rare scenarios, whereas passive learning depends heavily on the provided data.
Today, many active learning algorithms are based on concepts derived from Angluin’s *
algorithm [
The MAT concept is also used by other active learning algorithms. Kearns and Vazirani [
Internet Protocol Security (IPsec) is a VPN Layer 3 Initiator Responder
protocol suite used to securely communicate over an ISAKMP SA {proposals}
insecure channel. It includes three sub-protocols:
Internet Key Exchange protocol (IKE), the Authentica- ISAKMP SA {proposal} M
tion Header (AH), and the Encapsulating Security Pay- KEY EX {, } ian
lckoaeatyidos.n(E,IKSaPnE)dhptarhosettoswceoocul.vrIeeKresExiocisnhsma,naIgKienElavyn1udasmenddanfIoKargEaevmu2t,ehnwetnitothif- KEY EAXU{TH{ℎ,ℎ}} eodM
IKEv2 being the newer and recommended version [
Compared to other protocols, IPsec ofers a high de- Figure 1: IKEv1 between two parties
gree of customizability, allowing it to be fitted for many
use cases. However, in a cryptographic evaluation of the protocol, Ferguson and Schneier [
The IKEv1 protocol works in two main phases, both relying on the Internet Security Association and Key Management Protocol (ISAKMP). A typical key exchange between two parties, an initiator and a responder, can be seen in Fig. 1. In phase one (Main Mode), the initiator sends a Security Association (SA) to the responder. A SA essentially details important security attributes for a connection such as the encryption algorithm and key-size to use, as well as the authentication method and the used hashing algorithm.
These options are bundled in containers called proposals, with each proposal describing a possible security configuration. While the initiator can send multiple proposals to give the responder more options to choose from. In comparison, the responder must answer with only one proposal, provided it supports one of the suggestions. Subsequently, the two parties perform a Difie-Hellman key exchange and exchange nonces to generate a shared secret key. This secret key is used as a seed key for all further session keys. Following a successful key exchange, all further messages are encrypted. Finally, both parties exchange hashed authentication material (usually pre-shared keys or certificates). If the hashes can be verified, a secure channel is created and used for phase two communication.
The shorter phase two (Quick Mode) begins with another SA exchange. This time, however, the SA describes the security parameters of the ensuing ESP/AH communication. This is followed by a single acknowledge message from the initiator to confirm the agreed upon proposal. After the acknowledgment, all further communication is done via ESP/AH packets.
Model learning became a popular tool for creating behavioral models of various communication
protocols, e.g., TLS [
Environment Setup. As our SUL, we used a Linux Strongswan2 US.9.5/K5.15.0-25-generic. Learning was done using two VirtualBox 6.1 virtual machines (VMs) running standard Ubuntu 22.04 LTS distributions. Both VMs were allotted 4 GB of memory and one CPU core. All communication took place in an isolated virtual network to eliminate external influences. During learning, all power-saving options and similar potential causes of disruptions were disabled. The IPsec server was restarted before the start of each learning procedure to ensure identical conditions. We designated one VM as the initiator and one as the responder to create a typical client-server setup. The open-source IPsec implementation was installed on the responder VM and set to listen for incoming connections from the initiator VM. The Strongswan server was configured to use pre-shared keys for authentication and default recommended
abstract input abstract output
concrete input concrete output
(Initiator)
UDP
SUL
(Responder)
security settings. Additionally, it was set up to allow unencrypted notification messages, which
we used to reset the connection during the learning process. For learning, we used the Python
library AALpy [
Learning Setup. Figure 2 gives an overview of the learning setup, adapted from Tappler
et al. [
The abstract inputs consist of the initiator-to-responder messages: isakmp_sa, key_ex, auth,
ipsec_sa and ack. The responder-to-initiator outputs from Fig. 1 were extended by NONE
and ERROR, where NONE signifies a lack of response from the SUL and ERROR is used as a
collection of received error notifications. We use the KV [
Our mapper implements translation methods for each communication step in a typical
IPsecIKEv1 exchange, as described in Sect. 2. We use the Python library Scapy to construct IKEv1
packets. This approach allows us to change the fields and values of generated packets at will,
opening up the possibility of fuzz testing these fields in future work as shown by Pferscher and
Aichernig [
The IPsec packets generated by the mapper are then passed on to our interface for the SUL that handles all incoming and outgoing UDP packets. Additionally, it converts responses from the SUL into valid Scapy packets and passes them on to the mapper. The mapper class then parses the responses received from the interface and returns an abstract output representing the received data to the learning algorithm. Since part of communication is encrypted, we require a framework that correctly handles the en/decryption of messages. For each request, we store the base key and the responses for use in the next message, and update afected key material as needed. Most notably, the initialization vectors (IVs) are updated in almost every request and difer between messages. Informational requests also handle their IVs separately. For each request that we send, if available, we try to parse the response, decrypting it if necessary and resetting or adjusting internal variables as required to match the server.
Automata learning requires that the SUL can be reset to an initial state after each query. We implement this using a combination of the ISAKMP delete request and general ISAKMP informational error messages. While delete works for established connections in phase two of IKE, we require informational error messages to trigger a reset in phase one. Implementation was hindered at times by unclear RFC specifications, but this was overcome by manually comparing packet dumps and Strongswan logs to fix encryption errors.
Combating Non-determinism. During learning, the server occasionally exhibited nondeterministic behavior. For this, we implemented two methods of counteracting it. In our first method, we simply repeat the output query if we observe non-deterministic behavior. In this case, we select the output that occurs most often. Additionally, using timed waits after each input also helped to further decrease the number of non-determinism errors. However, learning still failed occasionally with these mitigation mechanisms for non-deterministic behavior.
A closer examination of the remaining non-deterministic behavior led to the discovery that it is caused by so-called retransmissions. Essentially, the IKE specification allows for previous messages to be retransmitted if deemed useful by the server. A possible trigger could be the ifnal message of an IKE exchange being skipped/lost. For example, if instead of an AUTH message, the server receives a phase two IPSEC SA message, the server would not know if it missed a message or if there was an error on the other party’s side. In this case, the Strongswan server reacts by retransmitting the previous message, prior to the missing one in an attempt to signal to the other party, that they should resend the missing message. To counteract this behavior, we implemented checks in our mapper to allow for the ignoring of retransmissions. If a repeated message ID is found, it is flagged as a retransmission. With this addition, the IPsec server behaved deterministically. The downside of this method is that it completely ignores the retransmissions, which could be a good source of information for fingerprinting diferent IPsec servers.
In our evaluation, we used two diferent learning setups to learn a model of the Linux Strongswan
server. The first setup considers retransmitted messages from the server as outputs, whereas the
second setup filters out any retransmitted messages. We included the model with retransmitted
messages in the Appendix A, see Fig. 4. The model without retransmission is shown in Fig. 3.
To enhance the readability of the models, we simplified the depicted models. The complete
models are available as supplementary material [
For learning the models, we compared the active automata learning algorithms: * and KV.
Both algorithms use an improved counterexample processing following Rivest and Schapire [
s2 auth/ AUTH s3 +/NONE isakmp_sa/ s1
key_ex/ +/NONE KEY_EX isakmp_sa/
ipsec_sa/
+/NONE ack/NONE isakmp_sa/ISAKMP_SA ack/ERROR ipsec_sa/
s4 s5 model with retransmission (Fig. 4) has 13 states, whereas the model without retransmissions (Fig. 3) has only six states. For readability, we group together several diferent error messages in the output ERROR. The models also include NONE responses, which were used in cases where the input misses sensible information to establish an encrypted communication. While observing the behavior of the server when exposed to completely non-sensible input is interesting from a security testing standpoint, as all specifications state that the encryption requires a prior keying procedure, we decided to ignore those few cases. However, for future work in the field of fuzzing, these edge-cases should be considered as well.
We state the learning results of learning without retransmissions, since learning was more reliable in this case. We repeated each experiment five times and averaged the results. KV required approximately 38 minutes (2296 seconds) to learn, 79 output queries and 60 conformance tests were performed in 753 and 991 steps respectively. Learning performed four equivalences queries. The learning results for the other model can be found in the Appendix A.
Examining both models, especially Fig. 4, we can clearly see the separation between the two phases of the IKEv1 protocol. Phase one (Main Mode) completes in state 3, and phase two (Quick Mode) begins right thereafter in state 4. Comparing the models, we see that for the states 0 to 3 both models are identical. This is likely due to the fact, that most diferences were caused by retransmissions which only occur in phase two. The model depicted in Fig. 3 shows streamlined behavior that fits our reference IKE exchange (see Fig. 1) almost perfectly. The clean automaton makes it easy to see, that after a connection has been established, we can still create new connections or restablish existing ones by sending another IPSEC SA message and then acknowledging the response.
The synthesis of a digital twin from the Linux Strongswan server not only provides interesting insight into the behavioral aspects of the implementation, especially regarding unexpected retransmitted messages. It also helped to test the general environment that is used to establish a VPN. A notable finding was the discovery of a very niche bug in a used Python Difie-Hellman (DH) key exchange library3. The bug was very elusive and only found thanks to the exhaustive number of packets sent by the learning algorithm. It turns out there was a very niche bug in the library where, if the most significant byte (MSB) was a zero, it would be omitted from the response, causing the local result to be one byte shorter than the value calculated by the SUL. Regardless, it could compromise the security of afected systems and therefore the maintainer 3https://github.com/TOPDapp/py-difie-hellman of the library has been notified of the problem. Due to the elusive nature of this bug, it would very likely not have been noticed without the exhaustive communication done by the model learning process and without seeing the resulting non-deterministic behavior of the SUL due to the truncated message.
Summary. We presented an automata learning framework that automates the generation of a digital twin of a VPN server. More precisely, the learned digital twin represents a behavioral model of the security-critical key-exchange procedure. We established a learning interface that enables active interaction with a VPN server. We found that the investigated VPN server occasionally retransmits previously sent messages, which violated our assumption about deterministic behavior. To deal with this problem, we adapted the learning interface to filter these retransmitted messages. With this adaption, we could reliably mine a new digital twin within less than one hour.
Discussion. Digital twins should adequately simulate the behavior of their twinned systems. When mining digital twins this property becomes critical. Compared to passive automata learning that simply uses given data, active approaches enforce checking behavioral conformance by testing for behavioral equivalence. Even though this equivalence check is limited by the exhaustiveness of the applied model-based testing technique, we can at least state that the system conforms according to the test suite. However, applying active learning techniques requires the establishment of an interface that enables the interaction with the SUL. Albeit creating a learning interface for a VPN server was not straightforward, the interface has to be created only once.
This paper presented a methodology for learning digital twins of software components. Even though the twinned system does not represent a physical twin in the classical sense, digital twins of software systems still have many application areas. First, the learned behavioral model creates a common understanding of the system. This can be especially useful if access to the twinned system is limited, e.g., third-party components. Secondly, the model can be used for further testing and verification purposes. In our case study, already the learning procedure of the digital twin revealed security issues in the libraries used to establish a secure VPN. Finally, the twin models can be used to simulate VPN components in a network infrastructure. This can be useful if we want to simulate diferences in behavior between distinct VPN servers. Instead of setting up each VPN server individually, the mined models can be used.
Future Work. In this paper, we discussed how digital twins can be automatically learned from a black-box system. In future work, we intend to use the digital twin to simulate behavior of the twinned system so that components in the network can be replaced by their twin model. In addition, we want to use the twin for model-based verification and testing purposes like stateful fuzz testing or model checking.
This work is supported by the LearnTwins project funded by FFG (Österreichische Forschungsförderungsgesellschaft) under grant 880852, and the “University SAL Labs” initiative of Silicon Austria Labs (SAL) and its Austrian partner universities for applied fundamental research for electronic based systems.
sa_main/INVALID-PAYLOAD-TYPE key_ex_main/INVALID-PAYLOAD-TYPE authenticate/ISAKMP_AUTH sa_quick/IPSEC_SA sa_main/None authenticate/None
sa_quick/IPSEC_SA key_ex_main/IPSEC_SA authenticate/IPSEC_SA authenticate/IPSEC_SA
sa_main/IPSEC_SA key_ex_main/IPSEC_SA ack_quick/None