Formal analysis of a TPM-based secrets distribution and storage scheme

Ronald Toegl, Georg Hofferek, Karin Greimel, Adrian Leung, Raphael C.W. Phan, Roderick Bloem

    Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-review

    2 Citations (Scopus)

    Abstract

    Trusted Computing introduces the Trusted Platform Module (TPM) as a root of trust on an otherwise untrusted computer. The TPM can be used to restrict the use of cryptographic keys to trusted states, i.e., to situations in which the computer runs trusted software. This allows for the distribution of intellectual property or secrets to a remote party with a reasonable security that such secrets will not be obtained by a malicious or compromised client. We model a specific protocol for the distribution of secrets proposed by Seving et al. A formal analysis using the NuSMV model checker shows that the protocol allows an intruder to give the client an arbitrary secret, without the client noticing. We propose an alternative that prevents this scenario.

    Original languageEnglish
    Title of host publicationProceedings of the 9th International Conference for Young Computer Scientists, ICYCS 2008
    Pages2289-2294
    Number of pages6
    DOIs
    Publication statusPublished - 2008
    EventInternational Conference for Young Computer Scientists 2008 - Zhang Jia Jie, Hunan, China
    Duration: 18 Nov 200821 Nov 2008
    Conference number: 9th
    https://ieeexplore.ieee.org/xpl/conhome/4708920/proceeding (Proceedings)

    Conference

    ConferenceInternational Conference for Young Computer Scientists 2008
    Abbreviated titleICYCS 2008
    CountryChina
    CityZhang Jia Jie, Hunan
    Period18/11/0821/11/08
    Internet address

    Keywords

    • Model checking
    • Protocol analysis
    • Trusted computing

    Cite this