Automated Analysis of Diffie-Hellman Protocols and Advanced Security Properties

2012 ◽  
Author(s):  
Benedikt Schmidt ◽  
Simon Meier ◽  
Cas Cremers ◽  
David Basin
Keyword(s):  
Automated Analysis ◽  
Diffie Hellman ◽  
Security Properties

scholarly journals Functional Encryption for Pattern Matching with a Hidden String

Cryptography ◽  
2021 ◽  
Vol 6 (1) ◽  
pp. 1
Author(s):  
Jongkil Kim ◽  
Yang-Wai Chow ◽  
Willy Susilo ◽  
Joonsang Baek ◽  
Intae Kim
Keyword(s):  
Access Control ◽  
Pattern Matching ◽  
Public Information ◽  
Functional Encryption ◽  
Fine Grained ◽  
Private Key ◽  
Diffie Hellman ◽  
Data Owner ◽  
Security Properties

We propose a new functional encryption for pattern matching scheme with a hidden string. In functional encryption for pattern matching (FEPM), access to a message is controlled by its description and a private key that is used to evaluate the description for decryption. In particular, the description with which the ciphertext is associated is an arbitrary string w and the ciphertext can only be decrypted if its description matches the predicate of a private key which is also a string. Therefore, it provides fine-grained access control through pattern matching alone. Unlike related schemes in the literature, our scheme hides the description that the ciphertext is associated with. In many practical scenarios, the description of the ciphertext cannot be public information as an attacker may abuse the message description to identify the data owner or classify the target ciphertext before decrypting it. Moreover, some data owners may not agree to reveal any ciphertext information since it simply gives greater advantage to the adversary. In this paper, we introduce the first FEPM scheme with a hidden string, such that the adversary cannot get any information about the ciphertext from its description. The security of our scheme is formally analyzed. The proposed scheme provides both confidentiality and anonymity while maintaining its expressiveness. We prove these security properties under the interactive general Diffie–Hellman assumption (i-GDH) and a static assumption introduced in this paper.

scholarly journals Scrutinizing the Vulnerability of Ephemeral Diffie–Hellman over COSE (EDHOC) for IoT Environment Using Formal Approaches

2021 ◽  
Vol 2021 ◽  
pp. 1-18
Author(s):  
Jiyoon Kim ◽  
Daniel Gerbi Duguma ◽  
Sangmin Lee ◽  
Bonam Kim ◽  
JaeDeok Lim ◽  
...  
Keyword(s):  
Task Force ◽  
Mutual Authentication ◽  
Key Exchange ◽  
Security Environment ◽  
Diffie Hellman ◽  
Verification Methods ◽  
Security Properties ◽  
Perfect Forward Secrecy ◽  
Resource Exhaustion ◽  
Future Work

Most existing conventional security mechanisms are insufficient, mainly attributable to their requirements for heavy processing capacity, large protocol message size, and longer round trips, for resource-intensive devices operating in an Internet of Things (IoT) context. These devices necessitate efficient communication and security protocols that are cognizant of the severe resource restrictions regarding energy, computation, communication, and storage. To realize this, the IETF (Internet Engineering Task Force) is currently working towards standardizing an ephemeral key-based lightweight and authenticated key exchange protocol called EDHOC (Ephemeral Diffie–Hellman over COSE). The protocol’s primary purpose is to build an OSCORE (Object Security for Constrained RESTful Environments) security environment by supplying crucial security properties such as secure key exchange, mutual authentication, perfect forward secrecy, and identity protection. EDHOC will most likely dominate IoT security once it becomes a standard. It is, therefore, imperative to inspect the protocol for any security flaw. In this regard, two previous studies have shown different security vulnerabilities of the protocol using formal security verification methods. Yet, both missed the vital security flaws we found in this paper: resource exhaustion and privacy attacks. In finding these vulnerabilities, we leveraged BAN-Logic and AVISPA to formally verify both EDHOC protocol variants. Consequently, we described these security flaws together with the results of the related studies and put forward recommended solutions as part of our future work.

scholarly journals Formal verification of the YubiKey and YubiHSM APIs in Maude-NPA

10.29007/c4xk ◽  
2018 ◽  
Author(s):  
Antonio González-Burgueño ◽  
Damián Aparicio-Sánchez ◽  
Santiago Escobar ◽  
Catherine Meadows ◽  
José Meseguer
Keyword(s):  
Automated Analysis ◽  
Cryptographic Protocol ◽  
Protocol Composition ◽  
Limited Support ◽  
Security Properties ◽  
Security Module ◽  
Complex Features ◽  
Exclusive Or ◽  
Event Based ◽  
Recent Version

We perform an automated analysis of two devices developed by Yubico: YubiKey, de- signed to authenticate a user to network-based services, and YubiHSM, Yubico’s hardware security module. Both are analyzed using the Maude-NPA cryptographic protocol an- alyzer. Although previous work has been done applying formal tools to these devices, there has not been any completely automated analysis. This is not surprising, because both YubiKey and YubiHSM, which make use of cryptographic APIs, involve a number of complex features: (i) discrete time in the form of Lamport clocks, (ii) a mutable memory for storing previously seen keys or nonces, (iii) event-based properties that require an analysis of sequences of actions, and (iv) reasoning modulo exclusive-or. Maude-NPA has provided support for exclusive-or for years but has not provided support for the other three features, which we show can also be supported by using constraints on natural numbers, protocol composition and reasoning modulo associativity. In this work, we have been able to automatically prove security properties of YubiKey and find the known at- tacks on the YubiHSM, in both cases beyond the capabilities of previous work using the Tamarin Prover due to the need of auxiliary user-defined lemmas and limited support for exclusive-or. Tamarin has recently been endowed with exclusive-or and we have rewritten the original specification of YubiHSM in Tamarin to use exclusive-or, confirming that both attacks on YubiHSM can be carried out by this recent version of Tamarin.

