A weakest precondition approach to active attacks analysis