Computationally sound analysis of protocols using bilinear pairings

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: symbol