A Decision Procedure and Typing Result for Alpha-Beta Privacy

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, branching and statefulness. Our first 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. Our second contribution is to show that, for a class of protocols satisfying certain syntactic conditions, it is sound to restrict the intruder model to a typed model, where the intruder only sends well-typed messages. Our typing result holds for an unbounded number of transitions.