Search

Secure message transmission in vehicular communications in smart cities is still a challenging task. Most of the related work employed the Public Key Infrastructure and Certification Revocation Lists (CRLs) for ensuring security and privacy. However, these work suffered from some issues such as 1) the time-consuming checking process and huge size of CRLs, 2) traceability attacks by linking unencrypted Basic Safety Messages (BSMs), and 3) extracting secret keys from the storage of parked vehicles or road-side units (RSU) by an adversary. To address the aforementioned issues, we thus propose a physically secure privacy-preserving message authentication protocol using Physical Unclonable Function (PUF) and Secret Sharing. The proposed protocol guarantees security and privacy against passive and active attacks even under memory leakage. The entities (i.e., vehicles and RSU) make use of their PUF to reconstruct a secret polynomial-share so that pairwise temporal secret keys (PTKs) can be established with other entities. Unlike existing protocols, BSMs are also encrypted in our protocol (by PTKs) to provide a higher level of security and thwart vehicles traceability attacks. To revoke a vehicle, RSU needs not broadcast CRLs. Instead, RSU distributes only a secure offset key using threshold Secret Sharing. Consequently, our revocation checking process has computation complexity O(1). Our protocol also eliminates the need for a third party in Vehicle-to-Vehicle communication to ensure expeditious transmission. Security analysis and performance evaluation show that our proposed protocol outperforms existing schemes in terms of security features, computation, and communication cost.

At present, millions of Ethereum smart contracts are created per year and attract financially motivated attackers. However, existing analyzers do not meet the need to precisely analyze the financial security of large numbers of contracts. In this paper, we propose and implement FASVERIF, an automated analyzer for fine-grained analysis of smart contracts' financial security. On the one hand, FASVERIF automatically generates models to be verified against security properties of smart contracts. On the other hand, our analyzer automatically generates the security properties, which is different from existing formal verifiers for smart contracts. As a result, FASVERIF can automatically process source code of smart contracts, and uses formal methods whenever possible to simultaneously maximize its accuracy. We evaluate FASVERIF on a vulnerabilities dataset by comparing it with other automatic tools. Our evaluation shows that FASVERIF greatly outperforms the representative tools using different technologies, with respect to accuracy and coverage of types of vulnerabilities.

Current formal approaches have been successfully used to find design flaws in many security protocols. However, it is still challenging to automatically analyze protocols due to their large or infinite state spaces. In this paper, we propose a novel framework that can automatically verifying security protocols without any human intervention. Experimental results show that SmartVerif automatically verifies security protocols that cannot be automatically verified by existing approaches. The case study also validates the effectiveness of our dynamic strategy., Comment: arXiv admin note: text overlap with arXiv:1403.1142, arXiv:1703.00426 by other authors

A basic ( $t$ , $n$ )-secret sharing (SS) scheme allows a secret $s$ to be divided into $n$ shares and shared among $n$ shareholders. In the scheme, any $t$ or more than $t$ shareholders can recover the secret while fewer than $t$ shareholders cannot obtain the secret $s$ . But an adversary without any valid share may obtain the secret if there are over $t$ participants in the secret reconstruction. To address this type of attack, we first introduce the notion of randomized component (RC), which binds a share with all participants and protects the share from being exposed to outside without any computational assumption; at the same time, RCs can be used to reconstruct the secret. As one of the applications of RCs, a ( $t$ , $m$ , $n$ )-group oriented SS scheme is proposed to cope with the attack in basic ( $t$ , $n$ )-SSs, in which once $m$ ( $m\ge t$ ) participants form a tightly couple group by generating RCs, the secret can be recovered only if all $m$ RCs are correct, which requires each participant to have a valid share in advance. Moreover, the scheme can secure the secret without any user authentication or share verification. Analyses show the proposed ( $t$ , $m$ , $n$ )-group oriented SS is asymptotically perfect and unconditionally secure. RCs can also be applied to build other schemes in a simple way, such as multi-SS, group authentication, and so on.

The ( t , n ) threshold secret sharing schemes (SSs) were introduced by Shamir and Blakley separately in 1979. Multilevel threshold secret sharing (MTSS) is a generalization of classical threshold SS, and it has been studied extensively in the literature. In an MTSS, shareholders are classified into different security subsets. The threshold value of a higher-level subset is smaller than the threshold value of a lower-level subset. Shareholders in each subset can recover the secret if the number of shares available is equal to or more than a threshold value. Furthermore, the share of a shareholder in a higher-level subset can be used as a share in the lower-level subset to recover the secret. Chinese Remainder Theorem (CRT) is one of popular tools used for designing SSs. For example, the Mignotte's scheme and Asmuth–Bloom's scheme are two classical ( t , n ) threshold SSs based on the CRT. So far, there was no CRT-based MTSS in the literature. In this paper, we propose the first MTSS based on the CRT. In our proposed scheme, one unique feature is that each shareholder needs to keep only one private share. Our proposed scheme is based on the Asmuth–Bloom's SS which is unconditionally secure.

With the rapid development of MANET, secure and practical authentication is becoming increasingly important. The existing works perform the research from two aspects, i.e., (a)secure key division and distributed storage, (b)secure distributed authentication. But there still exist several unsolved problems. Specifically, it may suffer from cheating problems and fault authentication attack, which can result in authentication failure and DoS attack towards authentication service. Besides, most existing schemes are not with satisfactory efficiency due to exponential arithmetic based on Shamir's scheme. In this paper, we explore the property of verifiable secret sharing(VSS) schemes with Chinese Remainder Theorem (CRT), then propose a secret key distributed storage scheme based on CRT-VSS and trusted computing for MANET. Specifically, we utilize trusted computing technology to solve two existing cheating problems in secret sharing area before. After that, we do the analysis of homomorphism property with CRT-VSS and design the corresponding shares-product sharing scheme with better concision. On such basis, a secure distributed Elliptic Curve-Digital Signature Standard signature (ECC-DSS) authentication scheme based on CRT-VSS scheme and trusted computing is proposed. Furthermore, as an important property of authentication scheme, we discuss the refreshing property of CRT-VSS and do thorough comparisons with Shamir's scheme. Finally, we provide formal guarantees towards our schemes proposed in this paper., Comment: under submission