Formal verification of revocation approaches in identity-based cryptography

Grundner-Culemann, Sophia (2024): Formal verification of revocation approaches in identity-based cryptography. Dissertation, LMU München: Fakultät für Mathematik, Informatik und Statistik

Abstract

Traditional public key cryptography relies on certificates to attribute a public key to the owner. This approach produces significant cost in secure communication because certificates need to be downloaded and their validity status needs to be tracked. Identity-based Cryptography (IBC) offers an alternative by deriving public keys directly from their owners’ unique identifiers, e.g. email addresses. This method eliminates the need to manage certificates. A Trusted Third Party (TTP) generates the user’s corresponding secret keys. A problem arises when a key is revoked because the owner must be able to continue using their identifier. There are several proposals to handle the revocation problem in IBC. However, there is little abstract analysis of this problem and the security considerations are limited to manual proofs for specific approaches and informal explanations of general properties. This work gives a broader overview: It systematizes revocation mechanisms overall, identifies three classes of revocation mechanisms in IBC and provides a formalization for an automated prover to analyze the security properties expected of each class. The overall systematization happens along two dimensions: 1. “explicit/implicit” (i.e. validity either needs to be checked or can be ignored by third parties) and 2. “directly/indirectly” (i.e. the mechanism manages revoked keys or it manages valid keys). All identity-based methods are implicit and indirect, obsoleting all secret keys at a certain cue and issuing new material to all non-revoked users. They differ in how users obtain new key material. This work identifies: 1. The renewal method, where keys are completely replaced, 2. the individual-update method, where each user receives a customized update token for their individual key, and 3. the universal-update method, where all users receive the same update token for their individual keys. The formalization captures the stages that all classes have in common and the processagnostic security goals they ideally achieve. It is adaptable to each class through the mathematical dependencies it models for the keys and yields a blueprint model for an automated analysis with a trace-based prover tool. The proof-of-concept implementation in Tamarin is the first high-level security analysis of IBC-revocation mechanisms. It confirms both the weaknesses to decryption key exposure that were found in individual update mechanisms if they fail to re-randomize the key in the update process and the collusion attack for the universal update approach that was previously only acknowledged indirectly. It also reconciles the notions of Decryption Key Exposure Resistance and of Forward-/Post-Compromise Security, which were previously never discussed together. Based on this work, research might consider more detailed mathematical context of a certain IBC scheme and its revocation mechanism if and when the problem of modeling distributive laws is solved. This would allow for a more fine-grained security analysis and increase trust in revocable identity-based mechanisms. More generally, the proposed formalization can be used as blueprint for the formal verification of obsolescence-based revocation mechanisms and applications that use key updates outside of IBC.

• Dokumententyp: Dissertationen (Dissertation, LMU München)
• Keywords: Identity-based Cryptography, IBE, Tamarin, Formal Verification, Cryptography, Symbolic Modeling
• Themengebiete: 000 Allgemeines, Informatik, Informationswissenschaft ; 000 Allgemeines, Informatik, Informationswissenschaft > 004 Informatik
• Fakultäten: Fakultät für Mathematik, Informatik und Statistik
• Sprache der Hochschulschrift: Englisch
• Datum der mündlichen Prüfung: 20. Dezember 2024
• 1. Bericht­erstatter:in: Kranzlmüller, Dieter