Rewriting Privacy

This invited paper extends on the invited talk of the same title held at WRLA 2022. It highlights, summarizes and connects the research works on (alpha, beta)-privacy, an approach to the verification of privacy properties of security protocols. While the de-facto standard is to express privacy as the trace equivalence of two processes, (alpha, beta)-privacy goes a radically different way to formulate privacy a reachability problem, where every state is characterized by two formulae alpha and beta. alpha formalizes all the information that has been deliberately given to the intruder. beta formalizes what the intruder actually has found out by observing messages, interacting with other agents, and the knowledge of the protocol. (alpha, beta)-privacy means that in no reachable state beta allows to derive more than alpha. We describe research papers that define (alpha, beta)-privacy for a fixed state; the application to vote secrecy and receipt-freeness; and finally a rewriting-based definition of (alpha, beta)-privacy for a distributed system.