Provable Security: the Good, the Bad, and the Ugly

Since modern cryptography was born around the late 1970s, a myriad of cryptographic constructions and protocols have been proposed. The field quickly developed into a science whose results have had great im pact on people’s lives. Some examples are secure communication over the internet, distributed digital currencies, electronic elections, and more. Such a progress was boosted by the diffusion of a methodology called the provable security paradigm. It provides a precise framework to formalize and prove the security of a cryptographic construction. Provable security is based on three pillars: (i) definitions, (ii) assump tions, and (iii) proofs. The definition states when the system can be considered secure and what are the capabilities of an adversary attack ing the construction. The proof demonstrates that the construction satisfies the definition, assuming that all the assumptions hold. Prov able security provides objective ways to compare different construc tions, as well as more reassurances on their security. However, it is not devoid of pitfalls. For example, a definition might not model the real world correctly, and thus any proof that a construction satisfies such definition would be worthless in practice. Furthermore, it might happen that security proofs containing errors will not get detected because of the complexity (or oversimplification) of the proof itself. This thesis explores such multifaceted nature of provable security through two parts. In the first part, we focus on the recent devel opment of automatic contact tracing systems (ACTs). When the COVID-19 pandemic hit, automatic contact tracing was proposed as an effective way to slow the spread of the virus down by detecting likely infected people earlier with the help of technology. Citizens would use a smartphone app, and users at risk of being infected - as they were in proximity of an infected individual - would be notified by the smartphone. Due to the widespread adoption that was expected for ACTs, privacy and integrity were both key concerns. The DP3T team proposed an ACT [114] which was shortly after implemented and deployed over smartphones by Apple and Google with the name of GAEN. Informal security assessments were per formed by the DP3T team, including wrong or misleading claims about the privacy and integrity guarantees that ACTs could provide. Sev eral attacks to DP3T pointed out by other researchers were deemed as inherent by analyses that considered very powerful adversaries. How ever, the concrete attacks could have been carried out by much weaker adversaries to which other ACTs could have possibly resisted. We model these and novel integrity and privacy attacks with a focus on mass surveillance and analyze the security of DP3T w.r.t. them. We propose two new ACTs named Pronto-C2 and Pronto-B2, which encom pass DP3T/GAEN both in terms of privacy and integrity guarantees. Our ACTs also demonstrate that such attacks are not inherent. Fi nally, we consider the terrorist attack conjectured by Vaudenay [116]. It involves a malicious party (i.e., the terrorist) bribing infected users to inject false alerts in the ACT. We show how to concretely implement automated terrorist attacks to jeopardize the integrity of GAEN. In the second part of this thesis, we provide novel contributions in the area of threshold cryptography. In particular, we focus on proofs over threshold relations, threshold ring signatures, and extendable threshold ring signatures. We point out several fallacies in the usage of the provable security paradigm in prior works published at major cryptography conferences [5, 64]. Such issues include errors in the se curity proofs as well as inadequate definitions where the real-world system’s requirements and adversary’s capabilities are not matched by the definition. We overcome such issues proposing stronger defini tions, new constructions, and revisited security proofs. Additionally, our new constructions improve the previous ones in terms of efficiency, security, and/or features. [edited by Author]