Limits of the BRSIM/UC soundness of Dolev-Yao-style XOR

摘要

The abstraction of cryptographic operations by term algebras, called Dolev-Yao models, is essential in almost all tool-supported methods for proving security protocols. Recently significant progress was made in proving that Dolev-Yao models can be sound with respect to actual cryptographic realizations and security definitions. The strongest results show this in the sense of blackbox reactive simulatability (BRSIM)/UC, a notion that essentially means the preservation of arbitrary security properties under arbitrary active attacks and in arbitrary protocol environments, with only small changes to the Dolev-Yao models and natural implementations. However, these results are so far restricted to core cryptographic systems like encryption and signatures. Typical modern tools and complexity results around Dolev-Yao models also allow operations with more algebraic properties, in particular XOR because of its clear structure and cryptographic usefulness. We show that it is not possible to extend the strong BRSIM/UC results to XOR, at least not with remotely the same generality and naturalness as for the core cryptographic systems. We also show that for every potential soundness result for XOR with secrecy implications, one significant change to typical Dolev-Yao models must be made. On the positive side, we show the soundness of a rather general Dolev-Yao model with XOR and its realization in the sense of BRSIM/UC under passive attacks.