Formal Modeling and Automatic Security Analysis of Two-Factor and Two-Channel Authentication Protocols