AN APPLICATION OF ESOP EXPRESSIONS TO SECURE COMPUTATIONS

2007 ◽  
Vol 16 (02) ◽  
pp. 191-198 ◽  
Author(s):  
TAKAAKI MIZUKI ◽  
TARO OTAGIRI ◽  
HIDEAKI SONE
Keyword(s):  
Minimal Model ◽  
Communication Complexity ◽  
Cryptographic Protocols ◽  
Historical Research ◽  
Cryptographic Protocol ◽  
Sum Of Products ◽  
Exclusive Or

This paper gives an application of exclusive-or sum-of-products (ESOP) expressions to designing cryptographic protocols. That is, this paper deals with secure computations in a minimal model, and gives a protocol which securely computes every function by means of the techniques of ESOP expressions. The communication complexity of our protocol is proportional to the size of an obtained multiple-valued-input ESOP expression. Since the historical research on minimizing ESOP expressions is now still active, our protocol will "automatically" turn to an efficient one as this research progresses. Thus, we hope that the existence of our cryptographic protocol would motivate further research on minimizing ESOP expressions.

USING SIMPLE DISJOINT DECOMPOSITION TO PERFORM SECURE COMPUTATIONS

2010 ◽  
Vol 19 (07) ◽  
pp. 1559-1569 ◽  
Author(s):  
MARINOS SAMPSON ◽  
DIMITRIOS VOUDOURIS ◽  
GEORGE PAPAKONSTANTINOU
Keyword(s):  
Minimal Model ◽  
Quantum Algorithms ◽  
Cryptographic Protocols ◽  
Secure Computation ◽  
Minimal Models ◽  
Function Decomposition ◽  
Exclusive Or

This paper deals with the use of a minimal model for performing secure computations. The communication is based on a protocol which makes use of disjoint function decomposition and more precisely of minimal ESCT (Exclusive-or Sum of Complex Terms) expressions in order to perform a secure computation. The complexity of this protocol is directly proportional to the size of the ESCT expression in use, which is much smaller in comparison to other proposed minimal models (e.g., ESOP). Moreover, quantum algorithms are discussed that provide significant speedup to the process of producing the ESCT expressions, when compared to conventional ones. Hence, this paper provides a very useful application of the ESCT expressions in the field of cryptographic protocols.

scholarly journals Verification of stateful cryptographic protocols with exclusive OR

2020 ◽  
Vol 28 (1) ◽  
pp. 1-34
Author(s):  
Jannik Dreier ◽  
Lucca Hirschi ◽  
Saša Radomirović ◽  
Ralf Sasse
Keyword(s):  
Cryptographic Protocols ◽  
Exclusive Or

A FRAMEWORK FOR A CRYPTOGRAPHIC PROTOCOL EVALUATION WORKBENCH

2001 ◽  
Vol 08 (04) ◽  
pp. 373-389 ◽  
Author(s):  
ALEC YASINSAC ◽  
WILLIAM A. WULF
Keyword(s):  
Evaluation Methods ◽  
Cryptographic Protocols ◽  
Ban Logic ◽  
Cryptographic Protocol ◽  
Evaluation Tools ◽  
Protocol Evaluation

Tools to evaluate Cryptographic Protocols (CPs) exploded into the literature after development of BAN Logic.2,3 Many of these were created to repair weaknesses in BAN Logic. Unfortunately, these tools are all complex and difficult to implement individually, with little or no effort available to implement multiple tools in a workbench environment. We propose a framework that allows a protocol analyst to exercise multiple CP evaluation tools in a single environment. Moreover, this environment exhibits characteristics that will enhance the effectiveness of the CP evaluation methods themselves.

COOPERATIVE RECONFIGURATION OF USER INTERFACE MODELS FOR LEARNING CRYPTOGRAPHIC PROTOCOLS

2012 ◽  
Vol 11 (06) ◽  
pp. 1127-1154 ◽  
Author(s):  
BENJAMIN WEYERS ◽  
WOLFRAM LUTHER ◽  
NELSON BALOIAN
Keyword(s):  
User Interface ◽  
User Interfaces ◽  
Evaluation Study ◽  
Cryptographic Protocols ◽  
Traditional Learning ◽  
Cryptographic Protocol ◽  
Formal Approach ◽  
Modeling Tools ◽  
Learning Success ◽  
Learning Scenarios

Cooperative work in learning environments has been shown to be a successful extension to traditional learning systems due to the great impact of cooperation on students' motivation and learning success. A recent evaluation study has confirmed our hypothesis that students who constructed their roles in a cryptographic protocol cooperatively as sequence of actions in a user interface were faster in finding a correct solution than students who worked on their own. Here, students of a cooperation group modeled a user interface collaboratively for simulation of a cryptographic protocol using interactive modeling tools on a shared touch screen. In this paper, we describe an extended approach to cooperative construction of cryptographic protocols. Using a formal language for modeling and reconfiguring user interfaces, students describe a protocol step-by-step, modeling subsequent situations and thereby actions of the protocol. The system automatically generates a colored Petri net, which is matched against an existing action logic specifying the protocol, thus allowing formal validation of the construction process. The formal approach to modeling of user interfaces covers a much broader field than a simple cryptographic protocol simulation. Still, this paper seeks at investigating the use of such a formal modeling approach in the context of cooperative learning of cryptographic protocols and to develop a basis for more complex learning scenarios.

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.

