One of the many different approaches to proving properties of a cryptographic security protocol is to encode it within a process calculus [6],[7],[11],[12],[14],[20], and then to apply standard techniques from concurrency theory such as modelchecking [19] or equational reasoning [4],[5],[8],[9],[13],[15]. A promising recent development is to verify properties such as secrecy and authenticity via behavioural type systems [1],[2],[3],[10],[16],[17],[18]. This tutorial reviews the known type systems and results in this area, and suggests areas for further research.