1 Department of Computer Science, Faculty of Science, Aarhus University, Aarhus University2 Computer Laboratory, University of Cambridge3 BRICS, Department of Computer Science, University of Aarhus, Ny Munkegade, DK-8000 Arhus C4 School of Computer Science, Soongsil University5 Department of Computer Science, University of Georgia
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