A Verifiable Language for Cryptographic Protocols

We develop a formal language for specifying cryptographic protocols in a structured and clear manner, which allows verification of many interesting properties; in particular confidentiality and integrity. The study sheds new light on the problem of creating intuitive and human readable languages, that are analysable with respect to interesting properties. Furthermore it motivates and is an example of, a novel, more general methodology of language design by first verbosely describing the semantics in a mathematical language, e.g. a logic, then restricting the properties of interest to be computable, and finally systematically transforming it into a more intuitive specification language, maintaining this tractability.