Polynomial ring with arbitrarily many variables in ZF
Your "functions with finite support" approach is the standard approach to take to this, and is very likely what any author who considers the question trivial has in mind. The correct notion of "finite" to take when defining monomials is the usual one, as you have done (this is necessary for the polynomial ring you get to be the free commutative $k$-algebra on its variables).
Just to give some evidence that this approach is standard, this is the definition of $k[X]$ used in Lang's Algebra, for instance. (Lang describes this construction rather tersely on page 106 as an example of the more general monoid algebra construction described on pages 104-5. Lang's construction of the set $M$ of monomials is a little different from yours: he defines it as a subset of the free abelian group on $X$, which he constructs as the group of finite-support functions $X\to\mathbb{Z}$ on page 38.)
Note that it is not actually necessary to observe that every polynomial involves only finitely many variables to define or verify the properties of addition and multiplication. Indeed, addition can just be defined pointwise on the coefficients and makes sense for arbitrary functions from $M$ to $k$. Multiplication also makes sense for arbitrary functions from $M$ to $k$ (which you can think of as formal power series): you just need to define the coefficient of a given monomial $x_1^{k_1}\dots x_n^{k_n}$ in a product, and you can do this by the usual convolution formula. You then just have to check that if two functions $M\to k$ each have finite support, then so does their product; this is straightforward (a monomial in the support of the product must be the product of monomials in the support of each of the factors). The verification of the basic properties of multiplication then works exactly as it does in the case of finitely many variables.
Here is an option which takes place between your two suggestions, without appealing to choice:
Direct limit of finitely generated subrings.
We define $k[X]$ to be the direct limit of the system $\{ k[Y]\mid Y\in[X]^{<\omega}\}$ with inclusions as the embeddings.
Now to check that the operations are well-defined we only need to check they restrict properly to finitely generated subrings. But that's true almost by definition.
Also, note that "the free commutative $k$-algebra generated by $X$ indeterminate" is a fairly robust algebraic description. And it can be interpreted, if need be, as a direct limit of finitely generated structures.