A PARALLEL ALGORITHM FOR MINIMIZING ESOP EXPRESSIONS

2014 ◽  
Vol 23 (01) ◽  
pp. 1450015 ◽  
Author(s):  
GEORGE PAPAKONSTANTINOU
Keyword(s):  
Boolean Function ◽  
Parallel Algorithms ◽  
Parallel Algorithm ◽  
Minimization Problem ◽  
Processing Time ◽  
Symmetric Functions ◽  
Sum Of Products ◽  
Speed Up ◽  
Exclusive Or

Two parallel algorithms are proposed in this paper for solving the problem of finding exact exclusive-or sum of products (ESOP) expressions for an arbitrary Boolean function. This minimization problem is a very difficult one and solutions have been proposed only for up to seven variables. The processing time for some symmetric functions of seven variables is of the order of weeks. The proposed algorithm is a hybrid one (OpenMP, MPI) and a speed-up of more than nine could be achieved, for a cluster of three nodes with four cores each.

scholarly journals Optimization of ProVerif programs for AKE-protocols

2021 ◽  
Vol 33 (5) ◽  
pp. 105-116
Author(s):  
Evgenii Maksimovich Vinarskii ◽  
Alexey Vasilyevich Demakov
Keyword(s):  
Formal Verification ◽  
Formal Methods ◽  
Distinctive Feature ◽  
Formal Specification ◽  
Cryptographic Protocols ◽  
Experimental Results ◽  
Automatic Verification ◽  
Cryptographic Protocol ◽  
Encryption Scheme ◽  
Program Model

Cryptographic protocols are used to establish a secure connection between “honest” agents who communicate strictly in accordance with the rules of the protocol. In order to make sure that the designed cryptographic protocol is cryptographically strong, various software tools are usually used. However, an adequate specification of a cryptographic protocol is usually presented as a set of requirements for the sequences of transmitted messages, including the format of such messages. The fulfillment of all these requirements leads to the fact that the formal specification for a real cryptographic protocol becomes cumbersome, as a result of which it is difficult to analyze it by formal methods. One of such rapidly developing tools for formal verification of cryptographic protocols is ProVerif. A distinctive feature of the ProVerif tool is that with large protocols, it often fails to analyze them, i.e. it can neither prove the security of the protocol nor refute it. In such cases, they resort either to the approximation of the problem, or to equivalent transformations of the program model in the ProVerif language, simplifying the ProVerif model. In this article, we propose a way to simplify the ProVerif specifications for AKE protocols using the El Gamal encryption scheme. Namely, we suggest equivalent transformations that allow us to construct a ProVerif specification that simplifies the analysis of the specification for the ProVerif tool. Experimental results for the Needham-Schroeder and Yahalom cryptoprotocols show that such an approach can be promising for automatic verification of real protocols.

scholarly journals My Genome Belongs to Me: Controlling Third Party Computation on Genomic Data

2019 ◽  
Vol 2019 (1) ◽  
pp. 108-132 ◽  
Author(s):  
Dominic Deuber ◽  
Christoph Egger ◽  
Katharina Fech ◽  
Giulio Malavolta ◽  
Dominique Schröder ◽  
...  
Keyword(s):  
Communication Complexity ◽  
Personal Information ◽  
Genomic Data ◽  
Computable Function ◽  
Third Party ◽  
Cryptographic Protocol ◽  
Time Data ◽  
Critical Feature ◽  
Garbled Circuits ◽  
Data Owner

Abstract An individual’s genetic information is possibly the most valuable personal information. While knowledge of a person’s DNA sequence can facilitate the diagnosis of several heritable diseases and allow personalized treatment, its exposure comes with significant threats to the patient’s privacy. Currently known solutions for privacy-respecting computation require the owner of the DNA to either be heavily involved in the execution of a cryptographic protocol or to completely outsource the access control to a third party. This motivates the demand for cryptographic protocols which enable computation over encrypted genomic data while keeping the owner of the genome in full control. We envision a scenario where data owners can exercise arbitrary and dynamic access policies, depending on the intended use of the analysis results and on the credentials of who is conducting the analysis. At the same time, data owners are not required to maintain a local copy of their entire genetic data and do not need to exhaust their computational resources in an expensive cryptographic protocol. In this work, we present METIS, a system that assists the computation over encrypted data stored in the cloud while leaving the decision on admissible computations to the data owner. It is based on garbled circuits and supports any polynomially-computable function. A critical feature of our system is that the data owner is free from computational overload and her communication complexity is independent of the size of the input data and only linear in the size of the circuit’s output. We demonstrate the practicality of our approach with an implementation and an evaluation of several functions over real datasets.

Sign in / Sign up

Export Citation Format

Share Document