The ISO 5-pass authentication in χ-Spaces

摘要

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. The χ-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 resulting in the preservation in the implementation of the properties proved in the formal model.