Using Task-Structured Probabilistic I/O Automata to Analyze Cryptographic Protocols