Extending NCP for protocols using public keys

This paper presents extensions to a technique for specifying and analyzing nonmonotonic cryptographic protocols (NCP) that use asymmetric keys. We introduce new actions and inference rules, as well as slight modifications to the update function. An important observation is that reasoning about the origin of messages is quite different when dealing with asymmetric key protocols. We also introduce the notion that keys in certificates should be bound to the principals receiving them. We extend the technique to meet the binding requirements and show how the flaw in the Denning and Sacco (1981) public key protocol, that was discovered by Abadi and Needham (1994), is revealed. We demonstrate the extended technique using one protocol of our own and the Needham and Schroeder (1978) public key protocol. Finally, we introduce and analyze a fix to a known weakness in Needham and Schroeder´s protocol using our extended technique