The reachability problem for cryptographic protocols with non-atomic keys can be solved via a simple constraint satisfaction procedure. Confidentiality can be posed as a reachability problem. The protocol model is a parametric strand model, with a free term algebra. We use term closure with respect to derivability rules to characterize the attacker. The problem is decidable when the number of legitimate strands is bounded. There is an implementation in Prolog, and it found a type-violation attack on the Needham-Schroeder-Lowe protocol.