The implementation relation is then proven using approximate simulation relations. This technique separates proof obligations into two categories: those requiring probabilistic reasoning, as well as those that do not. The latter is a good candidate for mechanization. We illustrate the general method by verifying the SZK property of the well-known identification protocol of Girault, Poupard and Stern.
Category / Keywords: foundations / formal verification, statistical zero knowledge Date: received 23 May 2007 Contact author: lcheung at theory csail mit edu Available format(s): PDF | BibTeX Citation Version: 20070525:085630 (All versions of this report) Short URL: ia.cr/2007/195 Discussion forum: Show discussion | Start new discussion