The automatic analysis of cryptographic protocols by using formal methods on concurrent languages is a subject widely treated in the literature. From its beginning in the decade of the 70s, the field has been gaining maturity and consolidation. The Timed Concurrent Constraint Language (tccp in short) is a declarative concurrent programming language which, like other concurrent languages, allows us to intuitively model concurrent and reactive systems. In particular, cryptographic protocols can be specified in a very compact way thanks to certain features such as the non-determinism and concurrency, which are necessary to model such kind of systems. In this work, we show a method to specify cryptographic protocols using tccp. We have defined specifications for the actions that principals usually do during a protocol run. Moreover, we have defined a hostile environment in which agents run the protocol. The environment is actually the representation of the popular intruder model of Dolev-Yao. We use the Needham-Schroeder public key authentication protocol to illustrate the approach.