In this talk, I will describe the Cryptyc project, which is to design a domain-specific language for authentication protocols based on the spi-calculus. The main novel feature of the language is the use of type-and-effect systems to capture correspondence properties of authentication protocols. A subject reduction result shows that any well-typed program is guaranteed to satisfy the correspondence property. I will also discuss current work on extending Cryptyc to deal with larger classes of examples.