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. Some declarative approaches based on CLP, Haskell or Maude have been proposed for the specification and analysis of communication protocols. In this paper, we propose the Timed Concurrent Constraint Language (tccp in short) as the specification language for protocols. tccp is a declarative concurrent programming language which allows one to intuitively model concurrent and reactive systems. Cryptographic protocols can be specified in a very compact way
thanks to certain features of the language such as the non-deterministic behavior and concurrency. We show how to specify the basic actions that are usually performed during a protocol run. Thereafter, we show how to specify the participants in the protocol. Finally, we specify the intruder model by means of a hostile environment in which principals run the protocol. The model considered for the intruder is the popular model of Dolev-Yao. We use along the paper the Needham-Schroeder public key authentication protocol to illustrate the approach. The basic actions and the intruder implementation can be reused for the specification of many different protocols.