scholarly journals Network Security System with Optimized Randomized Multiple Key Exchange Algorithm

2020 ◽  
Vol 9 (3) ◽  
pp. 1075-1080
Keyword(s):  
Network Security ◽  
Elliptic Curve ◽  
Key Exchange ◽  
Memory Requirement ◽  
Secret Key ◽  
Diffie Hellman ◽  
Shared Secret ◽  
Security Properties ◽  
Diffie Hellman Key Exchange ◽  
Shared Secret Key

This paper illustrates three different algorithms to provide shared secret key for security of the system. The proposed three algorithms namely 1) Modified Simple Password Key Exchange Scheme 2) Modified Diffie-Hellman Key exchange Scheme 3) Modified Elliptic Curve Scheme are meant to provide shared secret key for authentication process. Enhancements in terms of memory requirement, storage and other security properties such as authentication among mutual users, fraud prevention, attack etc., prove the validity of the proposed algorithms in proving authentication for the cryptographic identification of networks

Distributed Group Key Management for Secure Electronic Communication

2013 ◽  
Vol 385-386 ◽  
pp. 1591-1594
Author(s):  
Qiu Na Niu
Keyword(s):  
Key Management ◽  
Electronic Communication ◽  
Security Analysis ◽  
Group Key Management ◽  
Forward Secrecy ◽  
Group Key ◽  
Management Scheme ◽  
Diffie Hellman ◽  
Security Properties ◽  
Group Members

With the popularity of group-oriented applications, secure electronic communication among all group members has become a major issue. This paper proposes a distributed group-oriented key management scheme for secure electronic communication. The scheme deploys Elliptic Curve Diffie-Hellman (ECDH) which is more lightweight as compared to regular Diffie-Hellman. According to the security analysis, the proposed scheme provides a number of desirable security properties, including group key secrecy, forward secrecy and backward secrecy.

An IBE-Based Authenticated Key Transfer Protocol on Elliptic Curves

2020 ◽  
pp. 1112-1122
Author(s):  
Daya Sagar Gupta
Keyword(s):  
Elliptic Curve ◽  
Computational Cost ◽  
Session Key ◽  
Private Key ◽  
Diffie Hellman ◽  
Security Properties ◽  
Hard Problems ◽  
Identity Based ◽  
Symmetric Key ◽  
Transfer Protocol

The key exchanged using key transfer protocols is generally used for symmetric key encryption where this key is known as private key and used for both encryption as well as decryption. As we all know, many key transfer protocols including basic Diffie-Hellman protocol are proposed in the literature. However, many of these key transfer protocols either are proven insecure or had a burden of communication and computational cost. Therefore, a more secure and efficient key transfer protocol is needed. In this article, the author proposes an authenticated key transfer protocol that securely and efficiently negotiates a common session key between two end users. He calls this protocol as IBE-TP-AKE. This proposal is based on the elliptic-curve cryptography (ECC) and uses the idea of identity-based encryption (IBE) with pairing. The security of the proposed work is based on the hard problems of elliptic curve and their pairing. Further, the author has shown the security of his proposed protocol and proved it using the security properties discussed later.

Development and study of a method for cell separation during white blood cell segmentation on images of bone marrow preparations in information and measurement systems for diagnostics of acute leukemia

2020 ◽  
pp. 68-72
Author(s):  
V.G. Nikitaev ◽  
A.N. Pronichev ◽  
V.V. Dmitrieva ◽  
E.V. Polyakov ◽  
A.D. Samsonova ◽  
...  
Keyword(s):  
Bone Marrow ◽  
Blood Cell ◽  
Acute Leukemia ◽  
White Blood Cell ◽  
Cell Separation ◽  
Large Scale ◽  
Bone Marrow Cells ◽  
Automated Analysis ◽  
Cell Segmentation ◽  
Measurement Systems

The issues of using of information and measurement systems based on processing of digital images of microscopic preparations for solving large-scale tasks of automating the diagnosis of acute leukemia are considered. The high density of leukocyte cells in the preparation (hypercellularity) is a feature of microscopic images of bone marrow preparations. It causes the proximity of cells to eachother and their contact with the formation of conglomerates. Measuring of the characteristics of bone marrow cells in such conditions leads to unacceptable errors (more than 50%). The work is devoted to segmentation of contiguous cells in images of bone marrow preparations. A method of cell separation during white blood cell segmentation on images of bone marrow preparations under conditions of hypercellularity of the preparation has been developed. The peculiarity of the proposed method is the use of an approach to segmentation of cell images based on the watershed method with markers. Key stages of the method: the formation of initial markers and builds the lines of watershed, a threshold binarization, shading inside the outline. The parameters of the separation of contiguous cells are determined. The experiment confirmed the effectiveness of the proposed method. The relative segmentation error was 5 %. The use of the proposed method in information and measurement systems of computer microscopy for automated analysis of bone marrow preparations will help to improve the accuracy of diagnosis of acute leukemia.

Sign in / Sign up

Export Citation Format

Share Document