View article

The Gong, Needham and Yahalom (GNY) logic is a belief-based logic for analyzing cryptographic protocols. It o ers signi cant advantages over its predecessor, the Burrows, Abadi and Needham (BAN) logic, which has been successful in formally discovering aws and redundancies in several well-known protocols. Manual analysis of protocols using the GNY logic, however, is cumbersome, as the logic has a large set of inference rules. This report proposes a modi ed GNY logic, and describes the implementation of a protocol analysis tool based on that logic. The modi cations are introduced to ensure that the logical statements derivable from a given protocol are all deducible in a nite number of steps. The nature of the modi cations is such that no useful inferences are lost. The tool o ers a facility to automatically generate proofs of protocol goals. It also generates a logical description of the state attained after every protocol step, thus allowing the stepwise development of protocols. The tool has proved useful in mechanically verifying the need for several inference rules which are absent from the original GNY logic.