Visible to the public Biblio

Found 225 results

Filters: Keyword is cryptographic protocols  [Clear All Filters]
2020-08-03
Arthi, A., Aravindhan, K..  2019.  Enhancing the Performance Analysis of LWA Protocol Key Agreement in Vehicular Ad hoc Network. 2019 5th International Conference on Advanced Computing Communication Systems (ICACCS). :1070–1074.

Road accidents are challenging threat in the present scenario. In India there are 5, 01,423 road accidents in 2015. A day 400 hundred deaths are forcing to India to take car safety sincerely. The common cause for road accidents is driver's distraction. In current world the people are dominated by the tablet PC and other hand held devices. The VANET technology is a vehicle-to-vehicle communication; here the main challenge will be to deliver qualified communication during mobility. The paper proposes a standard new restricted lightweight authentication protocol utilizing key agreement theme for VANETs. Inside the planned topic, it has three sorts of validations: 1) V2V 2) V2CH; and 3) CH and RSU. Aside from this authentication, the planned topic conjointly keeps up mystery keys between RSUs for the safe communication. Thorough informal security analysis demonstrates the planned subject is skilled to guard different malicious attack. In addition, the NS2 Simulation exhibits the possibility of the proposed plan in VANET background.

2020-07-30
Su, Wei-Tsung, Chen, Wei-Cheng, Chen, Chao-Chun.  2019.  An Extensible and Transparent Thing-to-Thing Security Enhancement for MQTT Protocol in IoT Environment. 2019 Global IoT Summit (GIoTS). :1—4.
Message Queue Telemetry Transport (MQTT) is widely accepted as a data exchange protocol in Internet of Things (IoT) environment. For security, MQTT supports Transport Layer Security (MQTT-TLS). However, MQTT-TLS provides thing-to-broker channel encryption only because data can still be exposed after MQTT broker. In addition, ACL becomes impractical due to the increasing number of rules for authorizing massive IoT devices. For solving these problems, we propose MQTT Thing-to-Thing Security (MQTT-TTS) which provides thing-to-thing security which prevents data leak. MQTT-TTS also provides the extensibility to include demanded security mechanisms for various security requirements. Moreover, the transparency of MQTT-TTS lets IoT application developers implementing secure data exchange with less programming efforts. Our MQTT-TTS implementation is available on https://github.com/beebit-sec/beebit-mqttc-sdk for evaluation.
2020-07-24
Touati, Lyes.  2017.  Grouping-Proofs Based Access Control Using KP-ABE for IoT Applications. 2017 IEEE Trustcom/BigDataSE/ICESS. :301—308.
The Internet of Things (IoT) is a new paradigm in which every-day objects are interconnected between each other and to the Internet. This paradigm is receiving much attention of the scientific community and it is applied in many fields. In some applications, it is useful to prove that a number of objects are simultaneously present in a group. For example, an individual might want to authorize NFC payment with his mobile only if k of his devices are present to ensure that he is the right person. This principle is known as Grouping-Proofs. However, existing Grouping-Proofs schemes are mostly designed for RFID systems and don't fulfill the IoT characteristics. In this paper, we propose a Threshold Grouping-Proofs for IoT applications. Our scheme uses the Key-Policy Attribute-Based Encryption (KP-ABE) protocol to encrypt a message so that it can be decrypted only if at least k objects are simultaneously present in the same location. A security analysis and performance evaluation is conducted to show the effectiveness of our proposal solution.
2020-07-20
Masood, Raziqa, Pandey, Nitin, Rana, Q. P..  2017.  An approach of dredging the interconnected nodes and repudiating attacks in cloud network. 2017 4th IEEE Uttar Pradesh Section International Conference on Electrical, Computer and Electronics (UPCON). :49–53.
In cloud computing environment, there are malignant nodes which create a huge problem to transfer data in communication. As there are so many models to prevent the data over the network, here we try to prevent or make secure to the network by avoiding mallicious nodes in between the communication. So the probabiliostic approach what we use here is a coherent tool to supervise the security challenges in the cloud environment. The matter of security for cloud computing is a superficial quality of service from cloud service providers. Even, cloud computing dealing everyday with new challenges, which is in process to well investigate. This research work draws the light on aspect regarding with the cloud data transmission and security by identifying the malignanat nodes in between the communication. Cloud computing network shared the common pool of resources like hardware, framework, platforms and security mechanisms. therefore Cloud Computing cache the information and deliver the secure transaction of data, so privacy and security has become the bone of contention which hampers the process to execute safely. To ensure the security of data in cloud environment, we proposed a method by implementing white box cryptography on RSA algorithm and then we work on the network, and find the malignant nodes which hampering the communication by hitting each other in the network. Several existing security models already have been deployed with security attacks. A probabilistic authentication and authorization approach is introduced to overcome this attack easily. It observes corrupted nodes before hitting with maximum probability. here we use a command table to conquer the malignant nodes. then we do the comparative study and it shows the probabilistic authentication and authorization protocol gives the performance much better than the old ones.
Castiglione, Arcangelo, Palmieri, Francesco, Colace, Francesco, Lombardi, Marco, Santaniello, Domenico.  2019.  Lightweight Ciphers in Automotive Networks: A Preliminary Approach. 2019 4th International Conference on System Reliability and Safety (ICSRS). :142–147.
Nowadays, the growing need to connect modern vehicles through computer networks leads to increased risks of cyberattacks. The internal network, which governs the several electronic components of a vehicle, is becoming increasingly overexposed to external attacks. The Controller Area Network (CAN) protocol, used to interconnect those devices is the key point of the internal network of modern vehicles. Therefore, securing such protocol is crucial to ensure a safe driving experience. However, the CAN is a standard that has undergone little changes since it was introduced in 1983. More precisely, in an attempt to reduce latency, the transfer of information remains unencrypted, which today represents a weak point in the protocol. Hence, the need to protect communications, without introducing low-level alterations, while preserving the performance characteristics of the protocol. In this work, we investigate the possibility of using symmetric encryption algorithms for securing messages exchanged by CAN protocol. In particular, we evaluate the using of lightweight ciphers to secure CAN-level communication. Such ciphers represent a reliable solution on hardware-constrained devices, such as microcontrollers.
Urien, Pascal.  2019.  Designing Attacks Against Automotive Control Area Network Bus and Electronic Control Units. 2019 16th IEEE Annual Consumer Communications Networking Conference (CCNC). :1–4.
Security is a critical issue for new car generation targeting intelligent transportation systems (ITS), involving autonomous and connected vehicles. In this work we designed a low cost CAN probe and defined analysis tools in order to build attack scenarios. We reuse some threats identified by a previous work. Future researches will address new security protocols.
2020-07-16
Gariano, John, Djordjevic, Ivan B..  2019.  Covert Communications-Based Information Reconciliation for Quantum Key Distribution Protocols. 2019 21st International Conference on Transparent Optical Networks (ICTON). :1—5.

