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 equivalent categories of 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.