Search Results (276)

This article introduces a new method for modelling and verifying the execution of timed security protocols (TSPs) and their time-dependent security properties. The method, which is novel and reliable, uses an extension of interpreted systems, accessible semantics in multi-agent systems, and timed interpreted systems (TISs) with dense time semantics to model TSP executions. We enhance the models of TSPs by incorporating delays and varying lifetimes to capture real-life aspects of protocol executions. To illustrate the method, we model a timed version of the Needham–Schroeder Public Key Authentication Protocol. We have also developed a new bounded model checking reachability algorithm for the proposed structures, based on Satisfiability Modulo Theories (SMTs), and implemented it within the tool. The method comprises a new procedure for modelling TSP executions, translating TSPs into TISs, and translating TISs’ reachability problem into the SMT problem. The paper also includes thorough experimental results for nine protocols modelled by TISs and discusses the findings in detail. Full article

Property-driven hardware verification provides a promising way to uncover design vulnerabilities. However, developing security properties that check for highly concealed security vulnerabilities remains a significant challenge. In this paper, we propose a scheme, called HT-PGFV, to implement hardware Trojan security property assertion automatic generation and formal security verification for Trojan-infected designs. In our scheme, we develop a hardware Trojan security property assertion generation method for automated hardware which can extract hardware Trojan security properties from Trojan-infected designs by performing the three main steps of Trojan-infected signal identification based on feature matching, influence-cone-analysis-based Trojan path identification, and information flow trace mining, and formulate them as SystemVerilog assertions. In addition, we develop a formal security verification method based on information flow analysis which can formally verify hardware Trojan security properties and detect hardware Trojans violating information flow security policies by checking the security of information flows via our developed RT-level hardware information flow security models. The proposed method is demonstrated on several Trojan benchmarks from Trust-Hub. Experimental results show that our scheme can generate hardware Trojan security property assertions for Trojan-infected designs and detect information leakage and functionality change hardware Trojans activated by external inputs or internal conditions. Full article

In software engineering, errors or faults in software systems often lead to critical social problems. One effective methodology to tackle this problem is model checking, which is an automated formal verification technique. In traditional model checking, the task of finding specification errors is reduced to deterministic search techniques such as Depth-First Search. Recent research has shown that swarm intelligence offers a powerful search capability compared to traditional techniques. In particular, multi-swarm Particle Swarm Optimization is known to be efficient and can mitigate the state-space explosion problem, i.e., the exponential increase in the search space with a linear increase in the problem size. However, the state-space explosion problem is still significant when verifying very large systems. Further performance improvement is needed. To achieve this, we propose a novel memoization or cache mechanism for storing tentative solutions for reuse in the later stages of the search procedure. For each stage, a candidate solution computed by a swarm is summarized efficiently and heuristically to consolidate similar solutions into a single representative solution. We store the summary and its associated solutions in key-value maps. Instead of computing known solutions repeatedly, we retrieve the solution if the stored key matches the summary. We incorporated the proposed mechanism into a model-checking technique with multi-swarm Particle Swarm Optimization and evaluated the search performance. We show in this paper that the proposed mechanism improved time and space consumption while maintaining solution quality. Full article

The rapid evolution of mobile and optical communication technologies is driving the transition from 5G to 6G networks. This transition inevitably brings about changes in authentication scenarios, as new security demands emerge that go beyond the capabilities of existing frameworks. Therefore, it is necessary to address these evolving requirements and the associated key challenges: ensuring Perfect Forward Secrecy (PFS) to protect communications even if long-term keys are compromised and integrating Post-Quantum Cryptography (PQC) techniques to defend against the threats posed by quantum computing. These are essential for both radio and optical communications, which are foundational elements of future 6G infrastructures. The DMRN Protocol, introduced in 2022, represents a major advancement by offering both PFS and PQC while maintaining compatibility with existing 3rd Generation Partnership Project (3GPP) standards. Given the looming quantum-era challenges, it is imperative to analyze the protocol’s security architecture through formal verification. Accordingly, we formally analyze the DMRN Protocol using SVO logic and ProVerif to assess its effectiveness in mitigating attack vectors, such as malicious or compromised serving networks (SNs) and home network (HN) masquerading. Our research found that the DMRN Protocol has vulnerabilities in key areas such as mutual authentication and key exchange. In light of these findings, our study provides critical insights into the design of secure and quantum-safe authentication protocols for the transition to 6G networks. Furthermore, by identifying the vulnerabilities in and discussing countermeasures to address the DMRN Protocol, this study lays the groundwork for the future standardization of secure 6G Authentication and Key Agreement protocols. Full article