The rate at which a secure key can be generated in a quantum key distribution (QKD) protocol is limited by the channel loss and the quantum bit-error rate (QBER). Increases to the QBER can stem from detector noise, channel noise, or the presence of an eavesdropper, Eve. Eve is capable of obtaining information of the unsecure key by performing an attack on the quantum channel or by listening to all discussion performed via a noiseless public channel. Conventionally a QKD protocol will perform the information reconciliation over the authenticated public channel, revealing the parity bits used to correct for any quantum bit errors. In this invited paper, the possibility of limiting the information revealed to Eve during the information reconciliation is considered. Using a covert communication channel for the transmission of the parity bits, secure key rates are possible at much higher QBERs. This is demonstrated through the simulation of a polarization based QKD system implementing the BB84 protocol, showing significant improvement of the SKRs over the conventional QKD protocols.

2020-07-13
Kurbatov, Oleksandr, Shapoval, Oleksiy, Poluyanenko, Nikolay, Kuznetsova, Tetiana, Kravchenko, Pavel.  2019.  Decentralized Identification and Certification System. 2019 IEEE International Scientific-Practical Conference Problems of Infocommunications, Science and Technology (PIC S T). :507–510.
This article describes an approach to identification and certification in decentralized environment. The protocol proposes a way of integration for blockchain technology and web-of-trust concept to create decentralized public key infrastructure with flexible management for user identificators. Besides changing the current public key infrastructure, this system can be used in the Internet of Things (IoT). Each individual IoT sensor must correctly communicate with other components of the system it's in. To provide safe interaction, components should exchange encrypted messages with ability to check their integrity and authenticity, which is presented by this scheme.
2020-06-26
Salman, Ahmad, El-Tawab, Samy.  2019.  Efficient Hardware/Software Co-Design of Elliptic-Curve Cryptography for the Internet of Things. 2019 International Conference on Smart Applications, Communications and Networking (SmartNets). :1—6.

