How does one prove that Big Step semantics and Small Step semantics are equivalent for IMP?
Don't proceed by induction on $P$, i.e. by structural induction on the syntax of programs. This is because structural induction is quite weak, and is likely to fail on while loops.

Look at the inference rules for the big step semantics for while, in particular at the while-true rule which handles the case where the guard is true. In such case, you'll see that in one of the premises we have the same while loop. Roughly, the rule defines the behaviour of while in terms of itself.

(I didn't check your own rule, and used mine instead, but it should be simple to adapt the reasoning to yours.)

$$
\dfrac{
\sigma\models \phi \quad
\langle c, \sigma \rangle \to_b \sigma'
\quad
\langle while\ \phi\ do\ c, \sigma' \rangle \to_b \sigma''
}{\langle while\ \phi\ do\ c, \sigma \rangle \to_b \sigma''}
$$

If we proceed by structural induction, when we handle such case, we only get an induction hypothesis for $c$, wince it is a subterm of $while\ \phi\ do\ c$. That however provides no help in coping with he last premise involving the $while$ itself.

The solution is to use the induction principle generated by the rules for $\to_b$, instead. Doing that, when handling the rule above, we have two induction hypotheses, namely that the small step semantics 


reduces $\langle c, \sigma \rangle$ to some $\sigma'$ state in some $N$ steps
reduces $\langle while\ \phi\ do\ c, \sigma' \rangle$ to some $\sigma''$ state in some $M$ steps


Exploiting those properties, it is possible to show that, using (something like) $N+M+1$ steps, we can reduce $\langle while\ \phi\ do\ c, \sigma \rangle$ to $\sigma''$ using small steps.

The other rules can be handled in a similar way.

When you write such proofs, I strongly suggest to always check the while-true case first, since that's the "hardest". Checking it first helps avoiding wasting effort on other simpler (but long) cases, only to discover that the proof can not be completed and all the work done has to be thrown away.



Assume we have these as the inference rules for the big step semantics. (If rules omitted)
$$
\begin{array}{c}
\dfrac{
}{\langle skip, \sigma \rangle \to_b \sigma}
\qquad
\dfrac{
\langle e, \sigma \rangle \to_e v
}{\langle x:=e, \sigma \rangle \to_b \sigma[x\mapsto v]}
\\
\dfrac{
\langle c_1, \sigma \rangle \to_b \sigma'
\qquad
\langle c_2, \sigma' \rangle \to_b \sigma''
}{\langle c_1;c_2, \sigma \rangle \to_b \sigma''}
\\
\dfrac{
\sigma\models \lnot\phi \quad
}{\langle while\ \phi\ do\ c, \sigma \rangle \to_b \sigma}
\qquad
\dfrac{
\sigma\models \phi \quad
\langle c, \sigma \rangle \to_b \sigma'
\quad
\langle while\ \phi\ do\ c, \sigma' \rangle \to_b \sigma''
}{\langle while\ \phi\ do\ c, \sigma \rangle \to_b \sigma''}
\end{array}
$$

We immediately get the following induction principle.

Let $p(c,\sigma,\sigma')$ be any property of a command and two states.
To prove that
$$
\forall c,\sigma,\sigma'.\ \langle c \sigma \rangle \to_b \sigma' \implies p(c,\sigma,\sigma')
$$
it suffices to check all of the following:


$\forall \sigma.\ p(skip,\sigma,\sigma)$
$\forall x,e,\sigma,v.\ \langle e, \sigma \rangle \to_e v \implies
p(x:=e, \sigma, \sigma[x\mapsto v])$
$\forall \sigma,\sigma',\sigma''.\ 
p(c_1, \sigma, \sigma') \land p(c_2, \sigma', \sigma'')
\implies p(c_1;c_2, \sigma, \sigma'')$
$\forall \phi,c,\sigma.\ \sigma\models \lnot\phi \implies
p(while\ \phi\ do\ c, \sigma, \sigma)$
$\forall c,\phi,\sigma,\sigma',\sigma''.\ 
\sigma\models \phi \land
p(c, \sigma, \sigma') \land
p(while\ \phi\ do\ c, \sigma', \sigma'') \implies
p(while\ \phi\ do\ c, \sigma, \sigma'')$


Note that in item 4 we get the induction hypotheses on the subterms, very much like what would happen using structural induction.

In step 5, instead, we get both an induction hypothesis on the subterm $c$, and (crucial!) another induction hypothesis on the $while$ itself (on different states).

For your case, choose a suitable property $p(c,\sigma,\sigma')$ such as "there is some natural $N$ for which $c,\sigma$ terminates in $N$ small steps in stale $\sigma'$".