Deciding a Fragment of (α, β)-Privacy

Laouen Pablo Killian Fernet; Sebastian Alexander Mödersheim

Deciding a Fragment of (α, β)-Privacy

Laouen Pablo Killian Fernet, Sebastian Alexander Mödersheim

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

14 Downloads (Pure)

Abstract

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 language	English
Title of host publication	Proceedings of 17^th International Workshop on Security and Trust Management
Number of pages	22
Publication date	2021
Publication status	Published - 2021
Event	17^th International Workshop on Security and Trust Management - Virtual event, Darmstadt, Germany Duration: 8 Oct 2021 → 8 Oct 2021 Conference number: 17 https://www.nics.uma.es/stm2021/

Conference

Conference	17^th International Workshop on Security and Trust Management
Number	17
Location	Virtual event
Country/Territory	Germany
City	Darmstadt
Period	08/10/2021 → 08/10/2021
Internet address	https://www.nics.uma.es/stm2021/

Keywords

Privacy
Formal Methods
Security protocols
Automated verification

Access to Document

FulltextAccepted author manuscript, 390 KB

Cite this

@inproceedings{6d74d2f5f9c24d69889bee4e1edba44d,

title = "Deciding a Fragment of (α, β)-Privacy",

abstract = "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.",

keywords = "Privacy, Formal Methods, Security protocols, Automated verification",

author = "Fernet, {Laouen Pablo Killian} and M{\"o}dersheim, {Sebastian Alexander}",

year = "2021",

language = "English",

booktitle = "Proceedings of 17th International Workshop on Security and Trust Management",

note = "17<sup>th</sup> International Workshop on Security and Trust Management, STM2021 ; Conference date: 08-10-2021 Through 08-10-2021",

url = "https://www.nics.uma.es/stm2021/",

}

TY - GEN

T1 - Deciding a Fragment of (α, β)-Privacy

AU - Fernet, Laouen Pablo Killian

AU - Mödersheim, Sebastian Alexander

N1 - Conference code: 17

PY - 2021

Y1 - 2021

N2 - 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.

AB - 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.

KW - Privacy

KW - Formal Methods

KW - Security protocols

KW - Automated verification

M3 - Article in proceedings

BT - Proceedings of 17th International Workshop on Security and Trust Management

T2 - 17<sup>th</sup> International Workshop on Security and Trust Management

Y2 - 8 October 2021 through 8 October 2021

ER -

Deciding a Fragment of (α, β)-Privacy

Abstract

Conference

Keywords

Access to Document

Fingerprint

Cite this