Semi-automatic Synthesis of Security Policies by Invariant-Guided Abduction