Proof of soundness (integrity) of cryptographic protocols (Q1330133)

For reasons beyond the control of either the authors or the editors, this special section has been unusually long delayed in publication; so long in fact that a great deal of related work has been done in the interim. It would have been desirable to summarize these developments in this preface, but this would have changed the nature of the preface from a brief note describing the circumstances that led to the invitation to the authors to prepare the paper that makes up the special section, to a full fledged survey paper in itself. After careful consideration, it was decided that this would be inconsistent with the original intent for the special section. In 1990 a workshop on the Mathematical Concepts (or Principles) of Dependable Systems was held at the Mathematisches Forschungsinstitut Oberwolfach in Germany. The purpose of the workshop was to examine mathematical techniques developed to make it possible to prove the proper functioning of complex systems -- where the system could be either hardware, software, information protocols, etc., or combinations of these components. Principal researchers in each of these areas were invited to take part in the workshop, and did -- but as is so often the case at scientific meetings, one area emerged as a clear center of gravity for the workshop. This was the topic of applying formal methods to the proof of soundness or correctness of information or cryptographic protocols. The organizers of the workshop felt that the results reported in this area were so important to the cryptology community that they deserved publication as a whole, as opposed to publication as separate and isolated papers; hence this special section. This paper which is essentially an introduction for the invited paper that follows [\textit{R. Kemmerer}, \textit{C. Meadows} and \textit{J. Millen}, ibid. 7, No. 2, 79--130 (1994; Zbl 0814.94011)], describes the background for the workshop and the challenge problem(s) that provided a unifying theme for the three systems of formal analysis treated in it.