The Internet of Things (IoT) is connecting the world in a way humanity has never seen before. With applications in healthcare, agricultural, transportation, and more, IoT devices help in bridging the gap between the physical and the virtual worlds. These devices usually carry sensitive data which requires security and protection in transit and rest. However, the limited power and energy consumption make it harder and more challenging to implementing security protocols, especially Public-Key Cryptosystems (PKC). In this paper, we present a hardware/software co-design for Elliptic-Curve Cryptography (ECC) PKC suitable for lightweight devices. We present the implementation results for our design on an edge node to be used for indoor localization in a healthcare facilities.

2020-06-19
Gu, Chongyan, Chang, Chip Hong, Liu, Weiqiang, Yu, Shichao, Ma, Qingqing, O'Neill, Maire.  2019.  A Modeling Attack Resistant Deception Technique for Securing PUF based Authentication. 2019 Asian Hardware Oriented Security and Trust Symposium (AsianHOST). :1—6.

Due to practical constraints in preventing phishing through public network or insecure communication channels, simple physical unclonable function (PDF)-based authentication protocol with unrestricted queries and transparent responses is vulnerable to modeling and replay attacks. In this paper, we present a PUF-based authentication method to mitigate the practical limitations in applications where a resource-rich server authenticates a device with no strong restriction imposed on the type of PUF designs or any additional protection on the binary channel used for the authentication. Our scheme uses an active deception protocol to prevent machine learning (ML) attacks on a device. The monolithic system makes collection of challenge response pairs (CRPs) easy for model building during enrollment but prohibitively time consuming upon device deployment. A genuine server can perform a mutual authentication with the device at any time with a combined fresh challenge contributed by both the server and the device. The message exchanged in clear does not expose the authentic CRPs. The false PUF multiplexing is fortified against prediction of waiting time by doubling the time penalty for every unsuccessful authentication.

2020-06-12
Latif, M. Kamran, Jacinto, H S., Daoud, Luka, Rafla, Nader.  2018.  Optimization of a Quantum-Secure Sponge-Based Hash Message Authentication Protocol. 2018 IEEE 61st International Midwest Symposium on Circuits and Systems (MWSCAS). :984—987.

Hash message authentication is a fundamental building block of many networking security protocols such as SSL, TLS, FTP, and even HTTPS. The sponge-based SHA-3 hashing algorithm is the most recently developed hashing function as a result of a NIST competition to find a new hashing standard after SHA-1 and SHA-2 were found to have collisions, and thus were considered broken. We used Xilinx High-Level Synthesis to develop an optimized and pipelined version of the post-quantum-secure SHA-3 hash message authentication code (HMAC) which is capable of computing a HMAC every 280 clock-cycles with an overall throughput of 604 Mbps. We cover the general security of sponge functions in both a classical and quantum computing standpoint for hash functions, and offer a general architecture for HMAC computation when sponge functions are used.

2020-06-02
Krawec, Walter O..  2019.  Multi-Mediated Semi-Quantum Key Distribution. 2019 IEEE Globecom Workshops (GC Wkshps). :1—6.

A semi-quantum key distribution (SQKD) protocol allows two users A and B to establish a shared secret key that is secure against an all-powerful adversary E even when one of the users (e.g., B) is semi-quantum or classical in nature while the other is fully-quantum. A mediated SQKD protocol allows two semi-quantum users to establish a key with the help of an adversarial quantum server. We introduce the concept of a multi-mediated SQKD protocol where two (or more) adversarial quantum servers are used. We construct a new protocol in this model and show how it can withstand high levels of quantum noise, though at a cost to efficiency. We perform an information theoretic security analysis and, along the way, prove a general security result applicable to arbitrary MM-SQKD protocols. Finally, a comparison is made to previous (S)QKD protocols.

Ostrev, Dimiter.  2019.  Composable, Unconditionally Secure Message Authentication without any Secret Key. 2019 IEEE International Symposium on Information Theory (ISIT). :622—626.

