Steve Kremer: Computationally Sound Analysis of Protocols using Bilinear Pairings

Computationally Sound Analysis of Protocols using Bilinear Pairings

Steve Kremer and Laurent Mazaré. Computationally Sound Analysis of Protocols using Bilinear Pairings. Journal of Computer Security, 18(6):999–1033, IOS Press, November 2010.
doi:10.3233/JCS-2009-0388

Download

[PDF] [HTML]

Abstract

In this paper, we introduce a symbolic model to analyse protocols that use a bilinear pairing between two cyclic groups. This model consists in an extension of the Abadi-Rogaway logic and we prove that the logic is still computationally sound: symbolic indistinguishability implies computational indistinguishability provided that the Bilinear Decisional Diffie-Hellman assumption holds and that the encryption scheme is \textsfIND-CPA secure. We illustrate our results on classical protocols using bilinear pairing like Joux tripartite Diffie-Hellman protocol or the TAK-2 and TAK-3 protocols. We also investigate the security of a newly designed variant of the Burmester-Desmedt protocol using bilinear pairings. More precisely, we show for each of these protocols that the generated key is indistinguishable from a random element.

BibTeX

@article{KM-jcs09,
  abstract =      {In this paper, we introduce a symbolic model to
                   analyse protocols that use a bilinear pairing between
                   two cyclic groups. This model consists in an
                   extension of the Abadi-Rogaway logic and we prove
                   that the logic is still computationally sound:
                   symbolic indistinguishability implies computational
                   indistinguishability provided that the Bilinear
                   Decisional Diffie-Hellman assumption holds and that
                   the encryption scheme is \textsf{IND-CPA} secure.
                   We~illustrate our results on classical protocols
                   using bilinear pairing like Joux tripartite
                   Diffie-Hellman protocol or the TAK-2 and TAK-3
                   protocols. We also investigate the security of a
                   newly designed variant of the Burmester-Desmedt
                   protocol using bilinear pairings. More precisely, we
                   show for each of these protocols that the generated
                   key is indistinguishable from a random element.},
  author =        {Kremer, Steve and Mazar{\'e}, Laurent},
  DOI =           {10.3233/JCS-2009-0388},
  journal =       {Journal of Computer Security},
  month =         nov,
  number =        {6},
  pages =         {999-1033},
  publisher =     {{IOS} Press},
  title =         {Computationally Sound Analysis of Protocols using
                   Bilinear Pairings},
  volume =        {18},
  year =          {2010},
  nmonth =        {11},
  url =           {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KM-jcs09.pdf},
}