As a critical component of the security architecture of 5G network, the authentication protocol plays a role of the first safeguard in ensuring the communication security, such as the confidentiality of user data. EAP-TLS is one of such protocols being defined in the 5G standards to provide key services in the specific IoT circumstances. This protocol is currently under the process of standardization, and it is vital to guarantee that the standardized protocol is free from any design flaws, which may result in severe vulnerabilities and serious consequences when implemented in real systems. However, it is still unclear whether the proposed 5G EAP-TLS authentication protocol provides the claimed security guarantees. To fill this gap, we present in this work a comprehensive formal analysis of the security related properties of the 5G EAP-TLS authentication protocol based on the symbolic model checking approach. Specifically, we build the first formal model of the 5G EAP-TLS authentication protocol in the applied pi calculus, and perform an automated security analysis of the formal protocol model by using the ProVerif model checker. Our analysis results show that there are some subtle flaws in the current protocol design that may compromise the claimed security objectives. To this end, we also propose and verify a possible fix that is able to mitigate these flaws. To the best of our knowledge, this is the first thorough formal analysis of the 5G EAP-TLS authentication protocol.

Online sequential extreme learning machine (OS-ELM) and its variants provide a promising way to solve data stream problems, but most of them do not take the timeliness of the problems into account, which may degrade the performance of the model. The main reason is that these algorithms are unable to adapt to the latest data accordingly when the distribution of the data stream changes. To mitigate this limitation, the forgetting factor is introduced into the relevant models, which is used to balance the relative importance of past data and new data when necessary. However, there is no efficient way to set the forgetting factor properly so far. In this paper, we have developed a novel updating strategy for setting the forgetting factor and proposed a dynamic forgetting factor based OS-ELM algorithm (DOS-ELM). In the sequential learning phase of DOS-ELM, the forgetting factor can be adjusted dynamically according to the change degree of the model accuracy in each learning epoch. This updating process does not require setting any parameters artificially and thus greatly improves the flexibility of the model. The experimental results on ten classification problems, five regression problems, one time-series problem show that DOS-ELM can deal well with both stationary and non-stationary data stream problems. In addition, we have extended DOS-ELM to an online deep model named ML-DOS-ELM, which can handle more complex tasks such as the face recognition problem and the handwritten digit recognition problem. Our experimental evaluations show that both DOS-ELM and ML-DOS-ELM can achieve higher prediction accuracy compared to the other similar algorithms.

Time sensitive networking (TSN) is an emerging technology for in-vehicle networks, which has strict timing constraints and dependability requirements. The performance and efficiency of TSN depend on a reliable scheduling mechanism for real-time communications. Traditionally, the TSN scheduler is analyzed using simulations and testing, which are error-prone and inaccurate. In this article, we employ a timed model checker UPPAAL to formally model and analyze the TSN scheduler with a consideration of its transmission latency and time utilization. We first use the build-in assertion in UPPAAL to verify the deadlock-free property, safety property, and starvation-free property of our model. Then, we calculate the time utilization and the transmission delay of audio video bridging data frame under two scheduling mechanisms according to the simulation process. Then, we compared the time performance of this two scheduling mechanisms and found that each of them has their own advantages and disadvantages. This article provides a formal analysis framework for investigating scheduling strategies in TSN, which facilitates the designers to have a better understanding and development of TSN schedulers in the future.

This work presents a security analysis of the QUIC handshake protocol based on symbolic model checking. As a newly proposed secure transport protocol, the purpose of QUIC is to improve the transport performance of HTTPS traffic and enable rapid deployment and evolution of transport mechanisms. QUIC is currently in the IETF standardization process and will potentially carry a significant portion of Internet traffic in the emerging future. For a better understanding of the essential security properties, we have developed a formal model of the QUIC handshake protocol and perform a comprehensive formal security analysis by using two state-of-the-art model checking tools for cryptographic protocols, i.e., ProVeirf and Verifpal. Our analysis shows that ProVerif is generally more powerful than Verifpal in terms of verifying authentication properties. Moreover, both tools produce a counterexample to some security properties, which reveal a design flaw in the current protocol specification. Last but not least, we analyze the root causes of this counterexample and suggest a possible fix.

As a newly proposed secure transport protocol, QUIC aims to improve the transport performance of HTTPS traffic and enable rapid deployment and evolution of transport mechanisms. QUIC is currently in the IETF standardization process and will potentially carry a significant portion of Internet traffic in the emerging future. An important safety goal of QUIC protocol is to provide effective data service for users. To aim this safety requirement, we propose a formal analysis method to analyze the safety of QUIC handshake protocol by using model checker SPIN and cryptographic protocol verifier ProVerif. Our analysis shows the counterexamples to safety properties, which reveal a design flaw in the current protocol specification. To this end, we also propose and verify a possible fix that is able to mitigate these flaws.