one successor function—where you
are allowed to quantify over arbitrary
subsets of integers—is decidable. His
was the first result of that nature.
Buchi posed an open problem:
is the monadic second-order theory
decidable if you have two successor
functions. For example, one successor
function being 2x (double), and the
other one being 2x+ 1. I don’t know if
he realized how powerful the monadic theory of two successor functions
would turn out to be. I realized that
this is an incredibly powerful theory.
If you find a decision procedure for
that theory, then many other logical
theories can be demonstrated to be
decidable.
I set myself to work on this problem. My formulation was a generalization from infinite strings to infinite binary trees. You consider a tree where
you have a root, and the root has two
children, a child on the left and a right
child, and each of these has again two
children, a left child and a right child.
The tree branches out ad infinitum,
forming an infinite binary tree. Consider that tree with the two successor
functions, left child, right child, and
study the logical theory of the tree with
these two functions and quantifica-tion over arbitrary subsets of nodes of
the tree.
In 1966, I came as visitor to IBM
research at Yorktown Heights, and
one of my goals to find an appropriate
theory of automata on infinite binary
trees and prove the decidability of the
same problems that Dana Scott and I
had shown to be decidable for finite
automata on finite strings. I created
the appropriate theory of automata
on these infinite trees and showed
that it was decidable. I consider this
to be the most difficult research I
have ever done.
A remarkable feature of that original proof is that even though we are
dealing with finite automata, and with
trees that are infinite but countable,
the proof and all subsequent variants
employ transfinite induction up to the
first uncountable ordinal. Thus the
proof is a strange marriage between
the finite and countable with the uncountable.
This theory led to decision algorithms for many logical theories. That
included decidability of nonstandard
Great teaching
and great science
really flow together
and are not mutually
contradictory
or exclusive of
each other.
logics like modal logics and the temporal logics that are a tool for program
verification, especially in the work of
Amir Pnueli, Moshe Vardi, Orna Kup-ferman, and many others.
Keeping secrets
The next significant application of
my work on randomization was to
cryptography. Ueli Mauer suggested a
model of a cryptographic system that is
based on what he called the bounded
storage assumption. Namely, you have
a very intense public source of random bits that everybody can observe,
say beamed down from a satellite.
The sender and receiver have a short
common key that they establish say by
meeting, and they use that key in order
to select the same random bits out of
the public source of randomness. Out
of those bits, they construct so-called
one-time pads. If you assume that the
intensity of the random source is so
large that no adversary can store more
than, let us say, two-thirds of its bits,
then the one-time pad is really completely random to the adversary and
can be used for provably unbreakable
encryption.
Mauer initially proved the unbreak-
ability result under the assumption
that the adversary stores original bits
from the random source. However,
there remained an open question:
suppose your adversary could do some
operations on the original bits and
then store fewer bits than the num-
ber of source bits. Jonatan Aumann,
Yan Zong Ding, and I showed that
even if the adversary is computation-
ally unbounded, one can still obtain
unbreakable codes provided the ad-
versary cannot store all his computed
bits. This work created quite a stir and
was widely discussed, even in the pop-
ular press.
Privacy for Pirates and Bidders
In the late 1990s, [Dennis Shasha]
came to me and suggested that we work
together on devising a system for preventing piracy, to begin with, of software, but later on also music, videos,
and so on—any kind of digitized intellectual property. We started by reinventing variants of existing methods,
such as the use of safe co-processors
and other methods that were actually
current at the time and which, by the
way, have all either been defeated or
impose excessive constraints on use.
We then invented a new solution. Our
design protects privacy of legitimate
purchasers and even of pirates while
at the same time preventing piracy of
protected digitized content. For example, an engineering firm wanting
to win a contest to build a bridge can
purchase software for bridge design
without identifying itself. Thus competitors cannot find out that the firm
