Computational soundness about formal encryption in the presence of bilinear pairings and key cycles

Computationally sound symbolic analysis has been the topic of many recent works. Significant progress was made in proving that Dolev-Yao models offering the core cryptographic operations can be sound with respect to actual cryptographic realizations and security definitions. In this paper, we extend Dolev-Yao models to analyze protocols that use bilinear pairings and symmetric encryptions. Furthermore, we prove a computational soundness theorem of formal encryption in the presence of both key cycles and bilinear pairings at the same time, which is a non-trivial extension of former approaches.