We consider a setup in which the channel from Alice to Bob is less noisy than the channel from Eve to Bob. We show that there exist encoding and decoding which accomplish error correction and authentication simultaneously; that is, Bob is able to correctly decode a message coming from Alice and reject a message coming from Eve with high probability. The system does not require any secret key shared between Alice and Bob, provides information theoretic security, and can safely be composed with other protocols in an arbitrary context.

2020-06-01
Dhal, Subhasish, Bhuwan, Vaibhav.  2018.  Cryptanalysis and improvement of a cloud based login and authentication protocol. 2018 4th International Conference on Recent Advances in Information Technology (RAIT). :1–6.
Outsourcing services to cloud server (CS) becomes popular in these years. However, the outsourced services often involve with sensitive activity and CS naturally becomes a target of varieties of attacks. Even worse, CS itself can misuse the outsourced services for illegal profit. Traditional online banking system also can make use of a cloud framework to provide economical and high-speed online services to the consumers, which makes the financial dealing easy and convenient. Most of the banking organizations provide services through passbook, ATM, mobile banking, electronic banking (e-banking) etc. Among these, the e-banking and mobile banking are more convenient and becomes essential. Therefore, it is critical to provide an efficient, reliable and more importantly, secure e-banking services to the consumers. The cloud environment is suitable paradigm to a new, small and medium scale banking organization as it eliminates the requirement for them to start with small resources and increase gradually as the service demand rises. However, security is one of the main concerns since it deals with many sensitive data of the valuable customers. In addition to this, the access of various data needs to be restricted to prevent any unauthorized transaction. Nagaraju et al. presented a framework to achieve reliability and security in public cloud based online banking using multi-factor authentication concept. Unfortunately, the login and authentication protocol of this framework is prone to impersonation attack. In this paper, we have revised the framework to avoid this attack.
Jacomme, Charlie, Kremer, Steve.  2018.  An Extensive Formal Analysis of Multi-factor Authentication Protocols. 2018 IEEE 31st Computer Security Foundations Symposium (CSF). :1–15.
Passwords are still the most widespread means for authenticating users, even though they have been shown to create huge security problems. This motivated the use of additional authentication mechanisms used in so-called multi-factor authentication protocols. In this paper we define a detailed threat model for this kind of protocols: while in classical protocol analysis attackers control the communication network, we take into account that many communications are performed over TLS channels, that computers may be infected by different kinds of malwares, that attackers could perform phishing, and that humans may omit some actions. We formalize this model in the applied pi calculus and perform an extensive analysis and comparison of several widely used protocols - variants of Google 2-step and FIDO's U2F. The analysis is completely automated, generating systematically all combinations of threat scenarios for each of the protocols and using the P ROVERIF tool for automated protocol analysis. Our analysis highlights weaknesses and strengths of the different protocols, and allows us to suggest several small modifications of the existing protocols which are easy to implement, yet improve their security in several threat scenarios.
de Souza, Rick Lopes, Vigil, Martín, Custódio, Ricardo, Caullery, Florian, Moura, Lucia, Panario, Daniel.  2018.  Secret Sharing Schemes with Hidden Sets. 2018 IEEE Symposium on Computers and Communications (ISCC). :00713–00718.
Shamir's Secret Sharing Scheme is well established and widely used. It allows a so-called Dealer to split and share a secret k among n Participants such that at least t shares are needed to reconstruct k, where 0 \textbackslashtextbackslashtextless; t ≤ n. Nothing about the secret can be learned from less than t shares. To split secret k, the Dealer generates a polynomial f, whose independent term is k and the coefficients are randomly selected using a uniform distribution. A share is a pair (x, f(x)) where x is also chosen randomly using a uniform distribution. This scheme is useful, for example, to distribute cryptographic keys among different cloud providers and to create multi-factor authentication. The security of Shamir's Secret Sharing Scheme is usually analyzed using a threat model where the Dealer is trusted to split and share secrets as described above. In this paper, we demonstrate that there exists a different threat model where a malicious Dealer can compute shares such that a subset of less than t shares is allowed to reconstruct the secret. We refer to such subsets as hidden sets. We formally define hidden sets and prove lower bounds on the number of possible hidden sets for polynomials of degree t - 1. Yet, we show how to detect hidden sets given a set of n shares and describe how to create hidden sets while sharing a secret using a modification of Shamir's scheme.
2020-05-26
Hamamreh, Rushdi A., Ayyad, Mohammad, Jamoos, Mohammad.  2019.  RAD: Reinforcement Authentication DYMO Protocol for MANET. 2019 International Conference on Promising Electronic Technologies (ICPET). :136–141.
Mobile ad hoc network (MANET) does not have fixed infrastructure centralized server which manage the connections between the nodes. Rather, the nodes in MANET move randomly. Thus, it is risky to exchange data between nodes because there is a high possibility of having malicious node in the path. In this paper, we will describe a new authentication technique using message digest 5 (MD5), hashing for dynamic MANET on demand protocol (DYMO) based on reinforcement learning. In addition, we will describe an encryption technique that can be used without the need for a third party to distribute a secret key. After implementing the suggested model, results showed a remarkable enhancement in securing the path by increasing the packet delivery ratio and average throughput. On the other hand, there was an increase in end to end delay due to time spent in cryptographic operations.
Nithyapriya, J., Anandha Jothi, R., Palanisamy, V..  2019.  Protecting Messages Using Selective Encryption Based ESI Scheme for MANET. 2019 TEQIP III Sponsored International Conference on Microwave Integrated Circuits, Photonics and Wireless Networks (IMICPW). :50–54.
Mobile ad hoc network is a group of mobile nodes which have no centralized administrator. MANETs have dynamic topology since the nodes are moving. For this reason it is more prone to attacks that any node may be a misbehaving node. Every node acts as a router thereby it may lead the network with wrong routing. For these reasons MANETs have to be more protected than the wired networks. The mobile nodes will lavishly consume energy and so a security scheme that consumes less energy still provides ample protection to the messages have to be introduced. Here we propose an encryption scheme for the messages passing through MANET. The security scheme is based on selective encryption that is very robust, simple and with less computational capability.
2020-05-11
Chandre, Pankaj Ramchandra, Mahalle, Parikshit Narendra, Shinde, Gitanjali Rahul.  2018.  Machine Learning Based Novel Approach for Intrusion Detection and Prevention System: A Tool Based Verification. 2018 IEEE Global Conference on Wireless Computing and Networking (GCWCN). :135–140.
Now a day, Wireless Sensor Networks are widely used in military applications by its applications, it is extended to healthcare, industrial environments and many more. As we know that, there are some unique features of WSNs such as limited power supply, minimum bandwidth and limited energy. So, to secure traditional network, multiple techniques are available, but we can't use same techniques to secure WSNs. So to increase the overall security of WSNs, we required new ideas as well as new approaches. In general, intrusion prevention is the primary issue in WSNs and intrusion detection already reached to saturation. Thus, we need an efficient solution for proactive intrusion prevention towards WSNs. Thus, formal validation of protocols in WSN is an essential area of research. This research paper aims to formally verify as well as model some protocol used for intrusion detection using AVISPA tool and HLPSL language. In this research paper, the results of authentication and DoS attacks were detected is presented, but there is a need to prevent such type of attacks. In this research paper, a system is proposed in order to avoid intrusion using machine learning for the wireless sensor network. So, the proposed system will be used for intrusion prevention in a wireless sensor network.
2020-05-08
Hafeez, Azeem, Topolovec, Kenneth, Awad, Selim.  2019.  ECU Fingerprinting through Parametric Signal Modeling and Artificial Neural Networks for In-vehicle Security against Spoofing Attacks. 2019 15th International Computer Engineering Conference (ICENCO). :29—38.
Fully connected autonomous vehicles are more vulnerable than ever to hacking and data theft. The controller area network (CAN) protocol is used for communication between in-vehicle control networks (IVN). The absence of basic security features of this protocol, like message authentication, makes it quite vulnerable to a wide range of attacks including spoofing attacks. As traditional cybersecurity methods impose limitations in ensuring confidentiality and integrity of transmitted messages via CAN, a new technique has emerged among others to approve its reliability in fully authenticating the CAN messages. At the physical layer of the communication system, the method of fingerprinting the messages is implemented to link the received signal to the transmitting electronic control unit (ECU). This paper introduces a new method to implement the security of modern electric vehicles. The lumped element model is used to characterize the channel-specific step response. ECU and channel imperfections lead to a unique transfer function for each transmitter. Due to the unique transfer function, the step response for each transmitter is unique. In this paper, we use control system parameters as a feature-set, afterward, a neural network is used transmitting node identification for message authentication. A dataset collected from a CAN network with eight-channel lengths and eight ECUs to evaluate the performance of the suggested method. Detection results show that the proposed method achieves an accuracy of 97.4% of transmitter detection.
Boakye-Boateng, Kwasi, Lashkari, Arash Habibi.  2019.  Securing GOOSE: The Return of One-Time Pads. 2019 International Carnahan Conference on Security Technology (ICCST). :1—8.

