Skip to main content
Engineering LibreTexts

2.3: Hybrid Proofs of Security

  • Page ID
    7322
  • We will now show that one-time pad satisfies the new security definition. More precisely,

    Theorem \(\PageIndex{1}\) :

    Let OTP denote the one-time pad encryption scheme (Construction 1.2). Then OTP has onetime secrecy. That is, \(\mathscr{L}^{OTP}_{ots-L}\equiv\mathscr{L}^{OTP}_{ots-R}\).

    Given what we already know about one-time pad, it’s not out of the question that we could simply “eyeball” the claim \(\mathscr{L}^{OTP}_{ots-L}\equiv\mathscr{L}^{OTP}_{ots-R}\) Indeed, we have already shown that in both libraries the QUERY subroutine simply returns a uniformly random string. A direct proof along these lines is certainly possible.

    Instead of directly relating the behavior of the two libraries, however, we will instead show that:

    \[\mathscr{L}^{OTP}_{ots-L}\equiv\mathscr{L}_{hyb-1}\equiv\mathscr{L}_{hyb-3}\equiv\mathscr{L}_{hyb-4}\equiv\mathscr{L}^{OT}_{ots-R}\nonumber\]

    where \(\mathscr{L}_{hyb-1},...,\mathscr{L}_{hyb-4}\) are a sequence of what we call hybrid libraries. (It is not hard to see that the “\(\equiv\)” relation is transitive, so this proves that \(\mathscr{L}^{OTP}_{ots-L}\equiv\mathscr{L}^{OTP}_{ots-R}\) This style of proof is called a hybrid proof and it will be the standard way to prove security throughout this course.

    For the security of one-time pad, such a hybrid proof is likely overkill. But we use this opportunity to introduce the technique, since nearly every security proof we will see in this class will use the hybrid technique. Hybrid proofs have the advantage that it can be quite easy to justify that adjacent hybrids (e.g., \(\mathscr{L}_{hyb-1}\) and (\mathscr{L}_{hyb-(i+1)}\)) are interchangeable, so the method scales well even in proofs where the “endpoints” of the hybrid sequence are quite different.

    Proof:

    As described above, we will prove that

    \[\mathscr{L}^{OTP}_{ots-L}\equiv\mathscr{L}_{hyb-1}\equiv\mathscr{L}_{hyb-3}\equiv\mathscr{L}_{hyb-4}\equiv\mathscr{L}^{OT}_{ots-R}\nonumber\]

    for a particular sequence of \(\mathscr{L}_{hyb-i}\) libraries that we choose. For each hybrid, we highlight the differences from the previous one, and argue why adjacent hybrids are interchangeable.

    Screen Shot 2019-02-16 at 1.21.04 AM.png

    As promised, the hybrid sequence begins with \(\mathscr{L}^{OTP}_{ots-L}\). The details of one-time pad have been filled in and highlighted.

    Screen Shot 2019-02-16 at 1.21.33 AM.png

    Factoring out a block of statements into a subroutine does not affect the library’s behavior. Note that the new subroutine is exactly the \(\mathscr{L}_{otp-reallibrary} from Claim 2.2.1 (with the subroutine name changed to avoid naming conflicts). This is no accident!

    Screen Shot 2019-02-16 at 1.38.29 AM.png

    \(\mathscr{L}_{otp-real}\) has been replaced with ℒotp-rand. From Claim 2.2.1 along with the library composition lemma Lemma 2.1.1, this change has no effect on the library’s behavior

    Screen Shot 2019-02-16 at 1.28.01 AM.png

    The argument to QUERY’ has been changed from mL to mR. This has no effect on the library’s behavior since QUERY’ does not actually use its argument in these hybrids.

    The previous transition is the most important one in the proof, as it gives insight into how we came up with this particular sequence of hybrids. Looking at the desired endpoints of our sequence of hybrids — \(\mathscr{L}^{OTP}_{ots-L}\) and \(\mathscr{L}^{OTP}_{ots-R}\) — we see that they differ only in swapping mL for mR. If we are not comfortable eyeballing things, we’d like a better justification for why it is “safe” to exchange mL for mR. However, the one-time pad rule (Claim 2.2.1) shows that \(\mathscr{L}^{OTP}_{ots-L}\) in fact has the same behavior as a library \(\mathscr{L}_{hyb-2}\) that doesn’t use either of mL or mR. Now, in a program that doesn’t use \(m_L\) or \(m_R\), it is clear that we can switch them.

    Having made this crucial change, we can now perform the same sequence of steps, but in reverse.

    Screen Shot 2019-02-16 at 1.31.28 AM.png

    \(\mathscr{L}_{otp-rand}\) has been replaced with \(\mathscr{L}_{otp-rea}\)l. Again, this has no effect on the library’s behavior, due to Claim 2.2.1. Note that the library composition lemma is being applied with respect to a different common \(\mathscr{L}^{\ast}\) than before (now \(m_R\) instead of \(m_L\) is being used).

    Screen Shot 2019-02-16 at 1.28.19 AM.png

    A subroutine call has been inlined, which has no effect on the library’s behavior. The result is exactly \(\mathscr{L}^{OTP}_{ots-R}\).

    Putting everything together, we showed that \(\mathscr{L}^{OTP}_{ots-L}\equiv\mathscr{L}_{hyb-1}\equiv · · · \equiv \mathscr{L}_{hyb-4} \equiv \mathscr{L}^{OT}_{ots-R}\). This completes the proof, and we conclude that one-time pad satisfies the definition of one-time secrecy.

    Discussion:

    We have now seen our first example of a hybrid proof. The example illustrates features that are common to all hybrid proofs used in this course:

    • Proving security amounts to showing that two particular libraries, say \(\mathscr{L}_{left}\) and \(\mathscr{L}_{right}\), are interchangeable
    • To show this, we show a sequence of hybrid libraries, beginning with \(\mathscr{L}_{left}\) and ending with \(\mathscr{L}_{right}\). The hybrid sequence corresponds to a sequence of allowable modifications to the library. Each modification is small enough that we can easily justify why it doesn’t affect the calling program’s output probability.
    • Simple things like factoring out & inlining subroutines, changing unused variables, consistently renaming variables, removing & changing unreachable statements, or unrolling loops are always “allowable” modifications in a hybrid proof. As we progress in the course, we will add to our toolbox of allowable modifications. For instance, if we want to prove security of something that uses a one-time-secret encryption \(\Sigma\) as one of its components, then we are allowed to replace \(\mathscr{L}^{\Sigma}_{ots-L}\) with \(\mathscr{L}^{\Sigma}_{ots-R}\) as one of the steps in the hybrid proof