Computational Soundness of Asymmetric Bilinear Pairing-Based Protocols


IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences   Vol.E100-A   No.9   pp.1794-1803
Publication Date: 2017/09/01
Online ISSN: 1745-1337
DOI: 10.1587/transfun.E100.A.1794
Type of Manuscript: Special Section PAPER (Special Section on Discrete Mathematics and Its Applications)
formal methods,  computational soundness,  asymmetric bilinear pairing,  

Full Text: PDF(269.9KB)
>>Buy this Article

Asymmetric bilinear maps using Type-3 pairings are known to be advantageous in several points (e.g., the speed and the size of a group element) to symmetric bilinear maps using Type-1 pairings. Kremer and Mazaré introduce a symbolic model to analyze protocols based on bilinear maps, and show that the symbolic model is computationally sound. However, their model only covers symmetric bilinear maps. In this paper, we propose a new symbolic model to capture asymmetric bilinear maps. Our model allows us to analyze security of various protocols based on asymmetric bilinear maps (e.g., Joux's tripartite key exchange, and Scott's client-server ID-based key exchange). Also, we show computational soundness of our symbolic model under the decisional bilinear Diffie-Hellman assumption.