OK, let me try to expand on Chaum and van Antwerpen's proofs a bit. Please let me know if there's still something that doesn't convince you.
I'll start by rephrasing Chaum and van Antwerpen's theorem 1 using your notation:
Theorem 1: Even with infinite computing power, the probability that Sally can verify an invalid signature $s \ne m^k \bmod p$ is at most $1/q$.
To verify $s$, Victor chooses two random numbers $a$ and $b$ from $\mathbb Z_q = \{0, 1, \dotsc, q-1\}$ (see note below). However, the important bit is that Sally doesn't know $a$ and $b$; she only sees $c = s^a y^b \in G$.
Now, it's not hard to see that every value of $c$ seen by Sally corresponds to $q$ possible $(a,b)$ pairs: in particular, for any $a$ and $c$, we may solve for $b$ as follows:
$$\begin{aligned}
s^a y^b &= c \\
y^b &= s^{-a} c \\
b &= \operatorname{dlog}_y(s^{-a} c)\\
\end{aligned}$$
(This works because, in a cyclic group of prime order, the discrete logarithm is unique for any base not equal to 1; equivalently, $b \mapsto y^b$ is a bijection, and in fact a group homomorphism, from $\mathbb Z_q^+$ to $G$ for any $y \in G$, $y \ne 1$. The case $y = 1$ cannot occur, since $k \ne 0$ and $g \ne 1$ by construction.)
Now, assume that $s \in G$ and $m \ne 1$ (which Chaum and van Antwerpen's paper mandates). Then there exists some $x \in \mathbb Z_q$ such that $s = m^x$. If $x = k$, then the signature is valid, so an invalid signature must have $x \ne k$.
I'll now show that, if $x \ne k$, then for each of the $q$ different $(a,b)$ pairs corresponding to the $c$ sent by Victor, Sally would have to reply with a different $r$ to have it accepted. Like Chaum and van Antwerpen, I will do so using proof by contradiction. Specifically, assume that there exist two pairs $(a,b)$ and $(a^*,b^*)$ corresponding to the same $c$ and the same $r$. Then:
$$\begin{aligned}
m^{xa} g^{kb} =& c = m^{xa^*} g^{kb^*} &&&
m^{a} g^{b} =& r = m^{a^*} g^{b^*} \\
m^{xa} m^{-xa^*} =& g^{kb^*} g^{-kb} & \text{and} &&
m^{a} m^{-a^*} =& g^{b^*} g^{-b} \\
m^{x(a-a^*)} =& g^{k(b^*-b)} &&&
m^{a-a^*} =& g^{b^*-b} \\
\end{aligned}$$
Taking the base-$g$ discrete logarithm and letting $\mu = \operatorname{dlog}_g(m)$, we get $\mu x(a-a^*) = k(b^*-b)$ and $\mu (a-a^*) = b^*-b$. Substituting the latter into the former, we get $\mu x(a-a^*) = k \mu (a-a^*)$, and thus $x = k$. But this is only possible if the signature is, in fact, valid!
Thus, we've shown that, if $s \ne m^k$, any value of $r$ that Sally returns can only be valid for one $(a,b)$ pair. But since there are $q$ possible such pairs, each of which is equally likely, Sally has only a $1/q$ chance of guessing the correct one.
Note: This proof involves a few corner cases in which the version of the Chaum–van Antwerpen scheme given in the Handbook of Applied Cryptography differs from that in Chaum and van Antwerpen's original paper.
First, Chaum and van Antwerpen explicitly require that $m \ne 1$. This makes sense, since if $m = 1$, $s = m^k = 1$ regardless of $k$! I assume this is most likely just an oversight in the Handbook, but it may be important if the message $m$ might be chosen by an adversary.
Second, the Handbook says that $a$ and $b$ should be chosen at random from $\{1,2, \dotsc, q-1\}$, whereas Chaum and van Antwerpen also allow $a = 0$ and $b = 0$. Admittedly, these are somewhat peculiar cases — in particular, $a = 0$ implies that $c$ (and thus $r$, if Sally is honest) is independent of $s$ (and thus $m$)! Even so, these cases don't actually present a weakness, since they each occur only with probability $1/q$, and, importantly, Sally can't tell when they occur.
In fact, excluding $a = 0$ and $b = 0$ means that, at least in principle, Sally can exclude two of the possible $(a,b)$ pairs (or one, if $c=1$). Thus, the maximum probability of verifying an invalid signature may actually be as high as $1/(q-2)$. Of course, for practical values of $q$, that makes no real difference.
Also note that, in practice, one would usually use the compact representation recommended by Chaum and van Antwerpen, in which $G$ is mapped to $\{1, 2, \dotsc, q\} \subset \mathbb Z_p^*$ by the map $f(x) = \min(x, p-x)$, and the map $f$ is reapplied after any sequence of arithmetic operations in $\mathbb Z_p^*$. (This works because $p-1 \equiv -1 \bmod p$ is the generator of the order-2 subgroup of $\mathbb Z_p^*$.) Not only is this representation more compact than naively storing elements of $G$, but it makes it easy to map arbitrary messages to elements of $G \setminus \{1\}$ and avoids issues with bogus signatures outside $G$.
