Combining Abstract Interpretation and Model Checking for Analysing Security Properties of Java Bytecode