|
Abstract : |
In this talk, given in April 2000, I introduced the topic of the correctness of the sets of transactions supported by cryptographic processors. There has been much work on verifying crypto protocols, which are typically sets of 3-5 transactions exchanged by two principals. Yet when we look at actual implementations, there are typically 50 transactions supported by each principal?s cryptographic facility (which might be a smartcard, cryptoprocessor, cryptographic service provider or security software library). Just as there are failures in which an opponent can achieve an undesired result by cutting and pasting valid transactions, so also there are failures in which an opponent uses cryptographic transactions in an order that was not anticipated by the facility?s designer. I can make this clear using an example I discovered shortly after this talk was given, and which is discussed in some detail in my book [1]. It works against many of the security modules ? hardware cryptoprocessors ? used by banks to manage ATM networks in the 1980s., |