IEC 61850 is an international standard that is widely used in substation automation systems (SAS) in smart grids. During its development, security was not considered thus leaving SAS vulnerable to attacks from adversaries. IEC 62351 was developed to provide security recommendations for SAS against (distributed) denial-of-service, replay, alteration, spoofing and detection of devices attacks. However, real-time communications, which require protocols such as Generic Object-Oriented Substation Event (GOOSE) to function efficiently, cannot implement these recommendations due to latency constraints. There has been researching that sought to improve the security of GOOSE messages, however, some cannot be practically implemented due to hardware requirements while others are theoretical, even though latency requirements were met. This research investigates the possibility of encrypting GOOSE messages with One- Time Pads (OTP), leveraging the fact that encryption/decryption processes require the random generation of OTPs and modulo addition (XOR), which could be a realistic approach to secure GOOSE while maintaining latency requirements. Results show that GOOSE messages can be encrypted with some future work required.

2020-05-04
Karmakar, Kallol Krishna, Varadharajan, Vijay, Nepal, Surya, Tupakula, Uday.  2019.  SDN Enabled Secure IoT Architecture. 2019 IFIP/IEEE Symposium on Integrated Network and Service Management (IM). :581–585.
The Internet of Things (IoT) is increasingly being used in applications ranging from precision agriculture to critical national infrastructure by deploying a large number of resource-constrained devices in hostile environments. These devices are being exploited to launch attacks in cyber systems. As a result, security has become a significant concern in the design of IoT based applications. In this paper, we present a security architecture for IoT networks by leveraging the underlying features supported by Software Defined Networks (SDN). Our security architecture restricts network access to authenticated IoT devices. We use fine granular policies to secure the flows in the IoT network infrastructure and provide a lightweight protocol to authenticate IoT devices. Such an integrated security approach involving authentication of IoT devices and enabling authorized flows can help to protect IoT networks from malicious IoT devices and attacks.
2020-04-06
Mumtaz, Majid, Akram, Junaid, Ping, Luo.  2019.  An RSA Based Authentication System for Smart IoT Environment. 2019 IEEE 21st International Conference on High Performance Computing and Communications; IEEE 17th International Conference on Smart City; IEEE 5th International Conference on Data Science and Systems (HPCC/SmartCity/DSS). :758–765.
Authentication is the fundamental security service used in almost all remote applications. All such sensitive applications over an open network need authentication mechanism that should be delivered in a trusted way. In this paper, we design an RSA based authentication system for smart IoT environment over the air network using state-of-the-art industry standards. Our system provide security services including X.509 certificate, RSA based Public Key Infrastructure (PKI), challenge/response protocols with the help of proxy induced security service provider. We describe an innovative system model, protocol design, system architecture and evaluation against known threats. Also the implemented solution designed as an add on service for multiple other sensitive applications (smart city apps, cyber physical systems etc.) which needs the support of X.509 certificate based on hard tokens to populate other security services including confidentiality, integrity, non-repudiation, privacy and anonymity of the identities. The proposed scheme is evaluated against known vulnerabilities and given detail comparisons with popular known authentication schemes. The result shows that our proposed scheme mitigate all the known security risks and provide highest level assurance to smart gadgets.
Erfani, Shervin, Ahmadi, Majid.  2019.  Bitcoin Security Reference Model: An Implementation Platform. 2019 International Symposium on Signals, Circuits and Systems (ISSCS). :1–5.
Bitcoin is a cryptocurrency which acts as an application protocol that works on top of the IP protocol. This paper focuses on distinct Bitcoin security features, including security services, mechanisms, and algorithms. Further, we propose a well-defined security functional architecture to minimize security risks. The security features and requirements of Bitcoin have been structured in layers.
2020-04-03
Lipp, Benjamin, Blanchet, Bruno, Bhargavan, Karthikeyan.  2019.  A Mechanised Cryptographic Proof of the WireGuard Virtual Private Network Protocol. 2019 IEEE European Symposium on Security and Privacy (EuroS P). :231—246.

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.