A Decision Procedure for Alpha-Beta Privacy for a Bounded Number of Transitions

TY - CHAP

T1 - A Decision Procedure for Alpha-Beta Privacy for a Bounded Number of Transitions

AU - Fournet, Laouen

AU - Mödersheim, Sebastian

AU - Viganò, Luca

PY - 2023/7/6

Y1 - 2023/7/6

N2 - We present a decision procedure for verifying whether a protocol respects privacy goals, given a bound on the number of transitions. We consider multi message-analysis problems, where the intruder does not know exactly the structure of the messages but rather knows several possible structures and that the real execution corresponds to one of them. This allows for modeling a large class of security protocols, with standard cryptographic operators, non-determinism and branching. Our main contribution is the definition of a decision procedure for a fragment of alpha-beta privacy. Moreover, we have implemented a prototype tool as a proof-of-concept and a first step towards automation.

AB - We present a decision procedure for verifying whether a protocol respects privacy goals, given a bound on the number of transitions. We consider multi message-analysis problems, where the intruder does not know exactly the structure of the messages but rather knows several possible structures and that the real execution corresponds to one of them. This allows for modeling a large class of security protocols, with standard cryptographic operators, non-determinism and branching. Our main contribution is the definition of a decision procedure for a fragment of alpha-beta privacy. Moreover, we have implemented a prototype tool as a proof-of-concept and a first step towards automation.

M3 - Conference paper

BT - 2024 IEEE Computer Security Foundations Symposium

PB - IEEE Computer Society Press

ER -