There are two approaches to formally specify cryptographic protocols:
Computational Models
In computational models, keys and messages are bitstrings.
Symbolic Models
In symbolic models, messages and keys are terms, cryptographic primitive are black-box functions over term.