Katholieke Universiteit Leuven
Public key Kerberos (PKINIT) is a standard authentication and key establishment protocol. Unfortunately, it suffers from a security flaw when combined with smart cards. In particular, temporary access to a user's card enables an adversary to impersonate that user for an indefinite period of time, even after the adversary's access to the card is revoked. In this paper, the authors extend shoup's key exchange security model to the smart card setting, and examine PKINIT in this model. Using this formalization, they show that PKINIT is indeed flawed, propose a fix, and provide a proof that this fix leads to a secure protocol.