Replace MD5 file hashing by SHA-1, both because it's faster (by 25% on 64 bit Linux) and because MD5 is no longer allowed in US FIPS 140-2 environments.
Closes #2790.