相关论文: Timed Analysis of Security Protocols

Security protocols often use randomization to achieve probabilistic non-determinism. This non-determinism, in turn, is used in obfuscating the dependence of observable values on secret data. Since the correctness of security protocols is…

The paper wraps up the call for formal analysis of the new security handshake protocol EDHOC by providing an overview of the protocol as it was standardized, a summary of the formal security analyses conducted by the community, and a…

Security protocols are concurrent processes that communicate using cryptography with the aim of achieving various security properties. Recent work on their formal verification has brought procedures and tools for deciding trace equivalence…

Logics for security protocol analysis require the formalization of an adversary model that specifies the capabilities of adversaries. A common model is the Dolev-Yao model, which considers only adversaries that can compose and replay…

Web attacks, i.e. attacks exclusively using the HTTP protocol, are rapidly becoming one of the fundamental threats for information systems connected to the Internet. When the attacks suffered by web servers through the years are analyzed,…

Current formal verification of security protocols relies on specialized researchers and complex tools, inaccessible to protocol designers who informally evaluate their work with emulators. This paper addresses this gap by embedding symbolic…

Accurately measuring time passing is critical for many applications. However, in Trusted Execution Environments (TEEs) such as Intel SGX, the time source is outside the Trusted Computing Base: a malicious host can manipulate the TEE's…

High-precision time synchronization is a vital prerequisite for many modern applications and technologies, including Smart Grids, Time-Sensitive Networking (TSN), and 5G networks. Although the Precision Time Protocol (PTP) can accomplish…

We present a monitoring approach for verifying systems at runtime. Our approach targets systems whose components communicate with the monitors over unreliable channels, where messages can be delayed or lost. In contrast to prior works,…

This study evaluates the application of predictive analytics for real-time cyber-attack detection and response, focusing on how statistical and machine learning methods can improve decision-making in Security Operations Centers (SOCs).…

We introduce knowledge flow analysis, a simple and flexible formalism for checking cryptographic protocols. Knowledge flows provide a uniform language for expressing the actions of principals, assump- tions about intruders, and the…

Knowledge flow analysis offers a simple and flexible way to find flaws in security protocols. A protocol is described by a collection of rules constraining the propagation of knowledge amongst principals. Because this characterization…

When developing a safety-critical system it is essential to obtain an assessment of different design alternatives. In particular, an early safety assessment of the architectural design of a system is desirable. In spite of the plethora of…

There exists a verification gap between formal protocol specifications and their actual implementations, which this work aims to bridge via monitoring for compliance to the formal specification. We instrument the networking and…

This paper tackles the problems of generating concrete test cases for testing whether an application is vulnerable to attacks, and of checking whether security solutions are correctly implemented. The approach proposed in the paper aims at…

We introduce a prototype tool strategFTO addressing the verification of a security property in critical software. We consider a recent definition of timed opacity where an attacker aims to deduce some secret while having access only to the…

The previous work showed that the Y00 protocol could stay secure with the eavesdropper's guessing probability on the secret keys being strictly less than one under an unlimitedly long known-plaintext attack with quantum memory. However, an…

Many security protocols rely on the assumptions on the physical properties in which its protocol sessions will be carried out. For instance, Distance Bounding Protocols take into account the round trip time of messages and the transmission…

The importance of information security dramatically increased and will further grow due to the shape and nature of the modern computing industry. Software is published at a continuously increasing pace. The Internet of Things and security…

This paper addresses the problem of robust clock phase offset estimation for the IEEE 1588 precision time protocol (PTP) in the presence of delay attacks. Delay attacks are one of the most effective cyber attacks in PTP, as they cannot be…