Fault-based transition for crypto proof (a la Shoup) with big probability of fault - does it work? background

In [Shoup2004], Victor Shoup synthesizes the 'sequence of games' technique for proving security properties:
Roughly it consists in a sequence from game_0 to game_n, game_0 consisting in the property. You prove that for any two games the two probability of success are negligibly close, then you prove that the probability of success of game_n is negligibly close to the target probability; it follows that the probability of success for game_0 is negligibly close to the target probability, which proves the property.

Shoup identifies 3 types of transitions, namely indistinguishability-based, failure-event based and bridging step (which is a bit apart).

In the failure-event based transition, the two games are equivalent unless a failure event $F$ happens; then Shoup states:


  to prove that $Pr[S_i ]$ is negligibly close to $Pr[S_{i+1}]$, it suffices to prove that $Pr[F]$ is negligible.


EDIT writing it as a theorem could make it clearer:

Theorem(Shoup's Framework)
Let $(G_i)_{i=0..n}$ be a sequence of games with their respective "Fault" event $(S_i)_{i=0..n}$
If $\forall i ~ |Pr[S_i]-Pr[S_{i+1}]|$ negl. ("transition lemmas")
and If |Pr[S_n] - Target| negl.
Then |Pr[S_0] - Target| negl.

Lemma(Shoup's Fault-based transition)
If $Pr[S_{i+1}|$ not $F] = Pr[S_i]$
And $Pr[F]$ negl.
Then $|Pr[S_{i+1}]-Pr[S_i]|$ negl.

Question

It is not hard to prove that this is true. However I think that the requirement on $Pr[F]$ is way too strong: one can prove security with much more frequent faults.
Namely I think I can prove it holds for non-negligible $Pr[\bar{F}]$ (proba of non-fault) as soon as the success probability $Pr[S_{i+1}]$ is negligibly close to the target probability (which is 1/2 here, didn't look if it works for target 0).
The latter ("$Pr[S_{i+1}] - 1/2$ negligible") will prove right later in the proof anyway thanks to the other transitions.

Question: does the following theorem hold, and has it been added to Shoup's framework for crypto proofs ?

Argumentation

Lemma(My Fault-based transition):
(we assume Target = 1/2)
If Pr[$S_1$ | not F ] = Pr[$S_0$]
and If Pr[not F] non-negl.
and If |Pr[$S_1$]-1/2| negl
Then |Pr[$S_1$]-Pr[$S_0$]| negl.

proof

Let "OK" be then event "not F".
When a failure event happens,
the algorithm can still make a random guess before halting,
thus $Pr[S_1 | \bar{OK}] = 1/2$

$Pr[S_1] \geq Pr[S_1 | OK ].Pr[OK] + Pr[S_1 | \bar{OK}].Pr[\bar{OK}]$
$Pr[S_1] \geq Pr[S_0].Pr[OK] + ½ (1 - Pr[OK])$
$Pr[S_1] \geq Pr[OK](Pr[S_0] - ½) + ½$
$(Pr[S_1] - ½)\frac{1}{Pr[OK]} + ½ \geq Pr[S_0]$
$Pr[S_0] - Pr[S_1] \leq (½ - Pr[S_1])(1 + \frac{1}{Pr[OK]})$

Then since $(½ - Pr[S_1])$ is negligible
and $(1 + \frac{1}{Pr[OK]})$ is polynomially bounded,
$Pr[S_0] - Pr[S_1]$ is negligible which ends the proof.

Recall that the hypothesis "$|Pr[S_{i+1}] - 1/2|$ negligible" will be proven right later in the proof, so it's not a problem having it.
My experience of such proofs is that often you're proving a much stronger statement: in any execution of Game i+1, either everything is distributed identically to Game i or else F must have happened. In other words, the conditional distribution of game i+1 conditioned on F not happening is identical to the distribution of Game i.

For example, one of Bellare's applications of this technique is the "poisoned point" principle: you choose the value of a hash function or similar at a particular point. As long as the adversary does not query the function at this particular point, the new game is identically distributed to the old one. If he does query this point, you abort.

Of course what you will argue next is that since you chose your poisoned point at random, the chance of the adversary querying this exact point is negligible. But the actual game-hop doesn't depend on the probability of F happening, it only says either all is well or else F must have happened.

Failure events with non-negligible probabilities happen frequently in hybrid arguments. They tend to make for very lossy reductions of course but the principle stays the same, the hop itself is Pr[S_{i+1} = 1 | not F] = Pr[S_i = 1] and then you compute the probability of F in a separate step to get your "concrete security" constants.