next up previous
Next: Conclusions Up: CryptoLog: A Theorem Prover Previous: An Example: The

Future Work

We intend to extend the analyser in several ways.

At this moment, the assumptions generated by the action-statements are hard-coded in the analyser. We would like to remove the definition of the action-statements from the analyser and give them as input to the theorem prover. This has three major advantages:

For instance, the action Nonce (``generate a new nonce''), might mean different things in different protocols. In one protocol, it is sufficient that it is a number that has never been used before. Hence, a counter (kept in stable storage) that is incremented for each run of the protocol suffices. However, for another protocol, it might be essential that the nonce is not predictable (i.e. is chosen at random). By redefining the definition of Nonce we can easily accommodate the two different uses.

Secondly, we would like to add properties of cryptographic algorithms to the input part of the analyser and hence, remove the implicit assumption that the integrity of encrypted messages is always preserved.

However, a precondition for this extension is a complete type-system, which we intend to add to the analyser.

Thirdly, we are going to build a code generator that transforms the protocol specification into executable code. Since the specification contains useful implementation guidelines, this transformation should not be too difficult.

Finally, we will further investigate whether the analyser could easily be extended to predict hidden flaws (such as some attacks based on the interleaved execution of two runs of the protocol).

For instance, the analyser should be able to alert for the flaw in the original Needham-Schroeder protocol with public keys [1,5]. See also table 10-a. An intruder C waits until A starts the protocol with C; C can start another run of the protocol with B, pretending to be A (see also table 10-b).

 
Table 10:  The Needham-Schroeder protocol with public keys

We have here two separate runs of the protocol, in which a message (2b) cannot be deciphered by C; however, C can reuse that message in the first protocol run and get the secret from A.

We expect that it will not be too hard to add this capability to the analyser.



next up previous
Next: Conclusions Up: CryptoLog: A Theorem Prover Previous: An Example: The



Bart De Decker
Mon Aug 4 16:31:43 MET DST 1997