PGP User's Guide, Volume II: Special Topics -- RANDSEED: filename for random number seed