Mechanising a protocol for smart cards

Abstract

Paulson’s Inductive Approach for verifying traditional cryptographic protocols is tailored to those where agents make use of smart cards. An intruder can actively exploit other agents’ cards, which can be stolen or cloned. The approach is demonstrated on the Shoup-Rubin protocol, which is modelled and verified thoroughly. The protocol achieves strong goals of confidentiality, authentication and key distribution. However, our proofs highlight that a few messages require additional explicitness in order to guarantee those goals to the peers when the cards’ data buses are unreliable.