Continuous authentication helps mitigate the risk of session hijacking, insider attack, and privilege abuse. Applying zero trust principles, this paper proposes a family of four formally specified access control models to account for the use of continuous authentication to monitor user access patterns in user-facing software applications, each model providing increasingly expressive user modeling capabilities. We name these models Zero Trust Continuous Authentication (ZTCA). Deploying a ZTCA model requires the authoring of policies. To ease the challenge of developing ZTCA policies, we studied the problem of automatically generating ZTCA policies from declarative usability and security requirements. We devised a novel SAT encoding for the automated policy formulation problem, so that policy formulation can be performed by state-of-the-art SAT solvers. Empirical experiments demonstrate that our novel encoding approach runs significantly faster than a competing encoding approach previously published in the literature.