With the rapid development of wireless communication and big data analysis technologies, the storage of massive amounts of data relies on third-party trusted storage, such as cloud storage. However, once data are stored on third-party servers, data owners lose physical control over their data, making it challenging to ensure data integrity and security. To address this issue, researchers have proposed integrity auditing mechanisms that allow for the auditing of data integrity on cloud servers without retrieving all the data. To further enhance the availability of data stored on cloud servers, multiple replicas of the original data are stored on the server. However, in existing multi-replica auditing schemes, there is a problem of server fraud, where the server does not actually store the corresponding data replicas. To tackle this issue, this paper presents a formal definition of authentic replicas along with a security model for the authentic-replica sampling mechanism. Based on time-lock puzzles, identity-based encryption (IBE) mechanisms, and succinct proof techniques, we design an authentic replica auditing mechanism. This mechanism ensures the authenticity of replicas and can resist outsourcing attacks and generation attacks. Additionally, our schemes replace the combination of random numbers and replica correspondence tables with Linear Feedback Shift Registers (LFSRs), optimizing the original client-side generation and uploading of replica parameters from being linearly related to the number of replicas to a constant level. Furthermore, our schemes allow for the public recovery of replica parameters, enabling any third party to verify the replicas through these parameters. As a result, the schemes achieve public verifiability and meet the efficiency requirements for authentic-replica sampling in multi-cloud environments. This makes our scheme more suitable for distributed storage environments. The experiments show that our scheme makes the time for generating copy parameters negligible while also greatly optimizing the time required for replica generation. As the amount of replica data increases, the time spent does not grow linearly. Due to the multi-party aggregation design, the verification time is also optimal. Compared to the latest schemes, the verification time is reduced by approximately 30%. Full article

Formal requirements modeling and traceability management are essential for effectively implementing Model-Based Systems Engineering (MBSE). However, few studies have explored the integration of requirement modeling, traceability management, and verification within MBSE-based systems engineering methodologies. Moreover, the predominant modeling language for MBSE, SysML, lacks sufficient capabilities for requirement description and traceability management and for depicting physical attributes and executable capabilities, making it challenging to verify functional and non-functional requirements collaboratively. This paper proposes an integrated approach for requirement modeling, traceability management, and verification, building on the previously proposed integrated modeling and the simulation language called X language. Our contributions primarily include defining the ReqXL specification for MBSE-oriented requirement modeling based on X language, proposing an algorithm for automatically generating requirement traces, and an integrated framework for requirements modeling, traceability management, and verification was developed by combining the X language with ReqXL. These functionalities were customized on the self-developed integrated modeling and simulation platform, XLab, which is specifically tailored for the X language. Furthermore, we showcase the efficacy and promise of our approach through a case study involving the design of an aircraft electrical system. Full article

Authenticated key exchange is desired in scenarios where two participants must exchange sensitive information over an untrusted channel but do not trust each other at the outset of the exchange. As a unique hardware-based random oracle, physical unclonable functions (PUFs) can embed cryptographic hardness and binding properties needed for a secure, interactive authentication system. In this paper, we propose a lightweight protocol, termed PUF-MAKE, to achieve bilateral mutual authentication between two untrusted parties with the help of a trusted server and secure physical devices. At the end of the protocol, both parties are authenticated and possess a shared session key that they can use to encrypt sensitive information over an untrusted channel. The PUF’s underlying entropy hardness characteristics and the key-encryption-key (KEK) primitive act as the root of trust in the protocol’s construction. Other salient properties include a lightweight construction with minimal information stored on each device, a key refresh mechanism to ensure a fresh key is used for every authentication, and robustness against a wide range of attacks. We evaluate the protocol on a set of three FPGAs and a desktop server, with the computational complexity calculated as a function of primitive operations. A composable security model is proposed and analyzed considering a powerful adversary in control of all communications channels. In particular, session key confidentiality is proven through formal verification of the protocol under strong attacker (Dolev-Yao) assumptions, rendering it viable for high-security applications such as digital currency. Full article

The development of smart contracts remains in its early stages, with significant differences in underlying programming languages and application platforms resulting in a lack of standardization. This lack of standardization increases the susceptibility to vulnerabilities and associated financial losses. To address security vulnerabilities in smart contracts on the Ethereum blockchain platform, this paper proposes a security audit method based on formal verification. The method integrates an input module, static analysis module, formal verification module, analog execution module, and report and recommendation module, which can accurately discover the security vulnerabilities and logical flaws of smart contracts through formal verification and other analysis techniques, thus realizing correctness detection. During the experiment, the method detects 8 types of common vulnerabilities in 148 smart contracts and marks 21 smart contracts with vulnerabilities. After manual review and analysis, it is found that 17 of these 21 marked smart contracts do have security vulnerabilities. The experimental results show that the proposed method can accurately detect security vulnerabilities and logic flaws in smart contracts through formal verification and other analysis techniques before smart contracts are deployed, thus significantly improving the security of smart contracts and reducing the economic losses that may be caused by code defects. Full article

