A Light and Anonymous Three-Factor Authentication Protocol for Wireless Sensor Networks

Recently, wireless sensor networks (WSNs) have been widely used in a variety of fields, and make people’s lives more convenient and efficient. However, WSNs are usually deployed in a harsh and insecure environment. Furthermore, sensors with limited hardware resources have a low capacity for data processing and communication. For these reasons, research on efficient and secure real-time authentication and key agreement protocols based on the characteristics of WSNs has gradually attracted the attention of academics. Although many schemes have been proposed, most of them cannot achieve all known security features with satisfactory performance, among which anonymity, N-Factor security, and forward secrecy are the most vulnerable. In order to solve these shortcomings, we propose a new lightweight and anonymous three-factor authentication scheme based on symmetric cryptographic primitives for WSNs. By using the automated security verification tool ProVerif, BAN-logic verification, and an informal security analysis, we prove that our proposed scheme is secure and realizes all known security features in WSNs. Moreover, we show that our proposed scheme is practical and efficient through the comparison of security features and performance.

Study on Model-Based Systems Engineering Method for Modeling of Thermal Power System

Thermal power systems, particularly with large capacity and high operating parameters, are more and more complicated nowadays, which include machinery, electronics, electrical, hydraulic, thermal, control, and process-oriented subsystems. The traditional development method based on documents has the problems of difficulty to reuse the designed elements, weak traceability of requirements, and lack of top-level logic verification. Moreover, there is a large gap because different models, tools and terminology are used during design process. The gap results in inefficiencies and quality issues that can be very expensive. In this paper, a model-based systems engineering (MBSE) approach is introduced for the top-down design flow of thermal power systems. The MBSE method can perfected the requirement definition, complete the mapping of the requirements to the system elements, realize the function logic verification, and support requirements verification at all stages. A GOPPRR (graph, object, point, property, role, relationship) meta-modeling method is proposed to support the MBSE formalisms. An Architecture Analysis and Design Integrated Approach (Arcadia) framework is adopted to capture the complex architecture, which is a standardized modeling method including requirement analysis, function analysis, logic analysis, and architecture design. Based on the architecture-driven algorithm and code generation, the standardized modeling process can establish a traceable relationship at each design stage and can verify the availability of initial requirements. Moreover, the designed elements of previous work can be reused in other relative design processes. The proposed MBSE method in this paper is applied to establish a gas turbine performance simulation model. The entire modeling process is enhanced by managing the relative design information consistently. The performance of the design process with MBSE method is analyzed and compared from different aspects. The results show that the performance simulation model of the power system established by the MBSE method can effectively describe the requirements, functions, logic, and architecture during design process. Based on the MBSE method, the requirements of the system are refined, traced and verified.

Trustworthiness and a Zero Leakage OTMP-P2L Scheme Based on NP Problems for Edge Security Access

Resource constraints have prevented comprehensive cryptography and multifactor authentication in numerous Internet of Things (IoT) connectivity scenarios. Existing IoT systems generally adopt lightweight security protocols that lead to compromise and privacy leakage. Edge computing enables better access control and privacy protection, furthermore, blockchain architecture has achieved a trusted store of value by open-source and distributed consensus mechanisms. To embrace these new paradigms, we propose a scheme that employs one-time association multitasking proofs for peer to local authentication (OTMP-P2L). The scheme chooses relevant nondeterministic polynomial (NP) problem tasks, and manages localized trust and anonymity by using smart devices such as phones and pads, thereby enabling IoT devices to autonomously perform consensus validation with an enhanced message authentication code. This nested code is a one-time zero-knowledge proof that comprises multiple logic verification arguments. To increase diversity and reduce the workload of each one, these arguments are chained by a method that establishes some of the inputs of the following task from the output of previous tasks. We implemented a smart lock system and confirmed that the scheme outperforms IoT authentication methods. The result demonstrates superior flexibility through dynamic difficulty strategies and succinct non-interactive peer-to-peer (P2P) verification.

Least General Generalizations in Description Logic: Verification and Existence

We study two forms of least general generalizations in description logic, the least common subsumer (LCS) and most specific concept (MSC). While the LCS generalizes from examples that take the form of concepts, the MSC generalizes from individuals in data. Our focus is on the complexity of existence and verification, the latter meaning to decide whether a candidate concept is the LCS or MSC. We consider cases with and without a background TBox and a target signature. Our results range from coNP-complete for LCS and MSC verification in the description logic εℒ without TBoxes to undecidability of LCS and MSC verification and existence in εℒI with TBoxes. To obtain results in the presence of a TBox, we establish a close link between the problems studied in this paper and concept learning from positive and negative examples. We also give a way to regain decidability in εℒI with TBoxes and study single example MSC as a special case.