A Formal Model for Analyzing Fair Exchange Protocols Based on Event Logic

Fair exchange protocols play a critical role in enabling two distrustful entities to conduct electronic data exchanges in a fair and secure manner.These protocols are widely used in electronic payment systems and electronic contract signing,ensuring the reliability and security of network transactions.In order to address the limitations of current research methods and enhance the analytical capabilities for fair exchange protocols,this paper proposes a formal model for analyzing such protocols.The proposed model begins with a thorough analysis of fair exchange protocols,followed by the formal definition of fairness.This definition accurately captures the inherent requirements of fair exchange protocols.Building upon event logic,the model incorporates the time factor into predicates and introduces knowledge set axioms.This enhancement empowers the improved logic to effectively describe the state and knowledge of protocol participants at different time points,facilitating reasoning about their acquired knowledge.To maximize the intruder’s capabilities,channel errors are translated into the behaviors of the intruder.The participants are further categorized into honest participants and malicious participants,enabling a comprehensive evaluation of the intruder’s potential impact.By employing a typical fair exchange protocol as an illustrative example,this paper demonstrates the detailed steps of utilizing the proposed model for protocol analysis.The entire process of protocol execution under attack scenarios is presented,shedding light on the underlying reasons for the attacks and proposing corresponding countermeasures.The developedmodel enhances the ability to reason about and evaluate the security properties of fair exchange protocols,thereby contributing to the advancement of secure network transactions.

Security Analysis of Broadcaster Group Key Exchange Protocols

Group key exchange protocols are basic protocols to provide privacy and integrity in secure group communication. This paper discusses the security of one type of group key exchange protocols and defines the kind of protocols as broadcaster group protocols. It points out two attacks on this kind of protocols. The first attack can be avoided by using fresh values in each action during one session of the group protocol. The second attack should be related with concrete application. It also proposes a dynamic key agreement protocol as an example of solutions at the last part of the paper.

STRONGER PROVABLE SECURE MODEL FOR KEY EXCHANGE

The key exchange is a fundamental building block in the cryptography. Several provable security models for the key exchange protocol are proposed. To determine the exact properties required by the protocols, a single unified security model is essential, The eCK , eCK and CK models are examined and the result is proved that the eCK＇ model is the strongest provable security model for the key exchange. The relative security strength among these models is analyzed. To support the implication or non-implication relations among these models, the formal proofs and the counter-examples are given.

A Resistant Quantum Key Exchange Protocol and Its Corresponding Encryption Scheme

The emergence of quantum computer will threaten the security of existing public-key cryptosystems, including the Diffie Hellman key exchange protocol, encryption scheme and etc, and it makes the study of resistant quantum cryptography very urgent. This motivate us to design a new key exchange protocol and eneryption scheme in this paper. Firstly, some acknowledged mathematical problems was introduced, such as ergodic matrix problem and tensor decomposition problem, the two problems have been proved to NPC hard. From the computational complexity prospective, NPC problems have been considered that there is no polynomial-time quantum algorithm to solve them. From the algebraic structures prospective, non-commutative cryptography has been considered to resist quantum. The matrix and tensor operator we adopted also satisfied with this non-commutative algebraic structures, so they can be used as candidate problems for resisting quantum from perspective of computational complexity theory and algebraic structures. Secondly, a new problem was constructed based on the introduced problems in this paper, then a key exchange protocol and a public key encryption scheme were proposed based on it. Finally the security analysis, efficiency, recommended parameters, performance evaluation and etc. were also been given. The two schemes has the following characteristics, provable security,security bits can be scalable, to achieve high efficiency, quantum resistance, and etc.

Universally Composable Symbolic Analysis of Group Key Exchange Protocol

Canetti and Herzog have already proposed universally composable symbolic analysis(UCSA) to analyze mutual authentication and key exchange protocols. However,they do not analyze group key exchange protocol. Therefore,this paper explores an approach to analyze group key exchange protocols,which realize automation and guarantee the soundness of cryptography. Considered that there exist many kinds of group key exchange protocols and the participants’ number of each protocol is arbitrary. So this paper takes the case of Burmester-Desmedt(BD) protocol with three participants against passive adversary(3-BD-Passive) . In a nutshell,our works lay the root for analyzing group key exchange protocols automatically without sacrificing soundness of cryptography.

CLORKE-SFS:Certificateless One-Round Key Exchange Protocol with Strong Forward Security in Limited Communication Scenarios

Certificateless one-round key exchange(CL-ORKE)protocols enable each participant to share a common key with only one round of communication which greatly saves communication cost.CLORKE protocols can be applied to scenarios with limited communication,such as space communication.Although CL-ORKE protocols have been researched for years,lots of them only consider what secrets can be compromised but ignore the time when the secrets have been corrupted.In CL-ORKE protocols,the reveal of the long-term key attacks can be divided into two different attacks according to the time of the long-term key revealed:the attack to weak Forward Security(wFS)and the attack to strong Forward Security(sFS).Many CLKE protocols did not take into account the sFS property or considered sFS as wFS.In this paper,we first propose a new security model for CL-ORKE protocols which considers the sFS property as well as the Ephemeral Key Reveal attack.Then,we give a CL-ORKE protocol which is called CLORKE-SFS.CLORKE-SFS is provably secure under the proposed model provided the Elliptic Curve Computational Diffie-Hellman(ECCDH)and the Bilinear Computational Diffie-Hellman problem(BCDH)assumption hold.The security model and the protocol may give inspiration for constructing oneround key exchange protocols with perfect forward security in certificateless scenarios.

