A gauge symmetry means that the equations of motion do not uniquely determine the evolution of all the configuration variables, i.e., that the Euler-Lagrange system is under-determined. The canonical example is the case of classical electrodynamics, where the equations of motion are
\begin{equation}
(\partial^2\delta^\mu_\nu-\partial^\mu\partial_\nu)A_\mu=0\tag1
\end{equation}
Any configuration of the form $A_\mu=\partial_\mu\Lambda$, for arbitrary $\Lambda=\Lambda(x)$, trivially solves these equations, which means that given a solution $A$, the configuration $A+\partial\Lambda$ is also a solution. Therefore, the solution to the equations of motion is not unique, the system is under-determined, and there is a gauge symmetry. Even if we fix $\Lambda=0$ at the surface where the initial conditions are given, the function $\Lambda$ can be non-zero at any later time, and therefore both $A$ and $A+\partial \Lambda$ solve the equations of motion and satisfy the initial conditions.
When the system is under-determined, the system has no well-defined Green function, inasmuch as if the latter existed, the system could be evolved from its initial conditions to a unique solution at a later time. In this sense, a gauge theory has no propagator. In the classical case this poses no problem, but in the quantum-mechanical case this is a disaster, for the usual reasons (which we shall not summarise here).
The general analysis of gauge systems can be found in e.g. ref.1, which we encourage OP and anyone interested to read. In short, the cornerstone of the theory is Noether's second theorem, which can be summarised as an off-shell identity of the form
\begin{equation}
D^i\mathrm{EL}_i[\varphi]\equiv 0\tag2
\end{equation}
where $\mathrm{EL}$ is the Euler-Lagrange operator, and $D$ is a certain vector field that generates the gauge symmetry. This theorem implies that the Euler-Lagrange equations are not all independent, and therefore the system is under-determined, as mentioned before.
Of course, any transformation of the form
\begin{equation}
D^i=T^{ij}\mathrm{EL}_j,\qquad\text{with}\qquad T^{ij}=-T^{ji}\tag3
\end{equation}
trivially satisfies eq.2. These transformations, sometimes called skew, are not to be regarded as true gauge transformations; any system possesses them and they do not make the system under-determined. If all the gauge symmetries are skew, the equations of motion determine the evolution uniquely, and the system admits a propagator; the quantum-mechanical theory is safe and healthy (barring aside possible Gribov ambiguities as mentioned in the comments).
Consider for example a scalar theory with equations of motion
\begin{equation}
(\partial^2+m^2)\phi=0\tag4
\end{equation}
This system is invariant under $\phi\to\phi+\psi$, where $\psi(x)$ is any function that satisfies
\begin{equation}
(\partial^2+m^2)\psi=0\tag5
\end{equation}
Is this transformation a gauge symmetry? Of course not! This transformation is trivial, in the sense that it is merely a manifestation of the linear character of the equations of motion. If $\psi$ is zero at the surface where the initial conditions are given, then it will be zero at any later time, because $\psi$ is constrained to satisfy $(\partial^2+m^2)\psi=0$. The transformation $\phi\to\phi+\psi$ does not represent a redundancy, because $\psi$ is constrained to satisfy an equation whose solution is unique; fixing $\psi$ at a Cauchy surface fixes this function at any later time, so it does not represent a new degree of freedom.
Consider now our initial example, the equations of motion of electrodynamics, but now let us introduce the Lorentz gauge, $\partial\cdot A\equiv0$. The equations of motion read
\begin{equation}
\partial^2A=0,\qquad\partial\cdot A=0\tag6
\end{equation}
whose solution is now unique: the system does not have gauge degrees of freedom other than those that are trivial. Of course, the system is invariant under transformations of the form $A\to\partial \Lambda$, where $\Lambda$ is constrained to satisfy $\partial^2\Lambda=0$, but this is similar to our previous example: if $\Lambda$ is zero at the surface where the initial conditions are specified, it will remain zero at any later time, because it is constrained to
satisfy $\partial^2\Lambda=0$. This "residual gauge symmetry" is trivial as far as Noether's second theorem is concerned, in the sense that it does not make the system under-determined; the solution to the Euler-Lagrange system is unique, and the propagator is well-defined; the quantum-mechanical theory is safe and healthy.
You may argue that if the Lagrangian of the gauge-fixed theory is invariant under $\delta A=\partial \Lambda$, with $\partial^2\Lambda=0$, then the functional integral must diverge, because there are directions in the configuration space where the Lagrangian is constant. Convince yourself that this is not the case by comparing this invariance to the one discussed before, the invariance under $\delta\phi=\psi$ with $(\partial^2+m^2)\psi=0$. The functional integral of a scalar field is not divergent despite this invariance, and the reason is precisely the fact that Noether's second theorem does not apply: the invariance is trivial and it does not lead to an under-determined system of equations of motion. In a heuristic sense, you can say that the condition $\partial^2\Lambda=0$ is restrictive enough so that the transformation $\delta A=\partial\Lambda$ has measure zero in the space of field configurations -- it does not contribute to the functional integral.
References
- DeWitt, The global approach to quantum field theory, chapters 2-6.
