Idle port scanning uses side-channel attacks to bounce scans off of a "zombie" host to stealthily scan a victim IP address and determine if a port is open or closed, or infer IP-based trust relationships between the zombie and victim. In this paper, we present results from building a transition system model of a network protocol stack for an attacker, victim, and zombie, and testing this model for non-interference properties using model checking. We present two new methods of idle scans in this paper that resulted from our modeling effort, both of which have been verified through implementation. One is based on TCP RST rate limiting and the other on SYN caches. The latter does not require the attacker to send any packets to the victim on the port to be scanned, not even forged packets. This gives the attacker additional capabilities beyond known idle scan techniques, such as the ability to scan ports that are blocked by a firewall or locate hosts on trusted networks, to whic...