Invariant Evaluation through Introspection for Proving Security Properties