Security protocols are often defined in informal notations which have
no clear semantics and only describe the message sequence when the
protocol is successfully completed.  This can be a source of incorrect
interpretations of protocols as well as an obstacle to their formal
verification.

To address this problem, we formalize the syntax of the informal
notations and present their semi-automatic translation into Abadi and
Gordon's spi-calculus, one of the most successful frameworks for the
formal specification and verification of cryptographic protocols.  Our
main idea is to make the actions of each principal explicit on the
basis of its _knowledge_, i.e., what keys, nonces and names it knows
at each point in a protocol.