Normal Proofs in Intruder Theories

Given an arbitrary intruder deduction capability, modeled as an inference system S and a protocol, we show how to compute an inference system bS such that the security problem for an unbounded number of sessions is equivalent to the deducibility of some message in bS. Then, assuming that S has some subformula property, we lift such a property to bS, thanks to a proof normalisation theorem. In general, for an unbounded number of sessions, this provides with a complete deduction strategy. In case of a bounded number of sessions, our theorem implies that the security problem is co-NP-complete. As an instance of our result we get a decision algorithm for the theory of blind-signatures, which, to our knowledge, was not known before.

• Type: Conference
• Year: 2006
• Where: ASIAN
• Authors: Vincent Bernat, Hubert Comon-Lundh
• Keywords: Algorithms, Arbitrary Intruder Deduction, ASIAN 2006, Security Problem, Unbounded Number