We address a problem that arises in cryptographic protocol analysis
when the equational properties of the cryptosystem are taken into 
account: in many situations it is necessary to guarantee that certain 
terms generated during a state exploration are in normal form with 
respect to the equational theory. We give a tool-independent methodology 
for state exploration, based on unification and narrowing, that 
generates states that obey these irreducibility constraints, called 
contextual symbolic reachability analysis, prove its soundness and 
completeness, and describe its implementation in the Maude-NPA protocol 
analysis tool. Contextual symbolic reachability analysis also introduces 
a new type of unification mechanism, which we call asymmetric 
unification, in which any solution must leave the right side of the 
solution irreducible. We also present experiments showing the 
effectiveness of our methodology.