## 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.

### 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},
}
```