Stéphanie Delaune: Deducibility constraints and blind signatures

Deducibility constraints and blind signatures

Sergiu Bursuc, Hubert Comon-Lundh, and Stéphanie Delaune. Deducibility constraints and blind signatures. Information and Computation, 238:106–127, Elsevier Science Publishers, November 2014.

Download

[PDF]

Abstract

Deducibility constraints represent in a symbolic way the infinite set of possible executions of a finite protocol. Solving a deducibility constraint amounts to finding all possible ways of filling the gaps in a proof. For finite local inference systems, there is an algorithm that reduces any deducibility constraint to a finite set of solved forms. This allows one to decide any trace security property of cryptographic protocols.
We investigate here the case of infinite local inference systems, through the case study of blind signatures. We show that, in this case again, any deducibility constraint can be reduced to finitely many solved forms (hence we can decide trace security properties). We sketch also another example to which the same method can be applied.

BibTeX

@article{BCD-icomp13,
  abstract =      {Deducibility constraints represent in a symbolic way
                   the infinite set of possible executions of a finite
                   protocol. Solving a deducibility constraint amounts
                   to finding all possible ways of filling the gaps in a
                   proof. For finite local inference systems, there is
                   an algorithm that reduces any deducibility constraint
                   to a finite set of solved forms. This allows one to
                   decide any trace security property of cryptographic
                   protocols.\par We investigate here the case of
                   infinite local inference systems, through the case
                   study of blind signatures. We show that, in this case
                   again, any deducibility constraint can be reduced to
                   finitely many solved forms (hence we can decide trace
                   security properties). We sketch also another example
                   to which the same method can be applied.},
  author =        {Bursuc, Sergiu and Comon{-}Lundh, Hubert and
                   Delaune, St{\'e}phanie},
  OPTDOI =           {10.1016/j.ic.2014.07.006},
  journal =       {Information and Computation},
  month =         nov,
  pages =         {106-127},
  publisher =     {Elsevier Science Publishers},
  title =         {Deducibility constraints and blind signatures},
  volume =        {238},
  year =          {2014},
  nmonth =        {11},
  lsv-category =  {jour},
  wwwpublic =     {public and ccsb},
}