scholarly journals A Method for the Construction of a Cryptographic Group-theoretic Language

2017 ◽  
Vol 3 (4) ◽  
pp. 105-114
Author(s):  
T.J Odule ◽  
◽  
O.A kaka
Keyword(s):  
Cryptographic Protocols ◽  
Cryptographic Protocol ◽  
Hash Family ◽  
Universal Hashing ◽  
Protocol Group

This paper generalizes the theory of universal hashing in the construction of cryptographic protocols using group- theoretic language formalisms. This idea is due to Wegman and Carter who gave a construction in 1981 which is extremely useful when the number of authenticators is small compared to the number of possible source states (plaintext messages) in order to accommodate the situation where we would like to authenticate a sequence of messages with the same key. Unlike previous methods for doing this we do not require that each message in the sequence have a “counter” attached to it. We provide necessary definitions and theory and then give a construction which achieves our goals. Keywords: Universal hashing, projective hash family, cryptographic protocol, group-theoretic language,

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 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.

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.

Cryptographic Protocols

2017 ◽  
Author(s):  
Keith M. Martin
Keyword(s):  
Cryptographic Protocols ◽  
Cryptographic Protocol ◽  
Important Class ◽  
Key Establishment ◽  
Diffie Hellman

This chapter is concerned with cryptographic protocols. We begin with an explanation of what components a cryptographic protocol consists of. We then illustrate the complexity of designing a secure cryptographic protocol by considering an artificially simple scenario, for which we propose and analyse seven candidate protocols. For each of these protocols, we comment on whether, or under which conditions, they meet the required specification. We go on to look at the important class of authentication and key establishment protocols. We identify typical goals and examine some important protocols in this class, including the Diffie–Hellman protocol.

scholarly journals Asymmetric cryptographic protocols with a blockchain core: development problems and their solutions

2021 ◽  
pp. 175-180
Author(s):  
Anton Kudin ◽  
Polina Seliukh
Keyword(s):  
Secret Sharing ◽  
Cryptographic Protocols ◽  
Cryptographic Protocol ◽  
Interactive Proof ◽  
Axiomatic Construction

The problem of axiomatic construction of secure cryptographic protocols is closely related to the choice of basic cryptographic blocks from which a cryptographic protocol of arbitrary complexity can be built. Let’s call such blocks primitive cryptographic protocols. Along with a traditional choice as primitive secret sharing protocols and non-interactive proof protocols today blockchain is considered to be a primitive cryptographic protocol. The security of such cryptographic protocols with a blockchain core is studied a bit today. We consider the methods for increasing the security of protocols with blockchain core by using a new agreement protocol in the blockchain, which is secure in the information theoretically sense.

Cryptographic Protocol Verification Based on the Extension Rule

2014 ◽  
Vol 644-650 ◽  
pp. 3181-3184
Author(s):  
Hai Lin
Keyword(s):  
Formal Methods ◽  
Theorem Proving ◽  
Formal Method ◽  
Cryptographic Protocols ◽  
Strong Sense ◽  
Protocol Verification ◽  
Cryptographic Protocol ◽  
Effective Technique ◽  
Extension Rule

The design of cryptographic protocols is error-prone. People have found serious security flaws in major cryptographic protocols. In recent years, people use formal methods to guarantee the correctness of cryptographic protocols in a strong sense. Resolution-based theorem proving is a widely-used formal method, but there are other techniques as well. For example, the extension rule is another technique used to prove things formally. In this paper, we propose to prove the correctness of cryptographic protocols based on the extension rule. We show that this is an effective technique, which can help to find the security flaws in major cryptographic protocols.

scholarly journals Formalisation of Bayesian concealment

2021 ◽  
Author(s):  
Izumi Takeuti
Keyword(s):  
Probability Theory ◽  
Secret Sharing ◽  
Cryptographic Protocols ◽  
Cryptographic Protocol ◽  
Secret Sharing Scheme ◽  
Logical System ◽  
Effective Measure ◽  
Sharing Scheme ◽  
Contemporary Context

AbstractIn order to assure the concealment by cryptographic protocols, it is an effective measure to prove the concealment in a formal logical system. In the contemporary context of cryptographic protocol, the concealment has to be proved by using probability theory. There are several concepts of concealment in probability theory. One of them is Bayesian concealment. This study proposes a formal logical system to prove the Bayesian concealment of a secret sharing scheme.

Security Analysis of Wireless Authentication Protocols

2019 ◽  
Vol 9 (2) ◽  
pp. 247-252 ◽  
Author(s):  
Ashish Joshi ◽  
Amar Kumar Mohapatra
Keyword(s):  
Execution Time ◽  
Communication Systems ◽  
Security Analysis ◽  
Cryptographic Protocols ◽  
Command Line ◽  
Time Analysis ◽  
Authentication Protocols ◽  
Replay Attack ◽  
Peer Communication ◽  
Digital Communication Systems

Background & Objective: Cryptographic protocols had been evident method for ensuring con dentiality, Integrity and authentication in various digital communication systems. However the validation and analysis of such cryptographic protocols was limited to usage of formal mathematical models until few years back. Methods: In this paper, various popular cryptographic protocols have been studied. Some of these protocols (PAP, CHAP, and EAP) achieve security goals in peer to peer communication while others (RADIUS, DIAMETER and Kerberos) can work in multiparty environment. These protocols were validated and analysed over two popular security validation and analysis tools AVISPA and Scyther. The protocols were written according to their documentation using the HLPSL and SPDL for analysis over AVISPA and Scyther respectively. The results of these tools were analysed to nd the possible attack an each protocol. Afterwards The execution time analysis of the protocols were done by repeating the experiment for multiple iterations over the command line versions of these tools.As the literature review suggested, this research also validates that using password based protocols (PAP) is faster in terms of execution time as compared to other methods, Usage of nonces tackles the replay attack and DIAMETER is secure than RADIUS. Results and Conclusion: The results also showed us that DIAMETER is faster than RADIUS. Though Kerberos protocol was found to safe, the results tell us that it is compromisable under particular circumstances.

Sign in / Sign up

Export Citation Format

Share Document