We implement the ISO 5-pass authentication protocol and study its correctness using the χ-Space framework. χ-Spaces is a novel domain specific programming language designed for developing protocols and in particular security protocols. χ-Spaces programming language is an implementation of SPL (Security Protocol Language), a calculus for the description and formal verification of security protocols. χ-Spaces is meant to fill in the gap between a formal specification of a protocol and its implementation, ideally resulitng in the preservation in the implementation of the properties proved in the formal model.
Proceedings of the Security and Management Conference (sam), 2002, p. 490-495
securtiy protocols; formal verification; programming languages