|
|
Abstract:
Recently, many different approaches have been proposed for cryptographically sound symbolic analysis. Among others, the universally composable symbolic analysis (UCSA) framework layers Dolev-Yao style symbolic analysis on top of the universally composable (UC) security framework to construct general computationally sound proofs of security protocols. In this work, we first extend the simple symbolic model of the UCSA framework into a probabilistic multi-party protocol model, adding supports for two-party cryptographic primitives and corresponding ideal functionalities. Then we show this model still maintains soundness with respect to the UC framework. Finally, as a case study, we demonstrate the ability of current framework to analyze protocols that satisfy absolute anonymous property.
|