# Default values for badcrdfile.