Changyu Dong

Shaowei Wang, Jinn Li, Yun Peng et al.

Answering statistical queries over sensitive data under differential privacy (DP) is a common task in many settings, including databases, mobile computing, and data markets. In these scenarios, multiple analysts may issue the same query, while receiving answers generated under different privacy budgets due to differences in trust levels or willingness to pay. Existing approaches for such multi-tier DP queries either incur excessive cumulative privacy loss or suffer from suboptimal utility. In this paper, we propose a framework for multi-tier DP query release that simultaneously bound the cumulative privacy loss by the maximum privacy budget among all queries and achieve optimal utility comparable to that of single-tier mechanisms. Our framework applies to different classes of DP mechanisms. For noise-adding mechanisms (e.g., count queries with the two-sided Geometric mechanism in the curator model), we develop a general solution based on the characteristic functions of noise distributions. For other mechanisms (e.g., count queries under the local DP model with the Subset mechanism), we design mechanism-specific primitives for budget transformation and introduce a template-based strategy that attains optimal utility across different privacy regimes. Experimental results demonstrate the effectiveness of our framework.

Shaowei Wang, Changyu Dong, Xiangfu Song et al.

In data-driven applications, preserving user privacy while enabling valuable computations remains a critical challenge. Technologies like differential privacy have been pivotal in addressing these concerns. The shuffle model of DP requires no trusted curators and can achieve high utility by leveraging the privacy amplification effect yielded from shuffling. These benefits have led to significant interest in the shuffle model. However, the computation tasks in the shuffle model are limited to statistical estimation, making it inapplicable to real-world scenarios in which each user requires a personalized output. This paper introduces a novel paradigm termed Private Individual Computation (PIC), expanding the shuffle model to support a broader range of permutation-equivariant computations. PIC enables personalized outputs while preserving privacy, and enjoys privacy amplification through shuffling. We propose a concrete protocol that realizes PIC. By using one-time public keys, our protocol enables users to receive their outputs without compromising anonymity, which is essential for privacy amplification. Additionally, we present an optimal randomizer, the Minkowski Response, designed for the PIC model to enhance utility. We formally prove the security and privacy properties of the PIC protocol. Theoretical analysis and empirical evaluations demonstrate PIC's capability in handling non-statistical computation tasks, and the efficacy of PIC and the Minkowski randomizer in achieving superior utility compared to existing solutions.

Feng Hao, Roberto Metere, Siamak F. Shahandashti et al.

Simple Password Exponential Key Exchange (SPEKE) is a well-known Password Authenticated Key Exchange (PAKE) protocol that has been used in Blackberry phones for secure messaging and Entrust's TruePass end-to-end web products. It has also been included into international standards such as ISO/IEC 11770-4 and IEEE P1363.2. In this paper, we analyse the SPEKE protocol as specified in the ISO/IEC and IEEE standards. We identify that the protocol is vulnerable to two new attacks: an impersonation attack that allows an attacker to impersonate a user without knowing the password by launching two parallel sessions with the victim, and a key-malleability attack that allows a man-in-the-middle (MITM) to manipulate the session key without being detected by the end users. Both attacks have been acknowledged by the technical committee of ISO/IEC SC 27, and ISO/IEC 11770-4 revised as a result. We propose a patched SPEKE called P-SPEKE and present a formal analysis in the Applied Pi Calculus using ProVerif to show that the proposed patch prevents both attacks. The proposed patch has been included into the latest revision of ISO/IEC 11770-4 published in 2017.

Xiangfu Song, Changyu Dong, Dandan Yuan et al.

Recently, several practical attacks raised serious concerns over the security of searchable encryption. The attacks have brought emphasis on forward privacy, which is the key concept behind solutions to the adaptive leakage-exploiting attacks, and will very likely to become mandatory in the design of new searchable encryption schemes. For a long time, forward privacy implies inefficiency and thus most existing searchable encryption schemes do not support it. Very recently, Bost (CCS 2016) showed that forward privacy can be obtained without inducing a large communication overhead. However, Bost's scheme is constructed with a relatively inefficient public key cryptographic primitive, and has a poor I/O performance. Both of the deficiencies significantly hinder the practical efficiency of the scheme, and prevent it from scaling to large data settings. To address the problems, we first present FAST, which achieves forward privacy and the same communication efficiency as Bost's scheme, but uses only symmetric cryptographic primitives. We then present FASTIO, which retains all good properties of FAST, and further improves I/O efficiency. We implemented the two schemes and compared their performance with Bost's scheme. The experiment results show that both our schemes are highly efficient, and FASTIO achieves a much better scalability due to its optimized I/O.

Changyu Dong, Yilei Wang, Amjad Aldweesh et al.

Cloud computing has become an irreversible trend. Together comes the pressing need for verifiability, to assure the client the correctness of computation outsourced to the cloud. Existing verifiable computation techniques all have a high overhead, thus if being deployed in the clouds, would render cloud computing more expensive than the on-premises counterpart. To achieve verifiability at a reasonable cost, we leverage game theory and propose a smart contract based solution. In a nutshell, a client lets two clouds compute the same task, and uses smart contracts to stimulate tension, betrayal and distrust between the clouds, so that rational clouds will not collude and cheat. In the absence of collusion, verification of correctness can be done easily by crosschecking the results from the two clouds. We provide a formal analysis of the games induced by the contracts, and prove that the contracts will be effective under certain reasonable assumptions. By resorting to game theory and smart contracts, we are able to avoid heavy cryptographic protocols. The client only needs to pay two clouds to compute in the clear, and a small transaction fee to use the smart contracts. We also conducted a feasibility study that involves implementing the contracts in Solidity and running them on the official Ethereum network.

Roberto Metere, Changyu Dong

Aiming for strong security assurance, recently there has been an increasing interest in formal verification of cryptographic constructions. This paper presents a mechanised formal verification of the popular Pedersen commitment protocol, proving its security properties of correctness, perfect hiding, and computational binding. To formally verify the protocol, we extended the theory of EasyCrypt, a framework which allows for reasoning in the computational model, to support the discrete logarithm and an abstraction of commitment protocols. Commitments are building blocks of many cryptographic constructions, for example, verifiable secret sharing, zero-knowledge proofs, and e-voting. Our work paves the way for the verification of those more complex constructions.