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.