Smart cards can be formalised realistically within Paulson's inductive approach for security protocols. The cards can be stolen and/or cracked by an eavesdropper. The kernel of their built-in algorithm works correctly, so they can't be used as oracles, but their I/O interface doesn't, so they send correct outputs unreliably.
This makes it possible to model the Shoup-Rubin protocol (EUROCRYPT'96) and reason formally about its goals - integrity, authenticity, unicity, agent authentication, session-key knowledge, confidentiality. The analysis highlights the minimal conditions for the protocol to meet these goals, and shows some design weaknesses that are unknown to the authors' proof of security by the Bellare-Rogaway approach. It is also proved that adding explicitness strengthens the design.