Quite a bit of structure is actually definable in terms of the block cipher round function, and from this structure, one can produce block cipher round function invariants that measure cryptographic security.
A portion of this answer is essentially the same as my previous answer here, so in that case, we shall omit the proofs of the results.
If $G,H$ are groups, then we say that a function $\phi:G\rightarrow H$ is a heap homomorphism if there exists a group homomorphism $\psi:G\rightarrow H$ along with a $b\in H$ where $\phi(g)=b\psi(g)$ for all $b\in B.$ Equivalently, the mapping $\phi:G\rightarrow H$ is a heap homomorphism if and only if
$\phi(xy^{-1}z)=\phi(x)\phi(y)^{-1}\phi(z)$ whenever $x,y,z\in G$. A bijective heap homomorphism is said to be a heap automorphism.
For this post, let $U_{0},\dots,U_{n-1},V_{0},\dots,V_{n-1}$ be groups. Suppose that $I_{i}:U_{i}\rightarrow V_{i}$ is a group isomorphism whenever $0\leq i<n$. Let $K=U_{0}\times\dots\times U_{n-1},X=V_{0}\times\dots\times V_{n-1}$.
Then define a group isomorphism $\iota:K\rightarrow X$ by letting
$\iota(u_{0},\dots,u_{n-1})=(I_{0}(u_{0}),\dots,I_{n-1}(u_{n-1}))$.
If $0\leq i<n$, then let $s_{i}:V_{i}\rightarrow V_{i}$ be an arbitrary bijection.
Define a mapping $S:V_{0}\times\dots\times V_{n-1}\rightarrow V_{0}\times\dots\times V_{n-1}$ by letting $S(v_{0},\dots,v_{n-1})=(s_{0}(v_{0}),\dots,s_{n-1}(v_{n-1}))$.
Let $\Gamma:X\rightarrow X$ be a heap automorphism. Let $P=\Gamma\circ S$, and define a mapping $F:K\times X\rightarrow X$ by letting
$F(k,x)=\iota(k)P(x)$.
Proposition: The mappings $K^{2}\times X\rightarrow X,(j,k,x)\mapsto\iota(jk^{-1})x$ and $X^{3}\rightarrow X,(x,y,z)\mapsto xy^{-1}z$ are first order definable in $(K,X,F)$.
Let $\pi_{i}:X\rightarrow V_{i}$ be the projection group homomorphism. Let $\simeq_{i}$ be the equivalence relation on $X$ where we set $x\simeq_{i}y$ if and only if $\pi_{i}(x)=\pi_{i}(y)$. I claim that the set of equivalence relations $\{\simeq_{0},\dots,\simeq_{n-1}\}$ is higher order definable in $(K,X,F)$ under reasonable hypotheses about the block cipher $F$, but to prove this claim, we will need to go over a few lemmas. From the definability of $\{\simeq_{0},\dots,\simeq_{n-1}\}$, we can produce many block cipher round function invariants that measure non-linearity and also the avalanche effect.
For $0\leq i<n$, and $j\in U_{i}$, let $s_{i}^{j}$ be the permutation of $V_{i}$ defined by letting $s_{i}^{j}(v)=I_{i}(j)s_{i}(v)$.
If $0\leq i<n$, then let $H_{i}$ be the group of all permutations of $V_{i}$ generated by $s_{i}^{j}\circ(s_{i}^{k})^{-1},(s_{i}^{j})^{-1}\circ s_{i}^{k}$.
Let $H$ be the group of all permutations of $X$ generated by all permutations of the form $F_{j}^{-1}\circ F_{k},F_{j}\circ F_{k}^{-1}$. Observe that
$F_{j}\circ F_{k}^{-1}(x)=\iota(jk^{-1})(x)$ and $F_{j}^{-1}\circ F_{k}(x)=S^{-1}[\Gamma^{-1}[\iota(j^{-1}k)]S(x)]$. In particular,
$H$ is generated by the permutations of the form $x\mapsto\iota(m)(x)$ along with the permutations of the form $S^{-1}[\iota(m)S(x)]$. Said differently, $H$ is generated by the permutations of the form
$$(x_{0},\dots,x_{n-1})\mapsto(I_{0}(m_{0})(x_{0}),\dots,I_{n-1}(m_{n-1})(x_{n-1}))$$ and
$$(x_{0},\dots,x_{n-1})\mapsto(s_{0}^{-1}[I_{0}(m_{0})(s_{0}(x_{n-1}))],\dots,s_{n-1}^{-1}[I_{n-1}(m_{n-1})(s_{n-1}(x_{n-1}))]).$$
Thus, $H$ consists of all permutations of the form $h_{0}\times\dots\times h_{n-1}$ where $h_{i}\in H_{i}$ whenever $0\leq i<n$.
Therefore $H\simeq H_{0}\times\dots\times H_{n-1}$ as an external direct product. We may also write $H$ as an internal direct product $H_{0}^{\sharp},\dots,H_{n-1}^{\sharp}$ where $H_{i}^{\sharp}$ consists of all mappings $h\in H$ where if $h_{0},\dots,h_{n-1}$ are the mappings where $h(x_{0},\dots,x_{n-1})=(h_{0}(x_{0}),\dots,h_{n-1}(x_{n-1}))$ for all $x_{0},\dots,x_{n-1}$, then
$h_{j}$ is the identity function whenever $j\neq i$. Then $H_{i}^{\sharp}\simeq H_{i}$ whenever $0\leq i<n.$
We say that a group $G$ is superindecomposible if whenever $A,B$ are subgroups of $G$ with $ab=ba$ whenever $a\in A,b\in B$ and $G=AB$, then $|A|=1$ or $|B|=1$ (let me know in the comments if you can think of a better word than 'superindecomposible').
Theorem (Krull-Schmidt): Suppose that $G$ is a group that satisfies the ascending chain condition and descending chain condition on normal subgroups (any finite group satisfies this property). Furthermore, suppose that $G$ is written as an internal direct product of non-trivial directly indecomposible subgroups in two different ways, namely $G=G_{0}\times\dots\times G_{n-1}$ and $G=H_{0}\times\dots H_{n-1}$. Then there exists a permutation $\rho$ of $\{0,\dots,n-1\}$ such that
$G_{i}\simeq H_{\rho(i)}$ for $0\leq i<n$ and where
$$G=G_{0}\times\dots\times G_{r}\times H_{\rho(r+1)}\times\dots H_{\rho(n-1)}$$ whenever $0\leq r\leq n-1$.
Lemma: Suppose that $G$ is a finite group. If $G$ is an internal direct product of superindecomposible subgroups, then whenever we factor $G$ as internal direct products $G=G_{0}\times\dots\times G_{m-1}$ and $G=H_{0}\times\dots\times H_{n-1}$, then $m=n$, and there is some permutation $\rho:\{0,\dots,n-1\}\rightarrow\{0,\dots,n-1\}$ where $H_{i}=G_{\rho(i)}$ for $0\leq i<n$.
Theorem: There exists a higher order formula $\phi$ such that if the groups $H_{0},\dots,H_{n-1}$ are indecomposible, then $(K,X,F)\models\phi(z)$ if and only if $z=\{\simeq_{0},\dots,\simeq_{n-1}\}$.
Proof: Observe that the group $H$ is higher order definable in the structure $(K,X,F)$. Furthermore, the group $H$ has a unique up-to-permutation factorization
$H^{\sharp}_{0}\times\dots\times H^{\sharp}_{n-1}$ into its indecomposible factors. Therefore, the set of all indecomposible factors $\{H^{\sharp}_{0},\dots,H^{\sharp}_{n-1}\}$ is definable in $(K,X,F)$.
Now, for each $i$, let $\hat{\simeq}_{i}$ be the equivalence relation where we set
$x\hat{\simeq}_{i}y$ if and only if $h(x)=y$ for some $h\in H^{\sharp}_{i}$. Let
$\simeq_{i}$ be the equivalence relation on $X$ generated by
$\bigcup\{\hat{\simeq}_{j}\mid j\neq i\}$. Then $\{\simeq_{0},\dots,\simeq_{n-1}\}$ is definable from $\{H^{\sharp}_{0},\dots,H^{\sharp}_{n-1}\}$. Therefore, the set
$\{\simeq_{0},\dots,\simeq_{n-1}\}$ is definable in $(K,X,F)$. $\square$
From the definability of $\{\simeq_{0},\dots,\simeq_{n-1}\}$, we can define quite a few block cipher round function invariants.
If $T_{1},T_{2}$ are groups, and $f_{i}:T_{i}\rightarrow T_{i}$ for $i\in\{1,2\}$, then we say that $f_{1},f_{2}$ are affinely equivalent if there exists heap automorphisms $L_{1}:T_{1}\rightarrow T_{2},L_{2}:T_{2}\rightarrow T_{1}$ where
$f_{2}=L_{1}f_{1}L_{2}$. We say that a mapping $M$ is invariant under affine equivalence if $M(f)=M(g)$ whenever $f,g$ are affinely equivalent.
We say that a pair $(k,\Delta)$ is an S-boxification if $\Delta$ is a heap automorphism and whenever $x\simeq_{i}y$, then $\Delta\circ F_{k}(x)\simeq_{i}\Delta\circ F_{k}(y)$. The collection of all S-boxifications is higher order definable in $(K,X,F)$. Observe that there exists an S-boxification, namely the mapping $(e,\Gamma^{-1})$. Suppose now that
$(k,\Delta)$ is an S-boxification. Then it is easy to show that each $\simeq_{i}$ is a congruence with respect to $\Delta\Gamma^{-1}$. Therefore $\Delta=E\Gamma^{-1}$ for some heap automorphism $E$ where each $\simeq_{i}$ is a congruence with respect to $E$. Therefore, $\Delta\circ F_{k}=E'\circ S$ for some heap automorphism $E'$. Therefore, the quotient algebra $(X,\Delta\circ F_{k})/\simeq_{i}$ is affinely equivalent to $(V_{i},s_{i})$ for $0\leq i<n$. From these observations, we obtain the following fact.
Fact: If the mapping $M$ is invariant under affine equivalence and definable in higher order logic, then the mapping $M^{+}$ defined by letting
$M^{+}(F)=\{M(s_{0}),\dots,M(s_{n-1})\}$ is higher order definable in the structure $(K,X,F)$. Therefore, $M^{+}$ is a round function invariant parameter.