Chapter V in the book Local algebra by Serre, introduces the notion of a "relative intersection product" meaning that if $f: X \to Y$ is a morphism of varieties with $Y$ regular and $x,y$ are cycles on $X$ and $Y$ respectively then we can define a cycle on $X$ denoted $x \cdot_f y$ and this product is stated in terms of a formula involving $Tor$ functors. In the case where $x = X$ one then denotes the aforementioned product by $f^{*}y$ which is then defined to be the pullback of the cycle $y$ to $X$.
Since this is a book on commutative algebra, it is perhaps not very surprising that this last section concerning applications to algebraic geometry is very sketched and lacking in several ways. By this I mean that for instance some properties of the pullback are mentioned, a projection formula being one of them, but the reader is only given a vague idea of how spectral sequences can be applied to prove this. Another point I would like to make is that only varieties over algebraically closed fields are considered, but there doesn't seem to be any reason why this should not work more generally.
The book is concluded by mentioning that the Tor formula can be used to extend intersection theory, regular schemes being one class of objects this should work for, so I suppose that it should be possible to develop the ideas introduced in chapter V in more generality. However from what I understand even the Stacks-project does this in the same settings as Serre.
My question: Is there any reference that introduces the "$Tor$"-formula and uses it to define the pullback of a cycle $y$ by any morphism of schemes $f: X \to Y$ with $Y$ regular (and possibly $X$,$Y$ integral and of finite type over a field $k$ which is not necessarily algebraically closed) and also proves the projection formula $f_{*}(x \cdot_f y) = f_{*}(X) \cdot y$ when $f$ is proper and both sides are defined?
I would like to add that Suslin and Voevodsky use this aforementioned machinery in their article "Singular homology of abstract algebraic varieties" in the case where $f: X \to S$ is a finite surjective morphism of integral ($k$)-schemes with $Y$ regular, so it should at least hold in that case.
Note: I have only skimmed parts of "Local algebra", so I am aware of the possibility that my questions can have been thoroughly dealt with in some disguise already earlier in the book, or perhaps what I am seeking can easily be done if one is more familiar with intersection theory and homological algebra.