6 Fixed typos.

Your are writing $\times$ in the second but last line of your proof of the successor step. Are you aware of the fact that general iterated forcing is more complicated than taking the product? (There are cases, like Cohen forcing, where iteration is the same as product, though.)

Let me just discuss the two step iteration for the moment. The problem is that typically, the second forcing notion $P_1$ is not in your ground model $M$. For example, even if both $P_0$ and $P_1$ are supposed to be forcing with, say, closed subsets of the real line without isolated points (perfect sets) ordered by inclusion, the second forcing is not forcing with perfect sets in $M$ but with perfect sets in $M[G_0]$, where $G_0$ is $P_0$-generic over $M$. So in general, you only have a $P_0$-name $\dot P_1$ for the second forcing and you need to cook up an iteration $P_0*\dot P_1$ that is not just a product ($\dot P_1$ is not even a partial order at this point).

Now suppose that $P$ is a forcing notion in $M$ and $\dot Q$ is a $P$-name for a forcing notion (the name is in $M$, too). We argue in $M$. As a first approximation, $P*\dot Q$ consists of all pairs $(p,\dot q)$ where $p\in P$, $\dot q$ is a $P$-name and $p\Vdash\dot q\in\dot Q$.
This is ordered by letting $(p_0,\dot q_0)\leq(p_1,\dot q_1)$ iff $p_0\leq p_1$ and $p_0\Vdash\dot q_0\leq\dot q_1$.

The problem with this definition is that $P*\dot Q$ now is a proper class and not a set.
You have to restrict the names $\dot q$ that are allowed to some suitable set, either some $V_\alpha$ for sufficiently large $\alpha$ or to those $\dot q$ that appear as first coordinates in the name (for the underlying set of the partial order with the name) $\dot Q$.

Now, if $G$ is $P$-generic over $M$ and $H$ is $\dot Q_G$-generic over $M[G]$, then you can define a filter $F\subseteq P*\dot Q$ as follows:

$F=G*H=\{(p,\dot q)\in P*\dot Q:p\in G\wedge\dot q_G\in H\}$

This filter turns out to be $P*\dot Q$-generic over $M$ and $G$ and $H$ can be recovered from it. This also settles the question of iterations of finite length and successor steps.

Now. For iterations of limit length there is the problem that we cannot prove (at least I cannot prove) that given a sequence of filters that are generic over each other there is a smallest transitive model of ZFC containing the sequence.
This is why for infinite iterations one defines iterations of forcing notions rather than limits of sequences of models.

Given an iteration of forcing notions of length $\delta$, from a generic $G$ for the iteration we can recover generic filters $G_\alpha$, $\alpha<\delta$, for each step of the iteration, but not every sequence $(G_\alpha:\alpha<\delta)$ of generics gives rise to a generic filter for the iteration.
For example, generic sequences $(G_\alpha)_{\alpha<\delta}$ obtained using a finite support iteration look different from generic sequences obtained by countable support iteration of the same forcing notions.

I hope this clarifies things. I also recommend taking a look at Kunen's book Set Theory, An Introduction to Independence Proofs. I also have a follow up question here.

After seeing your comment, I added this: What I am saying above also applies to the situation where the posets are in the model.
If the posets are $P$ and $Q$ are in $M$, $G$ is $P$-generic over $M$ and $H$ is $Q$ generic over $M[G]$, then $G\times H$ (with the usual definition) is $P\times Q$-generic over $M$. (Iteration $*$ is just $\times$ in this case.) In the case of iterations of infinite length I believe it is still true that from a sequence of generic generics you cannot always get a single iterationgeneric.

How do we see that $G\times H$ is $P\times Q$-generic over $M$? Let $D\in M$ be a dense subset of $P\times Q$. Let $D_G=\{t:\exists s\in G((s,t)\in D)\}$. I claim this is dense in $Q$. Let $q\in Q$. By density of $D$, $D_q=\{s:(s,t)\in D\wedge t\leq q\}$ is dense in $P$. Hence there is $s\in G\cap D_q$. Now for some $t\leq q$, $(s,t)\in D$.
This implies the density of $D_G$.
Hence there is $t\in H\cap D_G$. It follows that there is $s\in G$ with $(s,t)\in D$. Thus, $D\cap(G\times H)\not=\emptyset$.

