Provable Security in Practice: Analysis of SSH and CBC mode
with Padding

by Gaven James Watson

RHUL-MA-2011-2

Abstract:

This thesis illustrates and examines the gap that exists
between theoretical and practical cryptography. Provable
security is a useful tool which allows cryptographers to
perform formal security analyses within a strict mathematical
framework. Unfortunately, the formal modelling of provable
security sometimes fails to match how particular schemes or
protocols are implemented in real life. We examine how certain
types of attack are not covered by the current techniques and
show how this can be remedied by expanding existing security
models to capture a much wider array of attacks.

We begin by studying padding oracle attacks, a powerful class
of side-channel, plaintext-recovering attacks introduced by
Vaudenay. These attacks have been shown to work in practice
against CBC mode when it is implemented in certain ways. In
particular, padding oracle attacks have been demonstrated for
certain implementations of SSL/TLS and IPsec. We develop new
security models and proofs of security for CBC mode (with
padding). These models show how to select padding schemes and
in what order to combine CBC mode encryption, padding and
authentication to provably provide a strong notion of security
incorporating padding oracle attacks.

Next we study the secure network protocol SSH. The first formal
security analysis of the SSH Binary Packet Protocol (BPP) was
performed by Bellare, Kohno and Namprempre. We present new
plaintext-recovery attacks against the SSH BPP which partially
invalidate this work. By examining why a combination of flaws
in the basic design of SSH leads implementations such as
OpenSSH to be open to our attacks, we are able to determine
what features are missing from Bellare et al.’s original
provable security analysis for SSH. Using this knowledge we
define new security models that accurately capture the
capabilities of real-world attackers, as well as
security-relevant features of the SSH specifications and the
OpenSSH implementation of SSH. Our new models then give us the
ability to prove that SSH using counter mode encryption is
secure against a much wider array of attacks, including our
plaintext-recovery attacks.

We conclude with further discussion of why the gap between
theory and practice exists and suggest other ways of narrowing
the gap.