UCT CS Research Document Archive

An Environment to Facilitate the Teaching of GNY-Based Security Protocol Analysis Techniques

Saul, Elton and Andrew Hutchison (2001) An Environment to Facilitate the Teaching of GNY-Based Security Protocol Analysis Techniques. In Proceedings Second World Conference in Information Security Education, Edith Cowen University, Perth, Western Australia.

Full text available as:
PDF - Requires Adobe Acrobat Reader or other PDF viewer.


The development of cryptographic logics to analyze security protocols has provided one technique for ensuring the correctness of security protocols. However, it is commonly acknowledged that analysis using a modal logic such as GNY tends to be inaccessible and obscure for the uninitiated. In this paper we describe a graphical tree-based specification environment which operates in conjunction with a Prolog-based GNY analyzer. This environment can be used to easily construct GNY statements using dynamically-constructed contextualized pop-up menus. We will show how this environment helps to distance students and protocol engineers from the syntactical element of GNY analysis, allowing them to focus more on the associated semantics and distil the critical issues that arise during protocol analysis. By freeing individuals to focus on an analysis, instead of hampering them with the necessary syntax, we can ensure that the fundamental concepts and advantages related to GNY analysis are kept in mind and applied as well.

EPrint Type:Conference Paper
Keywords:Security protocol analysis, GNY logic, cryptographic protocols, security education and practice
ID Code:122
Deposited By:Arnab, A
Deposited On:06 May 2004
Alternative Locations:http://www.cs.uct.ac.za/Research/DNA/resources/publications_repository/saul2001_wise2.pdf