One of the main security challenges when federating separate Internet of Things (IoT) administrative domains is effective Identity and Access Management, which is required to establish trust and secure communication between federated IoT devices. The primary goal of the work is to develop a “lightweight” protocol to enable authentication and authorization of IoT devices in federated environments and ensure the secure communication of IoT devices. We propose a novel Lightweight Authentication and Authorization Framework for Federated IoT (LAAFFI) which takes advantage of the unique fingerprint of IoT devices based on their configuration and additional hardware modules, such as Physical Unclonable Function, to provide flexible authentication and authorization based on Distributed Ledger technology. Moreover, LAAFFI supports IoT devices with limited computing resources and devices not equipped with secure storage space. We implemented a prototype of LAAFFI and evaluated its performance in the Hyperledger Fabric-based IoT framework. Three main metrics were evaluated: latency, throughput (number of operations or transactions per second), and network resource utilization rate (transmission overhead introduced by the LAAFFI protocol). The performance tests conducted confirmed the high efficiency and suitability of the protocol for federated IoT environments. Also, all LAAFFI components are scalable as confirmed by tests. We formally evaluated LAAFFI security using Verifpal as a formal verification tool. Based on the models developed for Verifpal, we validated their security properties, such as message secrecy, authenticity, and freshness. Our results show that the proposed solution can improve the security of federated IoT environments while providing zero-day interoperability and high scalability. Compared to existing solutions, LAAFFI is more efficient due to the use of symmetric cryptography and algorithms adapted for operations involving IoT devices. LAAFFI supports multiple authorization mechanisms, and since it also offers authentication and accountability, it meets the requirements of Authentication, Authorization and Accounting (AAA). It uses Distributed Ledger (DL) and smart contracts to ensure that the request complies with the policies agreed between the organizations. LAAFFI offers authentication of devices belonging to a single organization and different organizations, with the assurance that the encryption key will be shared with another device only if the appropriate security policy is met. The proposed protocol is particularly useful for ensuring the security of federated IoT environments created ad hoc for special missions, e.g., operations conducted by NATO countries and disaster relief operations Humanitarian Assistance and Disaster Relief (HADR) involving military forces and civilian services, where immediate interoperability is required. Full article

Vehicular ad hoc networks (VANETs), which are the backbone of intelligent transportation systems (ITSs), facilitate critical data exchanges between vehicles. This necessitates secure transmission, which requires guarantees of message availability, integrity, source authenticity, and user privacy. Moreover, the traceability of network participants is essential as it deters malicious actors and allows lawful authorities to identify message senders for accountability. This introduces a challenge: balancing privacy with traceability. Conditional privacy-preserving authentication (CPPA) schemes are designed to mitigate this conflict. CPPA schemes utilize cryptographic protocols, including certificate-based schemes, group signatures, identity-based schemes, and certificateless schemes. Due to the critical time constraints in VANETs, efficient batch verification techniques are crucial. Combining certificateless schemes with batch verification leads to certificateless aggregate signature (CLAS) schemes. In this paper, cryptanalysis of Xiong’s CLAS scheme revealed its vulnerabilities to partial key replacement and identity replacement attacks, alongside mathematical errors in the batch verification process. Our proposed CLAS scheme remedies these issues by incorporating an identity authentication module that leverages chameleon hashing within elliptic curve cryptography (CHAM-CLAS). The signature and verification modules are also redesigned to address the identified vulnerabilities in Xiong’s scheme. Additionally, we implemented the small exponents test within the batch verification module to achieve Type III security. While this enhances security, it introduces a slight performance trade-off. Our scheme has been subjected to formal security and performance analyses to ensure robustness. Full article

Workflows orchestrate a collection of computing tasks to form a complex workflow logic. Different from the traditional monolithic workflow management systems, modern workflow systems often manifest high throughput, concurrency and scalability. As service-based systems, execution time monitoring is an important part of maintaining the performance for those systems. We developed a trace profiling approach that leverages quantitative verification (also known as probabilistic model checking) to analyse complex time metrics for workflow traces. The strength of probabilistic model checking lies in the ability of expressing various temporal properties for a stochastic system model and performing automated quantitative verification. We employ semi-Makrov chains (SMCs) as the formal model and consider the first passage times (FPT) measures in the SMCs. Our approach maintains simple mergeable data summaries of the workflow executions and computes the moment parameters for FPT efficiently. We describe an application of our approach to AWS Step Functions, a notable workflow web service. An empirical evaluation shows that our approach is efficient for computer high-order FPT moments for sizeable workflows in practice. It can compute up to the fourth moment for a large workflow model with 10,000 states within 70 s. Full article

