We propose a method for engineering security protocols that are aware of timing aspects. We study a simplified version of the well-known Needham Schroeder protocol and the complete Yahalom protocol, where timing information allows the study of different attack scenarios. We model check the protocols using UPPAAL. Further, a taxonomy is obtained by studying and categorising protocols from the well known Clark Jacob library and the Security Protocol Open Repository (SPORE) library. Finally, we present some new challenges and threats that arise when considering time in the analysis, by providing a novel protocol that uses time challenges and exposing a timing attack over an implementation of an existing security protocol.
Timed automata are a common formalism for the verification of concurrent systems subject to timing constraints. They extend finite-state automata with clocks, that constrain the system behavior in locations, and to take transitions. While timed automata were originally designed for safety (in the wide sense of correctness w.r.t. a formal property), they were progressively used in a number of works to guarantee security properties. In this work, we review works studying security properties for timed automata in the last two decades. We notably review theoretical works, with a particular focus o…
This paper proposes SilentDelivery, a secure, scalable and cost-efficient protocol for implementing timed information delivery service in a decentralized blockchain network. SilentDelivery employs a novel combination of threshold secret sharing and decentralized smart contracts. The protocol maintains shares of the decryption key of the private information of an information sender using a group of mailmen recruited in a blockchain network before the specified future time-frame and restores the information to the information recipient at the required time-frame. To tackle the key challenges tha…
In the age of Big Data, enabling task scheduling while protecting users' privacy is critical for various decentralized applications in blockchain-based smart contract platforms. Such a privacy-preserving task scheduler requires the task input data to be secretly maintained until a prescribed task execution time and be automatically recorded into the blockchain to enabling the execution of the task at the execution time, even if the user goes offline. While straight-forward centralized approaches provide a basic solution to the problem, unfortunately they are limited to a single point of trust …
Many existing timed-release encryption schemes uses time-lock puzzles to avoid relying on a trusted timeserver or a key holder which could be a weak spot in data security. However, it is unavoidable to consume massive computing power for solving time-lock puzzles and it is difficult for encryptors to predict the amount of time to solve a puzzle by decryptors. In this study, an efficient dual-purpose proof-of-work consensus allows users to release a time-locked content, which is encrypted by an asymmetric key encryption scheme on a blockchain, without trust in any third-party agents. The releas…
Information leakage can have dramatic consequences on systems security. Among harmful information leaks, the timing information leakage is the ability for an attacker to deduce internal information depending on the system execution time. We address the following problem: given a timed system, synthesize the execution times for which one cannot deduce whether the system performed some secret behavior. We solve this problem in the setting of timed automata (TAs). We first provide a general solution, and then extend the problem to parametric TAs, by synthesizing internal timings making the TA sec…
A Logic Programming Approach for Formal Verification of NetBill Security and Transactions Protocol
使用形式化的技术来验证电子商务协议的安全特征将有助于增强此类协议的可靠性，从而提高其可用性。本文提出了应用逻辑编程技术对NetBill协议进行形式化验证的方法。本文采用ALSP（Action Language for Security Protocols）作为有效的形式化规约语言，SMODELS作为模型生成器，对协议进行形式化分析和攻击规划。
The Nakamoto longest chain protocol is remarkably simple and has been proven to provide security against any adversary with less than 50% of the total hashing power. Proof-of-stake (PoS) protocols are an energy efficient alternative; however existing protocols adopting Nakamoto's longest chain design achieve provable security only by allowing long-term predictability (which have serious security implications). In this paper, we prove that a natural longest chain PoS protocol with similar predictability as Nakamoto's PoW protocol can achieve security against any adversary with less than 1/(1+e)…
Information leakage can have dramatic consequences on systems security. Among harmful information leaks, the timing information leakage occurs whenever an attacker successfully deduces confidential internal information. In this work, we consider that the attacker has access (only) to the system execution time. We address the following timed opacity problem: given a timed system, a private location and a final location, synthesize the execution times from the initial location to the final location for which one cannot deduce whether the system went through the private location. We also consider…
In this paper we discuss the security of a distributed inner product (DIP) protocol [IEEE TIFS, 11(1), (2016), 59-73]. We show information leakage in this protocol that does not happen in an ideal execution of DIP functionality. In some scenarios, this information leakage enables one of the parties to completely learn the other party's input. We will give examples of such scenarios.
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 total execution time. The system, here modeled by timed automata, is deemed opaque if for any execution time, there are either no corresponding runs, or both public and private corresponding runs. We focus on the untimed control problem: exhibiting a controller, i.e., a set of allowed actions, such that the system restricted to those actions is fully timed-o…
The field of electric vehicle charging involves a complex combination of actors, devices, networks, and protocols. These protocols are being developed without a clear focus on security. In this paper, we give an overview of the main roles and protocols in use in the Netherlands. We describe a clear attacker model and security requirements, show that in light of this many of the protocols have security issues, and provide suggestions on how to address these issues. The most important conclusion is the need for end-to-end security for data in transit and long-term authenticity for data at rest. …
Smart contracts have recently been adopted by many security protocols. However, existing studies lack satisfactory theoretical support on how contracts benefit security protocols. This paper aims to give a systematic analysis of smart contract (SC)-based security protocols to fulfill the gap of unclear arguments and statements. We firstly investigate \textit{state of the art studies} and establish a formalized model of smart contract protocols with well-defined syntax and assumptions. Then, we apply our formal framework to two concrete instructions to explore corresponding advantages and desir…
ProVerif is a widely used security protocol verifier. Internally, ProVerif uses an abstract representation of the protocol by Horn clauses and a resolution algorithm on these clauses, in order to prove security properties of the protocol or to find attacks. In this paper, we present an overview of ProVerif and discuss some specificities of its resolution algorithm, related to the particular application domain and the particular clauses that ProVerif generates. This paper is a short summary that gives pointers to publications on ProVerif in which the reader will find more details.
In this paper, we show how practical the little theorem of witness functions is in detecting security flaws in some category of cryptographic protocols. We convey a formal analysis of the Needham-Schroeder symmetric-key protocol in the theory of witness functions. We show how it helps to teach about a security vulnerability in a given step of this protocol where the value of security of a particular sensitive ticket in a sent message unexpectedly plummets compared with its value when received. This vulnerability may be exploited by an intruder to mount a replay attack as described by Denning a…
Accountability is a recent paradigm in security protocol design which aims to eliminate traditional trust assumptions on parties and hold them accountable for their misbehavior. It is meant to establish trust in the first place and to recognize and react if this trust is violated. In this work, we discuss a protocol agnostic definition of accountability: a protocol provides accountability (w.r.t. some security property) if it can identify all misbehaving parties, where misbehavior is defined as a deviation from the protocol that causes a security violation. We provide a mechanized method for t…
Vehicular networks will enable a range of novel applications to enhance road traffic efficiency, safety, and reduce fuel consumption. As for other cyber-physical systems, security is essential to the deployment of these applications and standardisation efforts are ongoing. In this paper, we perform a systematic security evaluation of a vehicular platooning protocol through a thorough analysis of the protocol and security standards. We tackle the complexity of the resulting model with a proof strategy based on a relation on keys. The key relation forms a partial order, which encapsulates both s…
We present a framework suited to the analysis of cryptographic protocols that make use of time in their execution. We provide a process algebra syntax that makes time information available to processes, and a transition semantics that takes account of fundamental properties of time. Additional properties can be added by the user if desirable. This timed protocol framework can be implemented either as a simulation tool or as a symbolic analysis tool in which time references are represented by logical variables, and in which the properties of time are implemented as constraints on those time log…
IEEE 802.1X is an international standard for Port-based Network Access Control which provides authentication for devices applicant of either local network or wireless local network. This standard defines the packing of EAP protocol on IEEE 802. In this standard, authentication protocols become a complementary part of network security. There is a variety in EAP family protocols, regarding their speed and security. One of the fastest of these protocols is EAP-MD5 which is the main subject of this paper. Moreover, in order to improve EAP-MD5 security, a series of attacks against it have been inve…
By expanding the connection of objects to the Internet and their entry to human life, the issue of security and privacy has become important. In order to enhance security and privacy on the Internet, many security protocols have been developed. Unfortunately, the security analyzes that have been carried out on these protocols show that they are vulnerable to one or few attacks, which eliminates the use of these protocols. Therefore, the need for a security protocol on the Internet of Things (IoT) has not yet been resolved. Recently, Khor and Sidorov cryptanalyzed the Wang et al. protocol and p…
While the application of IoT in smart technologies becomes more and more proliferated, the pandemonium of its protocols becomes increasingly confusing. More seriously, severe security deficiencies of these protocols become evident, as time-to- market is a key factor, which satisfaction comes at the price of a less thorough security design and testing. This applies especially to the smart home domain, where the consumer-driven market demands quick and cheap solutions. This paper presents an overview of IoT application domains and discusses the most important wireless IoT protocols for smart hom…
The HashGraph Protocol is a Byzantine fault tolerant atomic broadcast protocol. Its novel use of locally stored metadata allows parties to recover a consistent ordering of their log just by examining their local data, removing the need for a voting protocol. Our paper's first contribution is to present a rewritten proof of security for the HashGraph Protocol that follows the consistency and liveness paradigm used in the atomic broadcast literature. In our second contribution, we show a novel adversarial strategy that stalls the protocol from committing data to the log for an expected exponenti…
The increased use of smart Electric Vehicles (EVs) and Plug-in Electric Vehicles (PEV) opened a new area of research and development. The number of EV charging sites has considerably increased in residential as well as in public areas. Within these EV charging sites, various entities need to communicate in a secure and efficient way. The Open Charge Point Protocol (OCPP) offers a way to coordinate this communication and is already being used in many implementations. However, only the latest OCPP 2.0 version of the protocol includes certain security features. In this article, we present the ent…
The Third Generation Partnership Project (3GPP) released its first 5G security specifications in March 2018. This paper reviews the 5G security architecture, requirements and main processes and evaluates them in the context of known and new protocol exploits. Although the security has been enhanced when compared to previous generations to tackle known protocol exploits, our analysis identifies some potentially unrealistic system assumptions that are critical for security as well as a number protocol edge cases that could render 5G systems vulnerable to adversarial attacks. For example, null en…
