On Machine-assisted Verification of Cryptography, and on Novel Eavesdropping Techniques

owing to the distributed-system aspects of multiple interleaved
protocol runs, awkward to make for humans. Even proofs published in
leading security conferences and journals are often subsequently
discovered incorrect. While some of these proofs can be corrected with
minor modifications, this situation naturally questions the
trustworthiness of paper-and-pencil security proofs for complex
applications. In the first part of this talk, I advocate the use of
machine-assisted verification to remedy this situation. I illustrates
why cryptographic proofs are particularly well-suited for
machine-assisted verification, and I highlight the research challenges
that have to be met for coming up with a comprehensive tool that can
be conveniently used by the crypto community.

The second part of the talk presents a novel eavesdropping technique
for spying at a distance on data that is displayed on an arbitrary
computer screen, including the currently prevalent LCD monitors. Our
technique exploits reflections of the screen's optical emanations in
various objects that one commonly finds in close proximity to the
screen and uses those reflections to recover the original screen
content. Such objects include eyeglasses, tea pots, spoons, plastic
bottles, and even the eye of the user. We have demonstrated that this
attack can be successfully mounted to spy on even small fonts using
inexpensive, off-the-shelf equipment (less than 1500 dollars) from a
distance of up to 10 meters. Relying on more expensive equipment
allowed us to conduct this attack from over 30 meters away,
demonstrating that similar attacks are feasible from the other side of
the street or from a close-by building. We additionally establish
theoretical limitations of the attack; these limitations may help to
estimate the risk that this attack can be successfully mounted in a
given environment.