Model Learning and Model Checking of IPSec Implementations for Internet of Things

With the development of Internet of Things (IoT) technology, the demand for secure communication by smart devices has dramatically increased, and the security of the IoT protocol has become the focus of cyberspace. Recently, some scholars have attempted to extend the IPSec protocol to IPv6 over Low-Power Wireless Personal Area Networks (6LoWPAN) to ensure end-to-end security, which makes it essential to analyze the vulnerability of the IPSec protocol to enhance the security of the IoT. In this study, we use a method combining model learning and model checking to analyze the dynamic vulnerability of IPSec protocol implementations. This method automatically infers the black-box model and compares it with the relevant specifications to expose the defects of the system implementation and search its logic vulnerabilities. We first employ model learning on three IPSec implementations to infer state machine models; then, we use model checking to verify that these models satisfy basic security properties and conform to the RFCs. Our analysis reveals three new security issues: a wrong interaction causing server exception and two violations of the standard.