If we would like to formalize proofs of correctness for cryptographic constructions which are sound with respect to notions of provable security, we are faced with a number of difficulties. Asymptotically formulated definitions, which depend on the use of probabilities and complexity classes, do not lend themselves to simple formalizations in logical systems.
We will present two systems for formalizing proofs about cryptographic constructions which address these difficulties. The first is a fairly general system of bounded arithmetic which eliminates the need for asymptotics through the use of nonstandard elements which are intended to represent ``large'' (that is, exponentially-sized) values. The price paid for the use of such elements is a restriction on the form of induction allowed in the system. Fortunately, the resulting scheme of bounded induction is sufficient for formalizing hybrid-style arguments. We prove a general soundness result for this system of bounded arithmetic which shows that it respects standard asymptotic notions of provable security. The second system we present is a more economical one which allows us to reason directly about computational indistinguishability without explicit reference to probabilities. The most significant feature of this system is an induction rule which captures hybrid-style arguments. The soundness of the second system is proved by showing that it may be interpreted in the first system.
Gates 4B (opposite 490), 10/2/01, 4:30 PM