2021 | COFFY – CryptOgraphy & Formal method For privacY

Axe : Scilex
Coordinateurs : Caroline Fontaine (CNRS, LMF, caroline.fontaine@lsv.fr) et Duong Hieu Phan (Telecom Paris, LTCI, hieu.phan@telecom-paris.fr )
Laboratoire gestionnaire : LMF
Autres laboratoires impliqués : DAVID, Inria, LIST, LIX, LMV, LTCI, SAMOVAR
Équipes concernées et liste des participants (ordre alphabétique) : DAVID EPI PETRUS, LIST (CEA) crypto group, LIX EPI GRACE & TYPICAL team, LMF security team, LMV crypto team, LTCI MC2 team, SAMOVAR R3S team

Présentation : Privacy is a part of security that is now a primary ingredient for today’s digital life. Several cryptographic primitives have been designed to address privacy issues, such as, for authentication: blind signatures, group signatures or anonymous credentials; and for confidentiality: homomorphic encryption, functional encryption or mix-nets. They are used and combined within protocols designed to ensure security but also privacy for telecommunications or emerging applications, such as e-voting, cloud service or big data, the demand for privacy becomes more and more important.

But studying and providing privacy properties is not easy. First because privacy can be relied to several definitions, some related with confidentiality of the data, and some others related with the anonymity, indistinguishability or unlinkability of the users. Second because the ability for the above-mentioned primitives and protocols to ensure privacy can be studied by several ways, each of them offering pros and cons. In a nutshell, four communities are working on this topic: cryptographers, who design primitives and protocols and provide hand-made proofs; formal methods researchers, who work on (semi-)automated ways to derive security proofs or point out flaws for these protocols; information technology (IT) researchers, who design security protocols while tweaking existing cryptographic primitives for specific real-world use case needs, and have to mathematically or formally prove that modifications did not alter the original properties; and researchers working on statistical disclosure control methods, for instance, differential privacy. In this working group, we would like to focus on the first three communities’ approaches, which use different mathematical structures and tools but address quite similar privacy issues and have in common their interest for computational attackers. But, of course, everyone is welcome to enrich and open discussions.

More precisely, as protocols become more and more huge and complex, and because it is important to handle powerful and realistic attackers who may use complex strategies, studying protocols security by hand cannot be considered as sufficient in many contexts. This is why we need (semi-)automated tools to handle security proofs and flaws detection. But to design such tools means to be able to provide accurate and manageable models for the underlying cryptographic primitives as well as for the privacy properties we want to guarantee. Even this is a challenge, but we also need logic and mathematical frameworks to be able to derive composability security results on the protocols. Handling these issues separately would provide very limited and not practical results, while melting expertise from cryptography, IT and formal methods communities we should progress on the way to reach a more realistic and powerful security analysis. On the theoretical side, we would like to develop a better understanding and modelling of the attackers and primitives, and beyond perhaps derive some design directions for new primitives better suited for their integration in (semi-)automated provers. On the practical side, and as the final goal is to handle realistic situations, it is important to focus on some use-cases. They will feed our brainstorming concerning different kinds of privacy issues, and lead to ad-hoc modelling (to identify and manage tradeoffs between the expressiveness, accuracy and logical capacities of the formal properties to be integrated in (semi-)automated frameworks). Use-cases may come from any participant that is interested in submitting challenging privacy issues, e.g. in telecommunications, distributed databases, etc.