Checking security properties by model checking