## Logics for reasoning about cryptographic constructions

### Bruce Kapron

### Victoria University (currently visiting Stanford)

### Joint work with Russell Impagliazzo, UCSD

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