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 ...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.展开更多
In this paper, we propose a partially non-cryptographic security routing protocol （PNCSR） that protects both routing and data forwarding operations through the same reactive approach. PNCSR only apply public-key cry...In this paper, we propose a partially non-cryptographic security routing protocol （PNCSR） that protects both routing and data forwarding operations through the same reactive approach. PNCSR only apply public-key cryptographic system in managing token, but it doesn＇t utilize any cryptographic primitives on the routing messages. In PNCSR, each node is fair. Local neighboring nodes collaboratively monitor each other and sustain each other. It also uses a novel credit strategy which additively increases the token lifetime each time a node renews its token. We also analyze the storage, computation, and communication overhead of PNCSR, and provide a simple yet meaningful overhead comparison. Finally, the simulation results show the effectiveness of PNCSR in various situations.展开更多
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...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.展开更多
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 pap...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.展开更多
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. Thi...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.展开更多
随着列车通信技术的发展,列车控制网络的环境愈发复杂,车载设备对网络带宽和网络拓扑复杂度的要求愈发严格,列车互联网的物理层载体逐渐从串行通信总线网过渡到了以太网。为了保证以太网协议栈在列车互联网中的正常运行,结合列车互联网...随着列车通信技术的发展,列车控制网络的环境愈发复杂,车载设备对网络带宽和网络拓扑复杂度的要求愈发严格,列车互联网的物理层载体逐渐从串行通信总线网过渡到了以太网。为了保证以太网协议栈在列车互联网中的正常运行,结合列车互联网的独特需求,列车通信网络(train communication network,TCN)联盟提出了列车实时数据协议(train real-time data protocol,TRDP),现已成为车载设备数据传输中不可或缺的重要一环。然而,在引入以太网架构的同时,传统计算机网络面临的安全风险也被带入了列车通信网络中。架构在以太网之上的TRDP,缺乏有效的安全防护机制,面临着恶意攻击、数据泄露、拒绝服务等一系列风险。在TRDP的础上,分析了TRDP消息数据、过程数据两种协议模式的区别和安全需求,结合列车互联网的实际情况,选取合适的加密协议,改进了协议细节,设计了基于加密协议的安全防护机制。并在此基础上搭建了一个模型系统,系统展示了如何将这些关键的密码技术组合起来,构建一个安全的列车互联网信息系统,并证明了系统在保证协议安全性的情况下,能够满足列车互联网对TRDP的性能需求。展开更多
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 an...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.展开更多
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...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.展开更多
基金National High Technical Research and Development Program of China(863 program)under Grant No. 2007AA01Z471
文摘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.
基金Supported bythe National Natural Science Foundationof China (60403027)
文摘In this paper, we propose a partially non-cryptographic security routing protocol （PNCSR） that protects both routing and data forwarding operations through the same reactive approach. PNCSR only apply public-key cryptographic system in managing token, but it doesn＇t utilize any cryptographic primitives on the routing messages. In PNCSR, each node is fair. Local neighboring nodes collaboratively monitor each other and sustain each other. It also uses a novel credit strategy which additively increases the token lifetime each time a node renews its token. We also analyze the storage, computation, and communication overhead of PNCSR, and provide a simple yet meaningful overhead comparison. Finally, the simulation results show the effectiveness of PNCSR in various situations.
基金the National Natural Science Foundation of China (60773086)
文摘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.
文摘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.
基金Supported by the National Natural Science Foundation of China (60873233)the Nature Science Foundation of Shaanxi Province, China (2006F19)the Technology Research Program of Xi’an, China (CXY08016)
文摘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.
文摘随着列车通信技术的发展,列车控制网络的环境愈发复杂,车载设备对网络带宽和网络拓扑复杂度的要求愈发严格,列车互联网的物理层载体逐渐从串行通信总线网过渡到了以太网。为了保证以太网协议栈在列车互联网中的正常运行,结合列车互联网的独特需求,列车通信网络(train communication network,TCN)联盟提出了列车实时数据协议(train real-time data protocol,TRDP),现已成为车载设备数据传输中不可或缺的重要一环。然而,在引入以太网架构的同时,传统计算机网络面临的安全风险也被带入了列车通信网络中。架构在以太网之上的TRDP,缺乏有效的安全防护机制,面临着恶意攻击、数据泄露、拒绝服务等一系列风险。在TRDP的础上,分析了TRDP消息数据、过程数据两种协议模式的区别和安全需求,结合列车互联网的实际情况,选取合适的加密协议,改进了协议细节,设计了基于加密协议的安全防护机制。并在此基础上搭建了一个模型系统,系统展示了如何将这些关键的密码技术组合起来,构建一个安全的列车互联网信息系统,并证明了系统在保证协议安全性的情况下,能够满足列车互联网对TRDP的性能需求。
文摘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.
基金supported by the National Natural Science Foundation of China(Grant No.90412011)the State Key Basic Research Program(973)(Grant No.2005CB321803)the State"863"High-tech Research and Development Project(Grant No.2003AA 144150).
文摘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.