In gas sensor networks, users can access the data collected by the sensor nodes, but there is a risk of data leakage during transmission. This paper proposes a lightweight bidirectional authentication protocol based on gas sensor physically unclonable functions (GS-PUFs) with authentication technology to guarantee the reliability of data from sensor nodes. A sensor PUF array is constructed by preparing gas sensors to enhance the data security of the physical layer and reduce hardware resource consumption. The authentication part of the protocol mainly uses lightweight encryption methods, consisting of PUF data, one-way cryptographic hash functions, and iso-or functions, to reduce the computational overhead of the authentication process. The protocol security is enhanced by encrypting the GS-PUF response as an irreversible hash value and verifying the hash value by the user, server, and sensor node to complete bidirectional authentication. The test results demonstrate that the protocol, verified through the ProVerif formal tool, can resist impersonation, replay, node tampering, and cloning attacks. Among the compared schemes, this protocol offers the highest security and the least resource overhead, making it effectively applicable in the Internet of Things and other fields. Full article

Consumer protection in the financial market has several dimensions. From a formal point of view, consumer rights are guaranteed by law. Educational programs are implemented in schools and the media to promote knowledge and responsible use of financial products and services. Despite the efforts made, the number of incorrect and suboptimal financial decisions is so high that the risk of households falling into excessive debt remains significant. The limited effectiveness of the law led to the claim that only effective education can reduce the risk of suboptimal financial decisions. Unfortunately, the efforts made in this area are not fully satisfactory. The study of financial knowledge of consumers, which was conducted in Poland in January 2024, aimed to verify consumer errors and their nature. As part of the consumer study, not only declared knowledge was verified, but also actual knowledge. The researchers’ doubts resulted from a comparison of the results of scientific research in this area with the current market situation. Consumers declare a high level of knowledge of economic and financial concepts. In practice, however, they make mistakes that do not only indicate behavioral cognitive errors but also a lack of knowledge. The test questions were constructed in such a way as to verify the declared knowledge (based on verification questions). These showed that the actual level of knowledge was lower than the declared one. A review of the literature and studies of financial knowledge and financial competence of consumers in Central European countries was also carried out. Analysis of the results allowed for the formulation of conclusions regarding the educational gap in relation to social characteristics. The conclusions resulting from the study raise questions about the effectiveness of the educational methods used and indicate possible directions of changes in the consumer regulation policy, the aim of which is to ensure a high level of consumer protection. Full article

Although the Linux kernel is widely used, its complexity makes errors common and potentially serious. Traditional formal verification methods often have high overhead and rely heavily on manual coding. They typically verify only specific functionalities of the kernel or target microkernels and do not support continuous verification of the entire kernel. To address these limitations, we introduce LMVM (Linux Kernel Modeling and Verification Method), a formal method based on type theory that ensures the correct design of the Linux architecture. In the model, the kernel is treated as a top-level type, subdivided into the following sublevels: subsystem, dentry, file, struct, function, and base. These types are defined in the structure and relationships. The verification process includes checking the design specifications for both type relationships and the presence of each type. Our contribution lies primarily in the following two points: 1. This is a lightweight verification. As long as the modeling is complete, architectural errors in the design phase can be identified promptly. 2. The designed “model refactor” module supports kernel updating, and the kernel can be continuously verified by extending the kernel model. To test its usefulness, we develop a set of security communication mechanisms in the kernel, which are verified using our method. Full article

In the Internet of Vehicles (IoV) environments, vehicles and roadside units (RSUs) communicate predominantly through public channels. These vehicles and RSUs exchange various data, such as traffic density, location, speed, etc. Therefore, secure and efficient authentication and key establishment (AKE) are needed to guarantee user privacy when exchanging data between vehicles and RSUs. Recently, a secure and computationally AKE scheme have been proposed to construct secure IoV environments. In their research, the authors asserted that their AKE scheme provides comprehensive security properties, protecting against various potential threats while simultaneously ensuring session key integrity, robust mutual authentication. This paper proved that the previous scheme does not prevent various attacks using logical and mathematical analyses. Moreover, we demonstrated that this scheme does not meet the essential security requirements and correctness of security assumptions. We perform the simulation proof using AVISPA, which is well known as a formal verification tool. To enhance the resilience of attacks, we propose solutions aimed at developing more robust and efficient AKE for IoV environments. Full article