Normal Proofs in Intruder Theories

12 years 5 months ago
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.
Vincent Bernat, Hubert Comon-Lundh
Added 20 Aug 2010
Updated 20 Aug 2010
Type Conference
Year 2006
Authors Vincent Bernat, Hubert Comon-Lundh
Comments (0)