Biblio

Cryptographic protocols are the basis for the security of any protected system, including the electronic voting system. One of the most effective ways to analyze protocol security is to use verifiers. In this paper, the formal verifier SPIN was used to analyze the security of the cryptographic protocol for e-voting, which is based on model checking using linear temporal logic (LTL). The cryptographic protocol of electronic voting is described. The main structural units of the Promela language used for simulation in the SPIN verifier are described. The model of the electronic voting protocol in the language Promela is given. The interacting parties, transferred data, the order of the messages transmitted between the parties are described. Security of the cryptographic protocol using the SPIN tool is verified. The simulation of the protocol with active intruder using the man in the middle attack (MITM) to substitute data is made. In the simulation results it is established that the protocol correctly handles the case of an active attack on the parties' authentication.

WireGuard is a free and open source Virtual Private Network (VPN) that aims to replace IPsec and OpenVPN. It is based on a new cryptographic protocol derived from the Noise Protocol Framework. This paper presents the first mechanised cryptographic proof of the protocol underlying WireGuard, using the CryptoVerif proof assistant. We analyse the entire WireGuard protocol as it is, including transport data messages, in an ACCE-style model. We contribute proofs for correctness, message secrecy, forward secrecy, mutual authentication, session uniqueness, and resistance against key compromise impersonation, identity mis-binding, and replay attacks. We also discuss the strength of the identity hiding provided by WireGuard. Our work also provides novel theoretical contributions that are reusable beyond WireGuard. First, we extend CryptoVerif to account for the absence of public key validation in popular Diffie-Hellman groups like Curve25519, which is used in many modern protocols including WireGuard. To our knowledge, this is the first mechanised cryptographic proof for any protocol employing such a precise model. Second, we prove several indifferentiability lemmas that are useful to simplify the proofs for sequences of key derivations.

Universally Composable (UC) framework provides the strongest security notion for designing fully trusted cryptographic protocols, and it is very challenging on applying UC security in the design of RFID mutual authentication protocols. In this paper, we formulate the necessary conditions for achieving UC secure RFID mutual authentication protocols which can be fully trusted in arbitrary environment, and indicate the inadequacy of some existing schemes under the UC framework. We define the ideal functionality for RFID mutual authentication and propose the first UC secure RFID mutual authentication protocol based on public key encryption and certain trusted third parties which can be modeled as functionalities. We prove the security of our protocol under the strongest adversary model assuming both the tags' and readers' corruptions. We also present two (public) key update protocols for the cases of multiple readers: one uses Message Authentication Code (MAC) and the other uses trusted certificates in Public Key Infrastructure (PKI). Furthermore, we address the relations between our UC framework and the zero-knowledge privacy model proposed by Deng et al. [1].

In several critical military missions, more than one decision level are involved. These decision levels are often independent and distributed, and sensitive pieces of information making up the military mission must be kept hidden from one level to another even if all of the decision levels cooperate to accomplish the same task. Usually, a mission is negotiated through insecure networks such as the Internet using cryptographic protocols. In such protocols, few security properties have to be ensured. However, designing a secure cryptographic protocol that ensures several properties at once is a very challenging task. In this paper, we propose a new secure protocol for multipart military missions that involve two independent and distributed decision levels having different security levels. We show that it ensures the secrecy, authentication, and non-repudiation properties. In addition, we show that it resists against man-in-the-middle attacks.

Prior remote attestation may not be suitable to scale to the proliferation of IoT device swarms. To this end, we propose a cooperative remote attestation scheme, which validates the security state and verifies the system integrity with the cooperation of neighbor devices. The efficiency of the proposed mechanism is analyzed as a cryptographic protocol and then discussed in terms of security and scalability.

This paper presents an efficiency and adaptive cryptographic protocol to ensure users' privacy and data integrity in RFID system. Radio Frequency Identification technology offers more intelligent systems and applications, but privacy and security issues have to be addressed before and after its adoption. The design of the proposed model is based on clustering configuration of the involved tags where they interchange the data with the reader whenever it sends a request. This scheme provides a strong mutual authentication framework that suits for real heterogeneous RFID applications such as in supply-chain management systems, healthcare monitoring and industrial environment. In addition, we contribute with a mathematical analysis to the delay analysis and optimization in a clustering topology tag-based. Finally, a formal security and proof analysis is demonstrated to prove the effectiveness of the proposed protocol and that achieves security and privacy.

Wireless security has been an active research area since the last decade. A lot of studies of wireless security use cryptographic tools, but traditional cryptographic tools are normally based on computational assumptions, which may turn out to be invalid in the future. Consequently, it is very desirable to build cryptographic tools that do not rely on computational assumptions. In this paper, we focus on a crucial cryptographic tool, namely 1-out-of-2 oblivious transfer. This tool plays a central role in cryptography because we can build a cryptographic protocol for any polynomial-time computable function using this tool. We present a novel 1-out-of-2 oblivious transfer protocol based on wireless channel characteristics, which does not rely on any computational assumption. We also illustrate the potential broad applications of this protocol by giving two applications, one on private communications and the other on privacy preserving password verification. We have fully implemented this protocol on wireless devices and conducted experiments in real environments to evaluate the protocol. Our experimental results demonstrate that it has reasonable efficiency.