Game-Based Automated Security Proofs for Cryptographic Protocols

Provable security has become a popular approach for analyzing the security of cryptographic protocols.However,writing and verifying proofs by hand are prone to errors.This paper advocates the automatic security proof framework with sequences of games.We make slight modifications to Blanchet's calculus to make it easy for parsing the initial game.The main contribution of this work is that it introduces algebraic properties with observational equivalences to automatic security proofs,and thus can deal with some practical cryptographic schemes with hard problems.We illustrate the use of algebraic properties in the framework by proving the semantic security of the ElGamal encryption scheme.

Algebra model and security analysis for cryptographic protocols

More and more cryptographic protocols have been used to achieve various security requirements of distributed systems in the open network environment. However cryptographic protocols are very difficult to design and analyze due to the complexity of the cryptographic protocol execution, and a large number of problems are unsolved that range from the theory framework to the concrete analysis technique. In this paper, we build a new algebra called cryptographic protocol algebra (CPA) for describing the message operations with many cryptographic primitives, and proposed a new algebra model for cryptographic protocols based on the CPA. In the model, expanding processes of the participants knowledge on the protocol runs are characterized with some algebraic notions such as subalgebra, free generator and polynomial algebra, and attack processes are modeled with a new notion similar to that of the exact sequence used in homological algebra. Then we develope a mathematical approach to the cryptographic protocol security analysis. By using algebraic techniques, we have shown that for those cryptographic protocols with some symmetric properties, the execution space generated by an arbitrary number of participants may boil down to a smaller space generated by several honest participants and attackers. Furthermore we discuss the composability problem of cryptographic protocols and give a sufficient condition under which the protocol composed of two correct cryptographic protocols is still correct, and we finally offer a counterexample to show that the statement may not be true when the condition is not met.

Breaking and Repairing the Certificateless Key Agreement Protocol from ASIAN 2006

The certificateless authenticated key agreement protocol proposed by Mandt et al does not haVE the property of key-compromise impersonation （K-CI） resilience. An improved protocol with a simple modification of their protocol is proposed in this paper. In particular, our improved protocol is proved to be immune to the K-CI attack and at the same time possess other security properties.

Security Analysis of an Attractive Online Authentication Standard：FIDO UAF Protocol

FIDO(Fast IDentity Online) Alliance proposed a set of standard in 2014 for change the nature of online authentication. By now, it has drawn attention from many companies, including Google, VISA, Intel etc. In this paper, we analyze the FIDO UAF(Universal Authentication Framework) Protocol, one of the two sets of specifications in the standard. We first present protocols' cryptographic abstractions for the registration and authentication protocols of the FIDO UAF. According to the abstractions, we discuss on selected security goals presented in the standard to study UAF security properties. We also propose three attacks, which the first two are based on an assumption that an attacker can corrupt the software installed on the user device, and the third is based on two users sharing a FIDO roaming authenticator. The results of the attacks are to impersonate the legitimate user to pass the online authentication.

New Semantic Model for Authentication Protocols in ASMs

A new semantic model in Abstract State Model (ASM) for authentication protocols is presented. It highlights the Woo-Lam's ideas for authentication, which is the strongest one in Lowe's definition hierarchy for entity authentication. Apart from the flexible and natural features in forming and analyzing protocols inherited from ASM, the model defines both authentication and secrecy properties explicitly in first order sentences as invariants. The process of proving security properties with respect to an authentication protocol blends the correctness and secrecy properties together to avoid the potential flaws which may happen when treated separately. The security of revised Helsinki protocol is shown as a case study. The new model is different from the previous ones in ASMs.

Cryptographic protocol security analysis based on bounded constructing algorithm

An efficient approach to analyzing cryptographic protocols is to develop automatic analysis tools based on formal methods. However, the approach has encountered the high computational complexity problem due to reasons that participants of protocols are arbitrary, their message concurrent. We propose an efficient structures are complex and their executions are automatic verifying algorithm for analyzing cryptographic protocols based on the Cryptographic Protocol Algebra （CPA） model proposed recently, in which algebraic techniques are used to simplify the description of cryptographic protocols and their executions. Redundant states generated in the analysis processes are much reduced by introducing a new algebraic technique called Universal Polynomial Equation and the algorithm can be used to verify the correctness of protocols in the infinite states space. We have implemented an efficient automatic analysis tool for cryptographic protocols, called ACT-SPA, based on this algorithm, and used the tool to check more than 20 cryptographic protocols. The analysis results show that this tool is more efficient, and an attack instance not offered previously is checked by using this tool.

Confidential machine learning on untrusted platforms:a survey

With the ever-growing data and the need for developing powerful machine learning models,data owners increasingly depend on various untrusted platforms(e.g.,public clouds,edges,and machine learning service providers)for scalable processing or collaborative learning.Thus,sensitive data and models are in danger of unauthorized access,misuse,and privacy compromises.A relatively new body of research confidentially trains machine learning models on protected data to address these concerns.In this survey,we summarize notable studies in this emerging area of research.With a unified framework,we highlight the critical challenges and innovations in outsourcing machine learning confidentially.We focus on the cryptographic approaches for confidential machine learning(CML),primarily on model training,while also covering other directions such as perturbation-based approaches and CML in the hardware-assisted computing environment.The discussion will take a holistic way to consider a rich context of the related threat models,security assumptions,design principles,and associated trade-offs amongst data utility,cost,and confidentiality.

Authenticated Diffie-Hellman Key Agreement Protocol with Forward Secrecy

Forward secrecy is an important security property in key agreement protocol. Based on Ham＇s protocol, in this paper a new authenticated Diffie-Hellman key agreement protocol with half forward secrecy is proposed. This protocol is also based on a single cryptographic assumption, and is user authentication and shared key authentication. More importantly, our protocol provides forward secrecy with respect to one of the parties. For this reason, besides the advantages of Ham＇s protocol, in practice, our protocol can reduce the damages resulted from the disclosure of the user＇s secret key and it is very beneficial to today＇s communication with portable devices.