Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols