A Formal Approach for Automated Reasoning about Off-Line and Undetectable On-Line Guessing