EECDH to prevent MITM attack in cloud computing

Cloud computing has reached the peak of Gartner hype cycle,and now the focus of the whole telecom industry is the ability to scale data storage with minimal investment.But data privacy and communication issues will occur with the increment of the cloud data storage.The key privacy concern for scalability is caused by the dynamic membership allocation and multi-owner data sharing.This paper addresses the issues faced by multiple owners through a mutual authentication mechanism using the Enhanced Elliptic Curve Diffie-Hellman(EECDH)key exchange protocol along with the Elliptic Curve Digital Signature Algorithm(ECDSA).The proposed EECDH scheme is used to exchange the secured shared key among multiple owners and also to eliminate the Man-In-The-Middle(MITM)attacks with less computational complexity.By leveraging these algorithms,the integrity of data sharing among multiple owners is ensured.The EECDH improves the level of security only slightly increasing the time taken to encrypt and decrypt the data,and it is secured against the MITM attacks,which is experimented using the AVISPA tool.

Formal Verification in 3oux Tripartite Diffie-Hellman Protocol

Security analysis of cryptographic protocols has been widely studied for many years.As far as we know,we have not found any methods to effectively analyze group key exchange protocols for the three parties yet,which did not sacrifice the soundness of cryptography.Recently,Canetti and Herzog have proposed Universally Composable Symbolic Analysis(UCSA) of two-party mutual authentication and key exchange protocol which is based on the symmetric encryption schemes.This scheme can analyze the protocols automatically and guarantee the soundness of cryptography.Therefore,we discuss group key exchange protocol which is based on Joux Tripartite Diffie-Hellman(JTDH) using UCSA.Our contribution is analyzing group key exchange protocol effectively without damaging the soundness of cryptography.

An Efficient Two-Party Key Exchange Protocol with Strong Security

Combined public key （CPK） cryptography does not need certificates to guarantee the authenticity of public keys and avoids the inherent key escrow problem of identity-based cryptography. Based on the efficient CPK scheme, we present an efficient three-round two-party authenticated key exchange protocol with strong security, which is provably secure in the standard model under the decisional Diffie-Hellman （DDH） assumption. The protocol can keep the session key secret from the adversary except that one party＇s ephemeral private key and static private key are all revealed to the adversary. Compared to the existing protocols, this protocol not only assures strong security but also is more efficient.

Security extension for the Canetti-Krawczyk model in identity-based systems

The Canetti-Krawczyk (CK) model is a formalism for the analysis of key-exchange protocols, which can guarantee many security properties for the protocols proved secure by this model. But we find this model lacks the ability to guarantee key generation center (KGC) forward secrecy, which is an important security property for key-agreement protocols based on Identity. The essential reason leading to this weakness is that it does not fully consider the attacker's capabilities. In this paper, the CK model is accordingly extended with a new additional attacker's capability of the KGC corruption in Identity-based systems, which enables it to support KGC forward secrecy.

Cryptanalysis of Schemes Based on Pseudoinverse Matrix

Advances in quantum computation threaten to break public key eryptosystems that are based on the difficulty of fac- torization or the difficulty of discrete logariths, although , no quantum algorithms have been found to be able to solve certain mathematical problems on non-commutative algebraic structures up to now. The proposed new quasi-inverse based cryptography scheme is vulnerable to a linear algebra attack based on the probable occurrence of weak keys in the generation process. In this paper, we illustrate that two of the quasi-inverse based cryptography are vulnerable to a structural attack and that it only requires polynomial time to obtain the equivalent keys for some given public keys. In addition, we conduct a detailed analysis on attack methods and provide some improved suggestions on these two schemes.

STEP AP 242 Managed Model-based 3D Engineering:An Application Towards the Automation of Fixture Planning

Fixture design and planning is one of the most important manufacturing activities, playing a pivotal role in deciding the lead time for product development. Fixture design, which affects the part-quality in terms of geometric accuracy and surface finish, can be enhanced by using the product manufacturing information(PMI) stored in the neutral standard for the exchange of product model data(STEP) file, thereby integrating design and manufacturing. The present paper proposes a unique fixture design approach, to extract the geometry information from STEP application protocol(AP) 242 files of computer aided design(CAD) models, for providing automatic suggestions of locator positions and clamping surfaces. Automatic feature extraction software "FiXplan", developed using the programming language C#, is used to extract the part feature, dimension and geometry information. The information from the STEP AP 242 file is deduced using geometric reasoning techniques, which in turn is utilized for fixture planning. The developed software is observed to be adept in identifying the primary, secondary, and tertiary locating faces and locator position configurations of prismatic components. Structural analysis of the prismatic part under different locator positions was performed using commercial finite element method software, ABAQUS, and the optimized locator position was identified on the basis of minimum deformation of the workpiece.The area-ratio(base locator enclosed area(%)/work piece base area(%)) for the ideal locator configuration was observed as 33%. Experiments were conducted on a prismatic workpiece using a specially designed fixture, for different locator configurations. The surface roughness and waviness of the machined surfaces were analysed using an Alicona non-contact optical profilometer. The best surface characteristics were obtained for the surface machined under the ideal locator positions having an area-ratio of 33%, thus validating the predicted numerical results. The efficiency, capability and applicability of the developed software is demonstrated for the finishing operation of a sensor cover – a typical prismatic component having applications in the naval industry, under different locator configurations.The best results were obtained under the proposed ideal locator configuration of area-ratio 33%.