Recently, many approaches have been proposed for building simple symbolic proofs of cryptographic protocols with computational soundness. However, most of them support only bare-bone execution model without any ideal setup, such as the existence of authenticated channel, and only deterministic protocols. Thus many protocols are not expressible in those models. Following the work of Canetti and Herzog [1], we propose a probabilistic symbolic model for analyzing cryptographic protocols and a general way of incorporating ideal setups by using a probabilistic process calculus. Each ideal setup in the symbolic model will correspond to an ideal functionality in the computational model. Furthermore, we show the computational faithfulness of this symbolic model with respect to a hybrid computational model in which ideal functionalities are employed. © 2008 Springer Berlin Heidelberg.
CITATION STYLE
Luo, Z. (2008). Computationally sound symbolic analysis of probabilistic protocols with ideal setups. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5324 LNCS, pp. 185–199). Springer Verlag. https://doi.org/10.1007/978-3-540-88733-1_13
Mendeley helps you to discover research relevant for your work.