Deciding a Fragment of (α, β)-Privacy

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

33 Downloads (Pure)


We show how to automate fragments of the logical framework (α, β)-privacy which provides an alternative to bisimilarity-based and tracebased definitions of privacy goals for security protocols. We consider the so-called message-analysis problem, which is at the core of (α, β)-privacy: given a set of concrete messages and their structure, which models can the intruder rule out? While in general this problem is undecidable, we give a decision procedure for a standard class of algebraic theories.
Original languageEnglish
Title of host publicationProceedings of 17th International Workshop on Security and Trust Management
Number of pages22
Publication date2021
Publication statusPublished - 2021
Event17th International Workshop on Security and Trust Management - Virtual event, Darmstadt, Germany
Duration: 8 Oct 20218 Oct 2021
Conference number: 17


Conference17th International Workshop on Security and Trust Management
LocationVirtual event
Internet address


  • Privacy
  • Formal Methods
  • Security protocols
  • Automated verification


Dive into the research topics of 'Deciding a Fragment of (α, β)-Privacy'. Together they form a unique fingerprint.

Cite this