Precise definition for cryptographic protocol?
There are several definitions of cryptographic protocols, each of which tries to capture some particular features of interest.

I start with Goldwasser, Micali, and Rackoff definition (1985): They first defined interactive Turing machines (ITM), based of which they defined (two-party) interactive protocols. An ITM is a special TM equipped with one read-only and one write-only communication tape. A pair of ITMs  constitutes an interactive protocol if the read-only communication tape of party A coincides with the write-only communication tape of party B, and vice versa. The power of parties and the adversary model is then defined accordingly (see the paper).

The multi-party case was later defined by Goldreich, Micali, and Wigderson (1987). They modeled a secure multi-party game in an elegant way, though the paper (as Goldreich states himself) leaves a lot of doors open. For a more concrete discussion see: http://www.wisdom.weizmann.ac.il/~oded/pp.html.

Finally, a much stronger model was proposed by Canetti (2001). In his paper, he defines a framework called Universal Composability (UC), based on which he defines the cryptographic protocols and puts forward a notion of security for them.

As far as I recall, the last paper cites a lot of other works which try to define and model security protocols. Therefore, I strongly advise you to take a look at it.