Modal logic approach for analyzing security protocol guessing attacks

In the field of security protocol formal verification, it is a new challenge to analyze security protocol guessing attacks. CKT5 logic, used as the base, is significantly extended in several aspects. Both public key cryptography and Vernam encryption are added to symmetric key cryptography of the original logic, which makes it more powerful in expressing security protocols. Perfect encryption hypothesis is not obeyed any more, and a series of definitions and rules are given to allow principals to guess and verify passwords. Theorems and lemmas given in this paper can describe features of on-line guessing attacks, and simplify the analysis procedure of guessing attacks. The extended logic can be used to analyze guessing attacks on security protocols including on-line guessing attacks.