caption The starting point is $\lib{prf-real}$.

lib \lib{prf-real}
    \key \gets \bits^\secpar

    proc \prfquery(X_1 \| X_2)
        Y_1 := F(\key,X_1)
        Y_2 := F(\key,Y_1 \oplus X_2)
        return $Y_2$
end

\equiv

caption We can add a cache $\prftable[\cdot]$ so that each output is computed only once.

lib
    \key \gets \bits^\secpar

    proc \prfquery(X_1 \| X_2)
        if $\prftable[X_1\|X_2]$ undefined:
            Y_1 := F(\key,X_1)
            \prftable[X_1\|X_2] := F(\key,Y_1 \oplus X_2)
        return $\prftable[X_1\|X_2]$
end

\equiv

caption Apply the PRF-security of $F$ in a 3-hop maneuver.

lib
    proc \prfquery(X_1 \| X_2)
        if $\prftable[X_1\|X_2]$ undefined:
            Y_1 := \prfquery_F(X_1)
            \prftable[X_1\|X_2] := \prfquery_F(Y_1 \oplus X_2)
        return $\prftable[X_1\|X_2]$
end
lib \lib{prf-real}^F
    \key \gets \bits^\secpar

    proc \prfquery_F(X)
        return $F(\key,X)$
end

\indist

lib
    proc \prfquery(X_1 \| X_2)
        if $\prftable[X_1\|X_2]$ undefined:
            Y_1 := \prfquery_F(X_1)
            \prftable[X_1\|X_2] := \prfquery_F(Y_1 \oplus X_2)
        return $\prftable[X_1\|X_2]$
end
lib \lib{prf-rand}^F
    proc \prfquery_F(X)
        if $\prftable[X]$ undefined:
            \prftable[X] \gets \bits^n
        return $\prftable[X]$
end

\equiv

lib
    proc \prfquery(X_1 \| X_2)
        if $\prftable[X_1\|X_2]$ undefined:
            if $R[X_1]$ undefined: $R[X_1] \gets \bits^\secpar$
            Y_1 := R[X_1]
            if $R[ Y_1 \oplus X_2 ]$ undefined:
                R[ Y_1 \oplus X_2 ] \gets \bits^\secpar
            \prftable[X_1\|X_2] := R[ Y_1 \oplus X_2 ]
        return $\prftable[X_1\|X_2]$
end

\equiv

caption Our intuition says that $Y_1 \oplus X_2$ never repeats; in other words, $R[Y_1 \oplus X_2]$ is always undefined. To argue this formally, let's trigger a bad event if this is not the case.

lib
    proc \prfquery(X_1 \| X_2)
        if $\prftable[X_1\|X_2]$ undefined:
            if $R[X_1]$ undefined: $R[X_1] \gets \bits^\secpar$
            Y_1 := R[X_1]
            if $R[ Y_1 \oplus X_2 ]$ defined: 
                \badvar := \mytrue
            else:
                R[ Y_1 \oplus X_2 ] \gets \bits^\secpar
            \prftable[X_1\|X_2] := R[ Y_1 \oplus X_2 ]
        return $\prftable[X_1\|X_2]$
end

\indist

caption If we can show that the bad event has negligible probability, then we can arbitrarily change the library's behavior after the bad event is triggered.

lib
    proc \prfquery(X_1 \| X_2)
        if $\prftable[X_1\|X_2]$ undefined:
            if $R[X_1]$ undefined: $R[X_1] \gets \bits^\secpar$
            Y_1 := R[X_1]
            if $R[ Y_1 \oplus X_2 ]$ defined: 
                \badvar := \mytrue
                R[ Y_1 \oplus X_2 ] \gets \bits^\secpar
            else:
                R[ Y_1 \oplus X_2 ] \gets \bits^\secpar
            \prftable[X_1\|X_2] := R[ Y_1 \oplus X_2 ]
        return $\prftable[X_1\|X_2]$
end

\equiv

caption Clean up the redundant logic.

lib
    proc \prfquery(X_1 \| X_2)
        if $\prftable[X_1\|X_2]$ undefined:
            if $R[X_1]$ undefined: $R[X_1] \gets \bits^\secpar$
            Y_1 := R[X_1]
            if $R[ Y_1 \oplus X_2 ]$ defined: 
                $\badvar := \mytrue$
            $R[ Y_1 \oplus X_2 ] \gets \bits^\secpar$
            \prftable[X_1\|X_2] := R[ Y_1 \oplus X_2 ]
        return $\prftable[X_1\|X_2]$
end

\equiv


caption We can swap the assignment order of $\prftable[X_1 \| X_2]$ and $R[Y_1 \oplus X_2]$.

lib
    proc \prfquery(X_1 \| X_2)
        if $\prftable[X_1\|X_2]$ undefined:
            if $R[X_1]$ undefined: $R[X_1] \gets \bits^\secpar$
            Y_1 := R[X_1]
            if $R[ Y_1 \oplus X_2 ]$ defined: 
                $\badvar := \mytrue$
            \prftable[X_1\|X_2] \gets \bits^\secpar
            R[ Y_1 \oplus X_2 ] := \prftable[X_1\|X_2]
        return $\prftable[X_1\|X_2]$
end

\equiv

caption We can move $\prftable[X_1\|X_2] \gets \bits^\secpar$ earlier. After doing so, it is clear that $R[\cdot]$ does not affect the output of $\prfquery$: It is used only to determine whether to trigger the bad event.

lib
    proc \prfquery(X_1 \| X_2)
        if $\prftable[X_1\|X_2]$ undefined:
            \prftable[X_1\|X_2] \gets \bits^\secpar

            if $R[X_1]$ undefined: $R[X_1] \gets \bits^\secpar$
            Y_1 := R[X_1]
            if $R[ Y_1 \oplus X_2 ]$ defined: 
                $\badvar := \mytrue$
            R[ Y_1 \oplus X_2 ] := \prftable[X_1\|X_2]
        return $\prftable[X_1\|X_2]$
end

\equiv

caption Instead of triggering the bad event as $\prfquery$ is called, we can do so at the end of time. This will not change the bad event's probability.

lib \lib{prf-rand}
    proc \prfquery(X_1 \| X_2)
        if $\prftable[X_1\|X_2]$ undefined:
            \prftable[X_1\|X_2] \gets \bits^\secpar
            \mathcal{X} := \mathcal{X} \cup \{ X_1 \| X_2 \}
        return $\prftable[X_1\|X_2]$

    proc end()
        for $X_1 \| X_2 \in \mathcal{X}$:
            if $R[X_1]$ undefined: $R[X_1] \gets \bits^\secpar$
            Y_1 := R[X_1]
            if $R[ Y_1 \oplus X_2 ]$ defined: 
                $\badvar := \mytrue$
            R[ Y_1 \oplus X_2 ] := \prftable[X_1\|X_2]
end