After seeing your comment, I added this: What I am saying above also applies to the situation where the posets are in the model.
If the posets are $P$ and $Q$ are in $M$, $G$ is $P$-generic over $M$and $H$ is $Q$ generic over $M[G]$, then $G\times H$ (with the usual definition) is $P\times Q$-generic over $M$. (Iteration $*$ is just $\times$ in this case.)In the case of iterations of infinite length I believe it is still true that from a sequence of generic you cannot always get a single iteration.

How do we see that $G\times H$ is $P\times Q$-generic over $M$? Let $D\in M$ be a dense subset of $P\times Q$. Let $D_G=\{t:\exists s\in G((s,t)\in D)\}$. I claim this is dense in $Q$.Let $q\in Q$. By density of $D$, $D_q=\{s:(s,t)\in D\wedge t\leq q\}$ is dense in $P$.Hence there is $s\in G\cap D_q$. Now for some $t\leq q$, $(s,t)\in D$.
This implies the density of $D_G$.
Hence there is $t\in H\cap D_G$. It follows that there is $s\in G$ with $(s,t)\in D$. Thus, $D\cap(G\times H)\not=\emptyset$.

Your are writing $\times$ in the second but last line of your proof of the successor step. Are you aware of the fact that general iterated forcing is more complicated than taking the product? (There are cases, like Cohen forcing, where iteration is the same as product, though.)

Let me just discuss the two step iteration for the moment. The problem is that typically, the second forcing notion $P_1$ is not in your ground model $M$. For example, even if both $P_0$ and $P_1$ are supposed to be forcing with, say, closed subsets of the real line without isolated points (perfect sets) ordered by inclusion, the second forcing is not forcing with perfect sets in $M$ but with perfect sets in $M[G_0]$, where $G_0$ is $P_0$-generic over $M$. So in general, you only have a $P_0$-name $\dot P_1$ for the second forcing and you need to cook up an iteration $P_0*\dot P_1$ that is not just a product ($\dot P_1$ is not even a partial order at this point).

Now suppose that $P$ is a forcing notion in $M$ and $\dot Q$ is a $P$-name for a forcing notion (the name is in $M$, too). We argue in $M$. As a first approximation, $P*\dot Q$ consists of all pairs $(p,\dot q)$ where $p\in P$, $\dot q$ is a $P$-name and $p\Vdash\dot q\in\dot Q$.
This is ordered by letting $(p_0,\dot q_0)\leq(p_1,\dot q_1)$ iff $p_0\leq p_1$ and $p_0\Vdash\dot q_0\leq\dot q_1$.

The problem with this definition is that $P*\dot Q$ now is a proper class and not a set.
You have to restrict the names $\dot q$ that are allowed to some suitable set, either some $V_\alpha$ for sufficiently large $\alpha$ or to those $\dot q$ that appear as first coordinates in the name (for the underlying set of the partial order with the name) $\dot Q$.

Now, if $G$ is $P$-generic over $M$ and $H$ is $\dot Q_G$-generic over $M[G]$, then you can define a filter $F\subseteq P*\dot Q$ as follows:

$F=\{(p,\dot q):p\in F=G*H=\{(p,\dot q)\in P*\dot Q:p\in G\wedge\dot q_G\in H\}$

This filter turns out to be $P*\dot Q$-generic over $M$ and $G$ and $H$ can be recovered from it. This also settles the question of iterations of finite length and successor steps.

Now. For iterations of limit length there is the problem that we cannot prove (at least I cannot prove) that given a sequence of filters that are generic over each other there is a smallest transitive model of ZFC containing the sequence.
This is why for infinite iterations one defines iterations of forcing notions rather than limits of sequences of models.

Given an iteration of forcing notions of length $\delta$, from a generic $G$ for the iteration we can recover generic filters $G_\alpha$, $\alpha<\delta$, for each step of the iteration, but not every sequence $(G_\alpha:\alpha<\delta)$ of generics gives rise to a generic filter for the iteration.
For example, generic sequences $(G_\alpha)_{\alpha<\delta}$ obtained using a finite support iteration look different from generic sequences obtained by countable support iteration of the same forcing notions.

I hope this clarifies things. I also recommend taking a look at Kunen's book Set Theory, An Introduction to Independence Proofs. I also have a follow up question here.

3 Corrected typos.
2 Clarified some things.
1