Degree Name

Master of Science (Hons.)


Department of Computer Science


The existence of strong cryptoalgorithms is not sufficient to guarantee the security and/or authentication required in a system. To obtain an assurance for the security and/or authentication required, the underlying cryptoalgorithm must be used within a set of rules or procedures known as a protocol. Even if the cryptoalgorithm were secure, it is possible to subvert the protocol. There are numerous instances of failures in protocols employing public key and private key cryptoalgorithms. Several systems exist for analysis of protocols, to find such failures in them. These systems use formal analysis methods based on a model of communicating state machines or modal logics of belief like BAN and GNY. Besides, it is difficult to understand the working of protocols by looking at the description of messages in them. This thesis proposes a graphical user interface based tool for aiding in the design and analysis of cryptographic protocols. It provides a feature to display the working of protocols in the form of a schematic diagram, as an educational tool for understanding protocols. Secondly, it provides an interface to an existing program for performing automated GNY logic analysis. The tool, we propose also provides facilities for single stepping through protocols whilst viewing the beliefs attained by the principals, viewing of proofs derived from the GNY tool, and a feature for run-time modification of initial assumptions. It has been used to perform analysis of well known protocols and the expected results are obtained for them.



Unless otherwise indicated, the views expressed in this thesis are those of the author and do not necessarily represent the views of the University of Wollongong.