I would like to proof the following theorem:

Let $\pi:X\rightarrow X/G$ be a principal $G$-bundle (say of varieties, Zariski locally trivial), then $\pi^*$ induces an equivalence between modules on the quotient and equivariant modules on the total space.

Now I would like to know if this can be proven along the following lines:

1. Define a model structure on some category $V$ containing the category of simplicial varieties. Maybe the category simplicial presheaves?

2. Define the category of quasi coherent modules over an object of $V$. For an ordinary variety $X$ this should be the category of quasicoherent $\mathcal O_X$-modules. For the "action simplex" $$... G\times G\times X \Rrightarrow G\times X \Rightarrow X$$ this should be the category of $G$ - equivariant qc $\mathcal O_X$-modules, where $G$ is an algebraic group and $X$ is an ordinary variety.

3. Proof that in the situation of the theorem the map from the action simplex to $X/G$ is a weak equivalence.

4. Proof that weak equivalences between objects of $V$ induce equivalences between the corresponding module categories.

I'm not yet experienced enough with model categories to judge if this program has a chance to go through. I am quite optimistic about the first three steps. However about the last one my only vague intuition is that homotopy equivalent topological spaces have "same" vector bundles. Maybe one can define a model structure such that weak equivalences are precisely the morphisms which induce equivalences between module categories?

So my questions are:

Has this a chance to work?

If yes: What is the model structure and does one proof 3+4? Is it done somewhere?
If no: Why not? Why is it a bad idea?

P.S. I know how to proof the theorem in a much easier, hands on way. In this question I am mainly interested in a proof along the above lines.