A Formalization of Off-Line Guessing for Security Protocol Analysis