Proper time gauge is $\dot N = 0;$ this can be imposed at the level of the action, as in Halliwell. Introduce a gauge-fixing term $S_{gf} = \int_{t'}^{t''} dt \left[ \Pi \left( \dot N - \chi \right) \right]$, so that the action is now $S + S_{gf} = \int_{t'}^{t''} dt \left[ p_{\alpha} \dot q ^{\alpha} - NH + \Pi \left( \dot N - \chi \right) \right]$. To make the action BRST invariant, add in the ghost action terms $S_{gh} = \int_{t'} ^{t''} dt \left[ \bar \rho \dot c + \bar c \dot \rho - \bar \rho \rho + c \{ \chi , H \} \bar c + \rho \frac{\partial \chi}{\partial N} \bar c \right]$ for a total action $S_{T} = S + S_{gf} + S_{gh} = \int_{t'}^{t''} dt \left[ p_{\alpha} \dot q ^{\alpha} - NH + \Pi \left( \dot N - \chi \right) +\bar \rho \dot c + \bar c \dot \rho - \bar \rho \rho + c \{ \chi , H \} \bar c + \rho \frac{\partial \chi}{\partial N} \bar c \right]$ (the ghost fields are Grassman variables satisfying boundary conditions $c(t') = 0 = c(t'')$). This is now invariant under BRST transformations (given in terms of Poisson brackets on a variable $F$ by $\delta F = \{ F , \Lambda \Omega \}$ where $\Omega = c H + \rho \Pi$ and $\Lambda$ is an anticommuting parameter (for BRST to be a true canonical transformation, $\Lambda$ should be constant). Then the full path integral over the extended phase space $(P,Q)$ (physical together with ghost variables) is

(1)where

(2)To change the gauge choice $\chi$, perform the BRST transformation given by $\Lambda = -\frac{i}{\hbar} \int dt \ \ \bar c \left( \tilde \chi - \chi \right)$. Because $\Lambda$ is not a constant, this is not a true canonical transformation on $(P,Q)$, and the measure picks up a Jacobian relating the Liouville measure on $( \tilde P, \tilde Q )$ to that on $(P,Q)$:

(3)This Jacobian has the effect of changing the gauge-fixing function from $\chi$ to $\tilde \chi$ in $S_{T}$. Note that since $S_{T}$ is invariant under BRST, we now have the same path integral, expressed in terms of $( \tilde P, \tilde Q )$ (which have the same initial and final conditions as $(P,Q)$, due to boundary conditions on $\bar c$). So this establishes independence of the propagator from gauge choice.