To overcome problems in understanding security protocols, a constructivist approach is used. Learners are enabled to experiment with a given protocol, either alone or in a team of co-learners. This means, to use pre-defined and automatically generated PROMELA building blocks for all communicating parties and to support students in playing some roles in an interactive way. To explain these building blocks more detailed, the Needham-Schroeder-Public-Key authentication protocol is given as an example.

All building blocks were realized by means of the preprocessor. A proper combination of simulation and visualization components cares for hiding unnecessary details and restricts on the essentials. The SPIN validator is used to check the correctness of students solutions or generate trail files to give a hint in case of a quandary. To allow collaborative experiments, the whole facility is embedded into a framework for application sharing. The latter is equipped with components for annotation and note taking as well as for recording.