Abstract
We define an epistemic logic or logic of knowledge, PL, and a formalism to undertake privacy-centric reasoning in security protocols, over a Dolev-Yao model. We are able to automatically verify all the privacy requirements that are commonplace in security-protocol verification (i.e., strong secrecy, anonymity, various types of unlinkablity including weak unlinkability), as well as privacy notions that are less studied (i.e., privacy regarding lists' membership). Our methodology does not vary with the property: it is uniform no matter the kind of privacy requirement specified and/or verified. We operate in the setting of a bounded number of protocol-sessions. We also implement Phoebe - a proof-of-concept model checker for this methodology. We use Phoebe to check all the aforementioned properties, and we also show-case it on the "benchmark" anonymity and unlinkability requirements of several well-known protocols.