{'fraction_non_alphanumeric': 0.025913338997451147, 'fraction_numerical': 0.0055225148683092605, 'mean_word_length': 4.633971291866029, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Towards a Formal Security Analysis of the Sevecom API

Sevecom 1 was an EU 6th Framework project aimed at defining “a consistent and futureproof solution to the problem of Vehicular communications VC [Vehicular communications]/IVC [Inter-Vehicular Communications] security”. An early conclusion of the project was that the solution must include the use of a tamper-resistant cryptographic device on board the vehicle. Indeed, the design of such a device has been a common conclusion of much recent research in the area [9]. A feature of the Sevecom project is that it defines the API for the tamper resistant device (TRD). This is a security-critical part of the design, since the API regulates how applications on the vehicle (which in the worst case may include malware, viruses, applications deliberately placed in the system by crooked vehicle owners, etc.) access the secret key material stored in the TRD. Flaws in the designs of previous APIs for similar devices in the ATM (cash machine) network and for cryptographic USB key tokens have been shown to lead to catastrophic attacks, whereby sensitive keys are revealed in the clear [2, 3]. In the last few years, we have been researching formal techniques for analysing such interfaces and checking them for flaws. This has resulted in the detection of a number of previously unknown flaws, as well as positive results of assurance of the absence of certain classes of attack on revised designs [4, 6, 10]. In this paper, we describe the first results of the application of our techniques to the Sevecom API. In doing so, we aim to make clear the security policy the device is intended to implement, and to investigate the extent to which it achieves this. We find that some, but not all, of the stated security goals are achieved by the design, and we show how the shortcomings can be exploited. We discuss changes to the API which prevent the exploit. The paper is structured as follows: first we describe the operation of the Sevecom API and the goals it sets out to achieve, in section 2. Then we describe our formal modelling approach in section 3, showing how we formalised the goals and the threat model, and explaining our abstractions. We give our results obtained using the SAT-based model checker SATMC in section 4. We describe our plans for further analysis and conclude in section 5.