Let $G$ be a finite group, and let $K$ be a field of characteristic zero.
Let $\phi(x\_1,\ldots,x\_n)$ be a first order formula in the language of group theory (so $\phi$ can be for example something of the form $\exists y\in G$ $y^2=x$ or $\exists y\_1,y\_2\in G $ $ x\_1=y\_1y\_2,x\_2=y\_2y\_1$).
For every such formula $\phi$ we consider the element 
$$t\_{\phi}:=\sum\_{\{(g\_1,\ldots g\_n)\in G^n| \phi(g\_1,\ldots g\_n)\}}g\_1\otimes g\_2\otimes\cdots\otimes g\_n$$
In other words, $t\_{\phi}$ is the sum over all tuples who satisfy the formula $\phi$. 
If now $\mu:G\to G$ is a group automorphism, then $\phi(g\_1,\ldots,g\_n)$ holds if and only if $\phi(\mu(g\_1),\ldots,\mu(g\_n))$ holds. It thus follows that the elements $t\_{\phi}$ are all $Aut(G)$-invariants inside $(KG)^{\otimes n}$.


Is there an elementary proof that the elements $t\_{\phi}$ span the invariant subspace $(KG^{\otimes n})^{Aut(G)}$?



First order formulas for finite groups and invariant theory
The assumption on the characteristic of $K$ implies that $(KG^{\otimes n})^{Aut(G)}$ is spanned by the indicator functions of the $Aut(G)$-orbits in $G^n$. So it suffices to observe that for every $(g\_1,\dots,g\_n) \in G^n$ the formula "$(x\_1,\dots,x\_n)$ belongs to the $Aut(G)$-orbit of $(g\_1,\dots,g\_n)$" is a first-order formula. 


But (if I remember correctly what a first-order formula is) this is clear, as it can be written as "$\exists (y\_g)\_{g \in G} \in G, y\_{g h}=y\_{g}y\_h, y\_g \neq y\_h$ if $g \neq h$ and $y\_{g\_i} = x\_i$".


