Verifying SeVeCom using set-based abstraction

Sebastian Mödersheim, Paolo Modesti

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    134 Downloads (Pure)


    We formally analyze the Secure Vehicle Communication system developed by the EU-project SeVeCom, using the AIF framework which is based on a novel set-abstraction technique. The model involves the hardware security modules (HSMs) of a number of cars, a certification authority, and the protocols executed between them. Each participant stores a database of keys that can be added or deleted depending on the different operations. The AIF-framework allows us to model and automatically analyze such databases without bounding the number of steps that the system can make and, in contrast to previous approaches in protocol abstraction, can handle databases that do not monotonically grow (and thus allow for revocation of keys). We report on two new attacks found and verify that under some reasonable assumptions, the system is secure in a black-box cryptography model.
    Original languageEnglish
    Title of host publicationIEEE International Wireless Communications and Mobile Computing Conference, IWCMC 2011, Istanbul, Turkey, 4-8 July, 2011
    Number of pages6
    Publication statusPublished - 12 Aug 2011
    Event2011 IEEE International Wireless Communications and Mobile Computing Conference - Istanbul, Turkey
    Duration: 4 Jul 20118 Jul 2011


    Conference2011 IEEE International Wireless Communications and Mobile Computing Conference


    Dive into the research topics of 'Verifying SeVeCom using set-based abstraction'. Together they form a unique fingerprint.

    Cite this