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.

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.

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.

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.

通用可组合符号化分析群组密钥协商协议(英文)

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.

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.

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