# BusCount: A Provable Replay Protection Solution for Automotive CAN Networks

Authors: Daniel Zelle; Sigrid Gürgens
Journal: Security and Communication Networks
 (2021)

---

## Abstract

Information technology has become eminent in the development of modern cars. More than 50 Electronic Control Units (ECUs) realize vehicular functions in hardware and software, ranging from engine control and infotainment to future autonomous driving systems. Not only do the connections to the outside world pose new threats, but also the in-vehicle communication between ECUs, realized by bus systems such as Controller Area Network (CAN), needs to be protected against manipulation and replay of messages. Multiple countermeasures were presented in the past making use of Message Authentication Codes and time stamps and message counters, respectively, to provide message freshness, most prominently AUTOSAR’s Secure Onboard Communication (SecOC). In this paper, we focus on the latter ones. As one aspect of this paper, using an adequate formal model and proof, we will show that the currently considered solutions exhibit deficiencies that are hard if not impossible to overcome within the scope of the respective approaches. We further present a hardware-based approach that avoids these deficiencies and formally prove its freshness properties. In addition, we show its practicability by a hardware implementation. Finally, we evaluate our approach in comparison to counter-based solutions currently being used.


---

## Body

## 1. Introduction

Information technology has become an integral part of modern vehicles. More than 50 interconnected Electronic Control Units (ECUs) realize vehicular functions in hardware and software ranging from engine control and connected infotainment systems to future autonomous driving systems. The in-vehicle communication between ECUs is realized with bus systems like CAN (Controller Area Network Bus [1]). Further, vehicles communicate with the outside world (e.g. with their manufacturer’s backend systems, with the garage’s On-Board-Diagnose (OBD) devices) via different communication interfaces. Usually, these interfaces are not strictly separated from the in-vehicle network (the OBD port for example must have access to a car’s ECUs to extract error codes). This poses serious security threats, one of the possible attack vectors being in-vehicle communication. The vehicle owner can for example install a tuning box to suppress or inject messages that control engine operations in order to achieve more horsepower. This in turn may damage the engine and violate the warranty. Moreover, third-party devices connected to the OBD port can inject messages to the regular in-vehicle network. In [2], Koscher et al. have shown various attack techniques like Packet Sniffing and Targeted Probing, Fuzzing, and Reverse-Engineering.Multiple countermeasures were presented in the past to protect in-vehicle networks (see Section2.4). Early work can be traced back to EVITA [3] that introduced Message Authentication Code (MAC) truncation in order to cope with the small bandwidth of field buses such as CAN. This approach has been adapted by AUTomotive Open System ARchitecture AUTOSAR in SecOC [4]. Including a freshness value in a message’s MAC can in principle prohibit fuzzing or replay attacks. Most of the current approaches consider a monotonic counter value.In this paper, we discuss our new counter-based approach BusCount based on our ideas introduced in [5], present its full formal verification, discuss its implementation and provide a practical evaluation. We further oppose it to a generic system that captures the principles of today’s counter-based approaches for freshness protection. The principle idea of our approach is to use the messages that are sent on a specific bus as a pulse generator for the counter of this bus, resulting in only one counter per bus. To cope with the loss of counter values e.g. caused by technical problems or an attack, our approach includes counter synchronization. Further, it requires the sending and reception of messages to be processed simultaneously to MAC generation and verification. Therefore, we propose a hardware-based solution: The CAN controller is enhanced by the functionality to maintain a counter and to manage MAC generation and verification while the main ECU processors can be inactive at times.In the next section, we present the principles of in-vehicle communication based on CAN, our attack model, the protection goals we will address, current work concerning the security of CAN-based communication, and finally the characteristics of the counter-based approaches currently being discussed. Section3 then describes the details of our approach BusCount. The following Section 4 briefly introduces our Security Modeling Framework SeMF that is then used in Sections 5 and 6, respectively, to formally model and verify both the generic counter approach and our bus counter approach. Based on these results, in Section 7.1 we present a comparison of the security aspects of both approaches while Section 7.2 introduces our proof of concept implementation showing its practicability and design decisions that substantiate our formal proof. Finally, we conclude with Section 8.


## 2. Principles of In-Vehicle Communication

CAN bus is the core technology for onboard communication in vehicles. Brakes, acceleration, and many further essential features are controlled by ECUs that communicate using CAN bus messages. An overview of different network structures is given in [6]. The CAN network is accessible via the OBD port allowing repair shops to access the car network. Modern vehicles also have connections through infotainment systems as well as telematic control units (TCUs) connecting the CAN bus to the outside world. By connecting the in-vehicle communication with the outside world, the necessity arose to protect its messages against malicious entities.In this section, we describe the basics of CAN bus communication, the attacker model we take as a basis, the most relevant protection goals, and the current approaches for protecting these goals.


### 2.1. Basics of CAN Communication in Vehicles

The CAN bus, specified in [1], is a field bus where each entity connected to it is able to send messages and listen to every message sent on the bus. The maximum transfer rate of the highspeed-CAN is 1 Mbit/s.A standard CAN message consists of 7 segments (Figure1): “Start of frame” bit, a message identifier, a control field, a data field, a checksum, a confirmation field, and an “end of frame” sequence.Figure 1
A single CAN frame.The 11 bit identifier which is the second section of a CAN message also represents the message’s priority which is used to handle collisions. The CAN bus uses Carrier Sense Multiple Access/Collision Resolution (CSMA/CR) to prevent collisions: All ECUs start sending a CAN message simultaneously and monitor its identifier while sending. In case a dominant 0 overwrites a 1 the ECU with the lower priority stops its transmission, thereby avoiding collisions.During the transmission of the message every ECU calculates the CRC (cyclic redundancy check) over the message and checks the correctness of it as soon as it gets transmitted by the sender. In case of a problem (e.g. if the CRC check has failed) an ECU interrupts a transmission with an error frame that invalidates the message for all receivers. Furthermore, an error counter is increased by 1 for every receiver and by 8 for the sender. Every successfully transmitted message decrements the counter. If a counter reaches 128, the ECU disables its CAN connection. This mechanism ensures that damaged ECUs do not block the entire bus communication.Successors of CAN, like CAN FD or CAN XL, differ mainly in the frequency of transmitting data payload. CAN FD can transmit up to 64 bytes while CAN XL can handle 2048 bytes.


### 2.2. Our Attack Model

Attacks on in-vehicle communication have been presented first by Kocher et al. in [2]. These attacks concern manipulation of brake control and vehicle acceleration via CAN Bus by message injection. In the real world, attacks on vehicle networks have been observed that manipulate in-vehicle communication by attaching devices to the bus system, like tuning devices, AdBlue emulators [7], unauthorized OBD dongles [8], etc.In our attack model, an attacker can send arbitrary messages on any bus she has access to. Moreover, she can overhear and record all communication on a bus she is connected to and replay all recorded messages. Finally, an attacker is able to flip bits of messages or send an error frame. This enables her to invalidate messages for other ECUs after having recorded them herself. In our scenario, an attacker does not have access to any cryptographic keys. This also includes that the attacker cannot manipulate ECUs by e.g. corrupting firmware which in turn implies that legitimate ECUs always act correctly. Furthermore, the attacker is not able to manipulate processes or storage of ECUs by physical attacks. In addition, the attacker is not able to produce a counter overflow as a sufficient counter length is chosen to prohibit this sort of attacks.


### 2.3. Protection Goals

A secure CAN bus communication in a vehicle needs to fulfill a set of requirements to prevent previously introduced attacks. These include e.g. data integrity, confidentiality, and availability. In the following, we explain those requirements we specifically address in this paper.Data Origin Authenticity: A message in a vehicle network should be accepted if and only if it has authentically for the recipient been sent by another valid member of the network. This property prevents attackers from manipulating messages or sending messages on the bus system from additional devices or replaced components without the intended recipient noticing.Immediacy: Contrary to many other IT-systems, it is important for an automotive system to receive and process messages within a certain time frame. Once this time frame has passed, messages might be authentic, but can still cause fatal results, e.g. if breaking signals sent by the anti-lock braking system are processed too late. Immediacy expresses the fact that a message sent at time t1 is accepted until t2 if and only if t2−t1 does not exceed a specified limit.Non-repeatability: The last important property for an automotive network is non-repeatability: If a message is accepted at timet1, the same message is not accepted at any later point in time. Thus, an attacker cannot eavesdrop on a message and successfully replay it at a later point in time.Many articles do not distinguish between the two above properties and use the more abstract concept of “message freshness” with “message replay” seeking to violate freshness. We adapt to this notation and distinguish the specific characteristics when necessary.


### 2.4. State of the Art CAN Bus Security

The security of bus communication in current vehicle networks has already been discussed in literature and standardization. Early work on MAC truncation for secure CAN bus communication can be traced back to [3]. In this section, we give an overview of state of the art with a focus on replay protection in CAN bus systems and compare the techniques.A lot of CAN bus security approaches introduce message authentication mechanisms, but not all introduce replay protection. The latest example of an approach without freshness values is TOUCAN: A proTocol tO secUre Controller Area Network presented by Bella et al. [9], which introduces a 24 bit truncated Chaskey MAC and a SPECK64 encryption for each CAN message.A more exotic approach for replay protection is used in LCAP by Hazem et al. [10]. LCAP appends a truncated element of a hash chain to the CAN message and encrypts the resulting message. An HMAC secures the transmission of the last element of the hash chain to initialize the communication. Woo et al. [11] periodically change HMAC keys to prevent replay attacks.Nürnberger and Rossow [12] developed VatiCAN, an HMAC based authentication procedure that sends a MAC in a separate message following the original CAN message. The MAC is then validated with a delay of about 4 ms. Replay protection is implemented with a monotonically incremented counter, its starting value being a random nonce generated by a central component for every message ID. The authors recommend this procedure only for a few CAN messages since it increases the bus load. Van Bulck et al. improved this approach in [13] by introducing software isolation and attestation as well as key update mechanisms.Hartkopp et al. presented a further approach to introduce freshness to CAN messages. MaCAN [14] formally verified in [15] introduces a central trusted time server which distributes time information over the network. This information is used as freshness value for message authentication.AUTOSAR specifies the protection of communication in vehicle networks based on a MAC and a freshness value. The specification of the Secure Onboard Communication (SecOC) [4] module suggests to add a truncated timestamp or message counter and a truncated authenticator to every message. The specific counter mechanism is based on splitting the counter (with a maximal length of 96 bits) into three different parts: the so-called “trip counter” that only changes essentially with every new trip, a “reset counter” that is reset periodically, and the actual “message counter”. Only the trip counter is stored in non-volatile memory, thus mitigating loss of counter values in case of sudden ECU shutdown. The truncated freshness value has a length between 0 and 8 bit. The truncated authenticator consists of the first 24 to 28 bits of the MAC covering the full freshness value and the message.Similar to SecOC many approaches in literature use counters and an application-level protocol to ensure replay protection. Kurachi et al. [16] suggest attaching a truncated MAC (8 bit) and a truncated monotonic counter (4 bit) to a message. A monitoring node verifies messages during transmission and overwrites invalid messages with an error frame. ECUs do not verify messages. Groll et al. [17] suggest an initialization phase to form groups of ECUs. These groups generate a shared symmetric key using an asymmetric key exchange. Within these groups, ECUs use the shared secret for authentic and confidential encryption. A counter should be part of the message to protect against replay attacks. Lin et al. presented an approach in [18] with symmetric keys for message authentication. A sender calculates a MAC for every receiver. Every ECU also holds two counters for replay protection per message ID, the last counter it has sent and the last one it has received. Every receiver can verify the MAC and process its corresponding message. The LeiA protocol by Radu et al. [19] is another solution that transfers MAC and counter value in a separate message. Every ECU has a session key for each relevant message ID derived from a long-term symmetric key and renewed after a certain period. VeCure [20] is a CAN authentication framework similar to VatiCAN. The authentication value is also transmitted via a separate message, but contrary to VatiCAN the second message includes a Node-ID besides a Message Counter and a four byte HMAC value.Alternatively, several approaches suggest the use of CAN+ [21], a protocol extension for CAN allowing to transport 120 bit additional data. The first approach is CANAuth presented by Van Herrewege et al. [22]. Another one is LiBrA-CAN [23]. LiBrA-CAN introduces (Linearly) Mixed MAC, which mixes multiple MACs of one message generated with different keys allowing receivers to verify a MAC even though they do not know all keys. The approach allows making sure receivers cannot impersonate a sender in a properly organized group. Both approaches send counter values in their messages to protect against replay attacks.Some works are also considering the implementation of a secure CAN bus controller. Their approaches introduce the calculation of MACs, denial of service countermeasures, or intrusion prevention mechanisms. [24] implemented a CAN controller including a physical unclonable function implementation, key generation and storage, and encryption and decryption allowing authenticated communication over CAN. However, the approach does not consider replay protection. Ueda et al. presented a CAN controller with integrated HMAC in [25]. To ensure replay protection a truncated monotonic value of 4 bits is part of every message. Messages which are not authentic are destroyed while correct messages update the counter.A new approach by Groza et al. [26] suggests replacing CAN IDs with a specific MAC-based algorithm that preserves the order of CAN IDs. In predefined time intervals the counter included in the MAC is incremented thus the IDs change. This approach increases the resistance against reverse engineering and denial of service attacks related to a specific ID. It does not provide data integrity and authenticity which needs an additional security protocol as mentioned in the paper. Moreover freshness is not guaranteed since the counter used in the MAC of the CAN ID does not change with every message. In case of constantly changing counter values (IDs) and if a significant limitation of ID range is acceptable this can be a viable alternative to transfer of fresh counter values.We observed that most of the presented approaches (cf. Table1) have similar ways to ensure replay protection and authentication of messages. All approaches add a MAC to a CAN message. While a MAC provides authenticity of a message, only in combination with a freshness value replay and delay attacks can be mitigated. Most approaches introduce a counter value to provide freshness since the usage of time or nonce values has disadvantages, discussed e.g. in [27]. The transmission of MAC and freshness values is either realized in an additional message or achieved by including truncated values in the same message. The verification of a complete message is performed by the receiver or an additional node. In the following section, we present a detailed generic model covering the characteristics of the current counter-based approaches for freshness. This model is then compared to our approach based on formal verifications of the security goals.Table 1
Comparison of different authentication approaches for CAN-Bus (HW: Hardware, SW: Software, C : Counter, T : Timestamp, N : Nonce,∗: not described)
HW changeSW changeCentral componentFreshness techniqueMACEncryptionTransfer techniques for MACSyncronisation of freshness valueAUTOSAR [2]-✓-C / T✓-28 bit data field✓CaCAN [24]✓✓✓C✓-8 bit data field-CANAuth [35]✓✓-C✓-CAN+(✓)Groll et al. [14]-✓✓C✓✓∗-LeiA [31]-✓-C✓-sep. message✓LibrA-CAN [16]-✓✓C✓-CAN+-Lin et al. [25]-✓-C✓-∗(✓)Ueda et al. [34]✓✓✓C✓-8 bit data field-VeCure [37]-✓-C✓-separate message-MaCAN [20]-✓✓T✓-32 bit data field✓VatiCAN [28]-✓✓C + N✓-separate message✓vulCAN [7]✓✓✓C + N✓-separate message(✓)Woo et al. [38]-(✓)(✓)key refresh✓✓CAN-FD-LCAP [21]-✓-hash chain-✓16 bit extended ID✓TouCAN [3]-✓--✓✓24 bit data field-Siddiqui et al. [33]✓✓✓-✓✓data field-CAN-TORO [15]✓✓✓Authenticated ID---(✓)


### 2.5. The Generic Counter Concept

Considering the recent research, we simplified the approaches in order to generate an abstract model to evaluate the security of software-based freshness techniques compared to our approach. Since a large majority of approaches favor counters for freshness values, we focus on this technique.Figure2 illustrates the abstract protocol we assume. To transmit a CAN message m which contains the ID and payload data msg an ECU first calculates a MAC covering m and a local counter ca derived by incrementing the previously used one (steps 1 and 2). For our analysis, the choice of the MAC algorithm is not important. In the next steps, m, ca and the authentication tag are concatenated (step 3) and the values are transmitted (step 4). Note that this transmission is not necessarily processed with one CAN message only, different techniques could apply here. Finally, a receiver gets the message, verifies the MAC and tests if its local counter cb is smaller than the counter in s. The check is not necessarily performed by the same entity which later processes m. If both checks are successful, the local counter is set to the counter in s and the message can be processed. Otherwise, the message is discarded.Figure 2
Process of Generic Counter Communication.Only some approaches consider an explicit synchronization of counter values which is necessary in case an ECU loses its counter value, e.g. due to a software error, a power loss (engine stop or malfunction) or an ECU without persistent memory. Most approaches that use synchronization introduce a central system sending an authenticated message containing the current counter value. In case a sender has an incorrect counter, the value needs to be provided by a dedicated entity or some client. In both cases the counter value is transmitted in the payload CAN message with a reserved ID. This message is secured identically to regular messages.Even though the generic counter protocol is fairly simple it represents the characteristic properties of all above mentioned protocols that increment counters after successful validation of the message. The fact that the local counters of message recipients only change when a message is accepted is a very important characteristic property. Consequently, these protocols cannot prohibit so-called delay attacks, as will be formally shown in Section5.2. For such an attack, the adversary with the abilities described in Section 2.2 stores and then invalidates a message and all subsequent ones related to the same counter. The reinserted message will then be accepted by the intended recipients at any later point in time if no further countermeasures are taken.


## 2.1. Basics of CAN Communication in Vehicles

The CAN bus, specified in [1], is a field bus where each entity connected to it is able to send messages and listen to every message sent on the bus. The maximum transfer rate of the highspeed-CAN is 1 Mbit/s.A standard CAN message consists of 7 segments (Figure1): “Start of frame” bit, a message identifier, a control field, a data field, a checksum, a confirmation field, and an “end of frame” sequence.Figure 1
A single CAN frame.The 11 bit identifier which is the second section of a CAN message also represents the message’s priority which is used to handle collisions. The CAN bus uses Carrier Sense Multiple Access/Collision Resolution (CSMA/CR) to prevent collisions: All ECUs start sending a CAN message simultaneously and monitor its identifier while sending. In case a dominant 0 overwrites a 1 the ECU with the lower priority stops its transmission, thereby avoiding collisions.During the transmission of the message every ECU calculates the CRC (cyclic redundancy check) over the message and checks the correctness of it as soon as it gets transmitted by the sender. In case of a problem (e.g. if the CRC check has failed) an ECU interrupts a transmission with an error frame that invalidates the message for all receivers. Furthermore, an error counter is increased by 1 for every receiver and by 8 for the sender. Every successfully transmitted message decrements the counter. If a counter reaches 128, the ECU disables its CAN connection. This mechanism ensures that damaged ECUs do not block the entire bus communication.Successors of CAN, like CAN FD or CAN XL, differ mainly in the frequency of transmitting data payload. CAN FD can transmit up to 64 bytes while CAN XL can handle 2048 bytes.


## 2.2. Our Attack Model

Attacks on in-vehicle communication have been presented first by Kocher et al. in [2]. These attacks concern manipulation of brake control and vehicle acceleration via CAN Bus by message injection. In the real world, attacks on vehicle networks have been observed that manipulate in-vehicle communication by attaching devices to the bus system, like tuning devices, AdBlue emulators [7], unauthorized OBD dongles [8], etc.In our attack model, an attacker can send arbitrary messages on any bus she has access to. Moreover, she can overhear and record all communication on a bus she is connected to and replay all recorded messages. Finally, an attacker is able to flip bits of messages or send an error frame. This enables her to invalidate messages for other ECUs after having recorded them herself. In our scenario, an attacker does not have access to any cryptographic keys. This also includes that the attacker cannot manipulate ECUs by e.g. corrupting firmware which in turn implies that legitimate ECUs always act correctly. Furthermore, the attacker is not able to manipulate processes or storage of ECUs by physical attacks. In addition, the attacker is not able to produce a counter overflow as a sufficient counter length is chosen to prohibit this sort of attacks.


## 2.3. Protection Goals

A secure CAN bus communication in a vehicle needs to fulfill a set of requirements to prevent previously introduced attacks. These include e.g. data integrity, confidentiality, and availability. In the following, we explain those requirements we specifically address in this paper.Data Origin Authenticity: A message in a vehicle network should be accepted if and only if it has authentically for the recipient been sent by another valid member of the network. This property prevents attackers from manipulating messages or sending messages on the bus system from additional devices or replaced components without the intended recipient noticing.Immediacy: Contrary to many other IT-systems, it is important for an automotive system to receive and process messages within a certain time frame. Once this time frame has passed, messages might be authentic, but can still cause fatal results, e.g. if breaking signals sent by the anti-lock braking system are processed too late. Immediacy expresses the fact that a message sent at time t1 is accepted until t2 if and only if t2−t1 does not exceed a specified limit.Non-repeatability: The last important property for an automotive network is non-repeatability: If a message is accepted at timet1, the same message is not accepted at any later point in time. Thus, an attacker cannot eavesdrop on a message and successfully replay it at a later point in time.Many articles do not distinguish between the two above properties and use the more abstract concept of “message freshness” with “message replay” seeking to violate freshness. We adapt to this notation and distinguish the specific characteristics when necessary.


## 2.4. State of the Art CAN Bus Security

The security of bus communication in current vehicle networks has already been discussed in literature and standardization. Early work on MAC truncation for secure CAN bus communication can be traced back to [3]. In this section, we give an overview of state of the art with a focus on replay protection in CAN bus systems and compare the techniques.A lot of CAN bus security approaches introduce message authentication mechanisms, but not all introduce replay protection. The latest example of an approach without freshness values is TOUCAN: A proTocol tO secUre Controller Area Network presented by Bella et al. [9], which introduces a 24 bit truncated Chaskey MAC and a SPECK64 encryption for each CAN message.A more exotic approach for replay protection is used in LCAP by Hazem et al. [10]. LCAP appends a truncated element of a hash chain to the CAN message and encrypts the resulting message. An HMAC secures the transmission of the last element of the hash chain to initialize the communication. Woo et al. [11] periodically change HMAC keys to prevent replay attacks.Nürnberger and Rossow [12] developed VatiCAN, an HMAC based authentication procedure that sends a MAC in a separate message following the original CAN message. The MAC is then validated with a delay of about 4 ms. Replay protection is implemented with a monotonically incremented counter, its starting value being a random nonce generated by a central component for every message ID. The authors recommend this procedure only for a few CAN messages since it increases the bus load. Van Bulck et al. improved this approach in [13] by introducing software isolation and attestation as well as key update mechanisms.Hartkopp et al. presented a further approach to introduce freshness to CAN messages. MaCAN [14] formally verified in [15] introduces a central trusted time server which distributes time information over the network. This information is used as freshness value for message authentication.AUTOSAR specifies the protection of communication in vehicle networks based on a MAC and a freshness value. The specification of the Secure Onboard Communication (SecOC) [4] module suggests to add a truncated timestamp or message counter and a truncated authenticator to every message. The specific counter mechanism is based on splitting the counter (with a maximal length of 96 bits) into three different parts: the so-called “trip counter” that only changes essentially with every new trip, a “reset counter” that is reset periodically, and the actual “message counter”. Only the trip counter is stored in non-volatile memory, thus mitigating loss of counter values in case of sudden ECU shutdown. The truncated freshness value has a length between 0 and 8 bit. The truncated authenticator consists of the first 24 to 28 bits of the MAC covering the full freshness value and the message.Similar to SecOC many approaches in literature use counters and an application-level protocol to ensure replay protection. Kurachi et al. [16] suggest attaching a truncated MAC (8 bit) and a truncated monotonic counter (4 bit) to a message. A monitoring node verifies messages during transmission and overwrites invalid messages with an error frame. ECUs do not verify messages. Groll et al. [17] suggest an initialization phase to form groups of ECUs. These groups generate a shared symmetric key using an asymmetric key exchange. Within these groups, ECUs use the shared secret for authentic and confidential encryption. A counter should be part of the message to protect against replay attacks. Lin et al. presented an approach in [18] with symmetric keys for message authentication. A sender calculates a MAC for every receiver. Every ECU also holds two counters for replay protection per message ID, the last counter it has sent and the last one it has received. Every receiver can verify the MAC and process its corresponding message. The LeiA protocol by Radu et al. [19] is another solution that transfers MAC and counter value in a separate message. Every ECU has a session key for each relevant message ID derived from a long-term symmetric key and renewed after a certain period. VeCure [20] is a CAN authentication framework similar to VatiCAN. The authentication value is also transmitted via a separate message, but contrary to VatiCAN the second message includes a Node-ID besides a Message Counter and a four byte HMAC value.Alternatively, several approaches suggest the use of CAN+ [21], a protocol extension for CAN allowing to transport 120 bit additional data. The first approach is CANAuth presented by Van Herrewege et al. [22]. Another one is LiBrA-CAN [23]. LiBrA-CAN introduces (Linearly) Mixed MAC, which mixes multiple MACs of one message generated with different keys allowing receivers to verify a MAC even though they do not know all keys. The approach allows making sure receivers cannot impersonate a sender in a properly organized group. Both approaches send counter values in their messages to protect against replay attacks.Some works are also considering the implementation of a secure CAN bus controller. Their approaches introduce the calculation of MACs, denial of service countermeasures, or intrusion prevention mechanisms. [24] implemented a CAN controller including a physical unclonable function implementation, key generation and storage, and encryption and decryption allowing authenticated communication over CAN. However, the approach does not consider replay protection. Ueda et al. presented a CAN controller with integrated HMAC in [25]. To ensure replay protection a truncated monotonic value of 4 bits is part of every message. Messages which are not authentic are destroyed while correct messages update the counter.A new approach by Groza et al. [26] suggests replacing CAN IDs with a specific MAC-based algorithm that preserves the order of CAN IDs. In predefined time intervals the counter included in the MAC is incremented thus the IDs change. This approach increases the resistance against reverse engineering and denial of service attacks related to a specific ID. It does not provide data integrity and authenticity which needs an additional security protocol as mentioned in the paper. Moreover freshness is not guaranteed since the counter used in the MAC of the CAN ID does not change with every message. In case of constantly changing counter values (IDs) and if a significant limitation of ID range is acceptable this can be a viable alternative to transfer of fresh counter values.We observed that most of the presented approaches (cf. Table1) have similar ways to ensure replay protection and authentication of messages. All approaches add a MAC to a CAN message. While a MAC provides authenticity of a message, only in combination with a freshness value replay and delay attacks can be mitigated. Most approaches introduce a counter value to provide freshness since the usage of time or nonce values has disadvantages, discussed e.g. in [27]. The transmission of MAC and freshness values is either realized in an additional message or achieved by including truncated values in the same message. The verification of a complete message is performed by the receiver or an additional node. In the following section, we present a detailed generic model covering the characteristics of the current counter-based approaches for freshness. This model is then compared to our approach based on formal verifications of the security goals.Table 1
Comparison of different authentication approaches for CAN-Bus (HW: Hardware, SW: Software, C : Counter, T : Timestamp, N : Nonce,∗: not described)
HW changeSW changeCentral componentFreshness techniqueMACEncryptionTransfer techniques for MACSyncronisation of freshness valueAUTOSAR [2]-✓-C / T✓-28 bit data field✓CaCAN [24]✓✓✓C✓-8 bit data field-CANAuth [35]✓✓-C✓-CAN+(✓)Groll et al. [14]-✓✓C✓✓∗-LeiA [31]-✓-C✓-sep. message✓LibrA-CAN [16]-✓✓C✓-CAN+-Lin et al. [25]-✓-C✓-∗(✓)Ueda et al. [34]✓✓✓C✓-8 bit data field-VeCure [37]-✓-C✓-separate message-MaCAN [20]-✓✓T✓-32 bit data field✓VatiCAN [28]-✓✓C + N✓-separate message✓vulCAN [7]✓✓✓C + N✓-separate message(✓)Woo et al. [38]-(✓)(✓)key refresh✓✓CAN-FD-LCAP [21]-✓-hash chain-✓16 bit extended ID✓TouCAN [3]-✓--✓✓24 bit data field-Siddiqui et al. [33]✓✓✓-✓✓data field-CAN-TORO [15]✓✓✓Authenticated ID---(✓)


## 2.5. The Generic Counter Concept

Considering the recent research, we simplified the approaches in order to generate an abstract model to evaluate the security of software-based freshness techniques compared to our approach. Since a large majority of approaches favor counters for freshness values, we focus on this technique.Figure2 illustrates the abstract protocol we assume. To transmit a CAN message m which contains the ID and payload data msg an ECU first calculates a MAC covering m and a local counter ca derived by incrementing the previously used one (steps 1 and 2). For our analysis, the choice of the MAC algorithm is not important. In the next steps, m, ca and the authentication tag are concatenated (step 3) and the values are transmitted (step 4). Note that this transmission is not necessarily processed with one CAN message only, different techniques could apply here. Finally, a receiver gets the message, verifies the MAC and tests if its local counter cb is smaller than the counter in s. The check is not necessarily performed by the same entity which later processes m. If both checks are successful, the local counter is set to the counter in s and the message can be processed. Otherwise, the message is discarded.Figure 2
Process of Generic Counter Communication.Only some approaches consider an explicit synchronization of counter values which is necessary in case an ECU loses its counter value, e.g. due to a software error, a power loss (engine stop or malfunction) or an ECU without persistent memory. Most approaches that use synchronization introduce a central system sending an authenticated message containing the current counter value. In case a sender has an incorrect counter, the value needs to be provided by a dedicated entity or some client. In both cases the counter value is transmitted in the payload CAN message with a reserved ID. This message is secured identically to regular messages.Even though the generic counter protocol is fairly simple it represents the characteristic properties of all above mentioned protocols that increment counters after successful validation of the message. The fact that the local counters of message recipients only change when a message is accepted is a very important characteristic property. Consequently, these protocols cannot prohibit so-called delay attacks, as will be formally shown in Section5.2. For such an attack, the adversary with the abilities described in Section 2.2 stores and then invalidates a message and all subsequent ones related to the same counter. The reinserted message will then be accepted by the intended recipients at any later point in time if no further countermeasures are taken.


## 3. BusCount: A Hardware Based Bus Counter Solution

In this section we describe BusCount, our approach for a hardware based secure CAN bus communication, which eliminates the possibilities of attackers with the abilities presented in Section2.2. We first introduce our approach to ensure immediacy, non-repeatability, and authenticity of messages on the bus and then elaborate on the synchronization mechanism for freshness values.In a bus system, each participant can see and thus count every message written to the bus. Hence, the number of messages sent on a particular bus is an inherent part of the system that can serve as a bus specific counter [5] known by all devices connected to it. Consequently, there is no need to send counters. Each bus of a vehicle system is equipped with its own counter. Its value changes automatically with each new message: An ECU sending/receiving a message reduces its local counter value by 1 and authenticates/verifies the message including the counter with a MAC. This idea can be also applied to any other bus network.The procedure of BusCount is described in more detail as follows (see Figure3 for a schematic representation):Figure 3
Process of CAN message transmission of BusCount.First, a sender ECU starts transmitting a messagem which is composed of a message ID and the payload msg. As soon as the transmission starts, the local counter ca of the sender is temporarily decremented (step 1.1). The counter is decremented instead of the usual incrementation because 0 is the dominant bit on the CAN bus thus a lower counter can overwrite a larger counter. This property is used for the synchronization of the counter explained in the next section. A receiver ECU, when receiving the start of the message, decrements its local counter cb and uses the result as its new counter value (step 2.1). Since sending and receiving of messages is processed simultaneously and thus the sender also receives its own message, it decrements its counter analogously. After the counters are decremented the sender starts sending mgs and both receiver and sender start calculating the MAC over the message m and their respective local counter using a shared key k. Finally, the tag ta of the sender’s MAC is transmitted (step 1.3) and received (step 2.3). All ECUs now evaluate the tag.If the evaluation is positivem can be processed. Otherwise, the receivers whose verification failed immediately transmit an error frame which has the effect that m is discarded by every ECU. Note that this effects also ECUs that do not implement the protocol: They will discard messages overwritten with an error frame. In case multiple errors occur, a synchronization is necessary.


### 3.1. Synchronization

Multiple transmission failures may indicate that an ECU is not synchronized. This situation can occur e.g. if the ECU is switched off without having been able to store the current correct counter value in persistent storage. Consequently, a synchronization between all entities of a bus is necessary. Our synchronization concept utilizes the mechanism used for collision resolving which is based on the fact that sending a 0 always overwrites a 1 on the CAN bus. Hence, in BusCount counters are decremented instead of the usual incrementation.The mechanism is illustrated in Figure4. One ECU initializes the synchronization by sending a predefined synchronization ID (Step 1.1). At the same time, each receiving ECU including the initiator of the synchronization, receiving the start of message bit, decrements its local counter. Now all ECUs, having identified the message as synchronization message, simultaneously start to send their respective newly decremented local counter in the data frame (Step 2.1 and 2.2). The lowest counter will overwrite larger counters and ECUs with larger counters stop sending (Step 3). An ECU with the lowest counter value (the actual sender of the synchronization message) sends a MAC over the ID and the counter value (Step 4.1 or 4.2). Each ECU as a recipient of this message verifies the correctness of the MAC and compares the counter to its local one. In case one check by any of the receivers fails, the rest of the message is overwritten with an error frame and is discarded by all controllers. Otherwise, every receiver replaces its local counter with the counter of the synchronization message.Figure 4
Synchronization of BusCount.In case multiple ECUs have the lowest counter in the network, each sends the same message without noticing each other. This concept has been used for example in [28] to implement a key exchange on a CAN bus.In contrast to other approaches that use a counter for every message ID, our approach allows to synchronize all participants of a bus communication with just one message. Further, no central entity is needed for the process, any ECU connected to the bus can initialize it. The only condition for it to work is that at least one ECU owns and processes the correct counter value.In Section7.2 we will discuss design decisions and introduce our proof of concept implementation. In the next section we will briefly introduce the Security Modeling Framework SeMF that is then used in Sections 5 and 6, respectively, to formally model and verify both the generic counter approach and our bus counter approach with respect to the desired security properties. The achieved results will then be discussed in Section 7.1.


## 3.1. Synchronization

Multiple transmission failures may indicate that an ECU is not synchronized. This situation can occur e.g. if the ECU is switched off without having been able to store the current correct counter value in persistent storage. Consequently, a synchronization between all entities of a bus is necessary. Our synchronization concept utilizes the mechanism used for collision resolving which is based on the fact that sending a 0 always overwrites a 1 on the CAN bus. Hence, in BusCount counters are decremented instead of the usual incrementation.The mechanism is illustrated in Figure4. One ECU initializes the synchronization by sending a predefined synchronization ID (Step 1.1). At the same time, each receiving ECU including the initiator of the synchronization, receiving the start of message bit, decrements its local counter. Now all ECUs, having identified the message as synchronization message, simultaneously start to send their respective newly decremented local counter in the data frame (Step 2.1 and 2.2). The lowest counter will overwrite larger counters and ECUs with larger counters stop sending (Step 3). An ECU with the lowest counter value (the actual sender of the synchronization message) sends a MAC over the ID and the counter value (Step 4.1 or 4.2). Each ECU as a recipient of this message verifies the correctness of the MAC and compares the counter to its local one. In case one check by any of the receivers fails, the rest of the message is overwritten with an error frame and is discarded by all controllers. Otherwise, every receiver replaces its local counter with the counter of the synchronization message.Figure 4
Synchronization of BusCount.In case multiple ECUs have the lowest counter in the network, each sends the same message without noticing each other. This concept has been used for example in [28] to implement a key exchange on a CAN bus.In contrast to other approaches that use a counter for every message ID, our approach allows to synchronize all participants of a bus communication with just one message. Further, no central entity is needed for the process, any ECU connected to the bus can initialize it. The only condition for it to work is that at least one ECU owns and processes the correct counter value.In Section7.2 we will discuss design decisions and introduce our proof of concept implementation. In the next section we will briefly introduce the Security Modeling Framework SeMF that is then used in Sections 5 and 6, respectively, to formally model and verify both the generic counter approach and our bus counter approach with respect to the desired security properties. The achieved results will then be discussed in Section 7.1.


## 4. The Security Modeling Framework SeMF

We use our Security Modeling Framework SeMF (see [29] for a detailed description) to formally model and verify the two counter systems discussed in this paper. SeMF is a powerful modeling framework that we have already successfully applied to a variety of different domains and abstraction levels. For example, we used it to verify that specific security properties of service based systems are preserved under composition [30]. We also applied it to model and verify the integration of device authentication based on TPM attestation with secure channel establishment via SSL [31]. Another example is [32] where we proved preservation of specific security properties for the composition of abstract security patterns.The basic idea of SeMF is to describe the system behavior by sequences of actions that capture essential changes in the system. As underlying formal semantics SeMF uses prefix closed formal languages (see e.g. [33]) whose alphabet is composed of the actions in the system. More specifically, it uses a set of agents ℙ (where the term “agent” can denote any entity acting in the system such as a human being, an ECU, etc.), and a set of actions Σ (e.g. specifying sending and receiving messages on a bus) performed by the agents. The system’s behavior is then formally described by a prefix closed formal language B⊆Σ∗ (Σ∗ denoting the set of all words composed of elements in Σ with ε∈Σ∗ denoting the empty word), i.e. by the set of its possible sequences of actions. A system model further comprises the agents’ local views (denoted by λP for agent P). The local view of different agents usually differs since it describes which parts of the system behavior the agents can actually see (an ECU for example may see its own internal actions, but not those of other ECUs). A system model finally includes the so-called agents’ “initial knowledge” WP⊆Σ∗ which is defined to be prefix closed and to contain B. This concept is used in order to specify system constraints and assumptions.Security properties are defined in terms of the system specification. The underlying formal semantics then allows formal validation, i.e. allows proving that a specific formal model satisfies specific security properties.The following notations are used: ForΥ⊆Σ∗ and ω∈Υ, ω−1Υ denotes the set of all continuations of ω in Υ. For Γ⊆Σ and ω∈Σ∗, cardΓ,ω denotes the number of occurrences of any action of Γ in ω, alphω denotes its alphabet (i.e. the set of its actions), preω is its set of prefixes, pre1ω denotes its first and suf1ω its last action. For ω=x1…xk∈Σ∗ and i∈1,…,k, prevactxi,P,ω denotes the last action before xi in ω performed by agent P (in case xi is P ’s first action, prevactxi,P,ω=ε). For ω∈Σ∗, the function actCnt:Σ×Σ∗⟶ℕs enumerates strictly monotonically increasing the actions of ω in their order of occurrence: actCnta,ε≔0 for all a∈Σ, act Cnta,ω≔1 for ω=a, and for cardΣ,ω=k>1 we define act Cntsuf1ω,ω≔act Cntsuf1prek−1ω,prek−1ω+1.We extend SeMF by a formal specification of actions and a homomorphism to extract any parameter of an action:Definition 1 (Set of actions).
LetP=par1,…,parna set of parametersn∈ℕand forj∈1,…,nletVjthe set of possible values ofparjwithV1≔Aa set of action names andV2≔ℙa set of agents. Then the setΣof actions of a systemScan be defined as follows:(1)Σ⊆∪pari1∈A,pari2∈ℙ,i3,…,ik⊆3,…,npari1,…,parik.
The sending of a message on a CAN bus can for example be formalized bysend,ECU,bus,msg. See Sections 5.1 and 6.1 for the concrete sets of actions of the two models introduced in this paper. In order to express relations between parameters of different actions, we need to extract them from the actions:Definition 2 (Parameter extraction).
LetΣbe defined as in Definition 1. We define a homomorphismκ∧parι:Σ⟶P∪Σby(2)κ∧parιpar1,…,park≔pari,ifpari=parι,par1,…,park,else.
The security property provided by a MAC mechanism can be formally specified by the concept of authenticity introduced in [34] : A set of actions Γ is authentic for agent P after a sequence ω of actions has happened if in all sequences that P considers possible after ω, some time in the past an action in Γ must have happened. Formally:Definition 3 (Authenticity).
A set of actionsΓ⊆Σis authentic forP∈ℙafter a sequence of actionsω∈Swith respect toWPifalphx∩Γ≠∅for allx∈λP−1λPω∩WP.
The following weaker property describes that in all sequences of a languageL that contain a specific action b, this action is preceded by one of the actions contained in Γ⊆Σ:Definition 4 (Precedence).
ForL⊆Σ∗,Γ⊆Σ,b∈Σthe propertyprecLΓ,bholds if for allω∈preLwithb∈alphωfollowsΓ∩alphω≠∅. We simply writeprecΓ,bif from the context the language referred to is clear.
Additionally to authenticity, we require the counter systems to provide immediacy and non-repeatability. In order to define a respective security property within SeMF we introduce the concept of aphase class that allows modeling that a particular action occurred within a particular period of the system. We base our definition on the concept of a phase introduced in [35]. Here a subset of Σ∗ is a phase for B if it is a prefix closed language consisting only of words which, as long as they are not maximal, show the same continuation behavior within the phase as within B. Our definition transforms this to arbitrary subsets of Σ∗, not requiring them to be prefix closed:Definition 5 (Phase class).
LetΥ⊆Σ∗. A languageΦΥ⊆Σ∗is a phase class forΥif the following holds:1.
ΦΥ∩Σ≠∅2.
∀ω,u∈Υwithω=uvandv∈ΦΥ\maxΦΥ∪εholds:ω−1Υ∩Σ⊆v−1ΦΥ∩Σ
Thus, a phase class is characterized by being closed with respect to concatenation. Maximal words in a phase class, denoted bymaxΦΥ, are those v∈ΦΥ for which holds va∉ΦΥ for all a∈Σ (i.e. no matter whether or not exists ω=uva∈Υ).
A phase class can be a very complex construct. However, in many cases phase classes are of interest that can be defined by the actions that start and terminate, respectively, the words. The following definition takes into account that an action can occur more than once in a word. Each starting action occurring in a wordω∈Υ starts a word of Φ. The word ends with the first ji occurrences of an action in Ti:Definition 6 ((S,T)-phase class).
LetΥ⊆Σ∗,S⊆Σ,T=T1∪…∪Tk⊆Σk∈ℕwithTi∩Tj=∅for alli≠j. Then ,Φ≔ΦΥ,S,T1,j1…,Tk,jk⊆Σ∗is a phase class forΥstarting withSand terminating with respect toT1,j1,…,Tk,jkif1
Φis a phase class forΥ,2
ΦΥ∩Σ=S3
for allvmaximal inΦthe following holds: Forω,u∈Υ,z∈Σ∗withω=uvzit followsz=εor there existsi∈1,…,ksuch thatsuf1v∈Ti, cardTi,v=ji, andcardTl,v<jlfor alll∈1,…,i−1,i+1,…,k.We call such a phase class anS,T1,j1,…,Tk,jk -phase class for Υ. If all words in the phase class terminate with the first occurrence of any t∈T, we simply call it an S,T -phase-class for Υ, denoted by ΦΥ,S,T.It can easily be shown that anS,T -phase class for a prefix closed language is itself prefix closed. S,T -phase classes are a very useful concept for the concrete specification of freshness properties. We can further combine these two concepts with authenticity:Definition 7 (Authenticity within a phase class).
LetB⊆Σ∗be the behavior of a system,ω∈B,b∈alphω, andΦWP⊆Σ∗a phase class for agentP’s initial knowledgeWP. A set of actionsΓ⊆Σis authentic forPafterωwithinΦWPand with respect toλPandbif (i) it is authentic forPafterωand if (ii) for allx∈λP−1λPω∩WPfor which existsu,z∈Σ∗andv∈ΦWPsuch thatx=uvzandb∈alphvit followsalphv∩Γ≠∅. If the property holds for allω∈B, we denote this property shortly byauthWiPhaseΓ,b,P,ΦWP.


## 5. Formalization and Verification of the Generic Counter Approach

In this section, we introduce our SeMF model of the generic counter system described in Section2.5 (denoted by GenCnt henceforth) and formally prove to which extend it satisfies the protection goals data origin authenticity, immediacy and non-repeatability of messages.


### 5.1. The Formal Generic Counter Model

Our SeMF model shall be as simple as possible. It needs to include ECUs connected to a bus whose messages shall be proven to be protected. It also needs to reflect our attack model introduced in Section2.2, hence must include devices (e.g. ECUs) that an attacker can use to monitor, record, resent and manipulate messages sent on the bus. It is obvious that messages sent on one bus may be accepted by ECUs connected to another bus if the key used for protecting these messages is the same for both buses. Hence we disregard this aspect and restrict our model to one group of honest devices, all owning the same MAC key for message protection, and a further device Eve representing dishonest behavior. All devices are connected to the same bus. Our model can easily be extended, for example by adding more groups, keys and buses, in case other aspects than those addressed in this paper shall be investigated. A special honest device is the Fresh Value Master (FvM) that is responsible for the synchronization of ECUs regarding their counter. We assume all honest devices to act according to a given specification (see Section 5.1.3). FvM only sends synchronization messages, i.e. messages with msgid=sync. Other honest devices receive synchronization messages and send and receive functional messages with msgid=fmsg. We do not distinguish between different types of functional messages and use just one with its corresponding message counter. Eve can send and receive all types of messages but does not own the MAC key and can thus not generate MACs.We use four different types of actions: sending and receiving (i.e. accepting) of messages, reading a message without processing it, and an action that models an ECU losing the correct message counter (denoted by genCnt henceforth). This action comprises any situation in which an ECU is not synchronized anymore, i.e. owns a counter smaller than the current correct counter value.While in many systems (e.g. in [4]) messages only contain a truncated message counter and MAC, respectively, in our model the counter’s complete value is included. This way we model the assumption that the recipients always succeed in determining the counter values used by the senders (after all, this aspect is not in the focus of our investigations).


#### 5.1.1. Agents, Parameters and Actions

For the formal specification of actions according to Definition1, we use the following sets:(1)
Set of agents:ℙgCnt≔ECUgC∪Eve with ECUgC≔ECU1gC,ECU2gC,FvM whose members are connected to the only bus of the system. FvM denotes the synchronization master and Eve denotes a further device being connected to the bus but not being member of ECUgC.(2)
set of action names:AgCnt=sendgC,readgC,recvgC,loseCntgC(3)
set of parameters:PgCnt≔aname,ecu,ecukey,ecucnt,prevcnt,bus,mackey,msgid,msg,cnt with aname∈AgCnt,ecu∈ℙgCnt,ecukey,mackey∈key∪ℕ, key being the key all honest ECUs use for MAC generation and verification, while ecukey∈ℕ for ecu=Eve. Further, ecucnt,prevcnt,cnt∈ℕ∪nocnt,bus∈bus,msgid∈sync,fmsg, and msg∈ℳ (ℳ being an arbitrary set of messages).(4)
The set of actionsΣgCnt is then defined as follows:(1)
sendgC,ecu,ecukey,ecucnt,prevcnt,bus,mackey,msgid,msg,cnt:ecu∈PgCnt sends a message on bus=bus. The message’s MAC (not explicitly modelled by a parameter of this action) is generated with mackey and covers msgid,msg and cnt. ecu∈ECUgC if none of the entire message bits as illustrated in Figure 1 has been written to the bus by Eve. ecu may or may not have generated the MAC. For ecu∈ECUgC, the parameter ecukey denotes ecu ’s MAC generation and verification key key, ecucnt denotes its local counter value after having performed the sendgC action, and prevcnt denotes the counter value resulting from ecu’s previous action (see Section 5.1.3 for the specific operations regarding an ECU’s counter). The message can be a functional message, indicated by msgid=fmsg, in which case the counter contained in the message’s payload is explicitly modelled by cnt, or a synchronization message with msgid=sync. In this case the message’s payload msg only contains the counter determined by the sender and the parameter cnt contains the constant nocnt. Note that there is the possibility that the message is altered (by a technical error or by Eve) after having been sent and may thus only cause a readgC action (see below).(2)
readgC,ecu,ecukey,ecucnt,prevcnt,bus,mackey,msgid,msg,cnt denotesecu∈ℙbCnt reading a message without processing it (i.e. without accepting it). The action does not change the local message counter ecucnt if ecu∈ECUgC (see Prop.A10 below).(3)
recvgC,ecu,ecukey,ecucnt,prevcnt,bus,mackey,msgid,msg,cnt denotes the successful reception and processing of a message by ecu∈ℙgCnt.(4)
With the actionloseCntgC,ecu,ecucnt,prevcnt,msgid we model the fact that ecu∈ECUgC has lost the correct counter value for some reason. This action comprises any situation in which an ECU is not synchronized anymore. As a consequence, its counter is set to a value smaller than the correct counter value.The idea of a generic counter-based system is that counter values should be strictly monotonically increasing. However, in real systems message transmission may fail due to transmission errors of the bus (e.g. by flipping a bit). Such a message is not accepted in which case the sender simply repeats it, using the same counter as before. We abstract from this since incidents of this type are not security relevant and assume all messages sent by an honest ECU not to suffer from physical failures of the system. This leads to the following definition of the correct counter for a specific action.Definition 8.
Letω=x1…xr∈ΣgCnt∗andk∈1,…,r. Then the correct counter for actionxkinωis defined as follows:(3)corCntgCxk,ω≔1,ifk=1,cardxi∈alphω|i∈1,…,k∧κ∧a namexi=sendgC∧κ∧cntx1<⋯<κ∧cntxk,ω,ifk>1.
This definition assumes that the very first message of any action sequence of the system is sent by an honest ECU.


#### 5.1.2. Introducing a Phase Class into the Model

In the GenCnt system, only messages with correct counters shall be received and accepted, i.e. their values shall be strictly monotonically increasing. Each counter therefore identifies a phase of the system that starts with sending the message containing it. Hence we use send actions to identify phase classes: Each send actions starts a new phase class, and the phase class ends with the next send action that in turn starts a new phase class. The formal definition of this particularS,T-phase class is based on Definition 6:Definition 9.
ForΥ⊆ΣgCnt∗anda∈ΣgCntwithκ∧anamea=sendgCwe define(4)Φa,Υ≔ΦΥ,a,a′.∈∑gCnt|κ∧anamea′=sendgC.
From a recipient’s point of view, when having performed a receive actionb containing a specific counter, the phase class “activating” this counter starts with the send action that writes this particular message onto the bus. Considering the characteristics of a CAN bus as described in Section 2.1, there cannot be any other send action between these two actions on the bus. Recall that a message manipulated by Eve is considered to have been sent by her. Consequently we do not have two consecutive sendgC actions. Hence for each receive action b occuring in a sequence of actions, the corresponding send action, denoted by σb, is unique. Consequently, each b determines a unique phase class Φa,Υ with a=σb. Thus for a specific receive action b∈ω we can rename the phase class it determines and denote it by Φσb,Υ. For the sake of completeness, for a send action s we define σs≔s.
For the rest of the paper we will use the particular phase classΦσb,WgCnt determined by a recvgC action b with WgCnt denoting all ECUs’ initial knowledge that we assume to be identical. In Section 5.2 we will explain how this phase class can be used to model immediacy and non-repeatability.


#### 5.1.3. Agents’ Local View and Initial Knowledge

The definition of the ECUs’ local view must take into account that they can see the messages sent on the bus they are connected to but cannot see who sent them nor the local parameters of the sender. Further, except for these send actions, ECUs can only see their own actions. Hence for allP∈ℙgCnt and for all a∈ΣgCnt we define λP as follows:(1)
κ∧ecua=λPa≔a(2)
κ∧ecua≠P∧κ∧anamea∈readgC,recvgC,loseCntgC⇒λPa≔ε(3)
κ∧ecua≠P∧κ∧anamea=sendgC⇒λPa≔sendgC,bus,κ∧mackeya,κ∧msgida,κ∧msga,κ∧cntaAgents’ Initial Knowledge The agents’ initial knowledge captures the constraints and assumptions that we know to hold for our system. If not specified otherwise, the properties refer to ω∈WgCnt.Prop.
A1. A receive action on bus is always preceded by the corresponding send action that writes the message onto the bus. Obviously, the parameter values of mackey, msgid, msg and cnt in b and σb are identical (we forgo the formal specification of this statement). The only actions that can happen in between are readgC,recvgC and loseCntgC actions by ECUs other than sender and receiver. Formally:
For allb∈ΣgCnt with κ∧aname=recvgC holds
(1)
precWgCntσb,b(2)
∀v∈ΦWbCnt,σb,b∀a∈alphv:κ∧ecua=κ∧ecuσb∨κ∧anamea=sendgC⇒a=pre1v=σbandκ∧ecua=κ∧ecub⇒a=suf1v=bProp.
A2. Only members of ECUgC own and can use key. Since Eve does not own this key and honest ECUs use only key to generate and verify a MAC, the MAC key contained in a send or receive action being equal to the ECU’s key and this being equal to key is equivalent to the ECU being member of ECUgC.
∀a∈alphω:κ∧anamea∈sendgC,recvgC⇒κ∧mackeya=κ∧ecukeya=key⇔κ∧ecua∈ECUgC.Prop.
A3. A recvgC action performed by an honest ECU (i.e. a member of ECUgC) must be preceded by the respective send action of an agent having generated the MAC, i.e. owning the key used for MAC generation:
∀ecu∈ECUgC:precWgCntsendgC,ecu′,ecukey′,ecucnt′,prevcnt′,bus,mackey,msgid,msg,cnt|ecukey′=mackey=key,recvgC,ecu,ecukey,ecucnt,prevcnt,bus,mackey,msgid,msg,cnt
Again, obviously, the parameter values ofmackey,msgid,msg and cnt in b and the send action are identical.Prop.
A4. The parameter prevcnt of an action performed by an honest ECU denotes the local message counter the ECU has used in its previous action. For the very first action of an ECU it is defined as the minimal value (which we assume without loss of generality to be equal to 1) of bCnt.
∀a∈alphω:κ∧ecu∈ECUgC⇒κ∧prevcnta=κ∧ecucntprevacta,κ∧ecua,ω. If for all ai∈ω with actCntai,ω<actCnta,ω holds κ∧ecuai≠κ∧ecua, it follows κ∧prevcnta=1.Prop.
A5. FvM is the only ECU that sends synchronization messages. It does not perform any other action.
∀a∈alphω:κ∧ecua=FvM⇔κ∧anamea=sendgC∧κ∧msgida=sync∧κ∧ecucnta=κ∧msga.Prop.
A6. It is obvious that synchronization messages including a wrong (i.e. too small) counter value open possibilities for all kinds of attacks. Hence we assume that a synchronization message sent by FvM always contains the correct counter value according to Definition 8.
∀x∈preω:κ∧ecusuf1x=FvM⇒κ∧msgsuf1x=corCntgCsuf1x,x.Prop.
A7. When an honest agent different to FvM receives (i.e. accepts) a synchronization message, it verifies that the message’s payload (which contains the counter) is greater than the local counter used in its previous action and then sets its local counter to the value of the message counter:
∀a∈alphω:κ∧anamea=recvgC∧κ∧ecua∈ΕCUgC\FvM⇒κ∧msga=κ∧ecucnta≥κ∧prevcnta+1.Prop.
A8. An honest agent other than FvM only sends functional messages. When doing so, it increments the counter used in its previous action by 1, uses this value as its new local counter value and as the value of cnt for MAC generation.
∀a∈alphω:κ∧anamea=sendgC∧κ∧ecua∈ΕCUgC\FvM⇔κ∧msgida=fmsg∧κ∧ecucnta=κ∧cnta=κ∧prevcnta+1.Prop.
A9. When an honest agent different to FvM receives (i.e. accepts) a functional message, it verifies that the message’s counter is greater than the local counter used in its previous action and then sets its local counter to the value of the message counter:
∀a∈alphω:κ∧anamea=recvgC∧κ∧ecua∈ΕCUgC\FvM⇒κ∧cnta=κ∧ecucnta≥κ∧prevcnta+1.Prop.
A10. An important property of the generic counter system GenCnt is that an ECU increases its counter value only in case it has received and accepted a message with a bigger counter value. Hence an action readgC by an honest ECU does not change ecu’s local counter value: ∀a∈alphω:κ∧anamea=readgC∧κ∧ecua∈ΕCUgC⇒κ∧ecucnta=κ∧prevcntaProp.
A11. An action loseCntgC performed by an honest ECU resets the ECU’s counter value to a value smaller than the correct one:
∀x∈preω:κ∧anamesuf1x=loseCntgC∧κ∧ecusuf1x∈ΕCUgC⇒κ∧ecucntsuf1x<corCntgCsuf1x,xProp.
A12. When an honest ECU performs two recvgC actions with its local genCnt value of the first one being bigger than or equal to the local genCnt value of the second one, it must have performed a loseCntgC action in between.
Forω=x1…xk,1≤i<l<j≤k, if κ∧anamexi=κ∧anamexj=recvgC and κ∧ecuxi=κ∧ecuxj∈ΕCUgC and κ∧ecucntxi≥κ∧ecucntxj then there exists xl∈alphω with κ∧anamexl=loseCntgC and κ∧ecuxl=κ∧ecuxi=κ∧ecuxj.
This concludes our system model specification. In the next section, we will show that the model allows certain states which violate a property that can be used for the specification of authenticity, immediacy and non-repeatability.


### 5.2. Formal Verification of the Generic Counter Concept

As stated in Section2.5, the security requirements the generic counter system (denoted by BgCnt) shall satisfy are data origin authenticity, immediacy and non-repeatability. More precisely, an honest ECU shall accept only messages authentically generated and sent by another honest ECU, thus providing data origin authenticity. Further, the message must contain the correct counter which ensures that no counter is accepted twice (since the correct counter is strictly monotonically increasing), thus providing non-repeatability. In order to express this, we use the phase class Φσb,WgCnt as defined in Definition 9 with b being a recvgC action. Each time an honest ecu receives a message, the message must authentically for ecu have been sent by a member of the same group, and this send action must be the one to trigger ecu’s recvgC action b, i.e. must be the start action σb of the phase class determined by b. Since the time period between sending and receiving messages on a CAN bus is very short, we can assume that it never exceeds the specified limit which implies immediacy. This can be formalized as follows:Theorem 1.
Letω∈BgCntandb≔recvgC,ecu,ecukey,ecucnt,prevcnt,bus,mackey,msgid,msg,cnt∈alphωwithecu∈ECUgC. Then the following property holds:(5)authWiPhasesendgC,ecu′,ecukey′,ecucnt′,prevcnt′,bus,mackey,msgid,msg,cnt|ecu′∈ECUgC,b,ecu,Φσb,WgCntProof 1.
Assume one of the honest ECUs different toFvM that is member of the group receives (i.e. accepts) a message. Without loss of generality assume it is ECU1gC∈ECUgC and b≔recvgC,ECU1gC,ecukey,ecucnt,prevcnt,bus,mackey,msgid,msg,cnt∈alphω for some ω∈BgCnt. By definition, λECU1gC keeps this action, thus b is also contained in each x∈λECU1gC−1λECU1gCω. Further, b is contained in ω∈BgCnt⊆WgCnt. So let x∈λECU1gC−1λECU1gCω∩WgCnt arbitrarily chosen. Since ECU1gC∈ECUgC, Prop.A2 implies that ecukey=mackey=key. Further, by Prop.A3, there is an action a1≔sendgC,ecu1,ecukey1,ecucnt1,prevcnt1,bus,mackey,msgid,msg,cnt∈alphx before ECU1gC’s receive action containing the same message, message ID and counter value and with ecukey1=mackey=key. Applying again Prop.A2 it follows ecu1∈ΕCUgC. Hence the message received in b has authentically for ECU1gC been sent by a member of ΕCUgC, i.e. data origin authenticity is satisfied.
Thereforeecu1=FvM and msgid=sync (Prop.A5) or ecu1=ECU2gC and msgid=fmsg (Prop.A8) (we disregard the fact that in principle ECU1gC could itself be the originator of this message and assume this issue to be addressed by e.g. unique message IDs). By Prop.A1 b is preceded by σb=sendgC,ecu′,ecukey′,ecucnt′,bus,mackey,msgid,msg,cnt that starts the phase class identified by b. By definition, the local view of ECU1gC does not reveal the sender, hence assume ecu′≠ecu1 and σb≠a1, i.e. assume that the authentic action a1 is not performed in the required phase class. Assume further that after having performed their respective last actions before a1 (denoted by a2 and a3, respectively), ecu1 and ECU1gC are synchronized, i.e. own the same counter which is the correct one for these actions. Let us assume ECU1gC performs a3, ecu1 performs a2 and κ∧ecucnta2=κ∧ecucnta3=k=corCntgCa2,x=corCntgCa3,x.
Assumeecu1=ECU2gC and κ∧msgida1=fmsg. Then Prop.A8 implies κ∧ecucnta1=κ∧prevcnta1+1=κ∧cnta1. Since a2 is the last action of ecu1 before a1, Prop.A4 implies that κ∧prevcnta1=κ∧ecucnta2. Prop.A3 implies cnt=κ∧cntb=κ∧cnta1 and it follows κ∧cnta1=κ∧ecucnta1=κ∧ecucnta2+1=k+1. This situation, depicted in Table 2 , is the basis for the subsequent case-by-case analysis (note that it is irrelevant whether a3 precedes a2 or vice versa).Table 2
Developing possible sequences
a3last action byECU1gCbeforea1κ^ecucnta2=kkis correct countera2last action byecu1beforea1κ^ecucnta3=k⋮no actions byECU1gCandecu1⋮a1sendgC,ecu1,ecukey,ecucnt1,prevcnt1,bus,mackey,msgid,msg,cntecucnt1=prevcnt1+1=κ^ecucnta2+1=k+1=cnt⋮σbsendgC,ecu′,ecukey′,ecucnt′,prevcnt′,bus,mackey,msgid,msg,cntcnt=k+1by Prop.A1brecvgC,ECU1gC,ecukey,ecucnt,prevcnt,bus,mackey,msgid,msg,cntecucnt=cnt=k+1


#### 5.2.1. Losing the counter

Assume thatECU1gC receives the message sent by ecu1 in a1 by performing an action a4 (i.e. σa4=a1). Then κ∧cnta4=κ∧cnta1=k+1 (Prop.A1) and Prop.A9 implies κ∧ecucnta4=κ∧cnta4=k+1. Prop.A9 also requires κ∧ecucnta4≥κ∧prevcnta4+1. This is the case, as by Prop.A4 we can conclude κ∧prevcnta4=κ∧ecucnta3 and thus k+1=κ∧ecucnta4≥κ∧ecucnta3+1 which by the assumption of ECU1gC and ecu1 being synchronized before a1 is equal to κ∧ecucnta2+1=k+1, hence κ∧ecucnta4=k+1≥k+1 is satisfied. Since with action b, ECU1 receives and accepts cnt=k+1, Prop.A12 implies that ECU1gC performs an action a5≔loseCntgC,ECU1gC,ecucnt5,prevcnt5,bus between a4 and b, and Prop.A11 implies that ecucnt5 is smaller than the correct counter value for this action which in turn is equal to or bigger than κ∧cnta5=k+1. Assume that between a4 and a5 there have been k′ send actions by members of ECUgC other than ECU1gC with correct counters, increasing its value to k+1+k′ without changing ECU1gC’s counter value (e.g. because it does not perform any action other than a5 between a4 and b). It follows ecucnt5<corCntgCa5,x=k+1+k′. On the other hand, in bECU1gC receives and accepts the message sent in σb with the counter cnt=k+1. So assuming ECU1gC’s loseCntgC action a5 to be its last action before b, Prop.A4 and Prop.A9 imply k+1=κ∧cntb=κ∧ecucntb≥κ∧prevcntb+1=ecucnt5. Both inequalities are satisfied for ecucnt5≤k+1−1=k. Thus ECU1gC may very well receive and accept the message sent in σb by ecu′∉ECUgC.The resulting sequence of actions is depicted in Table3. While it satisfies data origin authenticity, it violates immediacy, assuming that only the time period between writing a message onto the bus and reading it does not exceed the specified limit. It also violates non-repeatability as the message sent in a1 is accepted twice.Table 3
A first attack sequence.
a3action byECU1gCκ^ecucnta2=ka2action byecu1κ^ecucnta3=k⋮no actions byECU1gCandecu1⋮a1sendgC,ecu1,ecukey,ecucnt1,prevcnt1,bus,mackey,msgid,msg,cntecucnt4=cnt=k+1κ^ecucnta2+1=k+1=cnta4recvgC,ECU1gC,ecukey,ecucnt4,prevcnt4,bus,mackey,msgid,msg,cntecucnt4=cnt=k+1⋮a5loseCntgC,ECU1gC,ecucnt5,prevcnt5,busecucnt5<k+1+k′⋮no action byECU1gC⋮σbsendgC,ecu′,ecukey′,ecucnt′,prevcnt′,bus,mackey,msgid,msg,cntcnt=k+1brecvgC,ECU1gC,ecukey,ecucnt,prevcnt,bus,mackey,msgid,msg,cntecucnt=cnt=k+1It is not surprising that counter loss without timely synchronization opens up attack possibilities. The same result can be shown in caseecu1=FvM sends a synchronization message in a1. We then need to consider the fact that between a2 and a1, ECU2gC may have sent n messages that increase the correct counter of a1 accordingly. Further, instead of applying Prop.A8 we need to take into account that the counter is sent as the message’s payload, i.e. modeled by the parameter msg, and apply Prop.A5.We will now investigate whether sending of synchronization messages prohibits the above described attack. Assume therefore that with theloseCntgC action ECU1gC sets its local genCnt value to k′′<k+1+k′ and that between the loseCntgC action and b, ECU1gC receives one or more synchronization messages with a6 being the last one before b. Since cnt=k+1 is the counter accepted by ECU1gC in b and since the counter sent in a synchronization message is contained in its payload, κ∧msga6=msg6∈k″+1,k. Assume further these are the only messages sent on the bus. Then again by Prop.A4 and Prop.A7, cnt=k+1=κ∧cntb=κ∧ecucntb≥κ∧prevcntb+1=κ∧ecucnta6+1=κ∧msga6+1=msg6+1≥k″+2 which implies k″≤msg6−1≤k+1−2=k−1. According to Prop.A1, a6 is preceded by an action σa6 in which the synchronization message received by ECU1gC is written to the bus. The property further implies that between σa6 and a6, ECU1gC does not perform any further action, hence σa6 happens after ECU1gC’s loseCntgC action and in particular after a1. Recall now that we have assumed k to be the correct counter value of both a2 and a3 and that κ∧cnta1=k+1. If κ∧ecuσa6 was FvM, Prop.A6 would imply κ∧msgσa6≥k+1+1=k+2. Yet what ECU1gC accepts in a6 is msg6≤k+1−1=k. Thus κ∧ecuσa6≠FvM and since by Prop.A8 an honest agent other than FvM only sends functional messages, it follows κ∧ecuσa6=Eve.While by Prop.A3,a6 is preceded by an action a7≔sendgC,FvM,…,sync,…msg6,…, this does not necessarily interfere with the attack we are constructing here, assuming that ECU1gC does not receive (i.e. accept) this message but only performs a readgC action which does not change its local counter. This attack is illustrated in Table 4.Table 4
The second possible attack sequence.
a3action byECU1gCκ^ecucnta2=ka2action byecu1κ^ecucnta3=k⋮no actions byECU1gCandecu1⋮a1sendgC,ecu1,ecukey,ecucnt1,prevcnt1,bus,mackey,msgid,msg,cntecucnt1=prevent1+1=κ^ecucnta2+1=k+1=cnta4recvgC,ECU1gC,ecukey,ecucnt4,prevcnt4,bus,mackey,msgid,msg,cntecucnt4=cnt=k+1⋮a5loseCntgC,ECU1gC,ecucnt5,prevcnt5,busecucnt5<k+1+k′⋮a7sendgC,FvM,…,sync,…,msg6,…,a8readgC,ECU1gC,…,ecucnt8,prevcnt8,sync,…,msg6,…ecucnt8=prevcnt8=ecucnt5⋮σa6sendgC,Eve,…,sync,…,msg6,…,msg6∈k″+1,k+1−1a6recvgC,ECU1gC,ecukey,ecucnt6,prevcnt6,…,sync,…,msg6,…,ecucnt6=msg6≤k+1−1prevent6=ecucnt8=k″∧msg6≥k″+1σbsendgC,ecu′,ecukey′,ecucnt′,prevcnt′,bus,mackey,msgid,msg,cntcnt=k+1brecvgC,ECU1gC,ecukey,ecucnt,prevcnt,bus,mackey,msgid,msg,cntecucnt=cnt=k+1This attack uses an important characteristic of the generic counter systemGenCnt, captured in Prop.A10: It causes ECU1gC to keep the too small and thus incorrect counter since it does not correctly receive and accept the synchronization messages sent by FvM between a5 and b. The attack again violates immediacy and non-repeatability.


#### 5.2.2. Not losing the counter

Let us now consider the case in whichECU1gC only performs readgC actions between a3 and b and in particular does not perform an action a4, i.e. does not receive and accept the message sent by ecu1 in a1. As above, by Prop.A1 and Prop.A3 we know κ∧cnta1=κ∧cntb=κ∧cntσb. Since by Prop.A10 a readgC action does not change ECU1gC’s counter, consecutive application of Prop.A4 to the sequence of these readgC actions implies κ∧prevcntb=κ∧ecucnta3 and by Prop.A9 it follows k+1=cnt=κ∧cntb=κ∧ecucntb≥κ∧prevcntb+1=κ∧ecucnta3+1=k+1. This equation is always satisfied which means that there is no contradiction to κ∧ecuσb=ecu′≠ecu1. Therefore this sequence (illustrated in Table 5) is another example for violation of immediacy based on invalidation and replay of messages. Note that it does not violate non-repeatability as the message is only received and accepted once.Table 5
The third possible attack sequence.
a3action byECU1gCκ^ecucnta2=ka2action byecu1κ^ecucnta3=k⋮onlyreadgCactions byECU1gC⋮a1sendgC,ecu1,ecukey,ecucnt1,prevcnt1,bus,mackey,msgid,msg,cntecucnt1=prevcnt1+1=κ^ecucnta2+1=k+1=cnt⋮onlyreadgCactions byECU1gC⋮σbsendgC,ecu′,ecukey′,ecucnt′,prevcnt′,bus,mackey,msgid,msg,cntcnt=k+1brecvgC,ECU1gC,ecukey,ecucnt,prevcnt,bus,mackey,msgid,msg,cntecucnt=cnt=prevcnt+1=κ^ecucnta2=k+1The only case in which the desired properties hold is if by performinga4, ECU1gC receives and accepts the message sent in a1 and does not lose the correct counter value, i.e. does not perform a loseCntgC action between a4 and b. In this case ECU1gC sets its local counter κ∧ecucnta4 to k+1 (Prop.A9) and without losing the correct counter will not accept the same counter in action b anymore, as κ∧prevcntb=κ∧ecucnta4=k+1 and thus κ∧cntb=k+1≯κ∧prevcntb=k+1 as is required by Prop.A9.Our proof indicating possible attacks is based on the fact that certain messages are not received but only read byECU1gC. This can easily be accomplished by an attacker with the abilities described in Section 2.2. All she has to do is to monitor the respective message and then invalidate it and all following ones related to the relevant counter by changing a CRC bit or overwriting the message with an error frame. This will cause all ECUs connected to the bus to reject the messages. Since readgC actions do not change the ECUs’ local counter, any message containing a bigger counter will still be considered correct.In Section7.1 we will discuss the results achieved by the proof and compare them to the formal proofs of the bus counter-based system to be introduced in the next section.


## 5.1. The Formal Generic Counter Model

Our SeMF model shall be as simple as possible. It needs to include ECUs connected to a bus whose messages shall be proven to be protected. It also needs to reflect our attack model introduced in Section2.2, hence must include devices (e.g. ECUs) that an attacker can use to monitor, record, resent and manipulate messages sent on the bus. It is obvious that messages sent on one bus may be accepted by ECUs connected to another bus if the key used for protecting these messages is the same for both buses. Hence we disregard this aspect and restrict our model to one group of honest devices, all owning the same MAC key for message protection, and a further device Eve representing dishonest behavior. All devices are connected to the same bus. Our model can easily be extended, for example by adding more groups, keys and buses, in case other aspects than those addressed in this paper shall be investigated. A special honest device is the Fresh Value Master (FvM) that is responsible for the synchronization of ECUs regarding their counter. We assume all honest devices to act according to a given specification (see Section 5.1.3). FvM only sends synchronization messages, i.e. messages with msgid=sync. Other honest devices receive synchronization messages and send and receive functional messages with msgid=fmsg. We do not distinguish between different types of functional messages and use just one with its corresponding message counter. Eve can send and receive all types of messages but does not own the MAC key and can thus not generate MACs.We use four different types of actions: sending and receiving (i.e. accepting) of messages, reading a message without processing it, and an action that models an ECU losing the correct message counter (denoted by genCnt henceforth). This action comprises any situation in which an ECU is not synchronized anymore, i.e. owns a counter smaller than the current correct counter value.While in many systems (e.g. in [4]) messages only contain a truncated message counter and MAC, respectively, in our model the counter’s complete value is included. This way we model the assumption that the recipients always succeed in determining the counter values used by the senders (after all, this aspect is not in the focus of our investigations).


### 5.1.1. Agents, Parameters and Actions

For the formal specification of actions according to Definition1, we use the following sets:(1)
Set of agents:ℙgCnt≔ECUgC∪Eve with ECUgC≔ECU1gC,ECU2gC,FvM whose members are connected to the only bus of the system. FvM denotes the synchronization master and Eve denotes a further device being connected to the bus but not being member of ECUgC.(2)
set of action names:AgCnt=sendgC,readgC,recvgC,loseCntgC(3)
set of parameters:PgCnt≔aname,ecu,ecukey,ecucnt,prevcnt,bus,mackey,msgid,msg,cnt with aname∈AgCnt,ecu∈ℙgCnt,ecukey,mackey∈key∪ℕ, key being the key all honest ECUs use for MAC generation and verification, while ecukey∈ℕ for ecu=Eve. Further, ecucnt,prevcnt,cnt∈ℕ∪nocnt,bus∈bus,msgid∈sync,fmsg, and msg∈ℳ (ℳ being an arbitrary set of messages).(4)
The set of actionsΣgCnt is then defined as follows:(1)
sendgC,ecu,ecukey,ecucnt,prevcnt,bus,mackey,msgid,msg,cnt:ecu∈PgCnt sends a message on bus=bus. The message’s MAC (not explicitly modelled by a parameter of this action) is generated with mackey and covers msgid,msg and cnt. ecu∈ECUgC if none of the entire message bits as illustrated in Figure 1 has been written to the bus by Eve. ecu may or may not have generated the MAC. For ecu∈ECUgC, the parameter ecukey denotes ecu ’s MAC generation and verification key key, ecucnt denotes its local counter value after having performed the sendgC action, and prevcnt denotes the counter value resulting from ecu’s previous action (see Section 5.1.3 for the specific operations regarding an ECU’s counter). The message can be a functional message, indicated by msgid=fmsg, in which case the counter contained in the message’s payload is explicitly modelled by cnt, or a synchronization message with msgid=sync. In this case the message’s payload msg only contains the counter determined by the sender and the parameter cnt contains the constant nocnt. Note that there is the possibility that the message is altered (by a technical error or by Eve) after having been sent and may thus only cause a readgC action (see below).(2)
readgC,ecu,ecukey,ecucnt,prevcnt,bus,mackey,msgid,msg,cnt denotesecu∈ℙbCnt reading a message without processing it (i.e. without accepting it). The action does not change the local message counter ecucnt if ecu∈ECUgC (see Prop.A10 below).(3)
recvgC,ecu,ecukey,ecucnt,prevcnt,bus,mackey,msgid,msg,cnt denotes the successful reception and processing of a message by ecu∈ℙgCnt.(4)
With the actionloseCntgC,ecu,ecucnt,prevcnt,msgid we model the fact that ecu∈ECUgC has lost the correct counter value for some reason. This action comprises any situation in which an ECU is not synchronized anymore. As a consequence, its counter is set to a value smaller than the correct counter value.The idea of a generic counter-based system is that counter values should be strictly monotonically increasing. However, in real systems message transmission may fail due to transmission errors of the bus (e.g. by flipping a bit). Such a message is not accepted in which case the sender simply repeats it, using the same counter as before. We abstract from this since incidents of this type are not security relevant and assume all messages sent by an honest ECU not to suffer from physical failures of the system. This leads to the following definition of the correct counter for a specific action.Definition 8.
Letω=x1…xr∈ΣgCnt∗andk∈1,…,r. Then the correct counter for actionxkinωis defined as follows:(3)corCntgCxk,ω≔1,ifk=1,cardxi∈alphω|i∈1,…,k∧κ∧a namexi=sendgC∧κ∧cntx1<⋯<κ∧cntxk,ω,ifk>1.
This definition assumes that the very first message of any action sequence of the system is sent by an honest ECU.


### 5.1.2. Introducing a Phase Class into the Model

In the GenCnt system, only messages with correct counters shall be received and accepted, i.e. their values shall be strictly monotonically increasing. Each counter therefore identifies a phase of the system that starts with sending the message containing it. Hence we use send actions to identify phase classes: Each send actions starts a new phase class, and the phase class ends with the next send action that in turn starts a new phase class. The formal definition of this particularS,T-phase class is based on Definition 6:Definition 9.
ForΥ⊆ΣgCnt∗anda∈ΣgCntwithκ∧anamea=sendgCwe define(4)Φa,Υ≔ΦΥ,a,a′.∈∑gCnt|κ∧anamea′=sendgC.
From a recipient’s point of view, when having performed a receive actionb containing a specific counter, the phase class “activating” this counter starts with the send action that writes this particular message onto the bus. Considering the characteristics of a CAN bus as described in Section 2.1, there cannot be any other send action between these two actions on the bus. Recall that a message manipulated by Eve is considered to have been sent by her. Consequently we do not have two consecutive sendgC actions. Hence for each receive action b occuring in a sequence of actions, the corresponding send action, denoted by σb, is unique. Consequently, each b determines a unique phase class Φa,Υ with a=σb. Thus for a specific receive action b∈ω we can rename the phase class it determines and denote it by Φσb,Υ. For the sake of completeness, for a send action s we define σs≔s.
For the rest of the paper we will use the particular phase classΦσb,WgCnt determined by a recvgC action b with WgCnt denoting all ECUs’ initial knowledge that we assume to be identical. In Section 5.2 we will explain how this phase class can be used to model immediacy and non-repeatability.


### 5.1.3. Agents’ Local View and Initial Knowledge

The definition of the ECUs’ local view must take into account that they can see the messages sent on the bus they are connected to but cannot see who sent them nor the local parameters of the sender. Further, except for these send actions, ECUs can only see their own actions. Hence for allP∈ℙgCnt and for all a∈ΣgCnt we define λP as follows:(1)
κ∧ecua=λPa≔a(2)
κ∧ecua≠P∧κ∧anamea∈readgC,recvgC,loseCntgC⇒λPa≔ε(3)
κ∧ecua≠P∧κ∧anamea=sendgC⇒λPa≔sendgC,bus,κ∧mackeya,κ∧msgida,κ∧msga,κ∧cntaAgents’ Initial Knowledge The agents’ initial knowledge captures the constraints and assumptions that we know to hold for our system. If not specified otherwise, the properties refer to ω∈WgCnt.Prop.
A1. A receive action on bus is always preceded by the corresponding send action that writes the message onto the bus. Obviously, the parameter values of mackey, msgid, msg and cnt in b and σb are identical (we forgo the formal specification of this statement). The only actions that can happen in between are readgC,recvgC and loseCntgC actions by ECUs other than sender and receiver. Formally:
For allb∈ΣgCnt with κ∧aname=recvgC holds
(1)
precWgCntσb,b(2)
∀v∈ΦWbCnt,σb,b∀a∈alphv:κ∧ecua=κ∧ecuσb∨κ∧anamea=sendgC⇒a=pre1v=σbandκ∧ecua=κ∧ecub⇒a=suf1v=bProp.
A2. Only members of ECUgC own and can use key. Since Eve does not own this key and honest ECUs use only key to generate and verify a MAC, the MAC key contained in a send or receive action being equal to the ECU’s key and this being equal to key is equivalent to the ECU being member of ECUgC.
∀a∈alphω:κ∧anamea∈sendgC,recvgC⇒κ∧mackeya=κ∧ecukeya=key⇔κ∧ecua∈ECUgC.Prop.
A3. A recvgC action performed by an honest ECU (i.e. a member of ECUgC) must be preceded by the respective send action of an agent having generated the MAC, i.e. owning the key used for MAC generation:
∀ecu∈ECUgC:precWgCntsendgC,ecu′,ecukey′,ecucnt′,prevcnt′,bus,mackey,msgid,msg,cnt|ecukey′=mackey=key,recvgC,ecu,ecukey,ecucnt,prevcnt,bus,mackey,msgid,msg,cnt
Again, obviously, the parameter values ofmackey,msgid,msg and cnt in b and the send action are identical.Prop.
A4. The parameter prevcnt of an action performed by an honest ECU denotes the local message counter the ECU has used in its previous action. For the very first action of an ECU it is defined as the minimal value (which we assume without loss of generality to be equal to 1) of bCnt.
∀a∈alphω:κ∧ecu∈ECUgC⇒κ∧prevcnta=κ∧ecucntprevacta,κ∧ecua,ω. If for all ai∈ω with actCntai,ω<actCnta,ω holds κ∧ecuai≠κ∧ecua, it follows κ∧prevcnta=1.Prop.
A5. FvM is the only ECU that sends synchronization messages. It does not perform any other action.
∀a∈alphω:κ∧ecua=FvM⇔κ∧anamea=sendgC∧κ∧msgida=sync∧κ∧ecucnta=κ∧msga.Prop.
A6. It is obvious that synchronization messages including a wrong (i.e. too small) counter value open possibilities for all kinds of attacks. Hence we assume that a synchronization message sent by FvM always contains the correct counter value according to Definition 8.
∀x∈preω:κ∧ecusuf1x=FvM⇒κ∧msgsuf1x=corCntgCsuf1x,x.Prop.
A7. When an honest agent different to FvM receives (i.e. accepts) a synchronization message, it verifies that the message’s payload (which contains the counter) is greater than the local counter used in its previous action and then sets its local counter to the value of the message counter:
∀a∈alphω:κ∧anamea=recvgC∧κ∧ecua∈ΕCUgC\FvM⇒κ∧msga=κ∧ecucnta≥κ∧prevcnta+1.Prop.
A8. An honest agent other than FvM only sends functional messages. When doing so, it increments the counter used in its previous action by 1, uses this value as its new local counter value and as the value of cnt for MAC generation.
∀a∈alphω:κ∧anamea=sendgC∧κ∧ecua∈ΕCUgC\FvM⇔κ∧msgida=fmsg∧κ∧ecucnta=κ∧cnta=κ∧prevcnta+1.Prop.
A9. When an honest agent different to FvM receives (i.e. accepts) a functional message, it verifies that the message’s counter is greater than the local counter used in its previous action and then sets its local counter to the value of the message counter:
∀a∈alphω:κ∧anamea=recvgC∧κ∧ecua∈ΕCUgC\FvM⇒κ∧cnta=κ∧ecucnta≥κ∧prevcnta+1.Prop.
A10. An important property of the generic counter system GenCnt is that an ECU increases its counter value only in case it has received and accepted a message with a bigger counter value. Hence an action readgC by an honest ECU does not change ecu’s local counter value: ∀a∈alphω:κ∧anamea=readgC∧κ∧ecua∈ΕCUgC⇒κ∧ecucnta=κ∧prevcntaProp.
A11. An action loseCntgC performed by an honest ECU resets the ECU’s counter value to a value smaller than the correct one:
∀x∈preω:κ∧anamesuf1x=loseCntgC∧κ∧ecusuf1x∈ΕCUgC⇒κ∧ecucntsuf1x<corCntgCsuf1x,xProp.
A12. When an honest ECU performs two recvgC actions with its local genCnt value of the first one being bigger than or equal to the local genCnt value of the second one, it must have performed a loseCntgC action in between.
Forω=x1…xk,1≤i<l<j≤k, if κ∧anamexi=κ∧anamexj=recvgC and κ∧ecuxi=κ∧ecuxj∈ΕCUgC and κ∧ecucntxi≥κ∧ecucntxj then there exists xl∈alphω with κ∧anamexl=loseCntgC and κ∧ecuxl=κ∧ecuxi=κ∧ecuxj.
This concludes our system model specification. In the next section, we will show that the model allows certain states which violate a property that can be used for the specification of authenticity, immediacy and non-repeatability.


## 5.1.1. Agents, Parameters and Actions

For the formal specification of actions according to Definition1, we use the following sets:(1)
Set of agents:ℙgCnt≔ECUgC∪Eve with ECUgC≔ECU1gC,ECU2gC,FvM whose members are connected to the only bus of the system. FvM denotes the synchronization master and Eve denotes a further device being connected to the bus but not being member of ECUgC.(2)
set of action names:AgCnt=sendgC,readgC,recvgC,loseCntgC(3)
set of parameters:PgCnt≔aname,ecu,ecukey,ecucnt,prevcnt,bus,mackey,msgid,msg,cnt with aname∈AgCnt,ecu∈ℙgCnt,ecukey,mackey∈key∪ℕ, key being the key all honest ECUs use for MAC generation and verification, while ecukey∈ℕ for ecu=Eve. Further, ecucnt,prevcnt,cnt∈ℕ∪nocnt,bus∈bus,msgid∈sync,fmsg, and msg∈ℳ (ℳ being an arbitrary set of messages).(4)
The set of actionsΣgCnt is then defined as follows:(1)
sendgC,ecu,ecukey,ecucnt,prevcnt,bus,mackey,msgid,msg,cnt:ecu∈PgCnt sends a message on bus=bus. The message’s MAC (not explicitly modelled by a parameter of this action) is generated with mackey and covers msgid,msg and cnt. ecu∈ECUgC if none of the entire message bits as illustrated in Figure 1 has been written to the bus by Eve. ecu may or may not have generated the MAC. For ecu∈ECUgC, the parameter ecukey denotes ecu ’s MAC generation and verification key key, ecucnt denotes its local counter value after having performed the sendgC action, and prevcnt denotes the counter value resulting from ecu’s previous action (see Section 5.1.3 for the specific operations regarding an ECU’s counter). The message can be a functional message, indicated by msgid=fmsg, in which case the counter contained in the message’s payload is explicitly modelled by cnt, or a synchronization message with msgid=sync. In this case the message’s payload msg only contains the counter determined by the sender and the parameter cnt contains the constant nocnt. Note that there is the possibility that the message is altered (by a technical error or by Eve) after having been sent and may thus only cause a readgC action (see below).(2)
readgC,ecu,ecukey,ecucnt,prevcnt,bus,mackey,msgid,msg,cnt denotesecu∈ℙbCnt reading a message without processing it (i.e. without accepting it). The action does not change the local message counter ecucnt if ecu∈ECUgC (see Prop.A10 below).(3)
recvgC,ecu,ecukey,ecucnt,prevcnt,bus,mackey,msgid,msg,cnt denotes the successful reception and processing of a message by ecu∈ℙgCnt.(4)
With the actionloseCntgC,ecu,ecucnt,prevcnt,msgid we model the fact that ecu∈ECUgC has lost the correct counter value for some reason. This action comprises any situation in which an ECU is not synchronized anymore. As a consequence, its counter is set to a value smaller than the correct counter value.The idea of a generic counter-based system is that counter values should be strictly monotonically increasing. However, in real systems message transmission may fail due to transmission errors of the bus (e.g. by flipping a bit). Such a message is not accepted in which case the sender simply repeats it, using the same counter as before. We abstract from this since incidents of this type are not security relevant and assume all messages sent by an honest ECU not to suffer from physical failures of the system. This leads to the following definition of the correct counter for a specific action.Definition 8.
Letω=x1…xr∈ΣgCnt∗andk∈1,…,r. Then the correct counter for actionxkinωis defined as follows:(3)corCntgCxk,ω≔1,ifk=1,cardxi∈alphω|i∈1,…,k∧κ∧a namexi=sendgC∧κ∧cntx1<⋯<κ∧cntxk,ω,ifk>1.
This definition assumes that the very first message of any action sequence of the system is sent by an honest ECU.


## 5.1.2. Introducing a Phase Class into the Model

In the GenCnt system, only messages with correct counters shall be received and accepted, i.e. their values shall be strictly monotonically increasing. Each counter therefore identifies a phase of the system that starts with sending the message containing it. Hence we use send actions to identify phase classes: Each send actions starts a new phase class, and the phase class ends with the next send action that in turn starts a new phase class. The formal definition of this particularS,T-phase class is based on Definition 6:Definition 9.
ForΥ⊆ΣgCnt∗anda∈ΣgCntwithκ∧anamea=sendgCwe define(4)Φa,Υ≔ΦΥ,a,a′.∈∑gCnt|κ∧anamea′=sendgC.
From a recipient’s point of view, when having performed a receive actionb containing a specific counter, the phase class “activating” this counter starts with the send action that writes this particular message onto the bus. Considering the characteristics of a CAN bus as described in Section 2.1, there cannot be any other send action between these two actions on the bus. Recall that a message manipulated by Eve is considered to have been sent by her. Consequently we do not have two consecutive sendgC actions. Hence for each receive action b occuring in a sequence of actions, the corresponding send action, denoted by σb, is unique. Consequently, each b determines a unique phase class Φa,Υ with a=σb. Thus for a specific receive action b∈ω we can rename the phase class it determines and denote it by Φσb,Υ. For the sake of completeness, for a send action s we define σs≔s.
For the rest of the paper we will use the particular phase classΦσb,WgCnt determined by a recvgC action b with WgCnt denoting all ECUs’ initial knowledge that we assume to be identical. In Section 5.2 we will explain how this phase class can be used to model immediacy and non-repeatability.


## 5.1.3. Agents’ Local View and Initial Knowledge

The definition of the ECUs’ local view must take into account that they can see the messages sent on the bus they are connected to but cannot see who sent them nor the local parameters of the sender. Further, except for these send actions, ECUs can only see their own actions. Hence for allP∈ℙgCnt and for all a∈ΣgCnt we define λP as follows:(1)
κ∧ecua=λPa≔a(2)
κ∧ecua≠P∧κ∧anamea∈readgC,recvgC,loseCntgC⇒λPa≔ε(3)
κ∧ecua≠P∧κ∧anamea=sendgC⇒λPa≔sendgC,bus,κ∧mackeya,κ∧msgida,κ∧msga,κ∧cntaAgents’ Initial Knowledge The agents’ initial knowledge captures the constraints and assumptions that we know to hold for our system. If not specified otherwise, the properties refer to ω∈WgCnt.Prop.
A1. A receive action on bus is always preceded by the corresponding send action that writes the message onto the bus. Obviously, the parameter values of mackey, msgid, msg and cnt in b and σb are identical (we forgo the formal specification of this statement). The only actions that can happen in between are readgC,recvgC and loseCntgC actions by ECUs other than sender and receiver. Formally:
For allb∈ΣgCnt with κ∧aname=recvgC holds
(1)
precWgCntσb,b(2)
∀v∈ΦWbCnt,σb,b∀a∈alphv:κ∧ecua=κ∧ecuσb∨κ∧anamea=sendgC⇒a=pre1v=σbandκ∧ecua=κ∧ecub⇒a=suf1v=bProp.
A2. Only members of ECUgC own and can use key. Since Eve does not own this key and honest ECUs use only key to generate and verify a MAC, the MAC key contained in a send or receive action being equal to the ECU’s key and this being equal to key is equivalent to the ECU being member of ECUgC.
∀a∈alphω:κ∧anamea∈sendgC,recvgC⇒κ∧mackeya=κ∧ecukeya=key⇔κ∧ecua∈ECUgC.Prop.
A3. A recvgC action performed by an honest ECU (i.e. a member of ECUgC) must be preceded by the respective send action of an agent having generated the MAC, i.e. owning the key used for MAC generation:
∀ecu∈ECUgC:precWgCntsendgC,ecu′,ecukey′,ecucnt′,prevcnt′,bus,mackey,msgid,msg,cnt|ecukey′=mackey=key,recvgC,ecu,ecukey,ecucnt,prevcnt,bus,mackey,msgid,msg,cnt
Again, obviously, the parameter values ofmackey,msgid,msg and cnt in b and the send action are identical.Prop.
A4. The parameter prevcnt of an action performed by an honest ECU denotes the local message counter the ECU has used in its previous action. For the very first action of an ECU it is defined as the minimal value (which we assume without loss of generality to be equal to 1) of bCnt.
∀a∈alphω:κ∧ecu∈ECUgC⇒κ∧prevcnta=κ∧ecucntprevacta,κ∧ecua,ω. If for all ai∈ω with actCntai,ω<actCnta,ω holds κ∧ecuai≠κ∧ecua, it follows κ∧prevcnta=1.Prop.
A5. FvM is the only ECU that sends synchronization messages. It does not perform any other action.
∀a∈alphω:κ∧ecua=FvM⇔κ∧anamea=sendgC∧κ∧msgida=sync∧κ∧ecucnta=κ∧msga.Prop.
A6. It is obvious that synchronization messages including a wrong (i.e. too small) counter value open possibilities for all kinds of attacks. Hence we assume that a synchronization message sent by FvM always contains the correct counter value according to Definition 8.
∀x∈preω:κ∧ecusuf1x=FvM⇒κ∧msgsuf1x=corCntgCsuf1x,x.Prop.
A7. When an honest agent different to FvM receives (i.e. accepts) a synchronization message, it verifies that the message’s payload (which contains the counter) is greater than the local counter used in its previous action and then sets its local counter to the value of the message counter:
∀a∈alphω:κ∧anamea=recvgC∧κ∧ecua∈ΕCUgC\FvM⇒κ∧msga=κ∧ecucnta≥κ∧prevcnta+1.Prop.
A8. An honest agent other than FvM only sends functional messages. When doing so, it increments the counter used in its previous action by 1, uses this value as its new local counter value and as the value of cnt for MAC generation.
∀a∈alphω:κ∧anamea=sendgC∧κ∧ecua∈ΕCUgC\FvM⇔κ∧msgida=fmsg∧κ∧ecucnta=κ∧cnta=κ∧prevcnta+1.Prop.
A9. When an honest agent different to FvM receives (i.e. accepts) a functional message, it verifies that the message’s counter is greater than the local counter used in its previous action and then sets its local counter to the value of the message counter:
∀a∈alphω:κ∧anamea=recvgC∧κ∧ecua∈ΕCUgC\FvM⇒κ∧cnta=κ∧ecucnta≥κ∧prevcnta+1.Prop.
A10. An important property of the generic counter system GenCnt is that an ECU increases its counter value only in case it has received and accepted a message with a bigger counter value. Hence an action readgC by an honest ECU does not change ecu’s local counter value: ∀a∈alphω:κ∧anamea=readgC∧κ∧ecua∈ΕCUgC⇒κ∧ecucnta=κ∧prevcntaProp.
A11. An action loseCntgC performed by an honest ECU resets the ECU’s counter value to a value smaller than the correct one:
∀x∈preω:κ∧anamesuf1x=loseCntgC∧κ∧ecusuf1x∈ΕCUgC⇒κ∧ecucntsuf1x<corCntgCsuf1x,xProp.
A12. When an honest ECU performs two recvgC actions with its local genCnt value of the first one being bigger than or equal to the local genCnt value of the second one, it must have performed a loseCntgC action in between.
Forω=x1…xk,1≤i<l<j≤k, if κ∧anamexi=κ∧anamexj=recvgC and κ∧ecuxi=κ∧ecuxj∈ΕCUgC and κ∧ecucntxi≥κ∧ecucntxj then there exists xl∈alphω with κ∧anamexl=loseCntgC and κ∧ecuxl=κ∧ecuxi=κ∧ecuxj.
This concludes our system model specification. In the next section, we will show that the model allows certain states which violate a property that can be used for the specification of authenticity, immediacy and non-repeatability.


## 5.2. Formal Verification of the Generic Counter Concept

As stated in Section2.5, the security requirements the generic counter system (denoted by BgCnt) shall satisfy are data origin authenticity, immediacy and non-repeatability. More precisely, an honest ECU shall accept only messages authentically generated and sent by another honest ECU, thus providing data origin authenticity. Further, the message must contain the correct counter which ensures that no counter is accepted twice (since the correct counter is strictly monotonically increasing), thus providing non-repeatability. In order to express this, we use the phase class Φσb,WgCnt as defined in Definition 9 with b being a recvgC action. Each time an honest ecu receives a message, the message must authentically for ecu have been sent by a member of the same group, and this send action must be the one to trigger ecu’s recvgC action b, i.e. must be the start action σb of the phase class determined by b. Since the time period between sending and receiving messages on a CAN bus is very short, we can assume that it never exceeds the specified limit which implies immediacy. This can be formalized as follows:Theorem 1.
Letω∈BgCntandb≔recvgC,ecu,ecukey,ecucnt,prevcnt,bus,mackey,msgid,msg,cnt∈alphωwithecu∈ECUgC. Then the following property holds:(5)authWiPhasesendgC,ecu′,ecukey′,ecucnt′,prevcnt′,bus,mackey,msgid,msg,cnt|ecu′∈ECUgC,b,ecu,Φσb,WgCntProof 1.
Assume one of the honest ECUs different toFvM that is member of the group receives (i.e. accepts) a message. Without loss of generality assume it is ECU1gC∈ECUgC and b≔recvgC,ECU1gC,ecukey,ecucnt,prevcnt,bus,mackey,msgid,msg,cnt∈alphω for some ω∈BgCnt. By definition, λECU1gC keeps this action, thus b is also contained in each x∈λECU1gC−1λECU1gCω. Further, b is contained in ω∈BgCnt⊆WgCnt. So let x∈λECU1gC−1λECU1gCω∩WgCnt arbitrarily chosen. Since ECU1gC∈ECUgC, Prop.A2 implies that ecukey=mackey=key. Further, by Prop.A3, there is an action a1≔sendgC,ecu1,ecukey1,ecucnt1,prevcnt1,bus,mackey,msgid,msg,cnt∈alphx before ECU1gC’s receive action containing the same message, message ID and counter value and with ecukey1=mackey=key. Applying again Prop.A2 it follows ecu1∈ΕCUgC. Hence the message received in b has authentically for ECU1gC been sent by a member of ΕCUgC, i.e. data origin authenticity is satisfied.
Thereforeecu1=FvM and msgid=sync (Prop.A5) or ecu1=ECU2gC and msgid=fmsg (Prop.A8) (we disregard the fact that in principle ECU1gC could itself be the originator of this message and assume this issue to be addressed by e.g. unique message IDs). By Prop.A1 b is preceded by σb=sendgC,ecu′,ecukey′,ecucnt′,bus,mackey,msgid,msg,cnt that starts the phase class identified by b. By definition, the local view of ECU1gC does not reveal the sender, hence assume ecu′≠ecu1 and σb≠a1, i.e. assume that the authentic action a1 is not performed in the required phase class. Assume further that after having performed their respective last actions before a1 (denoted by a2 and a3, respectively), ecu1 and ECU1gC are synchronized, i.e. own the same counter which is the correct one for these actions. Let us assume ECU1gC performs a3, ecu1 performs a2 and κ∧ecucnta2=κ∧ecucnta3=k=corCntgCa2,x=corCntgCa3,x.
Assumeecu1=ECU2gC and κ∧msgida1=fmsg. Then Prop.A8 implies κ∧ecucnta1=κ∧prevcnta1+1=κ∧cnta1. Since a2 is the last action of ecu1 before a1, Prop.A4 implies that κ∧prevcnta1=κ∧ecucnta2. Prop.A3 implies cnt=κ∧cntb=κ∧cnta1 and it follows κ∧cnta1=κ∧ecucnta1=κ∧ecucnta2+1=k+1. This situation, depicted in Table 2 , is the basis for the subsequent case-by-case analysis (note that it is irrelevant whether a3 precedes a2 or vice versa).Table 2
Developing possible sequences
a3last action byECU1gCbeforea1κ^ecucnta2=kkis correct countera2last action byecu1beforea1κ^ecucnta3=k⋮no actions byECU1gCandecu1⋮a1sendgC,ecu1,ecukey,ecucnt1,prevcnt1,bus,mackey,msgid,msg,cntecucnt1=prevcnt1+1=κ^ecucnta2+1=k+1=cnt⋮σbsendgC,ecu′,ecukey′,ecucnt′,prevcnt′,bus,mackey,msgid,msg,cntcnt=k+1by Prop.A1brecvgC,ECU1gC,ecukey,ecucnt,prevcnt,bus,mackey,msgid,msg,cntecucnt=cnt=k+1


### 5.2.1. Losing the counter

Assume thatECU1gC receives the message sent by ecu1 in a1 by performing an action a4 (i.e. σa4=a1). Then κ∧cnta4=κ∧cnta1=k+1 (Prop.A1) and Prop.A9 implies κ∧ecucnta4=κ∧cnta4=k+1. Prop.A9 also requires κ∧ecucnta4≥κ∧prevcnta4+1. This is the case, as by Prop.A4 we can conclude κ∧prevcnta4=κ∧ecucnta3 and thus k+1=κ∧ecucnta4≥κ∧ecucnta3+1 which by the assumption of ECU1gC and ecu1 being synchronized before a1 is equal to κ∧ecucnta2+1=k+1, hence κ∧ecucnta4=k+1≥k+1 is satisfied. Since with action b, ECU1 receives and accepts cnt=k+1, Prop.A12 implies that ECU1gC performs an action a5≔loseCntgC,ECU1gC,ecucnt5,prevcnt5,bus between a4 and b, and Prop.A11 implies that ecucnt5 is smaller than the correct counter value for this action which in turn is equal to or bigger than κ∧cnta5=k+1. Assume that between a4 and a5 there have been k′ send actions by members of ECUgC other than ECU1gC with correct counters, increasing its value to k+1+k′ without changing ECU1gC’s counter value (e.g. because it does not perform any action other than a5 between a4 and b). It follows ecucnt5<corCntgCa5,x=k+1+k′. On the other hand, in bECU1gC receives and accepts the message sent in σb with the counter cnt=k+1. So assuming ECU1gC’s loseCntgC action a5 to be its last action before b, Prop.A4 and Prop.A9 imply k+1=κ∧cntb=κ∧ecucntb≥κ∧prevcntb+1=ecucnt5. Both inequalities are satisfied for ecucnt5≤k+1−1=k. Thus ECU1gC may very well receive and accept the message sent in σb by ecu′∉ECUgC.The resulting sequence of actions is depicted in Table3. While it satisfies data origin authenticity, it violates immediacy, assuming that only the time period between writing a message onto the bus and reading it does not exceed the specified limit. It also violates non-repeatability as the message sent in a1 is accepted twice.Table 3
A first attack sequence.
a3action byECU1gCκ^ecucnta2=ka2action byecu1κ^ecucnta3=k⋮no actions byECU1gCandecu1⋮a1sendgC,ecu1,ecukey,ecucnt1,prevcnt1,bus,mackey,msgid,msg,cntecucnt4=cnt=k+1κ^ecucnta2+1=k+1=cnta4recvgC,ECU1gC,ecukey,ecucnt4,prevcnt4,bus,mackey,msgid,msg,cntecucnt4=cnt=k+1⋮a5loseCntgC,ECU1gC,ecucnt5,prevcnt5,busecucnt5<k+1+k′⋮no action byECU1gC⋮σbsendgC,ecu′,ecukey′,ecucnt′,prevcnt′,bus,mackey,msgid,msg,cntcnt=k+1brecvgC,ECU1gC,ecukey,ecucnt,prevcnt,bus,mackey,msgid,msg,cntecucnt=cnt=k+1It is not surprising that counter loss without timely synchronization opens up attack possibilities. The same result can be shown in caseecu1=FvM sends a synchronization message in a1. We then need to consider the fact that between a2 and a1, ECU2gC may have sent n messages that increase the correct counter of a1 accordingly. Further, instead of applying Prop.A8 we need to take into account that the counter is sent as the message’s payload, i.e. modeled by the parameter msg, and apply Prop.A5.We will now investigate whether sending of synchronization messages prohibits the above described attack. Assume therefore that with theloseCntgC action ECU1gC sets its local genCnt value to k′′<k+1+k′ and that between the loseCntgC action and b, ECU1gC receives one or more synchronization messages with a6 being the last one before b. Since cnt=k+1 is the counter accepted by ECU1gC in b and since the counter sent in a synchronization message is contained in its payload, κ∧msga6=msg6∈k″+1,k. Assume further these are the only messages sent on the bus. Then again by Prop.A4 and Prop.A7, cnt=k+1=κ∧cntb=κ∧ecucntb≥κ∧prevcntb+1=κ∧ecucnta6+1=κ∧msga6+1=msg6+1≥k″+2 which implies k″≤msg6−1≤k+1−2=k−1. According to Prop.A1, a6 is preceded by an action σa6 in which the synchronization message received by ECU1gC is written to the bus. The property further implies that between σa6 and a6, ECU1gC does not perform any further action, hence σa6 happens after ECU1gC’s loseCntgC action and in particular after a1. Recall now that we have assumed k to be the correct counter value of both a2 and a3 and that κ∧cnta1=k+1. If κ∧ecuσa6 was FvM, Prop.A6 would imply κ∧msgσa6≥k+1+1=k+2. Yet what ECU1gC accepts in a6 is msg6≤k+1−1=k. Thus κ∧ecuσa6≠FvM and since by Prop.A8 an honest agent other than FvM only sends functional messages, it follows κ∧ecuσa6=Eve.While by Prop.A3,a6 is preceded by an action a7≔sendgC,FvM,…,sync,…msg6,…, this does not necessarily interfere with the attack we are constructing here, assuming that ECU1gC does not receive (i.e. accept) this message but only performs a readgC action which does not change its local counter. This attack is illustrated in Table 4.Table 4
The second possible attack sequence.
a3action byECU1gCκ^ecucnta2=ka2action byecu1κ^ecucnta3=k⋮no actions byECU1gCandecu1⋮a1sendgC,ecu1,ecukey,ecucnt1,prevcnt1,bus,mackey,msgid,msg,cntecucnt1=prevent1+1=κ^ecucnta2+1=k+1=cnta4recvgC,ECU1gC,ecukey,ecucnt4,prevcnt4,bus,mackey,msgid,msg,cntecucnt4=cnt=k+1⋮a5loseCntgC,ECU1gC,ecucnt5,prevcnt5,busecucnt5<k+1+k′⋮a7sendgC,FvM,…,sync,…,msg6,…,a8readgC,ECU1gC,…,ecucnt8,prevcnt8,sync,…,msg6,…ecucnt8=prevcnt8=ecucnt5⋮σa6sendgC,Eve,…,sync,…,msg6,…,msg6∈k″+1,k+1−1a6recvgC,ECU1gC,ecukey,ecucnt6,prevcnt6,…,sync,…,msg6,…,ecucnt6=msg6≤k+1−1prevent6=ecucnt8=k″∧msg6≥k″+1σbsendgC,ecu′,ecukey′,ecucnt′,prevcnt′,bus,mackey,msgid,msg,cntcnt=k+1brecvgC,ECU1gC,ecukey,ecucnt,prevcnt,bus,mackey,msgid,msg,cntecucnt=cnt=k+1This attack uses an important characteristic of the generic counter systemGenCnt, captured in Prop.A10: It causes ECU1gC to keep the too small and thus incorrect counter since it does not correctly receive and accept the synchronization messages sent by FvM between a5 and b. The attack again violates immediacy and non-repeatability.


### 5.2.2. Not losing the counter

Let us now consider the case in whichECU1gC only performs readgC actions between a3 and b and in particular does not perform an action a4, i.e. does not receive and accept the message sent by ecu1 in a1. As above, by Prop.A1 and Prop.A3 we know κ∧cnta1=κ∧cntb=κ∧cntσb. Since by Prop.A10 a readgC action does not change ECU1gC’s counter, consecutive application of Prop.A4 to the sequence of these readgC actions implies κ∧prevcntb=κ∧ecucnta3 and by Prop.A9 it follows k+1=cnt=κ∧cntb=κ∧ecucntb≥κ∧prevcntb+1=κ∧ecucnta3+1=k+1. This equation is always satisfied which means that there is no contradiction to κ∧ecuσb=ecu′≠ecu1. Therefore this sequence (illustrated in Table 5) is another example for violation of immediacy based on invalidation and replay of messages. Note that it does not violate non-repeatability as the message is only received and accepted once.Table 5
The third possible attack sequence.
a3action byECU1gCκ^ecucnta2=ka2action byecu1κ^ecucnta3=k⋮onlyreadgCactions byECU1gC⋮a1sendgC,ecu1,ecukey,ecucnt1,prevcnt1,bus,mackey,msgid,msg,cntecucnt1=prevcnt1+1=κ^ecucnta2+1=k+1=cnt⋮onlyreadgCactions byECU1gC⋮σbsendgC,ecu′,ecukey′,ecucnt′,prevcnt′,bus,mackey,msgid,msg,cntcnt=k+1brecvgC,ECU1gC,ecukey,ecucnt,prevcnt,bus,mackey,msgid,msg,cntecucnt=cnt=prevcnt+1=κ^ecucnta2=k+1The only case in which the desired properties hold is if by performinga4, ECU1gC receives and accepts the message sent in a1 and does not lose the correct counter value, i.e. does not perform a loseCntgC action between a4 and b. In this case ECU1gC sets its local counter κ∧ecucnta4 to k+1 (Prop.A9) and without losing the correct counter will not accept the same counter in action b anymore, as κ∧prevcntb=κ∧ecucnta4=k+1 and thus κ∧cntb=k+1≯κ∧prevcntb=k+1 as is required by Prop.A9.Our proof indicating possible attacks is based on the fact that certain messages are not received but only read byECU1gC. This can easily be accomplished by an attacker with the abilities described in Section 2.2. All she has to do is to monitor the respective message and then invalidate it and all following ones related to the relevant counter by changing a CRC bit or overwriting the message with an error frame. This will cause all ECUs connected to the bus to reject the messages. Since readgC actions do not change the ECUs’ local counter, any message containing a bigger counter will still be considered correct.In Section7.1 we will discuss the results achieved by the proof and compare them to the formal proofs of the bus counter-based system to be introduced in the next section.


## 5.2.1. Losing the counter

Assume thatECU1gC receives the message sent by ecu1 in a1 by performing an action a4 (i.e. σa4=a1). Then κ∧cnta4=κ∧cnta1=k+1 (Prop.A1) and Prop.A9 implies κ∧ecucnta4=κ∧cnta4=k+1. Prop.A9 also requires κ∧ecucnta4≥κ∧prevcnta4+1. This is the case, as by Prop.A4 we can conclude κ∧prevcnta4=κ∧ecucnta3 and thus k+1=κ∧ecucnta4≥κ∧ecucnta3+1 which by the assumption of ECU1gC and ecu1 being synchronized before a1 is equal to κ∧ecucnta2+1=k+1, hence κ∧ecucnta4=k+1≥k+1 is satisfied. Since with action b, ECU1 receives and accepts cnt=k+1, Prop.A12 implies that ECU1gC performs an action a5≔loseCntgC,ECU1gC,ecucnt5,prevcnt5,bus between a4 and b, and Prop.A11 implies that ecucnt5 is smaller than the correct counter value for this action which in turn is equal to or bigger than κ∧cnta5=k+1. Assume that between a4 and a5 there have been k′ send actions by members of ECUgC other than ECU1gC with correct counters, increasing its value to k+1+k′ without changing ECU1gC’s counter value (e.g. because it does not perform any action other than a5 between a4 and b). It follows ecucnt5<corCntgCa5,x=k+1+k′. On the other hand, in bECU1gC receives and accepts the message sent in σb with the counter cnt=k+1. So assuming ECU1gC’s loseCntgC action a5 to be its last action before b, Prop.A4 and Prop.A9 imply k+1=κ∧cntb=κ∧ecucntb≥κ∧prevcntb+1=ecucnt5. Both inequalities are satisfied for ecucnt5≤k+1−1=k. Thus ECU1gC may very well receive and accept the message sent in σb by ecu′∉ECUgC.The resulting sequence of actions is depicted in Table3. While it satisfies data origin authenticity, it violates immediacy, assuming that only the time period between writing a message onto the bus and reading it does not exceed the specified limit. It also violates non-repeatability as the message sent in a1 is accepted twice.Table 3
A first attack sequence.
a3action byECU1gCκ^ecucnta2=ka2action byecu1κ^ecucnta3=k⋮no actions byECU1gCandecu1⋮a1sendgC,ecu1,ecukey,ecucnt1,prevcnt1,bus,mackey,msgid,msg,cntecucnt4=cnt=k+1κ^ecucnta2+1=k+1=cnta4recvgC,ECU1gC,ecukey,ecucnt4,prevcnt4,bus,mackey,msgid,msg,cntecucnt4=cnt=k+1⋮a5loseCntgC,ECU1gC,ecucnt5,prevcnt5,busecucnt5<k+1+k′⋮no action byECU1gC⋮σbsendgC,ecu′,ecukey′,ecucnt′,prevcnt′,bus,mackey,msgid,msg,cntcnt=k+1brecvgC,ECU1gC,ecukey,ecucnt,prevcnt,bus,mackey,msgid,msg,cntecucnt=cnt=k+1It is not surprising that counter loss without timely synchronization opens up attack possibilities. The same result can be shown in caseecu1=FvM sends a synchronization message in a1. We then need to consider the fact that between a2 and a1, ECU2gC may have sent n messages that increase the correct counter of a1 accordingly. Further, instead of applying Prop.A8 we need to take into account that the counter is sent as the message’s payload, i.e. modeled by the parameter msg, and apply Prop.A5.We will now investigate whether sending of synchronization messages prohibits the above described attack. Assume therefore that with theloseCntgC action ECU1gC sets its local genCnt value to k′′<k+1+k′ and that between the loseCntgC action and b, ECU1gC receives one or more synchronization messages with a6 being the last one before b. Since cnt=k+1 is the counter accepted by ECU1gC in b and since the counter sent in a synchronization message is contained in its payload, κ∧msga6=msg6∈k″+1,k. Assume further these are the only messages sent on the bus. Then again by Prop.A4 and Prop.A7, cnt=k+1=κ∧cntb=κ∧ecucntb≥κ∧prevcntb+1=κ∧ecucnta6+1=κ∧msga6+1=msg6+1≥k″+2 which implies k″≤msg6−1≤k+1−2=k−1. According to Prop.A1, a6 is preceded by an action σa6 in which the synchronization message received by ECU1gC is written to the bus. The property further implies that between σa6 and a6, ECU1gC does not perform any further action, hence σa6 happens after ECU1gC’s loseCntgC action and in particular after a1. Recall now that we have assumed k to be the correct counter value of both a2 and a3 and that κ∧cnta1=k+1. If κ∧ecuσa6 was FvM, Prop.A6 would imply κ∧msgσa6≥k+1+1=k+2. Yet what ECU1gC accepts in a6 is msg6≤k+1−1=k. Thus κ∧ecuσa6≠FvM and since by Prop.A8 an honest agent other than FvM only sends functional messages, it follows κ∧ecuσa6=Eve.While by Prop.A3,a6 is preceded by an action a7≔sendgC,FvM,…,sync,…msg6,…, this does not necessarily interfere with the attack we are constructing here, assuming that ECU1gC does not receive (i.e. accept) this message but only performs a readgC action which does not change its local counter. This attack is illustrated in Table 4.Table 4
The second possible attack sequence.
a3action byECU1gCκ^ecucnta2=ka2action byecu1κ^ecucnta3=k⋮no actions byECU1gCandecu1⋮a1sendgC,ecu1,ecukey,ecucnt1,prevcnt1,bus,mackey,msgid,msg,cntecucnt1=prevent1+1=κ^ecucnta2+1=k+1=cnta4recvgC,ECU1gC,ecukey,ecucnt4,prevcnt4,bus,mackey,msgid,msg,cntecucnt4=cnt=k+1⋮a5loseCntgC,ECU1gC,ecucnt5,prevcnt5,busecucnt5<k+1+k′⋮a7sendgC,FvM,…,sync,…,msg6,…,a8readgC,ECU1gC,…,ecucnt8,prevcnt8,sync,…,msg6,…ecucnt8=prevcnt8=ecucnt5⋮σa6sendgC,Eve,…,sync,…,msg6,…,msg6∈k″+1,k+1−1a6recvgC,ECU1gC,ecukey,ecucnt6,prevcnt6,…,sync,…,msg6,…,ecucnt6=msg6≤k+1−1prevent6=ecucnt8=k″∧msg6≥k″+1σbsendgC,ecu′,ecukey′,ecucnt′,prevcnt′,bus,mackey,msgid,msg,cntcnt=k+1brecvgC,ECU1gC,ecukey,ecucnt,prevcnt,bus,mackey,msgid,msg,cntecucnt=cnt=k+1This attack uses an important characteristic of the generic counter systemGenCnt, captured in Prop.A10: It causes ECU1gC to keep the too small and thus incorrect counter since it does not correctly receive and accept the synchronization messages sent by FvM between a5 and b. The attack again violates immediacy and non-repeatability.


## 5.2.2. Not losing the counter

Let us now consider the case in whichECU1gC only performs readgC actions between a3 and b and in particular does not perform an action a4, i.e. does not receive and accept the message sent by ecu1 in a1. As above, by Prop.A1 and Prop.A3 we know κ∧cnta1=κ∧cntb=κ∧cntσb. Since by Prop.A10 a readgC action does not change ECU1gC’s counter, consecutive application of Prop.A4 to the sequence of these readgC actions implies κ∧prevcntb=κ∧ecucnta3 and by Prop.A9 it follows k+1=cnt=κ∧cntb=κ∧ecucntb≥κ∧prevcntb+1=κ∧ecucnta3+1=k+1. This equation is always satisfied which means that there is no contradiction to κ∧ecuσb=ecu′≠ecu1. Therefore this sequence (illustrated in Table 5) is another example for violation of immediacy based on invalidation and replay of messages. Note that it does not violate non-repeatability as the message is only received and accepted once.Table 5
The third possible attack sequence.
a3action byECU1gCκ^ecucnta2=ka2action byecu1κ^ecucnta3=k⋮onlyreadgCactions byECU1gC⋮a1sendgC,ecu1,ecukey,ecucnt1,prevcnt1,bus,mackey,msgid,msg,cntecucnt1=prevcnt1+1=κ^ecucnta2+1=k+1=cnt⋮onlyreadgCactions byECU1gC⋮σbsendgC,ecu′,ecukey′,ecucnt′,prevcnt′,bus,mackey,msgid,msg,cntcnt=k+1brecvgC,ECU1gC,ecukey,ecucnt,prevcnt,bus,mackey,msgid,msg,cntecucnt=cnt=prevcnt+1=κ^ecucnta2=k+1The only case in which the desired properties hold is if by performinga4, ECU1gC receives and accepts the message sent in a1 and does not lose the correct counter value, i.e. does not perform a loseCntgC action between a4 and b. In this case ECU1gC sets its local counter κ∧ecucnta4 to k+1 (Prop.A9) and without losing the correct counter will not accept the same counter in action b anymore, as κ∧prevcntb=κ∧ecucnta4=k+1 and thus κ∧cntb=k+1≯κ∧prevcntb=k+1 as is required by Prop.A9.Our proof indicating possible attacks is based on the fact that certain messages are not received but only read byECU1gC. This can easily be accomplished by an attacker with the abilities described in Section 2.2. All she has to do is to monitor the respective message and then invalidate it and all following ones related to the relevant counter by changing a CRC bit or overwriting the message with an error frame. This will cause all ECUs connected to the bus to reject the messages. Since readgC actions do not change the ECUs’ local counter, any message containing a bigger counter will still be considered correct.In Section7.1 we will discuss the results achieved by the proof and compare them to the formal proofs of the bus counter-based system to be introduced in the next section.


## 6. Formalization and Verification of BusCount

In this section, we introduce the formal model and verification of our hardware-based counter approach.


### 6.1. The Formal Bus Counter Model

We model the bus counter-based system (denoted byBusCnt henceforth) as similar as possible to the generic counter model. One important difference is that it does not need a central freshness value master since all ECUs send synchronization messages simultaneously. Hence the set of agents is defined as ℙbCnt=ECUbC∪Eve with ECUbC≔ECU1bC,ECU2bC,ECU3bC.As inGenCnt, the BusCnt system has only one bus bus=bus all agents are being connected to. Further, members of ECUbC are honest and own the key key, while Eve, not being member of this group, does not own this key. We use the same set of action parameters, but a different specification of agents’ behavior (after all, we model a different system). The set of actions ΣbCnt is defined as follows:(i)
sendbC,ecu,ecukey,ecucnt,prevcnt,bus,mackey,msgid,msg,cnt denotes a send action as described in Section 5.1.1, except that the counter value cnt is covered by the MAC but not transmitted. As in the GenCnt model, the message may be altered (by a technical error or by Eve) after having been sent and may thus only cause a readbC action (see below).(ii)
readbC,ecu,ecukey,ecucnt,prevcnt,bust,mackey,msgid,msg,cnt denotes agent ecu∈ℙbCnt reading a message without processing it afterwards. In contrast to the respective readgC action of the GenCnt model, the readbC action of the BusCnt model changes the state of an ecu being member of ECUbC by decrementing its local bCnt value (stored with the last action and thus modeled by the parameter prevcnt) (see Prop.B13 in Section 6.1.1 below). This captures the fact that ecu reacts to the “start of message” bit on bus but discards the respective message (e.g. because the CRC verification fails) in which case it does not perform the receive action. Note that the sender of a message always reads its own action bey performing a readbC action.(iii)
recvbC,ecu,ecukey,ecucnt,prevcnt,bus,mackey,msgid,msg,cnt denotes the successful reception and processing of a message by ecu∈ℙbCnt.(iv)
As in theGenCnt system, with loseCntbC,ecu,ecucnt,prevcnt,bus we model the fact that ecu∈ℙbCnt has lost the correct counter value for some reason and thus is no longer synchronized. Since in the BusCnt system counter values decrease, its counter is set to a value bigger than the correct counter value (see Section 6.1.1 for more details).


#### 6.1.1. Agents’ Local View and Initial Knowledge

Again, the agents’ local view is defined analogously to the generic counter model: All agents see their own actions completely and see the messages sent on the CAN bus they are connected to but cannot see who sent them nor the values of parameters stored locally by the sender. Further, agents cannot see actionsreadbC,recvbC and loseCntbC performed by other agents.As already pointed out in Section 5.1.3, with specifying the agents’ initial knowledge we capture the characteristics of our system. In the following, we list all properties we assume to be satisfied by the agents’ initial knowledgeWbCnt with reference to the respective property in Section 5.1.3 (if any) in which case we omit the formalization. Analogously to Section 5.1.3, if not specified otherwise, the properties refer to ω∈WbCnt. We denote the correct counter for a specific action a in ω by corCntbCa,ω. In Lemma 2 (see Section 6.2) we will show how its value is determined.Prop.
B1 (analogous to first statement of Prop.A1). A readbC and recvbC action, respectively, on bus is always preceded by the corresponding send action that writes the message onto the bus. Obviously, the parameter values of mackey,msgid,msg and cnt in b and σb are identical (we forgo the formalization of the latter statement).
For allb∈ΣbCnt with κ∧aname∈readbC,recvbC holds precWbCntσb,b.Prop.
B2 (Prop.A2). Only members of ECUbC own and can use key=key. Since Eve does not own this key and honest ECUs use only key to generate and verify a MAC, the MAC key contained in a send or receive action being equal to key=key is equivalent to the ECU being member of ECUbC.Prop.
B3 (Prop.A3). A recvbC action performed by an honest ECU (i.e. a member of ECUbC) must be preceded by the respective send action of an agent having generated the MAC, i.e. owning the key used for MAC generation. Again, obviously, the parameter values of mackey,msgid,msg and cnt in b and σb are identical.Prop.
B4 (Prop.A4). The parameter prevcnt of an action performed by an honest ECU denotes the local bCnt value as result of the ECU’s previous action. For the very first action of an ECU it is defined as the maximal value of bCnt, denoted by bCntmax. Formally:
∀a∈alphω:κ∧prevcnta=κ∧ecucntprevacta,κ∧ecua,ω. If for all ai∈ω with actCntai,ω<actCnta,ω holds κ∧ecuai≠κ∧ecua, it follows κ∧prevcnta=bCntmax.Prop.
B5. In Section 7.2.2 we will discuss which starting value of bCnt to choose in order to avoid counter overflow. Further, as explained in Section 2.2, we assume that memory failures and attacks cannot cause counter overflow. Hence we can assume that such a failure never results into a local counter value stored by an ECU being smaller than the correct one (see Prop.B17 below). For our formal model we assume that the local counter value of ECUs is always sufficiently large such that counter decrementation can result into the value 0 only in the last phase class of an action sequence. Formally:
∀a∈alphω:κ∧prevcnta>0Prop.
B6 (analog to Prop.A8). When an honest ECU sends a synchronization message, it includes as its message payload the local bCnt value of its previous action decremented by 1 but does not change the local bCnt value.
∀a∈alphω:κ∧anamea=sendbC∧κ∧ecua∈ECUbC∧κ∧msgida=sync⇒κ∧msga=κ∧prevcnta−1∧κ∧ecucnta=κ∧prevcnta.Prop.
B7. We assume that there always exists an ECU owning the correct counter value. Since our synchronization concept utilizes the mechanism used for collision resolving (a 0 written to the CAN bus always overwrites a 1), the correct counter always overwrites any incorrect one. Therefore a sendbC action containing a synchronization message that is actually performed by an honest ECU always contains the correct counter. Formally:
a∈alphω∧κ∧anamea=sendbC∧κ∧ecua∈ECUbC∧κ∧msgida=sync⇒κ∧msga=corCntbCa,ω.Prop.
B8. When monitoring a synchronization message being written to the bus, an honest ECU decrements its previously used counter value by 1 and verifies that the result is less or equal to the counter sent as the message’s payload. The error frame parameter being equal to no indicates that this check has been successful (and that the MAC check that we do not formalize explicitly has been successful as well). It then uses this value as its new local counter.
∀a∈alphω:κ∧anamea∈readbC,recvbC∧κ∧ecua∈ECUbC∧κ∧msgida=sync∧κ∧errorFramea=no⇒κ∧ecucnta=κ∧msga≤κ∧prevcnta−1.
Whilea is actually a recvbC action, our proofs do not depend on distinguishing between readbC and recvbC actions of synchronization messages.Prop.
B9 (analog to Prop.A8). When an honest ECU sends a functional message, it includes as its counter value the local bCnt value of its previous action decremented by 1 but does not change the local bCnt value. (It changes the value of ecucnt with the action of reading its own message that the ECU performs simultaneously to sending, see Prop.B10 and Prop.B13.)
∀a∈alphω:κ∧anamea=sendbC∧κ∧ecua∈ECUbC∧κ∧msgida=fmsg⇒κ∧cnta=κ∧prevcnta−1∧κ∧ecucnta=κ∧prevcnta.Prop.
B10 (analog to Prop.A9). When an honest ECU receives and accepts a functional message, it decrements its previously used counter value by 1 and verifies that the message’s cnt value is equal to the result. It then sets its local bCnt value ecucnt to the message’s counter.
∀a∈alphω:κ∧anamea=recvbC∧κ∧ecua∈ECUbC∧κ∧msgida=fmsg⇒κ∧ecucnta=κ∧cnta=κ∧prevcnta−1.Prop.
B11. All honest ECUs, when reading a message, check the message’s MAC, independently of whether or not they accept it. In case of a functional message, this involves the ECU’s local counter, more concretely the counter value used by the ECU in its previous action decremented by 1. If such a check succeeds which is a necessary condition for the error frame being set to no, this value is the one that was used to generate the message’s MAC. Note that this assumes that an attacker that owns the correct counter and a MAC cannot guess the corresponding message.
Lets∈alphω with κ∧anames=sendbC and v∈Φs,WbCnt. Then the following holds:
∀b∈a∈alphv|κ∧anamea∈readbC,recvbC∧κ∧ecua∈ECUbC∧κ∧msgida=fmsg:κ∧errorFrameb=no⇒κ∧cntb=κ∧ecucntb=κ∧prevcnta−1.
Note that in our very simple model with only one type of functional message, a successful check indicated byerrorFrame=no actually results into a recvbC action. However, considering also readbC actions with errorFrame=no allows to extend the model with respect to more types of functional messages without having to change the assumptions.Prop.
B12. As explained in Section 3, if an ECU’s checks concerning for example a message’s MAC fails and it therefore writes an error-frame, all other ECUs join in and write an error-frame as well, no matter whether or not their checks failed. Hence all readbC and recvbC actions induced by a specific sendbC action have the same value for the parameter errorFrame. Since a message is only received and accepted if all checks have been successful, the error frame of a recvbC action is always set to no. Formally:
Lets∈alphω with κ∧anames=sendbC and v∈Φs,WbCnt. Let further Rv≔b∈alphv|κ∧anameb∈readbC,recvbC denote the readbC and recvbC actions in v. Then for all bi,bj∈Rv the following holds:
κ∧errorFramebi=κ∧errorFramebjandκ∧anamebi=recvbC⇒κ∧errorFramebi=no.Prop.
B13 (in contrast to Prop.A10). When an honest ECU reads a message, it always decrements its previously used bCnt value by 1 and uses the result as its new local bCnt value. This behavior is independent of whether or not its checks fail, i.e. independent of the errorFrame value. Formally:
∀a∈alphω:κ∧anamea=readbC∧κ∧ecua∈ECUbC⇒κ∧ecucnta=κ∧prevcnta−1.Prop.
B14. In a phase class Φs,WbCnt with κ∧anames=sendbC (i.e. a phase class that starts with a specific sendbC action and ends with the next sendbC action, see Definition 9), all honest ECUs including the sender either read or receive the message or perform a loseCnt action. They do not perform any other action.
Lets∈ΣbCnt with κ∧anames=sendbC and v maximal in Φs,WbCnt. Then for all ecu∈ECUbC exists exactly one c∈alphv such that κ∧ecuc=ecu and κ∧anamec∈readbC,recvbC,loseCntbC.Prop.
B15 (analog to Prop.A6). In every phase class Φs,WbCnt with κ∧anames=sendbC there is an honest ECU owning the correct counter and performing a read or recvbC action in this phase class, but no loseCnt action. Here, owning the correct counter means that the ECU has used and stored the correct counter value in its previous action and can thus use it in the next action.
Lets∈alphω with κ∧anames=sendbC. Then for all v maximal in Φs,WbCnt exists an action b∈alphv with κ∧anameb∈read,recv,ECU∗s≔κ∧ecub∈ECUbC and κ∧prevcntb=corCntbCb,ω+1.Prop.
B16 (analog to Prop.A12). If an ECU is not synchronized at a specific action, i.e. does not use the correct counter relevant for this action, it must have performed an action loseCntbC before. Note that using a counter value refers to the parameter prevcnt.
∀a∈alphω:κ∧prevcnta−1≠corCntbCa,ω⇒∃a′∈alphω:κ∧anamea′=loseCntbC∧κ∧ecua′=κ∧ecua∧actCnta′,ω<actCnta,ωProp.
B17 (analog to Prop.A11). As explained in Prop.B5, memory failures never result into decrease of the counter value stored by an ECU. This implies that an action loseCntbC performed by an honest ECU resets the ECU’s counter to a value bigger than the correct one. For formal reasons we assign a counter value higher than the maximal value the system starts with to a loseCnt action if it is the first action of an action sequence.
∀a∈alphω:(1)
a≠pre1ω∧κ∧anamea=loseCnt∧κ∧ecua∈ECUbC⇒κ∧ecucnta>corCntbCa,ω.(2)
a=pre1ω∧κ∧anamea=loseCnt∧κ∧ecua∈ECUbC⇒κ∧ecucnta=bCntmax+1
Analogously to Section5.1.2 we model immediacy and non-repeatability by the phase class Φσb,WbCnt as defined in Definition 9 determined by a fixed but arbitrary recvbC action b. In the following section we will show that BusCnt satisfies both properties.


### 6.2. Formal Proof of bCnt System

The idea of theBusCnt system is that counter values included in the MACs of sent messages are strictly monotonically decreasing (instead of strictly monotonically increasing as in the GenCnt system). However, in contrast to the GenCnt system, in BusCnt each send action inevitably induces a readbC or recvbC action and thus a decrement of the counter, no matter whether or not a check failed. In case a system does not suffer any anomalies (i.e. all actors act correctly and counter value change is never caused by physical irregularities), the counter used by the ECUs is always the correct one. Lemma 2 will show how it is determined. For its proof we need the following technical Lemma:Lemma 1.
Letω∈WbCntcor≔ω∈WbCnt|κ∧ecua∈ECUbC∧κ∧anamea≠loseCnt for all a∈alphω. Let furtherSω≔a∈alphω|κ∧anamea=sendbCwithactCntsi,ω<actCntsi+k,ωfor allsi,si+k∈Sωi,k∈ℕ. Then for allb∈alphωwithκ∧anameb∈readbC,recvbCthe following holds:1.
κ∧msgidb=fmsg⇒κ∧ecucntb=κ∧cntb2.
κ∧msgidb=sync⇒κ∧ecucntb=κ∧msgbProof 2.
Ifκ∧anameb=recvbC, the assertions follow directly by Prop.B10 and Prop.B12 together with Prop.B8, respectively. Let now κ∧anameb=readbC. We show the assertions of this case by induction over the number of consecutive phase classes Φsi,WbCntcor.Induction basis:i=1. Consider v∈Φs1,WbCntcor and b∈alphv. Let κ∧msgidb=fmsg and assume κ∧ecus1=κ∧ecub. Then Prop.B13 and Prop.B4 imply κ∧ecucntb=κ∧prevcntb−1=κ∧ecucnts1−1. Further, by Prop.B1, κ∧cntb=κ∧cnts1. Now by Prop.B9, κ∧cnts1=κ∧prevcnts1−1=κ∧ecucnts1−1. Together this leads to κ∧cntb=κ∧ecucnts1−1=κ∧ecucntb.
Assume nowκ∧ecub≠κ∧ecus1. Since Prop.B1 requires a send action before any readbC or recvbC action and since s1 is the first send action in ω, there is no other action in ω before s1. Prop.B14 implies that b is the first κ∧ecub∈Ωκ∧prevcntb=bCntmax and thus Prop.B13 implies κ∧ecucntb=κ∧prevcntb−1=bCntmax−1. s1 being the first action in ω, it is the first action of κ∧ecus1 as well and Prop.B4 implies κ∧prevcnts1=bCntmax. By Prop.B9 it follows κ∧cnts1=κ∧prevcnts1−1=bCntmax−1. Further, by Prop.B1, κ∧cntb=κ∧cnts1. Together we can conclude κ∧cnts1=κ∧cnts1=bCntmax−1=κ∧ecucntb.
In caseκ∧msgidb=sync, we can argue analogously by replacing every occurrence of κ∧cnt by κ∧msg and applying Prop.B6 instead of Prop.B9.
Induction hypothesis: For v∈Φsi,WbCntcor and b∈alphv, let assertions 1 and 2 hold.
Induction step: Consider v∈Φsi+1,WbCntcor,b∈alphv with κ∧anameb∈readbC,recvbC and κ∧msgidb=fmsg. First we again assume κ∧ecub=κ∧ecusi+1. b being a readbC action, Prop.B13 implies κ∧ecucntb=κ∧prevcntb−1 which by Prop.B4 and Prop.B14 is equal to κ∧ecucntsi+1−1. Further, by Prop.B9, κ∧cntsi+1=κ∧prevcntsi+1−1 and κ∧ecucntsi+1=κ∧prevcntsi+1. Since Prop.B1 implies κ∧cntsi+1=κ∧cntsi+1, it follows κ∧cntb=κ∧prevcntsi+1−1=κ∧ecucntsi+1−1=κ∧ecucntb.
Assume nowκ∧ecub≠κ∧ecusi+1. As above, Prop.B13 implies κ∧ecucntb=κ∧prevcntb−1. Since by Prop.B14 all ECUs perform a readbC or recvbC action in the previous phase class Φsi,WbCntcor (loseCntbC actions are excluded by definition), this holds in particular for κ∧ecub and κ∧ecusi+1. Hence for all maximal v′ in Φsi,WbCntcor there exist readbC or recvbC actions b′∈alphv′ performed by κ∧ecub and a∈alphv′ performed by κ∧ecusi+1, being the previous actions of κ∧ecub and κ∧ecusi+1, respectively. Prop.B4 implies κ∧ecucntb=κ∧prevcntb−1=κ∧ecucntb′−1 which by induction hypothesis is equal to κ∧cntb′−1. This in turn is equal to κ∧cntsi−1=κ∧cnta−1 by Prop.B1. Again by induction hypothesis, the latter expression is equal to κ∧ecucnta−1. Prop.B4 implies equality to κ∧prevcntsi+1−1 which by Prop.B9 is equal to κ∧cntsi+1. Prop.B1 finally implies equality to κ∧cntb, hence κ∧cntb=κ∧ecucntb.
Again, in caseκ∧msgidb=sync, the analogous proof is achieved by replacing every occurrence of κ∧cnt by κ∧msg and applying Prop.B6 instead of Prop.B9.Lemma 2.
LetWbCntcorandSωas defined in Lemma 1. Let furtherω∈WbCntcoranda∈alphω. Then the following holds:1.
κ∧msgida=fmsg⇒κ∧cnta=bCntmax−cards∈Sω|actCnts,ω≤actCnta,ω≥02.
κ∧msgida=sync⇒κ∧msga=bCntmax−cards∈Sω|actCnts,ω≤actCnta,ω≥0
Further, for allsi−1,si∈Sω(i.e. withactCntsi−1,ω<actCntsi,ωandi∈ℕ,i≥2holds(i)
κ∧msgidsi−1=κ∧msgidsi=fmsg⇒κ∧cntsi=κ∧cntsi−1−1(ii)
κ∧msgidsi−1=κ∧msgidsi=sync⇒κ∧msgsi=κ∧msgsi−1−1(iii)
κ∧msgidsi−1=fmsg∧κ∧msgidsi=sync⇒κ∧msgsi=κ∧cntsi−1−1(iv)
κ∧msgidsi−1=sync∧κ∧msgidsi=fmsg⇒κ∧cntsi=κ∧msgsi−1−1Note that item 1 implies that the parametercnt of actions concerning a functional message never reaches the value 0 unless there occur no more sendbC actions after the action a. The analogous statement holds for the parameter msg of actions concerning synchronization messages.Proof 3.
We prove assertions 1 and 2 by induction over the lengthl∈ℕ of a word ω∈WbCntcor.Induction basis:l=1, i.e. ω=a1. Since Prop.B1 requires a sendbC action before any readbC or recvbC action, a1 cannot be a readbC or recvbC action. Since further by definition ω does not contain any loseCnt action, κ∧anamea1=sendbC. Prop.B4 implies κ∧prevcnta1=bCntmax. If κ∧msgida1=fmsg, by Prop.B9 it follows κ∧cnta1=κ∧prevcnta1−1=bCntmax−1=bCntmax−cards∈Sa1|actCnts,a1≤actCnta1,a1. Further, by Prop.B5 κ∧prevcnta1=bCntmax>0 which implies κ∧prevcnta1−1=bCntmax−1≥0. Thus item 1 holds for ω=a1 containing a functional message. If on the other hand κ∧msgida1=sync, by Prop.B6 it follows κ∧msga1=κ∧prevcnta1−1 which as above implies the assertion, thus item 2 holds for ω=a1.Induction hypothesis: Let ωi=a1…aii≥2,i∈ℕ. Then for all a∈alphωi holds:(1)
κ∧msgida=fmsg⇒κ∧cnta=bCntmax−cards∈Sωi|actCnts,ωi≤actCnta,ωi≥0(2)
κ∧msgida=sync⇒κ∧msga=bCntmax−cards∈Sωi|actCnts,ωi≤actCnta,ωi≥0Induction step: Consider ωi+1≔a1…aiai+1.(1) Assumeκ∧anameai+1=sendbC. By Prop.B14 and the fact that ωi+1 does not contain any loseCntbC actions, it follows that ai is a recvbC or readbC action. This in turn is preceded by a sendbC action σai (see Prop.B1). So we have ωi+1=a1…σai…aiai+1 (σai may or may not be equal to a1). Let vi a maximal word in Φσai,WbCntcor, i.e. vi starts with σai and ends with ai+1, and all other actions in between are readbC and recvbC actions, the last one being ai. By Prop.B1, for all these readbC and recvbC actions b∈alphvi holds κ∧cntb=κ∧cntσai=κ∧cntai. Since all ECUs perform exactly one readbC or recvbC action in vi, there is exactly one recvbC or readbC action b∗∈alphvi performed by ecu∗≔κ∧ecuai+1, being the last action performed by ecu∗ before ai+1.(a)
Assumeκ∧msgidai+1=fmsg. If κ∧msgidb∗=fmsg as well, Lemma 1 implies κ∧ecucntb∗=κ∧cntb∗. Since ai+1 contains a functional message, Prop.B9 implies κ∧cntai+1=κ∧prevcntai+1−1=κ∧ecucntb∗−1=κ∧cntb∗−1. By Prop.B1 this is equal to κ∧cntσai−1=κ∧cntai−1. Prop.B1 also implies κ∧msgidai=κ∧msgidb∗=fmsg, hence by induction hypothesis it follows κ∧cntai+1=κ∧cntai−1=bCntmax−cards∈Sωi+1|actCnts,ωi+1≤actCntai,ωi+1−1. Finally, since ai+1 is the sendbC action directly following ai, κ∧cntai+1=bCntmax−cards∈Sωi+1|actCnts,ωi+1≤actCntai+1,ωi+1. Further, since κ∧cntai+1=κ∧prevcntai+1−1 and by Prop.B5 κ∧prevcntai+1>0, it follows κ∧cntai+1≥0.If on the other handκ∧msgidb∗=sync, Lemma 1 implies κ∧ecucntb∗=κ∧msgb∗. Using Prop.B9, we can then deduce κ∧cntai+1=κ∧ecucntb∗−1=κ∧msgb∗−1 which by Prop.B1 is equal to κ∧msgai−1. As above, the assertion follows.
(b)
Assumeκ∧msgidai+1=sync. In this case we can use Prop.B6 to deduce κ∧msgai+1=κ∧prevcntai+1−1. If κ∧msgidb∗=fmsg, the rest of the proof is identical to the case where this is combined with a functional message of ai+1, if κ∧msgidb∗=sync, the arguments regarding ai+1 being a synchronization message apply. This ends the proof for the case κ∧anameai+1=sendbC.(2)
Assumeκ∧anameai+1∈readbC,recvbC. Then Prop.B1 implies that there is an action σai+1 which is either equal to ai or occurs before ai.(a) Letσai+1=ai. By Prop.B1 it follows κ∧cntai+1=κ∧cntai,κ∧msgai+1=κ∧msgai and κ∧msgidai+1=κ∧msgidai. Since ai is the last send action before the recvbC/readbC action ai+1, the number of send actions before these two actions including ai is identical, i.e. cards∈Sωi+1|actCnts,ωi+1≤actCntai,ωi+1=cards∈Sωi+1|actCnts,ωi+1≤actCntai+1,ωi+1. If κ∧msgidai=fmsg, the induction hypothesis implies 0≤κ∧cntai=bCntmax−cards∈Sωi+1|actCnts,ωi+1≤actCntai,ωi+1=bCntmax−cards∈Sωi+1|actCnts,ωi+1≤actCntai+1,ωi+1=κ∧cntai+1. If κ∧msgidai=sync, the induction hypothesis implies 0≤κ∧msgai=bCntmax−cards∈Sωi+1|actCnts,ωi+1≤actCntai,ωi+1=bCntmax−cards∈Sωi+1|actCnts,ωi+1≤actCntai+1,ωi+1=κ∧msgai+1.(b) Letσai+1=:a′ with actCnta′,ωi+1>actCntai,ωi+1. Then Prop.B14 and the fact that ωi+1 does not contain any loseCntbC actions implies that ai is a readbC or recvbC action. Again, by Prop.B1 it follows κ∧cntai=κ∧cntσai=κ∧cntσai+1=κ∧cntai+1 and the equivalent equations for the parameters msg and msgid. Now we can again conclude that the number of send actions before ai is identical to those before ai+1 and as above, by induction hypothesis for the cases κ∧msgidai=fmsgid and κ∧msgidai=sync, respectively, it follows the assertion. This concludes the proof of assertions 1 and 2.
We now prove assertions (i)–(iv) of the Lemma. So assume the first statement holds regarding functional messages. Then it holds in particular for two consecutivesendbC actions si−1 and si in a word ω∈WbCntcor, each sending a functional message. Then κ∧cntsi=bCntmax−cards∈Sω|actCnts,ω≤actCntsi,ω=bCntmax−cards∈Sω|actCnts,ω≤actCntsi−1,ω+1=bCntmax−cards∈Sω|actCnts,ω≤actCntsi−1,ω−1=κ∧cntsi−1−1. The only difference between a sendbC action s containing a synchronization message and one containing a functional message is that the value bCntmax minus the cardinality of sendbC actions happening before s and including s is assigned to the counter of s in the first case and to the message of s in the second case. Hence, the respective statements for all other combinations of synchronization and functional sendbC actions can be shown analogously.The above Lemma uses properties that describe the behavior of honest agents when sending, receiving or reading a message and shows the resulting counter value. This behavior does not depend on whether or not any involved send action is performed by an honest ECU. Hence the counter value included in actions of sequences inWbCntcor can be considered the correct one for actions in WbCnt.Definition 10.
Forω∈WbCntanda∈alphωwe define(9)corCntbCa,ω≔bCntmax−cards∈Sω|actCnts,ω≤actCnta,ω.
We now considerWbCnt again and first show a Lemma whose important statement is that a synchronization message received by an ECU never contains a counter smaller than the correct one for this action. In general the Lemma states that an honest ECU owning the correct counter before processing a readbC or recvbC action (denoted by the parameter prevcnt of the action), also owns the correct counter afterwards (denoted by the parameter ecucnt).Lemma 3.
Letω∈WbCntanda∈alphω. Then the following holds:(10)κ∧anamea∈readbC,recvbC∧κ∧prevcnta=corCntbCa,ω+1⇒κ∧ecucnta=corCntbCa,ω.Proof 4.
Assumeκ∧anamea=readbC. Then by Prop.B13 κ∧ecucnta=κ∧prevcnta−1=corCntbCa,ω+1−1=corCntbCa,ω. The same follows by Prop.B10 for a being a recvbC action of a functional message. So let κ∧anamea=recvbC and κ∧msgida=sync. Prop.B12 implies κ∧errorFramea=no and thus by Prop.B8 it follows κ∧ecucnta≤κ∧prevcnta−1=corCntbCa,ω+1−1. In case of κ∧ecucnta=κ∧prevcnta−1 the assertion holds. So let κ∧ecucnta<κ∧prevcnta−1, i.e. κ∧ecucnta<corCntbCa,ω. Prop.B16 implies that before a, κ∧ecua performs a loseCnt action a′ and by Prop.B17, if a′≠pre1ω, it follows κ∧ecucnta′>corCntbCa′,ω. For simplicity we assume that a′ is the last action of κ∧ecua in ω before a. By Prop.B14, every ECU performs only one action per phase class, hence a′ happens in the phase class Φs′,WbCnt that ends with σa, i.e. in the phase class directly occuring before the one including a. Lemma 2 implies that corCntbCa′,ω=corCntbCa,ω+1. So we have corCntbCa,ω+1=κ∧prevcnta=κ∧ecucnta′>corCntbCa′,ω=corCntbCa,ω+1. This constitutes a contradiction, hence κ∧ecucnta=corCntbCa,ω holds. In case a′ is not the previous action of κ∧ecua, we can argue analogously.
Leta′=pre1ω. Since a′ is the first action and not a sendbC action, Lemma 2 implies corCntbCa′,ω=bCntmax. As above, we have corCntbCa,ω+1=κ∧prevcnta=κ∧ecucnta′ which by Prop.B17 is equal to bCntmax+1=corCntbCa′,ω+1. This implies corCntbCa,ω=corCntbCa′,ω. However, since σa happens before the recvbC action a (and after the loseCntbC action a′), by Lemma 2corCntbCa=bCntmax−1≠bCntmax=corCntbCa′,ω. So again this constitutes a contradiction, hence κ∧ecucnta=corCntbCa,ω always holds.We can now prove our main Theorem. As in Section5.2, the property we want to prove is that whenever an honest ECU receives and accepts a message (action b), the sendbC action σb having triggered b and starting the phase class determined by b must have authentically for the ECU been performed by an agent being member of the same group, and the message must contain the correct counter. In contrast to the proof regarding the GenCnt system, for the BusCnt system (formally denoted by BbCnt) we can show that this property is always satisfied, i.e. that both immediacy and non-repeatability hold.Theorem 2.
Letω∈BbCntandb≔recvbC,ecu,ecukey,ecucnt,prevcnt,bus,mackey,msgid,msg,cnt∈alphωwithecu∈ECUbC. Then the following property holds:(11)authWiPhasesend,ecu′,ecukey′,ecucnt′,prevcnt′,bus,mackey,msgid,msg,cnt|ecu′∈ECUbC,b,ecu,Φσb,WbCnt.Proof 5.
Analogously to Section5.2, without loss of generality we assume ECU1bC∈ECUbC to perform a receive action b≔recvbC,ECU1bC,ecukey,ecucnt,prevcnt,bus,mackey,msgid,msg,cnt∈alphω and consider an arbitrary x∈λECU1bC−1λECU1bCω∩WbCnt (which by definition of λECU1bC and BbCnt⊆WbCnt contains b). Since ECU1bC∈ECUbC, by Prop.B2 it follows mackey=key=ecukey. Further, by Prop.B3 there is an action a1≔sendbC,ecu1,ecukey1,ecucnt1,prevcnt1,bus,mackey,msgid,msg,cnt∈alphx before the receive action b by ECU1bC containing the same message ID, message and counter value and with ecukey1=mackey. Again by Prop.B2 it follows ecu1∈ECUbC which proves that the message received in b has authentically for ECU1bC been generated and sent by a member of ECUbC.
Further, by Prop.B1 the receive actionb by ECU1bC is preceded by a send action σb=sendbC,ecu′,ecukey′,ecucnt′,prevcnt′,bus,mackey,msgid,msg,cnt triggering b.
Letv maximal in Φσb,WbCnt with b∈alphv. Since κ∧anameb=recvbC, Prop.B12 implies κ∧errorFrameb=no and thus κ∧errorFramec=no for all c∈alphv with κ∧anamec∈readbC,recvbC. By Prop.B15 one of the actions readbC,recvbC in v is performed by an ECU owning the correct counter, i.e. there exists c∗∈alphv with κ∧anamec∗∈readbC,recvbC,ECU∗σb≔κ∧ecuc∗∈ECUbC,κ∧errorFramec∗=no and κ∧prevcntc∗=corCntbCc∗,x+1. Lemma 3 implies κ∧ecucntc∗=corCntbCc∗,x. Recall that Prop.B1 and Prop.B3 imply that the values of the parameters msg,msgid and cnt in a1,σb,b and c∗ are identical.(1)
Assumeκ∧msgidc∗=fmsg and assume further that when sending the message, ecu1 is synchronized, i.e. includes the correct counter as the message’s counter value. By Prop.B9 it follows κ∧cnta1=κ∧prevcnta1−1=corCntbCa1,x. Since all readbC and recvbC actions in v have errorFrame=no, Prop.B11 implies κ∧cntc∗=κ∧ecucntc∗, hence κ∧cntc∗=corCntbCc∗,x. It follows κ∧cntσb=κ∧cnta1=κ∧cntc∗=corCntbCc∗,x. Now if a1≠σb, the number of sendbC actions until a1 is smaller than the number of sendbC actions until σb. Since by Lemma 2 the correct counter minus any number of sendbC actions is always bigger or equal to 0, it follows that the correct counter for σb is different to the one for a1. More specifically, it is smaller, i.e. corCntbCσb,x≤corCntbCa1,x−1. Further, again by Lemma 2, the number of send actions having occurred until σb is equal to those having occurred until a readbC or recvbC action induced by σb, i.e. corCntbCσb,x=corCntbCc∗,x. This implies κ∧cnta1=κ∧cntσb=κ∧cntc∗=corCntbCc∗,x=corCntbCσb,x≤corCntbCa1,x−1. This constitutes a contradiction to our assumption that ecu1 is synchronized in a1 and sends κ∧cnta1=corCntbCa1,x. Thus a1=σb.(2)
Assumeκ∧msgidc∗=sync and ecu1 is synchronized which by Prop.B7 implies that it sends the correct counter as the message’s payload, i.e. κ∧msga1=corCntbCa1,x. Further, c∗ being a readbC or recvbC action with κ∧errorFramec∗=no, Prop.B8 implies κ∧ecucntc∗=κ∧msgc∗≤κ∧prevcntc∗−1. Hence it follows corCntbCc∗,x=κ∧ecucntc∗=κ∧msgc∗≤κ∧prevcntc∗−1=corCntbCc∗,x and thus κ∧msgc∗=corCntbCc∗,x. Assume a1≠σb. As above, Lemma 2 implies corCntbCσb,x≤corCntbCa1,x−1 and corCntbCσb,x=corCntbCc∗,x. Since by Prop.B1 κ∧msga1=κ∧msgσb=κ∧msgc∗, it follows corCntbCa1,x=κ∧msga1=κ∧msgc∗=corCntbCc∗,x=corCntbCσb,x≤corCntbCa1,x−1. This again constitutes a contradiction, thus it follows a1=σb.(3)
Assumeecu1 is not synchronized in a1. By Prop.B16 it has performed an action loseCntbC before a1, denoted by a2. If a2≠pre1x, by Prop.B17, κ∧ecucnta2 is set to a value bigger than the action’s correct counter value: κ∧ecucnta2>corCntbCa2,x. If a2=pre1x, Prop.B17 implies κ∧ecucnta2=bCntmax+1>corCntbCa2,x as well. Assume for simplicity that ecu1 ’s next action after a2 is a1. Then κ∧prevcnta1=κ∧ecucnta2>corCntbCa2,x. Let κ∧msgida1=fmsg. Then by Prop.B9, κ∧cnta1=κ∧prevcnta1−1=κ∧ecucnta2−1>corCntbCa2,x−1. Now a1 is the first sendbC action after a2 since a sendbC action in between would imply another action by ecu1 (Prop.B14). Lemma 2 implies corCntbCa2,x−1=corCntbCa1,x. Hence ecu1 not being synchronized results into κ∧cnta1>corCntbCa1,x. If a2 is not ecu1 ’s last action before a1 we can argue analogously only with a longer sequence of actions and counters in between a2 and a1 to consider, being decreased step by step. By Prop.B1 κ∧cnta1=κ∧cntσb=κ∧cntc∗ always holds. Hence corCntbCa1,x<κ∧cntc∗=κ∧cnta1. By Lemma 2 and the definition of corCntbC, corCntbCσb,x=corCntbCc∗,x, and since ECU∗ owns the correct counter in c∗, by Prop.B15 it follows κ∧prevcntc∗=corCntbCc∗,x+1 and Lemma 3 implies κ∧ecucntc∗=corCntbCc∗,x. Together these statements imply corCntbCσb,x=κ∧ecucntc∗. Further, Lemma 2 implies corCntbCa1,x≥corCntbCσb,x, no matter whether or not a1 and σb are identical. Hence κ∧ecucntc∗=corCntbCσb,x≤corCntbCa1,x and therefore κ∧ecucntc∗≤corCntbCa1,x<κ∧cntc∗. Prop.B11 implies κ∧errorFramec∗=yes, and by Prop.B12 it follows κ∧errorFrameb=yes and therefore κ∧anameb≠recvbC, a contradiction to the assumption we started the proof with. Hence corCntbCa1,x=κ∧cnta1 in the case of κ∧msgida1=fmsg.Ifκ∧msgida1=sync, we can decude κ∧errorFrameb=yes and thus the same contradiction by exchanging the parameter cnt by msg and applying Prop.B6 instead of Prop.B9 to deduce κ∧msga1>corCntbCa1,x. Further, Lemma 2 implies κ∧msga1=κ∧msgσb=κ∧msgc∗ and it follows κ∧msgc∗>corCntbCa1,x. With the same arguments as above, this implies κ∧msgc∗>κ∧ecucntc∗. Prop.B8 implies κ∧errorFramec∗=yes and again by by Prop.B12 it follows κ∧errorFrameb=yes and therefore κ∧anameb≠recvbC. So again the assumption of ecu1 not being synchronized leads to a contradiction. This concludes our proof.
The above, proof shows that our approach indeed satisfies data origin authenticity as well as immediacy and non-repeatability. In contrast, the generic counter system violates the latter ones. In the next section, we will discuss the security related differences in more detail. We will then introduce our proof of concept implementation showing its practicability and design decisions that substantiate our formal proof.


## 6.1. The Formal Bus Counter Model

We model the bus counter-based system (denoted byBusCnt henceforth) as similar as possible to the generic counter model. One important difference is that it does not need a central freshness value master since all ECUs send synchronization messages simultaneously. Hence the set of agents is defined as ℙbCnt=ECUbC∪Eve with ECUbC≔ECU1bC,ECU2bC,ECU3bC.As inGenCnt, the BusCnt system has only one bus bus=bus all agents are being connected to. Further, members of ECUbC are honest and own the key key, while Eve, not being member of this group, does not own this key. We use the same set of action parameters, but a different specification of agents’ behavior (after all, we model a different system). The set of actions ΣbCnt is defined as follows:(i)
sendbC,ecu,ecukey,ecucnt,prevcnt,bus,mackey,msgid,msg,cnt denotes a send action as described in Section 5.1.1, except that the counter value cnt is covered by the MAC but not transmitted. As in the GenCnt model, the message may be altered (by a technical error or by Eve) after having been sent and may thus only cause a readbC action (see below).(ii)
readbC,ecu,ecukey,ecucnt,prevcnt,bust,mackey,msgid,msg,cnt denotes agent ecu∈ℙbCnt reading a message without processing it afterwards. In contrast to the respective readgC action of the GenCnt model, the readbC action of the BusCnt model changes the state of an ecu being member of ECUbC by decrementing its local bCnt value (stored with the last action and thus modeled by the parameter prevcnt) (see Prop.B13 in Section 6.1.1 below). This captures the fact that ecu reacts to the “start of message” bit on bus but discards the respective message (e.g. because the CRC verification fails) in which case it does not perform the receive action. Note that the sender of a message always reads its own action bey performing a readbC action.(iii)
recvbC,ecu,ecukey,ecucnt,prevcnt,bus,mackey,msgid,msg,cnt denotes the successful reception and processing of a message by ecu∈ℙbCnt.(iv)
As in theGenCnt system, with loseCntbC,ecu,ecucnt,prevcnt,bus we model the fact that ecu∈ℙbCnt has lost the correct counter value for some reason and thus is no longer synchronized. Since in the BusCnt system counter values decrease, its counter is set to a value bigger than the correct counter value (see Section 6.1.1 for more details).


### 6.1.1. Agents’ Local View and Initial Knowledge

Again, the agents’ local view is defined analogously to the generic counter model: All agents see their own actions completely and see the messages sent on the CAN bus they are connected to but cannot see who sent them nor the values of parameters stored locally by the sender. Further, agents cannot see actionsreadbC,recvbC and loseCntbC performed by other agents.As already pointed out in Section 5.1.3, with specifying the agents’ initial knowledge we capture the characteristics of our system. In the following, we list all properties we assume to be satisfied by the agents’ initial knowledgeWbCnt with reference to the respective property in Section 5.1.3 (if any) in which case we omit the formalization. Analogously to Section 5.1.3, if not specified otherwise, the properties refer to ω∈WbCnt. We denote the correct counter for a specific action a in ω by corCntbCa,ω. In Lemma 2 (see Section 6.2) we will show how its value is determined.Prop.
B1 (analogous to first statement of Prop.A1). A readbC and recvbC action, respectively, on bus is always preceded by the corresponding send action that writes the message onto the bus. Obviously, the parameter values of mackey,msgid,msg and cnt in b and σb are identical (we forgo the formalization of the latter statement).
For allb∈ΣbCnt with κ∧aname∈readbC,recvbC holds precWbCntσb,b.Prop.
B2 (Prop.A2). Only members of ECUbC own and can use key=key. Since Eve does not own this key and honest ECUs use only key to generate and verify a MAC, the MAC key contained in a send or receive action being equal to key=key is equivalent to the ECU being member of ECUbC.Prop.
B3 (Prop.A3). A recvbC action performed by an honest ECU (i.e. a member of ECUbC) must be preceded by the respective send action of an agent having generated the MAC, i.e. owning the key used for MAC generation. Again, obviously, the parameter values of mackey,msgid,msg and cnt in b and σb are identical.Prop.
B4 (Prop.A4). The parameter prevcnt of an action performed by an honest ECU denotes the local bCnt value as result of the ECU’s previous action. For the very first action of an ECU it is defined as the maximal value of bCnt, denoted by bCntmax. Formally:
∀a∈alphω:κ∧prevcnta=κ∧ecucntprevacta,κ∧ecua,ω. If for all ai∈ω with actCntai,ω<actCnta,ω holds κ∧ecuai≠κ∧ecua, it follows κ∧prevcnta=bCntmax.Prop.
B5. In Section 7.2.2 we will discuss which starting value of bCnt to choose in order to avoid counter overflow. Further, as explained in Section 2.2, we assume that memory failures and attacks cannot cause counter overflow. Hence we can assume that such a failure never results into a local counter value stored by an ECU being smaller than the correct one (see Prop.B17 below). For our formal model we assume that the local counter value of ECUs is always sufficiently large such that counter decrementation can result into the value 0 only in the last phase class of an action sequence. Formally:
∀a∈alphω:κ∧prevcnta>0Prop.
B6 (analog to Prop.A8). When an honest ECU sends a synchronization message, it includes as its message payload the local bCnt value of its previous action decremented by 1 but does not change the local bCnt value.
∀a∈alphω:κ∧anamea=sendbC∧κ∧ecua∈ECUbC∧κ∧msgida=sync⇒κ∧msga=κ∧prevcnta−1∧κ∧ecucnta=κ∧prevcnta.Prop.
B7. We assume that there always exists an ECU owning the correct counter value. Since our synchronization concept utilizes the mechanism used for collision resolving (a 0 written to the CAN bus always overwrites a 1), the correct counter always overwrites any incorrect one. Therefore a sendbC action containing a synchronization message that is actually performed by an honest ECU always contains the correct counter. Formally:
a∈alphω∧κ∧anamea=sendbC∧κ∧ecua∈ECUbC∧κ∧msgida=sync⇒κ∧msga=corCntbCa,ω.Prop.
B8. When monitoring a synchronization message being written to the bus, an honest ECU decrements its previously used counter value by 1 and verifies that the result is less or equal to the counter sent as the message’s payload. The error frame parameter being equal to no indicates that this check has been successful (and that the MAC check that we do not formalize explicitly has been successful as well). It then uses this value as its new local counter.
∀a∈alphω:κ∧anamea∈readbC,recvbC∧κ∧ecua∈ECUbC∧κ∧msgida=sync∧κ∧errorFramea=no⇒κ∧ecucnta=κ∧msga≤κ∧prevcnta−1.
Whilea is actually a recvbC action, our proofs do not depend on distinguishing between readbC and recvbC actions of synchronization messages.Prop.
B9 (analog to Prop.A8). When an honest ECU sends a functional message, it includes as its counter value the local bCnt value of its previous action decremented by 1 but does not change the local bCnt value. (It changes the value of ecucnt with the action of reading its own message that the ECU performs simultaneously to sending, see Prop.B10 and Prop.B13.)
∀a∈alphω:κ∧anamea=sendbC∧κ∧ecua∈ECUbC∧κ∧msgida=fmsg⇒κ∧cnta=κ∧prevcnta−1∧κ∧ecucnta=κ∧prevcnta.Prop.
B10 (analog to Prop.A9). When an honest ECU receives and accepts a functional message, it decrements its previously used counter value by 1 and verifies that the message’s cnt value is equal to the result. It then sets its local bCnt value ecucnt to the message’s counter.
∀a∈alphω:κ∧anamea=recvbC∧κ∧ecua∈ECUbC∧κ∧msgida=fmsg⇒κ∧ecucnta=κ∧cnta=κ∧prevcnta−1.Prop.
B11. All honest ECUs, when reading a message, check the message’s MAC, independently of whether or not they accept it. In case of a functional message, this involves the ECU’s local counter, more concretely the counter value used by the ECU in its previous action decremented by 1. If such a check succeeds which is a necessary condition for the error frame being set to no, this value is the one that was used to generate the message’s MAC. Note that this assumes that an attacker that owns the correct counter and a MAC cannot guess the corresponding message.
Lets∈alphω with κ∧anames=sendbC and v∈Φs,WbCnt. Then the following holds:
∀b∈a∈alphv|κ∧anamea∈readbC,recvbC∧κ∧ecua∈ECUbC∧κ∧msgida=fmsg:κ∧errorFrameb=no⇒κ∧cntb=κ∧ecucntb=κ∧prevcnta−1.
Note that in our very simple model with only one type of functional message, a successful check indicated byerrorFrame=no actually results into a recvbC action. However, considering also readbC actions with errorFrame=no allows to extend the model with respect to more types of functional messages without having to change the assumptions.Prop.
B12. As explained in Section 3, if an ECU’s checks concerning for example a message’s MAC fails and it therefore writes an error-frame, all other ECUs join in and write an error-frame as well, no matter whether or not their checks failed. Hence all readbC and recvbC actions induced by a specific sendbC action have the same value for the parameter errorFrame. Since a message is only received and accepted if all checks have been successful, the error frame of a recvbC action is always set to no. Formally:
Lets∈alphω with κ∧anames=sendbC and v∈Φs,WbCnt. Let further Rv≔b∈alphv|κ∧anameb∈readbC,recvbC denote the readbC and recvbC actions in v. Then for all bi,bj∈Rv the following holds:
κ∧errorFramebi=κ∧errorFramebjandκ∧anamebi=recvbC⇒κ∧errorFramebi=no.Prop.
B13 (in contrast to Prop.A10). When an honest ECU reads a message, it always decrements its previously used bCnt value by 1 and uses the result as its new local bCnt value. This behavior is independent of whether or not its checks fail, i.e. independent of the errorFrame value. Formally:
∀a∈alphω:κ∧anamea=readbC∧κ∧ecua∈ECUbC⇒κ∧ecucnta=κ∧prevcnta−1.Prop.
B14. In a phase class Φs,WbCnt with κ∧anames=sendbC (i.e. a phase class that starts with a specific sendbC action and ends with the next sendbC action, see Definition 9), all honest ECUs including the sender either read or receive the message or perform a loseCnt action. They do not perform any other action.
Lets∈ΣbCnt with κ∧anames=sendbC and v maximal in Φs,WbCnt. Then for all ecu∈ECUbC exists exactly one c∈alphv such that κ∧ecuc=ecu and κ∧anamec∈readbC,recvbC,loseCntbC.Prop.
B15 (analog to Prop.A6). In every phase class Φs,WbCnt with κ∧anames=sendbC there is an honest ECU owning the correct counter and performing a read or recvbC action in this phase class, but no loseCnt action. Here, owning the correct counter means that the ECU has used and stored the correct counter value in its previous action and can thus use it in the next action.
Lets∈alphω with κ∧anames=sendbC. Then for all v maximal in Φs,WbCnt exists an action b∈alphv with κ∧anameb∈read,recv,ECU∗s≔κ∧ecub∈ECUbC and κ∧prevcntb=corCntbCb,ω+1.Prop.
B16 (analog to Prop.A12). If an ECU is not synchronized at a specific action, i.e. does not use the correct counter relevant for this action, it must have performed an action loseCntbC before. Note that using a counter value refers to the parameter prevcnt.
∀a∈alphω:κ∧prevcnta−1≠corCntbCa,ω⇒∃a′∈alphω:κ∧anamea′=loseCntbC∧κ∧ecua′=κ∧ecua∧actCnta′,ω<actCnta,ωProp.
B17 (analog to Prop.A11). As explained in Prop.B5, memory failures never result into decrease of the counter value stored by an ECU. This implies that an action loseCntbC performed by an honest ECU resets the ECU’s counter to a value bigger than the correct one. For formal reasons we assign a counter value higher than the maximal value the system starts with to a loseCnt action if it is the first action of an action sequence.
∀a∈alphω:(1)
a≠pre1ω∧κ∧anamea=loseCnt∧κ∧ecua∈ECUbC⇒κ∧ecucnta>corCntbCa,ω.(2)
a=pre1ω∧κ∧anamea=loseCnt∧κ∧ecua∈ECUbC⇒κ∧ecucnta=bCntmax+1
Analogously to Section5.1.2 we model immediacy and non-repeatability by the phase class Φσb,WbCnt as defined in Definition 9 determined by a fixed but arbitrary recvbC action b. In the following section we will show that BusCnt satisfies both properties.


## 6.1.1. Agents’ Local View and Initial Knowledge

Again, the agents’ local view is defined analogously to the generic counter model: All agents see their own actions completely and see the messages sent on the CAN bus they are connected to but cannot see who sent them nor the values of parameters stored locally by the sender. Further, agents cannot see actionsreadbC,recvbC and loseCntbC performed by other agents.As already pointed out in Section 5.1.3, with specifying the agents’ initial knowledge we capture the characteristics of our system. In the following, we list all properties we assume to be satisfied by the agents’ initial knowledgeWbCnt with reference to the respective property in Section 5.1.3 (if any) in which case we omit the formalization. Analogously to Section 5.1.3, if not specified otherwise, the properties refer to ω∈WbCnt. We denote the correct counter for a specific action a in ω by corCntbCa,ω. In Lemma 2 (see Section 6.2) we will show how its value is determined.Prop.
B1 (analogous to first statement of Prop.A1). A readbC and recvbC action, respectively, on bus is always preceded by the corresponding send action that writes the message onto the bus. Obviously, the parameter values of mackey,msgid,msg and cnt in b and σb are identical (we forgo the formalization of the latter statement).
For allb∈ΣbCnt with κ∧aname∈readbC,recvbC holds precWbCntσb,b.Prop.
B2 (Prop.A2). Only members of ECUbC own and can use key=key. Since Eve does not own this key and honest ECUs use only key to generate and verify a MAC, the MAC key contained in a send or receive action being equal to key=key is equivalent to the ECU being member of ECUbC.Prop.
B3 (Prop.A3). A recvbC action performed by an honest ECU (i.e. a member of ECUbC) must be preceded by the respective send action of an agent having generated the MAC, i.e. owning the key used for MAC generation. Again, obviously, the parameter values of mackey,msgid,msg and cnt in b and σb are identical.Prop.
B4 (Prop.A4). The parameter prevcnt of an action performed by an honest ECU denotes the local bCnt value as result of the ECU’s previous action. For the very first action of an ECU it is defined as the maximal value of bCnt, denoted by bCntmax. Formally:
∀a∈alphω:κ∧prevcnta=κ∧ecucntprevacta,κ∧ecua,ω. If for all ai∈ω with actCntai,ω<actCnta,ω holds κ∧ecuai≠κ∧ecua, it follows κ∧prevcnta=bCntmax.Prop.
B5. In Section 7.2.2 we will discuss which starting value of bCnt to choose in order to avoid counter overflow. Further, as explained in Section 2.2, we assume that memory failures and attacks cannot cause counter overflow. Hence we can assume that such a failure never results into a local counter value stored by an ECU being smaller than the correct one (see Prop.B17 below). For our formal model we assume that the local counter value of ECUs is always sufficiently large such that counter decrementation can result into the value 0 only in the last phase class of an action sequence. Formally:
∀a∈alphω:κ∧prevcnta>0Prop.
B6 (analog to Prop.A8). When an honest ECU sends a synchronization message, it includes as its message payload the local bCnt value of its previous action decremented by 1 but does not change the local bCnt value.
∀a∈alphω:κ∧anamea=sendbC∧κ∧ecua∈ECUbC∧κ∧msgida=sync⇒κ∧msga=κ∧prevcnta−1∧κ∧ecucnta=κ∧prevcnta.Prop.
B7. We assume that there always exists an ECU owning the correct counter value. Since our synchronization concept utilizes the mechanism used for collision resolving (a 0 written to the CAN bus always overwrites a 1), the correct counter always overwrites any incorrect one. Therefore a sendbC action containing a synchronization message that is actually performed by an honest ECU always contains the correct counter. Formally:
a∈alphω∧κ∧anamea=sendbC∧κ∧ecua∈ECUbC∧κ∧msgida=sync⇒κ∧msga=corCntbCa,ω.Prop.
B8. When monitoring a synchronization message being written to the bus, an honest ECU decrements its previously used counter value by 1 and verifies that the result is less or equal to the counter sent as the message’s payload. The error frame parameter being equal to no indicates that this check has been successful (and that the MAC check that we do not formalize explicitly has been successful as well). It then uses this value as its new local counter.
∀a∈alphω:κ∧anamea∈readbC,recvbC∧κ∧ecua∈ECUbC∧κ∧msgida=sync∧κ∧errorFramea=no⇒κ∧ecucnta=κ∧msga≤κ∧prevcnta−1.
Whilea is actually a recvbC action, our proofs do not depend on distinguishing between readbC and recvbC actions of synchronization messages.Prop.
B9 (analog to Prop.A8). When an honest ECU sends a functional message, it includes as its counter value the local bCnt value of its previous action decremented by 1 but does not change the local bCnt value. (It changes the value of ecucnt with the action of reading its own message that the ECU performs simultaneously to sending, see Prop.B10 and Prop.B13.)
∀a∈alphω:κ∧anamea=sendbC∧κ∧ecua∈ECUbC∧κ∧msgida=fmsg⇒κ∧cnta=κ∧prevcnta−1∧κ∧ecucnta=κ∧prevcnta.Prop.
B10 (analog to Prop.A9). When an honest ECU receives and accepts a functional message, it decrements its previously used counter value by 1 and verifies that the message’s cnt value is equal to the result. It then sets its local bCnt value ecucnt to the message’s counter.
∀a∈alphω:κ∧anamea=recvbC∧κ∧ecua∈ECUbC∧κ∧msgida=fmsg⇒κ∧ecucnta=κ∧cnta=κ∧prevcnta−1.Prop.
B11. All honest ECUs, when reading a message, check the message’s MAC, independently of whether or not they accept it. In case of a functional message, this involves the ECU’s local counter, more concretely the counter value used by the ECU in its previous action decremented by 1. If such a check succeeds which is a necessary condition for the error frame being set to no, this value is the one that was used to generate the message’s MAC. Note that this assumes that an attacker that owns the correct counter and a MAC cannot guess the corresponding message.
Lets∈alphω with κ∧anames=sendbC and v∈Φs,WbCnt. Then the following holds:
∀b∈a∈alphv|κ∧anamea∈readbC,recvbC∧κ∧ecua∈ECUbC∧κ∧msgida=fmsg:κ∧errorFrameb=no⇒κ∧cntb=κ∧ecucntb=κ∧prevcnta−1.
Note that in our very simple model with only one type of functional message, a successful check indicated byerrorFrame=no actually results into a recvbC action. However, considering also readbC actions with errorFrame=no allows to extend the model with respect to more types of functional messages without having to change the assumptions.Prop.
B12. As explained in Section 3, if an ECU’s checks concerning for example a message’s MAC fails and it therefore writes an error-frame, all other ECUs join in and write an error-frame as well, no matter whether or not their checks failed. Hence all readbC and recvbC actions induced by a specific sendbC action have the same value for the parameter errorFrame. Since a message is only received and accepted if all checks have been successful, the error frame of a recvbC action is always set to no. Formally:
Lets∈alphω with κ∧anames=sendbC and v∈Φs,WbCnt. Let further Rv≔b∈alphv|κ∧anameb∈readbC,recvbC denote the readbC and recvbC actions in v. Then for all bi,bj∈Rv the following holds:
κ∧errorFramebi=κ∧errorFramebjandκ∧anamebi=recvbC⇒κ∧errorFramebi=no.Prop.
B13 (in contrast to Prop.A10). When an honest ECU reads a message, it always decrements its previously used bCnt value by 1 and uses the result as its new local bCnt value. This behavior is independent of whether or not its checks fail, i.e. independent of the errorFrame value. Formally:
∀a∈alphω:κ∧anamea=readbC∧κ∧ecua∈ECUbC⇒κ∧ecucnta=κ∧prevcnta−1.Prop.
B14. In a phase class Φs,WbCnt with κ∧anames=sendbC (i.e. a phase class that starts with a specific sendbC action and ends with the next sendbC action, see Definition 9), all honest ECUs including the sender either read or receive the message or perform a loseCnt action. They do not perform any other action.
Lets∈ΣbCnt with κ∧anames=sendbC and v maximal in Φs,WbCnt. Then for all ecu∈ECUbC exists exactly one c∈alphv such that κ∧ecuc=ecu and κ∧anamec∈readbC,recvbC,loseCntbC.Prop.
B15 (analog to Prop.A6). In every phase class Φs,WbCnt with κ∧anames=sendbC there is an honest ECU owning the correct counter and performing a read or recvbC action in this phase class, but no loseCnt action. Here, owning the correct counter means that the ECU has used and stored the correct counter value in its previous action and can thus use it in the next action.
Lets∈alphω with κ∧anames=sendbC. Then for all v maximal in Φs,WbCnt exists an action b∈alphv with κ∧anameb∈read,recv,ECU∗s≔κ∧ecub∈ECUbC and κ∧prevcntb=corCntbCb,ω+1.Prop.
B16 (analog to Prop.A12). If an ECU is not synchronized at a specific action, i.e. does not use the correct counter relevant for this action, it must have performed an action loseCntbC before. Note that using a counter value refers to the parameter prevcnt.
∀a∈alphω:κ∧prevcnta−1≠corCntbCa,ω⇒∃a′∈alphω:κ∧anamea′=loseCntbC∧κ∧ecua′=κ∧ecua∧actCnta′,ω<actCnta,ωProp.
B17 (analog to Prop.A11). As explained in Prop.B5, memory failures never result into decrease of the counter value stored by an ECU. This implies that an action loseCntbC performed by an honest ECU resets the ECU’s counter to a value bigger than the correct one. For formal reasons we assign a counter value higher than the maximal value the system starts with to a loseCnt action if it is the first action of an action sequence.
∀a∈alphω:(1)
a≠pre1ω∧κ∧anamea=loseCnt∧κ∧ecua∈ECUbC⇒κ∧ecucnta>corCntbCa,ω.(2)
a=pre1ω∧κ∧anamea=loseCnt∧κ∧ecua∈ECUbC⇒κ∧ecucnta=bCntmax+1
Analogously to Section5.1.2 we model immediacy and non-repeatability by the phase class Φσb,WbCnt as defined in Definition 9 determined by a fixed but arbitrary recvbC action b. In the following section we will show that BusCnt satisfies both properties.


## 6.2. Formal Proof of bCnt System

The idea of theBusCnt system is that counter values included in the MACs of sent messages are strictly monotonically decreasing (instead of strictly monotonically increasing as in the GenCnt system). However, in contrast to the GenCnt system, in BusCnt each send action inevitably induces a readbC or recvbC action and thus a decrement of the counter, no matter whether or not a check failed. In case a system does not suffer any anomalies (i.e. all actors act correctly and counter value change is never caused by physical irregularities), the counter used by the ECUs is always the correct one. Lemma 2 will show how it is determined. For its proof we need the following technical Lemma:Lemma 1.
Letω∈WbCntcor≔ω∈WbCnt|κ∧ecua∈ECUbC∧κ∧anamea≠loseCnt for all a∈alphω. Let furtherSω≔a∈alphω|κ∧anamea=sendbCwithactCntsi,ω<actCntsi+k,ωfor allsi,si+k∈Sωi,k∈ℕ. Then for allb∈alphωwithκ∧anameb∈readbC,recvbCthe following holds:1.
κ∧msgidb=fmsg⇒κ∧ecucntb=κ∧cntb2.
κ∧msgidb=sync⇒κ∧ecucntb=κ∧msgbProof 2.
Ifκ∧anameb=recvbC, the assertions follow directly by Prop.B10 and Prop.B12 together with Prop.B8, respectively. Let now κ∧anameb=readbC. We show the assertions of this case by induction over the number of consecutive phase classes Φsi,WbCntcor.Induction basis:i=1. Consider v∈Φs1,WbCntcor and b∈alphv. Let κ∧msgidb=fmsg and assume κ∧ecus1=κ∧ecub. Then Prop.B13 and Prop.B4 imply κ∧ecucntb=κ∧prevcntb−1=κ∧ecucnts1−1. Further, by Prop.B1, κ∧cntb=κ∧cnts1. Now by Prop.B9, κ∧cnts1=κ∧prevcnts1−1=κ∧ecucnts1−1. Together this leads to κ∧cntb=κ∧ecucnts1−1=κ∧ecucntb.
Assume nowκ∧ecub≠κ∧ecus1. Since Prop.B1 requires a send action before any readbC or recvbC action and since s1 is the first send action in ω, there is no other action in ω before s1. Prop.B14 implies that b is the first κ∧ecub∈Ωκ∧prevcntb=bCntmax and thus Prop.B13 implies κ∧ecucntb=κ∧prevcntb−1=bCntmax−1. s1 being the first action in ω, it is the first action of κ∧ecus1 as well and Prop.B4 implies κ∧prevcnts1=bCntmax. By Prop.B9 it follows κ∧cnts1=κ∧prevcnts1−1=bCntmax−1. Further, by Prop.B1, κ∧cntb=κ∧cnts1. Together we can conclude κ∧cnts1=κ∧cnts1=bCntmax−1=κ∧ecucntb.
In caseκ∧msgidb=sync, we can argue analogously by replacing every occurrence of κ∧cnt by κ∧msg and applying Prop.B6 instead of Prop.B9.
Induction hypothesis: For v∈Φsi,WbCntcor and b∈alphv, let assertions 1 and 2 hold.
Induction step: Consider v∈Φsi+1,WbCntcor,b∈alphv with κ∧anameb∈readbC,recvbC and κ∧msgidb=fmsg. First we again assume κ∧ecub=κ∧ecusi+1. b being a readbC action, Prop.B13 implies κ∧ecucntb=κ∧prevcntb−1 which by Prop.B4 and Prop.B14 is equal to κ∧ecucntsi+1−1. Further, by Prop.B9, κ∧cntsi+1=κ∧prevcntsi+1−1 and κ∧ecucntsi+1=κ∧prevcntsi+1. Since Prop.B1 implies κ∧cntsi+1=κ∧cntsi+1, it follows κ∧cntb=κ∧prevcntsi+1−1=κ∧ecucntsi+1−1=κ∧ecucntb.
Assume nowκ∧ecub≠κ∧ecusi+1. As above, Prop.B13 implies κ∧ecucntb=κ∧prevcntb−1. Since by Prop.B14 all ECUs perform a readbC or recvbC action in the previous phase class Φsi,WbCntcor (loseCntbC actions are excluded by definition), this holds in particular for κ∧ecub and κ∧ecusi+1. Hence for all maximal v′ in Φsi,WbCntcor there exist readbC or recvbC actions b′∈alphv′ performed by κ∧ecub and a∈alphv′ performed by κ∧ecusi+1, being the previous actions of κ∧ecub and κ∧ecusi+1, respectively. Prop.B4 implies κ∧ecucntb=κ∧prevcntb−1=κ∧ecucntb′−1 which by induction hypothesis is equal to κ∧cntb′−1. This in turn is equal to κ∧cntsi−1=κ∧cnta−1 by Prop.B1. Again by induction hypothesis, the latter expression is equal to κ∧ecucnta−1. Prop.B4 implies equality to κ∧prevcntsi+1−1 which by Prop.B9 is equal to κ∧cntsi+1. Prop.B1 finally implies equality to κ∧cntb, hence κ∧cntb=κ∧ecucntb.
Again, in caseκ∧msgidb=sync, the analogous proof is achieved by replacing every occurrence of κ∧cnt by κ∧msg and applying Prop.B6 instead of Prop.B9.Lemma 2.
LetWbCntcorandSωas defined in Lemma 1. Let furtherω∈WbCntcoranda∈alphω. Then the following holds:1.
κ∧msgida=fmsg⇒κ∧cnta=bCntmax−cards∈Sω|actCnts,ω≤actCnta,ω≥02.
κ∧msgida=sync⇒κ∧msga=bCntmax−cards∈Sω|actCnts,ω≤actCnta,ω≥0
Further, for allsi−1,si∈Sω(i.e. withactCntsi−1,ω<actCntsi,ωandi∈ℕ,i≥2holds(i)
κ∧msgidsi−1=κ∧msgidsi=fmsg⇒κ∧cntsi=κ∧cntsi−1−1(ii)
κ∧msgidsi−1=κ∧msgidsi=sync⇒κ∧msgsi=κ∧msgsi−1−1(iii)
κ∧msgidsi−1=fmsg∧κ∧msgidsi=sync⇒κ∧msgsi=κ∧cntsi−1−1(iv)
κ∧msgidsi−1=sync∧κ∧msgidsi=fmsg⇒κ∧cntsi=κ∧msgsi−1−1Note that item 1 implies that the parametercnt of actions concerning a functional message never reaches the value 0 unless there occur no more sendbC actions after the action a. The analogous statement holds for the parameter msg of actions concerning synchronization messages.Proof 3.
We prove assertions 1 and 2 by induction over the lengthl∈ℕ of a word ω∈WbCntcor.Induction basis:l=1, i.e. ω=a1. Since Prop.B1 requires a sendbC action before any readbC or recvbC action, a1 cannot be a readbC or recvbC action. Since further by definition ω does not contain any loseCnt action, κ∧anamea1=sendbC. Prop.B4 implies κ∧prevcnta1=bCntmax. If κ∧msgida1=fmsg, by Prop.B9 it follows κ∧cnta1=κ∧prevcnta1−1=bCntmax−1=bCntmax−cards∈Sa1|actCnts,a1≤actCnta1,a1. Further, by Prop.B5 κ∧prevcnta1=bCntmax>0 which implies κ∧prevcnta1−1=bCntmax−1≥0. Thus item 1 holds for ω=a1 containing a functional message. If on the other hand κ∧msgida1=sync, by Prop.B6 it follows κ∧msga1=κ∧prevcnta1−1 which as above implies the assertion, thus item 2 holds for ω=a1.Induction hypothesis: Let ωi=a1…aii≥2,i∈ℕ. Then for all a∈alphωi holds:(1)
κ∧msgida=fmsg⇒κ∧cnta=bCntmax−cards∈Sωi|actCnts,ωi≤actCnta,ωi≥0(2)
κ∧msgida=sync⇒κ∧msga=bCntmax−cards∈Sωi|actCnts,ωi≤actCnta,ωi≥0Induction step: Consider ωi+1≔a1…aiai+1.(1) Assumeκ∧anameai+1=sendbC. By Prop.B14 and the fact that ωi+1 does not contain any loseCntbC actions, it follows that ai is a recvbC or readbC action. This in turn is preceded by a sendbC action σai (see Prop.B1). So we have ωi+1=a1…σai…aiai+1 (σai may or may not be equal to a1). Let vi a maximal word in Φσai,WbCntcor, i.e. vi starts with σai and ends with ai+1, and all other actions in between are readbC and recvbC actions, the last one being ai. By Prop.B1, for all these readbC and recvbC actions b∈alphvi holds κ∧cntb=κ∧cntσai=κ∧cntai. Since all ECUs perform exactly one readbC or recvbC action in vi, there is exactly one recvbC or readbC action b∗∈alphvi performed by ecu∗≔κ∧ecuai+1, being the last action performed by ecu∗ before ai+1.(a)
Assumeκ∧msgidai+1=fmsg. If κ∧msgidb∗=fmsg as well, Lemma 1 implies κ∧ecucntb∗=κ∧cntb∗. Since ai+1 contains a functional message, Prop.B9 implies κ∧cntai+1=κ∧prevcntai+1−1=κ∧ecucntb∗−1=κ∧cntb∗−1. By Prop.B1 this is equal to κ∧cntσai−1=κ∧cntai−1. Prop.B1 also implies κ∧msgidai=κ∧msgidb∗=fmsg, hence by induction hypothesis it follows κ∧cntai+1=κ∧cntai−1=bCntmax−cards∈Sωi+1|actCnts,ωi+1≤actCntai,ωi+1−1. Finally, since ai+1 is the sendbC action directly following ai, κ∧cntai+1=bCntmax−cards∈Sωi+1|actCnts,ωi+1≤actCntai+1,ωi+1. Further, since κ∧cntai+1=κ∧prevcntai+1−1 and by Prop.B5 κ∧prevcntai+1>0, it follows κ∧cntai+1≥0.If on the other handκ∧msgidb∗=sync, Lemma 1 implies κ∧ecucntb∗=κ∧msgb∗. Using Prop.B9, we can then deduce κ∧cntai+1=κ∧ecucntb∗−1=κ∧msgb∗−1 which by Prop.B1 is equal to κ∧msgai−1. As above, the assertion follows.
(b)
Assumeκ∧msgidai+1=sync. In this case we can use Prop.B6 to deduce κ∧msgai+1=κ∧prevcntai+1−1. If κ∧msgidb∗=fmsg, the rest of the proof is identical to the case where this is combined with a functional message of ai+1, if κ∧msgidb∗=sync, the arguments regarding ai+1 being a synchronization message apply. This ends the proof for the case κ∧anameai+1=sendbC.(2)
Assumeκ∧anameai+1∈readbC,recvbC. Then Prop.B1 implies that there is an action σai+1 which is either equal to ai or occurs before ai.(a) Letσai+1=ai. By Prop.B1 it follows κ∧cntai+1=κ∧cntai,κ∧msgai+1=κ∧msgai and κ∧msgidai+1=κ∧msgidai. Since ai is the last send action before the recvbC/readbC action ai+1, the number of send actions before these two actions including ai is identical, i.e. cards∈Sωi+1|actCnts,ωi+1≤actCntai,ωi+1=cards∈Sωi+1|actCnts,ωi+1≤actCntai+1,ωi+1. If κ∧msgidai=fmsg, the induction hypothesis implies 0≤κ∧cntai=bCntmax−cards∈Sωi+1|actCnts,ωi+1≤actCntai,ωi+1=bCntmax−cards∈Sωi+1|actCnts,ωi+1≤actCntai+1,ωi+1=κ∧cntai+1. If κ∧msgidai=sync, the induction hypothesis implies 0≤κ∧msgai=bCntmax−cards∈Sωi+1|actCnts,ωi+1≤actCntai,ωi+1=bCntmax−cards∈Sωi+1|actCnts,ωi+1≤actCntai+1,ωi+1=κ∧msgai+1.(b) Letσai+1=:a′ with actCnta′,ωi+1>actCntai,ωi+1. Then Prop.B14 and the fact that ωi+1 does not contain any loseCntbC actions implies that ai is a readbC or recvbC action. Again, by Prop.B1 it follows κ∧cntai=κ∧cntσai=κ∧cntσai+1=κ∧cntai+1 and the equivalent equations for the parameters msg and msgid. Now we can again conclude that the number of send actions before ai is identical to those before ai+1 and as above, by induction hypothesis for the cases κ∧msgidai=fmsgid and κ∧msgidai=sync, respectively, it follows the assertion. This concludes the proof of assertions 1 and 2.
We now prove assertions (i)–(iv) of the Lemma. So assume the first statement holds regarding functional messages. Then it holds in particular for two consecutivesendbC actions si−1 and si in a word ω∈WbCntcor, each sending a functional message. Then κ∧cntsi=bCntmax−cards∈Sω|actCnts,ω≤actCntsi,ω=bCntmax−cards∈Sω|actCnts,ω≤actCntsi−1,ω+1=bCntmax−cards∈Sω|actCnts,ω≤actCntsi−1,ω−1=κ∧cntsi−1−1. The only difference between a sendbC action s containing a synchronization message and one containing a functional message is that the value bCntmax minus the cardinality of sendbC actions happening before s and including s is assigned to the counter of s in the first case and to the message of s in the second case. Hence, the respective statements for all other combinations of synchronization and functional sendbC actions can be shown analogously.The above Lemma uses properties that describe the behavior of honest agents when sending, receiving or reading a message and shows the resulting counter value. This behavior does not depend on whether or not any involved send action is performed by an honest ECU. Hence the counter value included in actions of sequences inWbCntcor can be considered the correct one for actions in WbCnt.Definition 10.
Forω∈WbCntanda∈alphωwe define(9)corCntbCa,ω≔bCntmax−cards∈Sω|actCnts,ω≤actCnta,ω.
We now considerWbCnt again and first show a Lemma whose important statement is that a synchronization message received by an ECU never contains a counter smaller than the correct one for this action. In general the Lemma states that an honest ECU owning the correct counter before processing a readbC or recvbC action (denoted by the parameter prevcnt of the action), also owns the correct counter afterwards (denoted by the parameter ecucnt).Lemma 3.
Letω∈WbCntanda∈alphω. Then the following holds:(10)κ∧anamea∈readbC,recvbC∧κ∧prevcnta=corCntbCa,ω+1⇒κ∧ecucnta=corCntbCa,ω.Proof 4.
Assumeκ∧anamea=readbC. Then by Prop.B13 κ∧ecucnta=κ∧prevcnta−1=corCntbCa,ω+1−1=corCntbCa,ω. The same follows by Prop.B10 for a being a recvbC action of a functional message. So let κ∧anamea=recvbC and κ∧msgida=sync. Prop.B12 implies κ∧errorFramea=no and thus by Prop.B8 it follows κ∧ecucnta≤κ∧prevcnta−1=corCntbCa,ω+1−1. In case of κ∧ecucnta=κ∧prevcnta−1 the assertion holds. So let κ∧ecucnta<κ∧prevcnta−1, i.e. κ∧ecucnta<corCntbCa,ω. Prop.B16 implies that before a, κ∧ecua performs a loseCnt action a′ and by Prop.B17, if a′≠pre1ω, it follows κ∧ecucnta′>corCntbCa′,ω. For simplicity we assume that a′ is the last action of κ∧ecua in ω before a. By Prop.B14, every ECU performs only one action per phase class, hence a′ happens in the phase class Φs′,WbCnt that ends with σa, i.e. in the phase class directly occuring before the one including a. Lemma 2 implies that corCntbCa′,ω=corCntbCa,ω+1. So we have corCntbCa,ω+1=κ∧prevcnta=κ∧ecucnta′>corCntbCa′,ω=corCntbCa,ω+1. This constitutes a contradiction, hence κ∧ecucnta=corCntbCa,ω holds. In case a′ is not the previous action of κ∧ecua, we can argue analogously.
Leta′=pre1ω. Since a′ is the first action and not a sendbC action, Lemma 2 implies corCntbCa′,ω=bCntmax. As above, we have corCntbCa,ω+1=κ∧prevcnta=κ∧ecucnta′ which by Prop.B17 is equal to bCntmax+1=corCntbCa′,ω+1. This implies corCntbCa,ω=corCntbCa′,ω. However, since σa happens before the recvbC action a (and after the loseCntbC action a′), by Lemma 2corCntbCa=bCntmax−1≠bCntmax=corCntbCa′,ω. So again this constitutes a contradiction, hence κ∧ecucnta=corCntbCa,ω always holds.We can now prove our main Theorem. As in Section5.2, the property we want to prove is that whenever an honest ECU receives and accepts a message (action b), the sendbC action σb having triggered b and starting the phase class determined by b must have authentically for the ECU been performed by an agent being member of the same group, and the message must contain the correct counter. In contrast to the proof regarding the GenCnt system, for the BusCnt system (formally denoted by BbCnt) we can show that this property is always satisfied, i.e. that both immediacy and non-repeatability hold.Theorem 2.
Letω∈BbCntandb≔recvbC,ecu,ecukey,ecucnt,prevcnt,bus,mackey,msgid,msg,cnt∈alphωwithecu∈ECUbC. Then the following property holds:(11)authWiPhasesend,ecu′,ecukey′,ecucnt′,prevcnt′,bus,mackey,msgid,msg,cnt|ecu′∈ECUbC,b,ecu,Φσb,WbCnt.Proof 5.
Analogously to Section5.2, without loss of generality we assume ECU1bC∈ECUbC to perform a receive action b≔recvbC,ECU1bC,ecukey,ecucnt,prevcnt,bus,mackey,msgid,msg,cnt∈alphω and consider an arbitrary x∈λECU1bC−1λECU1bCω∩WbCnt (which by definition of λECU1bC and BbCnt⊆WbCnt contains b). Since ECU1bC∈ECUbC, by Prop.B2 it follows mackey=key=ecukey. Further, by Prop.B3 there is an action a1≔sendbC,ecu1,ecukey1,ecucnt1,prevcnt1,bus,mackey,msgid,msg,cnt∈alphx before the receive action b by ECU1bC containing the same message ID, message and counter value and with ecukey1=mackey. Again by Prop.B2 it follows ecu1∈ECUbC which proves that the message received in b has authentically for ECU1bC been generated and sent by a member of ECUbC.
Further, by Prop.B1 the receive actionb by ECU1bC is preceded by a send action σb=sendbC,ecu′,ecukey′,ecucnt′,prevcnt′,bus,mackey,msgid,msg,cnt triggering b.
Letv maximal in Φσb,WbCnt with b∈alphv. Since κ∧anameb=recvbC, Prop.B12 implies κ∧errorFrameb=no and thus κ∧errorFramec=no for all c∈alphv with κ∧anamec∈readbC,recvbC. By Prop.B15 one of the actions readbC,recvbC in v is performed by an ECU owning the correct counter, i.e. there exists c∗∈alphv with κ∧anamec∗∈readbC,recvbC,ECU∗σb≔κ∧ecuc∗∈ECUbC,κ∧errorFramec∗=no and κ∧prevcntc∗=corCntbCc∗,x+1. Lemma 3 implies κ∧ecucntc∗=corCntbCc∗,x. Recall that Prop.B1 and Prop.B3 imply that the values of the parameters msg,msgid and cnt in a1,σb,b and c∗ are identical.(1)
Assumeκ∧msgidc∗=fmsg and assume further that when sending the message, ecu1 is synchronized, i.e. includes the correct counter as the message’s counter value. By Prop.B9 it follows κ∧cnta1=κ∧prevcnta1−1=corCntbCa1,x. Since all readbC and recvbC actions in v have errorFrame=no, Prop.B11 implies κ∧cntc∗=κ∧ecucntc∗, hence κ∧cntc∗=corCntbCc∗,x. It follows κ∧cntσb=κ∧cnta1=κ∧cntc∗=corCntbCc∗,x. Now if a1≠σb, the number of sendbC actions until a1 is smaller than the number of sendbC actions until σb. Since by Lemma 2 the correct counter minus any number of sendbC actions is always bigger or equal to 0, it follows that the correct counter for σb is different to the one for a1. More specifically, it is smaller, i.e. corCntbCσb,x≤corCntbCa1,x−1. Further, again by Lemma 2, the number of send actions having occurred until σb is equal to those having occurred until a readbC or recvbC action induced by σb, i.e. corCntbCσb,x=corCntbCc∗,x. This implies κ∧cnta1=κ∧cntσb=κ∧cntc∗=corCntbCc∗,x=corCntbCσb,x≤corCntbCa1,x−1. This constitutes a contradiction to our assumption that ecu1 is synchronized in a1 and sends κ∧cnta1=corCntbCa1,x. Thus a1=σb.(2)
Assumeκ∧msgidc∗=sync and ecu1 is synchronized which by Prop.B7 implies that it sends the correct counter as the message’s payload, i.e. κ∧msga1=corCntbCa1,x. Further, c∗ being a readbC or recvbC action with κ∧errorFramec∗=no, Prop.B8 implies κ∧ecucntc∗=κ∧msgc∗≤κ∧prevcntc∗−1. Hence it follows corCntbCc∗,x=κ∧ecucntc∗=κ∧msgc∗≤κ∧prevcntc∗−1=corCntbCc∗,x and thus κ∧msgc∗=corCntbCc∗,x. Assume a1≠σb. As above, Lemma 2 implies corCntbCσb,x≤corCntbCa1,x−1 and corCntbCσb,x=corCntbCc∗,x. Since by Prop.B1 κ∧msga1=κ∧msgσb=κ∧msgc∗, it follows corCntbCa1,x=κ∧msga1=κ∧msgc∗=corCntbCc∗,x=corCntbCσb,x≤corCntbCa1,x−1. This again constitutes a contradiction, thus it follows a1=σb.(3)
Assumeecu1 is not synchronized in a1. By Prop.B16 it has performed an action loseCntbC before a1, denoted by a2. If a2≠pre1x, by Prop.B17, κ∧ecucnta2 is set to a value bigger than the action’s correct counter value: κ∧ecucnta2>corCntbCa2,x. If a2=pre1x, Prop.B17 implies κ∧ecucnta2=bCntmax+1>corCntbCa2,x as well. Assume for simplicity that ecu1 ’s next action after a2 is a1. Then κ∧prevcnta1=κ∧ecucnta2>corCntbCa2,x. Let κ∧msgida1=fmsg. Then by Prop.B9, κ∧cnta1=κ∧prevcnta1−1=κ∧ecucnta2−1>corCntbCa2,x−1. Now a1 is the first sendbC action after a2 since a sendbC action in between would imply another action by ecu1 (Prop.B14). Lemma 2 implies corCntbCa2,x−1=corCntbCa1,x. Hence ecu1 not being synchronized results into κ∧cnta1>corCntbCa1,x. If a2 is not ecu1 ’s last action before a1 we can argue analogously only with a longer sequence of actions and counters in between a2 and a1 to consider, being decreased step by step. By Prop.B1 κ∧cnta1=κ∧cntσb=κ∧cntc∗ always holds. Hence corCntbCa1,x<κ∧cntc∗=κ∧cnta1. By Lemma 2 and the definition of corCntbC, corCntbCσb,x=corCntbCc∗,x, and since ECU∗ owns the correct counter in c∗, by Prop.B15 it follows κ∧prevcntc∗=corCntbCc∗,x+1 and Lemma 3 implies κ∧ecucntc∗=corCntbCc∗,x. Together these statements imply corCntbCσb,x=κ∧ecucntc∗. Further, Lemma 2 implies corCntbCa1,x≥corCntbCσb,x, no matter whether or not a1 and σb are identical. Hence κ∧ecucntc∗=corCntbCσb,x≤corCntbCa1,x and therefore κ∧ecucntc∗≤corCntbCa1,x<κ∧cntc∗. Prop.B11 implies κ∧errorFramec∗=yes, and by Prop.B12 it follows κ∧errorFrameb=yes and therefore κ∧anameb≠recvbC, a contradiction to the assumption we started the proof with. Hence corCntbCa1,x=κ∧cnta1 in the case of κ∧msgida1=fmsg.Ifκ∧msgida1=sync, we can decude κ∧errorFrameb=yes and thus the same contradiction by exchanging the parameter cnt by msg and applying Prop.B6 instead of Prop.B9 to deduce κ∧msga1>corCntbCa1,x. Further, Lemma 2 implies κ∧msga1=κ∧msgσb=κ∧msgc∗ and it follows κ∧msgc∗>corCntbCa1,x. With the same arguments as above, this implies κ∧msgc∗>κ∧ecucntc∗. Prop.B8 implies κ∧errorFramec∗=yes and again by by Prop.B12 it follows κ∧errorFrameb=yes and therefore κ∧anameb≠recvbC. So again the assumption of ecu1 not being synchronized leads to a contradiction. This concludes our proof.
The above, proof shows that our approach indeed satisfies data origin authenticity as well as immediacy and non-repeatability. In contrast, the generic counter system violates the latter ones. In the next section, we will discuss the security related differences in more detail. We will then introduce our proof of concept implementation showing its practicability and design decisions that substantiate our formal proof.


## 7. Evaluation

In this section, we will evaluate both the security and the practicability of our bus counter approach. More specifically, in the next section we will discuss the formal proof results concerning the satisfaction of the security requirements immediacy and non-repeatability by the generic and the BusCnt system, respectively, and highlight the differences. In Section7.2 we will then demonstrate the feasibility of our BusCnt approach based on a practical implementation and discuss design decisions.


### 7.1. Security Aspects

One fundamental difference between our approach and the generic counter-based approach is that in the BusCnt system the pulse generator is an integral component of the system itself: The very writing onto the bus causes a change of the local bus counter values of all ECUs connected to it as they inevitably read (part of) the message (even if not accepting it) and decrement their counters. By this read action, the message’s counter and thus its MAC is invalidated. Hence, any subsequent message written onto the bus must use a smaller counter in order to be accepted. This prohibits message delay and replication.Another important aspect is the assignment of computations to the controller that in traditional CAN communication systems is processed by the application layer. This concerns in particular MAC calculation and verification and checks regarding the size of the message’s counter. Performing these checks on controller level enables to use the error frame mechanism of CAN in case of a failed check which in return results in invalidation of the respective message and prevention of its acceptance by any of the ECUs connected to the same bus.These two aspects together allowed to formally prove that the BusCnt system satisfies both immediacy and non-repeatability, provided at least one of the ECUs owns the correct counter. The inevitable decrease of the counter value with every new message prohibits message delay, and the checks performed by the controllers allow immediate invalidation of any manipulated message.One of the core assumptions of our proof is the correctness of at least one counter value in the bus network. It is based on two observations: First, ECUs are designed to be safe and thus hardware or software failures occur significantly less often compared to regular PC hardware. Second, an incorrect counter value may be the result of the shutdown process, as an ECU may not be able to store the counter value in time to persistent storage. However, the likelihood for this failure to occur is reduced in our approach since only a single value per bus needs to be stored. In contrast, traditional counter-based approaches use various counters for different types of messages. Moreover, a bus has a large number of ECUs connected to it and only one needs to store the correct counter value at the end of a ride. Therefore, the probability that our assumption does not hold is insignificant.On the other hand, an ECU not being synchronized, i.e. not owning the correct counter, may in principle cause a safety problem: If it sends a functional message, MAC verification by ECUs owning the correct counter will fail and result into an error frame. If the ECU itself receives a functional message containing the correct counter, its own MAC verification will fail and cause an error frame as well. Too many error frame events will cause the ECU to change into an inactive state. This safety problem can be minimized by adequate synchronization approaches as discussed in Section7.2.2 below.In contrast to the BusCnt system, our proof of the generic counter-based approach indicates that it exhibits several weaknesses. First, it cannot ensure immediacy and non-repeatability (neither of synchronization nor of functional messages) in case an ECU loses its counter. Once being active again the ECU will accept any replayed message whose counter is still in the required range (i.e. bigger than its own counter). This violates immediacy, assuming that only the period between writing a message onto the bus and reading it does not exceed a specified limit. It also violates non-repeatability since the attack is possible even if the replayed message has already been accepted before.The counter synchronization mechanism of GenCnt does not prohibit this attack as synchronization messages themselves are susceptible to delay attacks, i.e. recorded and then invalidated by an attacker by destroying their CRC or by interrupting the message with an error frame. These messages will then not be accepted by the ECUs with the consequence that an unsynchronized ECU cannot be synchronized. It will therefore accept delayed synchronization and functional messages at any later point in time the attacker chooses for a replay, thus violating immediacy. Hence, the synchronization mechanism of the generic counter-based system is no guarantee for ensuring immediacy and non-repeatability.Even if no counter loss occurs, violation of immediacy by a delay of messages cannot be prohibited. This is due to the fact that the counter value stored by the intended recipients of a message does not change as long as all messages relevant for the respective counter are invalidated by the attacker and thus not accepted. Consequently, the intended recipients will accept any relayed message since it still contains a counter being valid from their point of view.One question that comes to mind is whether it would be sufficient to equip the Fresh Value Manager FvM of the GenCnt system with the ability to perform all security checks by the controller in order to avoid the above-described attacks. However, it turns out that this measure alone is not enough. First, the FvM behavior would need to be changed as it must increment its own local counter value with every sent message, independently of whether or not the message is accepted. In other words, the determination of what is the correct counter for a message would need to be adapted to the one used for the BusCnt system. Otherwise, the FvM would not be able to detect the repetition of a message as it would still consider the old counter to be correct. Since the sender of a message that has caused an error frame normally simply resets its counter and resends the message, the FvM would additionally need to adjust the sender’s counter. Secondly, the system would need to be changed to using one single counter per bus since otherwise the FvM is not able to assign an error frame to the counter used in a message that has been interrupted before writing the message ID to the bus. All these changes result in a system that is in some of its main aspects equivalent to the BusCnt system.There are some assumptions in our proof regarding the satisfaction of immediacy and non-repeatability by the BusCnt system that need to be substantiated by specific design decisions. This concerns for example the size of the counter that must prohibit overflow. In the BusCnt system, an attacker can accelerate the pulse generator by inserting messages onto the bus. Independently of being accepted, they will cause the connected ECUs to decrement their counters faster than they normally would. However, in Section7.2.2 below, we discuss the counter length necessary to avoid counter overflow even in the presence of such an attack and show how this length can be implemented in praxis. Other assumptions concern storage errors that we assume never to result in a counter being smaller than the correct one as this could lead to counter overflow as well. This is an issue for all counter-based approaches, adequate measures for detection of such incidents is out of the scope of this paper.A final security aspect concerns the truncation of MACs which in principle enables an attacker to construct its own message and to determine the corresponding truncated MAC by brute force. This holds in particular for synchronization messages. So if an attacker was able to construct and insert a synchronization message containing e.g. the counter 0…0 with a correct MAC, it could take over the whole bus communication. This is an issue for all approaches using MAC truncation (e.g. for AUTOSARs SecOC). As a counter-measure, we have chosen a specific number of failed synchronization messages as indicator of a brute force attack which we deem small enough to recognize such attacks and on the other hand big enough to not cause unnecessary dysfunction of the bus. See Section7.2.2 for more details on this aspect.


### 7.2. Practical Aspects

To evaluate the practical aspects of our work we implemented a proof of concept of BusCount to demonstrate the general feasibility of the mechanisms. Moreover, we want to show the suggested approach can be implemented at a low cost. We first introduce our development setup and describe the design decisions before presenting the evaluation we performed bsaed on this implementation.


#### 7.2.1. Setup

For the implementation of our security enhanced CAN controller, we chose a low-cost FPGA (ICE40HX8K-B-EVN) with only 7680 logic cells and a maximum frequency of 12 MHz. The FPGA is connected with a CAN transceiver (MCP2561) that converts logical CAN messages into physical signals for a CAN bus.We used an open-source implementation1 as a basis for our CAN controller. We extended the controller with an SLCAN2 protocol to communicate with a connected ECU. The ECU is simulated by a Raspberry Pi 2B running a default Linux SocketCAN3. The software does not need to be modified besides the fact that the payload is reduced by the length of the MAC. A second FPGA with the same setup was introduced to perform MAC verifications and synchronization tests. The correctness of the CAN implementation and the compatibility with regular CAN bus devices was evaluated with a remaining bus simulation using a Vector VN5610 in combination with CANoe v9. The hardware setup of our proof of concept (see Figure5) contains:Figure 5
Evaluation setup for BusCount.


#### 7.2.2. Design Decisions

We decided to use a truncated MAC value with a size of 24 bit to be compatible with AUTOSAR SecOC. Since CAN has a very limited message size per package we decided to use the counter implicitly. This requires more explicit synchronizations yet does not disrupt the system’s functionality due to the fast synchronization mechanism of our protocol. Corresponding to the 24 bit MAC the remaining payload of a CAN message is 40 bits. The counter transferred with the described synchronization mechanism would then also be restricted to these 40 bits. A CAN bus can transmit up to 17,543 messages per second [36], thus a 40 bit counter suffices for about 725.4 days 240/17,543⋅60⋅60⋅24 of non-stop communication before an overflow occurs. An attacker may even reduce the duration by starting CAN messages and stopping them immediately with an error frame. This increases the number of messages sent by an attacker (15 bits per message) compared to a regular sender (minimum 44 bits per message) to about 51,459 messages per second 17,543⋅44/15. We consider a counter value that could overflow after only 247.3 days 240/51,459⋅60⋅60⋅24 not sufficient in an attack scenario, thus we increased the counter by additional 18 bits which can be transmitted using the extended message ID of the CAN specification for synchronization messages. The 58 bit counter is sufficient for about 82,884.75 years 258/51,459⋅60⋅60⋅24⋅365. In order to counter brute force attacks and to increase the security of the truncated MAC we suggest renewing the key regularly by deriving it from the current counter value.Furthermore, we needed to make sure the synchronization cannot be attacked by a brute force attack. An attacker may try to forge a synchronization message setting the counter to 0 which would lead to an overflow or would establish the number 0 as the counter value of all subsequent messages. Since we suggest to transfer only a 24 bit MAC, attacks cannot be prevented by the key size. For this reason we count the number of failed synchronizations. If more than 16 failed synchronizations during a car ride or 128 failed synchronizations in total have been detected, the ECUs need to consider the bus no longer trustworthy and must enable the driver to safely stop the car. The 128 synchronizations give an attacker a 0.000977%1281224127/224128 chance to forge a synchronization message successfully. A recovery process for a car network is out of the scope of this paper. Compared to the generic counter-based approach, our synchronization solution has the advantage that it is independent of functional disruptions regarding a central entity (fresh value master): Any ECU can initialize synchronization, and all ECUs join in, sending their respective synchronization messages simultaneously. This mechanism allows the synchronization of all ECUs connected to one bus during the transmission time of only one message.The bus counter-based security protocol does not change the CAN frame and thus it can work with default CAN controllers in one network. The adaptation to CAN FD and CAN XL is also possible. Further, it is compatible with SecOC with respect to the message structure.The introduction of error frames in conjunction with security checks potentially changes the safety considerations of ISO26262 regarding CAN bus communication. A CAN controller sending a message which results in an error frame increments its error counter by 8 while receiving controllers increment their error counter by 1. Successful message transfer reduces the counter by 1. If an error counter exceeds the value 128, the respective controller changes intobus-off mode and is not able to send or receive data anymore and a hardware reset is necessary. However, there are only two cases that our security mechanisms could cause a bus-off state. In the first case, the attacker is the sender of unauthorized messages by delay, replay, or forging of messages. In this scenario, the attacker performs a denial of service attack which she could also perform in every other secure or non-secure CAN BUS by inserting error frames. The second scenario is the startup of a vehicle where every CAN controller is out of synchronization. In the worst case, ECUs might join the network one by one, each of them sending an error frame caused by a failed check based on its wrong counter value, and then initiate a synchronization. To prevent this we suggest that after waking up and before starting to send error frames, a CAN controller first initiates a synchronization in case of an invalid message. Thus, the ECU is in sync as soon as it joins the network.


#### 7.2.3. Performance Evaluation

The CAN controller implementation we adapted to work on the ICE40HX8K consumed 4,483 of the 7,680 logic cells. The remaining logic cells need to be sufficient for processing a MAC algorithm, the synchronization, and the counter mechanism. Moreover, the MAC algorithm needs to be fast enough to calculate the MAC during the transmission of the truncated MAC value (24⋅4=c). The time consumed by the sending process is longer since much more bits are transmitted prior to the truncated MAC value. Finally, the MAC algorithm needs to calculate the MAC over at most 131 bits (58 bit counter value + 29 ID + 4 bit data length + 40 bit data) for classic CAN.The remaining 3,197 cells are not sufficient to implement a regular cipher, like AES or HMAC with SHA2, with low latency together with the counter and synchronization mechanism. For this reason, we evaluated several lightweight ciphers regarding their number of rounds, state size, and table size. Based on these results we implemented our CAN controller in combination with the two CBC-MAC algorithms Present80 [37] and Prince [38] and the HMAC algorithm SipHash [39]. All three have a block size of 64 bit, so two blocks need to be processed at most. We evaluated the number of cycles each algorithm needs for this task. Table 6 shows the results of our evaluation. The number of cycles as well as the number of logical cells needed for the CAN controller including the different ciphers.Table 6
Evaluation of ciphers for secure CAN controller.
AlgorithmCyclesLogic cells (total)Plain CAN controller-4,483SipHash [39]136,024Prince [38]305,947Present80 [37]685,599The smallest (in terms of cells needed) but also the slowest algorithm was Present80. Our implementation of the controller with Present80 needed 5,599 logic cells and 68 cycles for two blocks. Prince only needed 30 cycles while increasing the number of logic cells needed to 5,947. SipHash was only slightly larger with 6,024 logic cells, but needs only 13 cycles to compute a MAC over two blocks. Since the security of Present80 is lower and the number of blocks increases drastically regarding CAN FD (10 blocks for 579 bits of authentic data) and CAN XL (258 blocks for at most 16,466 bits of authentic data), we recommend SipHash for a fast and size efficient MAC algorithm in our approach. Additionally, cryptanalysises [40,41] of SipHash did not reveal problems with this cryptographic primitive.


## 7.1. Security Aspects

One fundamental difference between our approach and the generic counter-based approach is that in the BusCnt system the pulse generator is an integral component of the system itself: The very writing onto the bus causes a change of the local bus counter values of all ECUs connected to it as they inevitably read (part of) the message (even if not accepting it) and decrement their counters. By this read action, the message’s counter and thus its MAC is invalidated. Hence, any subsequent message written onto the bus must use a smaller counter in order to be accepted. This prohibits message delay and replication.Another important aspect is the assignment of computations to the controller that in traditional CAN communication systems is processed by the application layer. This concerns in particular MAC calculation and verification and checks regarding the size of the message’s counter. Performing these checks on controller level enables to use the error frame mechanism of CAN in case of a failed check which in return results in invalidation of the respective message and prevention of its acceptance by any of the ECUs connected to the same bus.These two aspects together allowed to formally prove that the BusCnt system satisfies both immediacy and non-repeatability, provided at least one of the ECUs owns the correct counter. The inevitable decrease of the counter value with every new message prohibits message delay, and the checks performed by the controllers allow immediate invalidation of any manipulated message.One of the core assumptions of our proof is the correctness of at least one counter value in the bus network. It is based on two observations: First, ECUs are designed to be safe and thus hardware or software failures occur significantly less often compared to regular PC hardware. Second, an incorrect counter value may be the result of the shutdown process, as an ECU may not be able to store the counter value in time to persistent storage. However, the likelihood for this failure to occur is reduced in our approach since only a single value per bus needs to be stored. In contrast, traditional counter-based approaches use various counters for different types of messages. Moreover, a bus has a large number of ECUs connected to it and only one needs to store the correct counter value at the end of a ride. Therefore, the probability that our assumption does not hold is insignificant.On the other hand, an ECU not being synchronized, i.e. not owning the correct counter, may in principle cause a safety problem: If it sends a functional message, MAC verification by ECUs owning the correct counter will fail and result into an error frame. If the ECU itself receives a functional message containing the correct counter, its own MAC verification will fail and cause an error frame as well. Too many error frame events will cause the ECU to change into an inactive state. This safety problem can be minimized by adequate synchronization approaches as discussed in Section7.2.2 below.In contrast to the BusCnt system, our proof of the generic counter-based approach indicates that it exhibits several weaknesses. First, it cannot ensure immediacy and non-repeatability (neither of synchronization nor of functional messages) in case an ECU loses its counter. Once being active again the ECU will accept any replayed message whose counter is still in the required range (i.e. bigger than its own counter). This violates immediacy, assuming that only the period between writing a message onto the bus and reading it does not exceed a specified limit. It also violates non-repeatability since the attack is possible even if the replayed message has already been accepted before.The counter synchronization mechanism of GenCnt does not prohibit this attack as synchronization messages themselves are susceptible to delay attacks, i.e. recorded and then invalidated by an attacker by destroying their CRC or by interrupting the message with an error frame. These messages will then not be accepted by the ECUs with the consequence that an unsynchronized ECU cannot be synchronized. It will therefore accept delayed synchronization and functional messages at any later point in time the attacker chooses for a replay, thus violating immediacy. Hence, the synchronization mechanism of the generic counter-based system is no guarantee for ensuring immediacy and non-repeatability.Even if no counter loss occurs, violation of immediacy by a delay of messages cannot be prohibited. This is due to the fact that the counter value stored by the intended recipients of a message does not change as long as all messages relevant for the respective counter are invalidated by the attacker and thus not accepted. Consequently, the intended recipients will accept any relayed message since it still contains a counter being valid from their point of view.One question that comes to mind is whether it would be sufficient to equip the Fresh Value Manager FvM of the GenCnt system with the ability to perform all security checks by the controller in order to avoid the above-described attacks. However, it turns out that this measure alone is not enough. First, the FvM behavior would need to be changed as it must increment its own local counter value with every sent message, independently of whether or not the message is accepted. In other words, the determination of what is the correct counter for a message would need to be adapted to the one used for the BusCnt system. Otherwise, the FvM would not be able to detect the repetition of a message as it would still consider the old counter to be correct. Since the sender of a message that has caused an error frame normally simply resets its counter and resends the message, the FvM would additionally need to adjust the sender’s counter. Secondly, the system would need to be changed to using one single counter per bus since otherwise the FvM is not able to assign an error frame to the counter used in a message that has been interrupted before writing the message ID to the bus. All these changes result in a system that is in some of its main aspects equivalent to the BusCnt system.There are some assumptions in our proof regarding the satisfaction of immediacy and non-repeatability by the BusCnt system that need to be substantiated by specific design decisions. This concerns for example the size of the counter that must prohibit overflow. In the BusCnt system, an attacker can accelerate the pulse generator by inserting messages onto the bus. Independently of being accepted, they will cause the connected ECUs to decrement their counters faster than they normally would. However, in Section7.2.2 below, we discuss the counter length necessary to avoid counter overflow even in the presence of such an attack and show how this length can be implemented in praxis. Other assumptions concern storage errors that we assume never to result in a counter being smaller than the correct one as this could lead to counter overflow as well. This is an issue for all counter-based approaches, adequate measures for detection of such incidents is out of the scope of this paper.A final security aspect concerns the truncation of MACs which in principle enables an attacker to construct its own message and to determine the corresponding truncated MAC by brute force. This holds in particular for synchronization messages. So if an attacker was able to construct and insert a synchronization message containing e.g. the counter 0…0 with a correct MAC, it could take over the whole bus communication. This is an issue for all approaches using MAC truncation (e.g. for AUTOSARs SecOC). As a counter-measure, we have chosen a specific number of failed synchronization messages as indicator of a brute force attack which we deem small enough to recognize such attacks and on the other hand big enough to not cause unnecessary dysfunction of the bus. See Section7.2.2 for more details on this aspect.


## 7.2. Practical Aspects

To evaluate the practical aspects of our work we implemented a proof of concept of BusCount to demonstrate the general feasibility of the mechanisms. Moreover, we want to show the suggested approach can be implemented at a low cost. We first introduce our development setup and describe the design decisions before presenting the evaluation we performed bsaed on this implementation.


### 7.2.1. Setup

For the implementation of our security enhanced CAN controller, we chose a low-cost FPGA (ICE40HX8K-B-EVN) with only 7680 logic cells and a maximum frequency of 12 MHz. The FPGA is connected with a CAN transceiver (MCP2561) that converts logical CAN messages into physical signals for a CAN bus.We used an open-source implementation1 as a basis for our CAN controller. We extended the controller with an SLCAN2 protocol to communicate with a connected ECU. The ECU is simulated by a Raspberry Pi 2B running a default Linux SocketCAN3. The software does not need to be modified besides the fact that the payload is reduced by the length of the MAC. A second FPGA with the same setup was introduced to perform MAC verifications and synchronization tests. The correctness of the CAN implementation and the compatibility with regular CAN bus devices was evaluated with a remaining bus simulation using a Vector VN5610 in combination with CANoe v9. The hardware setup of our proof of concept (see Figure5) contains:Figure 5
Evaluation setup for BusCount.


### 7.2.2. Design Decisions

We decided to use a truncated MAC value with a size of 24 bit to be compatible with AUTOSAR SecOC. Since CAN has a very limited message size per package we decided to use the counter implicitly. This requires more explicit synchronizations yet does not disrupt the system’s functionality due to the fast synchronization mechanism of our protocol. Corresponding to the 24 bit MAC the remaining payload of a CAN message is 40 bits. The counter transferred with the described synchronization mechanism would then also be restricted to these 40 bits. A CAN bus can transmit up to 17,543 messages per second [36], thus a 40 bit counter suffices for about 725.4 days 240/17,543⋅60⋅60⋅24 of non-stop communication before an overflow occurs. An attacker may even reduce the duration by starting CAN messages and stopping them immediately with an error frame. This increases the number of messages sent by an attacker (15 bits per message) compared to a regular sender (minimum 44 bits per message) to about 51,459 messages per second 17,543⋅44/15. We consider a counter value that could overflow after only 247.3 days 240/51,459⋅60⋅60⋅24 not sufficient in an attack scenario, thus we increased the counter by additional 18 bits which can be transmitted using the extended message ID of the CAN specification for synchronization messages. The 58 bit counter is sufficient for about 82,884.75 years 258/51,459⋅60⋅60⋅24⋅365. In order to counter brute force attacks and to increase the security of the truncated MAC we suggest renewing the key regularly by deriving it from the current counter value.Furthermore, we needed to make sure the synchronization cannot be attacked by a brute force attack. An attacker may try to forge a synchronization message setting the counter to 0 which would lead to an overflow or would establish the number 0 as the counter value of all subsequent messages. Since we suggest to transfer only a 24 bit MAC, attacks cannot be prevented by the key size. For this reason we count the number of failed synchronizations. If more than 16 failed synchronizations during a car ride or 128 failed synchronizations in total have been detected, the ECUs need to consider the bus no longer trustworthy and must enable the driver to safely stop the car. The 128 synchronizations give an attacker a 0.000977%1281224127/224128 chance to forge a synchronization message successfully. A recovery process for a car network is out of the scope of this paper. Compared to the generic counter-based approach, our synchronization solution has the advantage that it is independent of functional disruptions regarding a central entity (fresh value master): Any ECU can initialize synchronization, and all ECUs join in, sending their respective synchronization messages simultaneously. This mechanism allows the synchronization of all ECUs connected to one bus during the transmission time of only one message.The bus counter-based security protocol does not change the CAN frame and thus it can work with default CAN controllers in one network. The adaptation to CAN FD and CAN XL is also possible. Further, it is compatible with SecOC with respect to the message structure.The introduction of error frames in conjunction with security checks potentially changes the safety considerations of ISO26262 regarding CAN bus communication. A CAN controller sending a message which results in an error frame increments its error counter by 8 while receiving controllers increment their error counter by 1. Successful message transfer reduces the counter by 1. If an error counter exceeds the value 128, the respective controller changes intobus-off mode and is not able to send or receive data anymore and a hardware reset is necessary. However, there are only two cases that our security mechanisms could cause a bus-off state. In the first case, the attacker is the sender of unauthorized messages by delay, replay, or forging of messages. In this scenario, the attacker performs a denial of service attack which she could also perform in every other secure or non-secure CAN BUS by inserting error frames. The second scenario is the startup of a vehicle where every CAN controller is out of synchronization. In the worst case, ECUs might join the network one by one, each of them sending an error frame caused by a failed check based on its wrong counter value, and then initiate a synchronization. To prevent this we suggest that after waking up and before starting to send error frames, a CAN controller first initiates a synchronization in case of an invalid message. Thus, the ECU is in sync as soon as it joins the network.


### 7.2.3. Performance Evaluation

The CAN controller implementation we adapted to work on the ICE40HX8K consumed 4,483 of the 7,680 logic cells. The remaining logic cells need to be sufficient for processing a MAC algorithm, the synchronization, and the counter mechanism. Moreover, the MAC algorithm needs to be fast enough to calculate the MAC during the transmission of the truncated MAC value (24⋅4=c). The time consumed by the sending process is longer since much more bits are transmitted prior to the truncated MAC value. Finally, the MAC algorithm needs to calculate the MAC over at most 131 bits (58 bit counter value + 29 ID + 4 bit data length + 40 bit data) for classic CAN.The remaining 3,197 cells are not sufficient to implement a regular cipher, like AES or HMAC with SHA2, with low latency together with the counter and synchronization mechanism. For this reason, we evaluated several lightweight ciphers regarding their number of rounds, state size, and table size. Based on these results we implemented our CAN controller in combination with the two CBC-MAC algorithms Present80 [37] and Prince [38] and the HMAC algorithm SipHash [39]. All three have a block size of 64 bit, so two blocks need to be processed at most. We evaluated the number of cycles each algorithm needs for this task. Table 6 shows the results of our evaluation. The number of cycles as well as the number of logical cells needed for the CAN controller including the different ciphers.Table 6
Evaluation of ciphers for secure CAN controller.
AlgorithmCyclesLogic cells (total)Plain CAN controller-4,483SipHash [39]136,024Prince [38]305,947Present80 [37]685,599The smallest (in terms of cells needed) but also the slowest algorithm was Present80. Our implementation of the controller with Present80 needed 5,599 logic cells and 68 cycles for two blocks. Prince only needed 30 cycles while increasing the number of logic cells needed to 5,947. SipHash was only slightly larger with 6,024 logic cells, but needs only 13 cycles to compute a MAC over two blocks. Since the security of Present80 is lower and the number of blocks increases drastically regarding CAN FD (10 blocks for 579 bits of authentic data) and CAN XL (258 blocks for at most 16,466 bits of authentic data), we recommend SipHash for a fast and size efficient MAC algorithm in our approach. Additionally, cryptanalysises [40,41] of SipHash did not reveal problems with this cryptographic primitive.


## 7.2.1. Setup

For the implementation of our security enhanced CAN controller, we chose a low-cost FPGA (ICE40HX8K-B-EVN) with only 7680 logic cells and a maximum frequency of 12 MHz. The FPGA is connected with a CAN transceiver (MCP2561) that converts logical CAN messages into physical signals for a CAN bus.We used an open-source implementation1 as a basis for our CAN controller. We extended the controller with an SLCAN2 protocol to communicate with a connected ECU. The ECU is simulated by a Raspberry Pi 2B running a default Linux SocketCAN3. The software does not need to be modified besides the fact that the payload is reduced by the length of the MAC. A second FPGA with the same setup was introduced to perform MAC verifications and synchronization tests. The correctness of the CAN implementation and the compatibility with regular CAN bus devices was evaluated with a remaining bus simulation using a Vector VN5610 in combination with CANoe v9. The hardware setup of our proof of concept (see Figure5) contains:Figure 5
Evaluation setup for BusCount.


## 7.2.2. Design Decisions

We decided to use a truncated MAC value with a size of 24 bit to be compatible with AUTOSAR SecOC. Since CAN has a very limited message size per package we decided to use the counter implicitly. This requires more explicit synchronizations yet does not disrupt the system’s functionality due to the fast synchronization mechanism of our protocol. Corresponding to the 24 bit MAC the remaining payload of a CAN message is 40 bits. The counter transferred with the described synchronization mechanism would then also be restricted to these 40 bits. A CAN bus can transmit up to 17,543 messages per second [36], thus a 40 bit counter suffices for about 725.4 days 240/17,543⋅60⋅60⋅24 of non-stop communication before an overflow occurs. An attacker may even reduce the duration by starting CAN messages and stopping them immediately with an error frame. This increases the number of messages sent by an attacker (15 bits per message) compared to a regular sender (minimum 44 bits per message) to about 51,459 messages per second 17,543⋅44/15. We consider a counter value that could overflow after only 247.3 days 240/51,459⋅60⋅60⋅24 not sufficient in an attack scenario, thus we increased the counter by additional 18 bits which can be transmitted using the extended message ID of the CAN specification for synchronization messages. The 58 bit counter is sufficient for about 82,884.75 years 258/51,459⋅60⋅60⋅24⋅365. In order to counter brute force attacks and to increase the security of the truncated MAC we suggest renewing the key regularly by deriving it from the current counter value.Furthermore, we needed to make sure the synchronization cannot be attacked by a brute force attack. An attacker may try to forge a synchronization message setting the counter to 0 which would lead to an overflow or would establish the number 0 as the counter value of all subsequent messages. Since we suggest to transfer only a 24 bit MAC, attacks cannot be prevented by the key size. For this reason we count the number of failed synchronizations. If more than 16 failed synchronizations during a car ride or 128 failed synchronizations in total have been detected, the ECUs need to consider the bus no longer trustworthy and must enable the driver to safely stop the car. The 128 synchronizations give an attacker a 0.000977%1281224127/224128 chance to forge a synchronization message successfully. A recovery process for a car network is out of the scope of this paper. Compared to the generic counter-based approach, our synchronization solution has the advantage that it is independent of functional disruptions regarding a central entity (fresh value master): Any ECU can initialize synchronization, and all ECUs join in, sending their respective synchronization messages simultaneously. This mechanism allows the synchronization of all ECUs connected to one bus during the transmission time of only one message.The bus counter-based security protocol does not change the CAN frame and thus it can work with default CAN controllers in one network. The adaptation to CAN FD and CAN XL is also possible. Further, it is compatible with SecOC with respect to the message structure.The introduction of error frames in conjunction with security checks potentially changes the safety considerations of ISO26262 regarding CAN bus communication. A CAN controller sending a message which results in an error frame increments its error counter by 8 while receiving controllers increment their error counter by 1. Successful message transfer reduces the counter by 1. If an error counter exceeds the value 128, the respective controller changes intobus-off mode and is not able to send or receive data anymore and a hardware reset is necessary. However, there are only two cases that our security mechanisms could cause a bus-off state. In the first case, the attacker is the sender of unauthorized messages by delay, replay, or forging of messages. In this scenario, the attacker performs a denial of service attack which she could also perform in every other secure or non-secure CAN BUS by inserting error frames. The second scenario is the startup of a vehicle where every CAN controller is out of synchronization. In the worst case, ECUs might join the network one by one, each of them sending an error frame caused by a failed check based on its wrong counter value, and then initiate a synchronization. To prevent this we suggest that after waking up and before starting to send error frames, a CAN controller first initiates a synchronization in case of an invalid message. Thus, the ECU is in sync as soon as it joins the network.


## 7.2.3. Performance Evaluation

The CAN controller implementation we adapted to work on the ICE40HX8K consumed 4,483 of the 7,680 logic cells. The remaining logic cells need to be sufficient for processing a MAC algorithm, the synchronization, and the counter mechanism. Moreover, the MAC algorithm needs to be fast enough to calculate the MAC during the transmission of the truncated MAC value (24⋅4=c). The time consumed by the sending process is longer since much more bits are transmitted prior to the truncated MAC value. Finally, the MAC algorithm needs to calculate the MAC over at most 131 bits (58 bit counter value + 29 ID + 4 bit data length + 40 bit data) for classic CAN.The remaining 3,197 cells are not sufficient to implement a regular cipher, like AES or HMAC with SHA2, with low latency together with the counter and synchronization mechanism. For this reason, we evaluated several lightweight ciphers regarding their number of rounds, state size, and table size. Based on these results we implemented our CAN controller in combination with the two CBC-MAC algorithms Present80 [37] and Prince [38] and the HMAC algorithm SipHash [39]. All three have a block size of 64 bit, so two blocks need to be processed at most. We evaluated the number of cycles each algorithm needs for this task. Table 6 shows the results of our evaluation. The number of cycles as well as the number of logical cells needed for the CAN controller including the different ciphers.Table 6
Evaluation of ciphers for secure CAN controller.
AlgorithmCyclesLogic cells (total)Plain CAN controller-4,483SipHash [39]136,024Prince [38]305,947Present80 [37]685,599The smallest (in terms of cells needed) but also the slowest algorithm was Present80. Our implementation of the controller with Present80 needed 5,599 logic cells and 68 cycles for two blocks. Prince only needed 30 cycles while increasing the number of logic cells needed to 5,947. SipHash was only slightly larger with 6,024 logic cells, but needs only 13 cycles to compute a MAC over two blocks. Since the security of Present80 is lower and the number of blocks increases drastically regarding CAN FD (10 blocks for 579 bits of authentic data) and CAN XL (258 blocks for at most 16,466 bits of authentic data), we recommend SipHash for a fast and size efficient MAC algorithm in our approach. Additionally, cryptanalysises [40,41] of SipHash did not reveal problems with this cryptographic primitive.


## 8. Conclusions and Future Work

In this paper, we have presented a detailed discussion and formal evaluation of our hardware-based approach BusCount for the security protection of automotive CAN networks. We further opposed this to the characteristics of counter-based approaches currently being used.The fundamental difference between currently considered approaches and ours is that in ours the pulse generator is an integral component of the system itself: The very writing onto a bus causes a change of the counter values of all ECUs connected to it as they inevitably read the message (even if not accepting it) and decrement their counters. Since the number of messages sent on the bus cannot be manipulated, the correct counter value cannot be manipulated as well. By this read action, the message’s counter and thus its MAC is invalidated. Another important aspect is the assignment of MAC calculation and verification and checks regarding the size of the message’s counter to the controller. This enables to use the error frame mechanism of CAN communication in case of a failed check which results in invalidation of all messages whose MAC is not based on the correct counter value. These messages will then not be accepted by any of the ECUs. Software-based approaches do not have this possibility since they verify the MAC on application-level after the controller completely received the message.We formally proved that our bus counter approach satisfies data origin authenticity as well as immediacy and non-repeatability (also denoted by message freshness), both during regular operation and in case an ECU loses its counter. Our proof is based on the assumption that simultaneous loss of counter values does not occur, i.e. that there is always at least one ECU per bus owning the correct value. This assumption seems appropriate, given the low possibility of it being violated. It enables our synchronization mechanism to take advantage of the physical characteristics of a CAN bus and ensures that always the correct counter value is sent.On the other hand, current counter-based systems cannot assure message freshness if an ECU loses its counter. Immediacy is even violated in case an ECU does not lose its counter: An attacker can invalidate all messages relevant for a specific counter and insert them again at a later point in time without the ECU being able to notice this manipulation. This is due to the fact that the ECU’s local counter value only changes if it actually accepts a message.Compared to other approaches, our bus counter mechanism offers several practical advantages: It avoids the necessity to include (parts of) the counter in the messages which saves bandwidth, and it requires only one counter per bus to be stored instead of one counter per message ID favored by currently discussed approaches. This reduces both storage capacities and the risk of ECUs being unsynchronized.The synchronization solution of BusCount has the advantage that it is independent of functional disruptions regarding a central fresh value master that is being used by other counter-based approaches: Any ECU can initialize synchronization, and all ECUs join in, sending their respective synchronization messages simultaneously. This mechanism allows the synchronization of all ECUs connected to the same bus during the transmission time of only one message.It must be noted that our approach cannot be realized with currently available ECUs. On the other hand, it does not change the CAN frame and can thus work with default CAN controllers in one network. It can also be adapted to CAN FD and CAN XL and is compatible with SecOC with respect to the message structure. Moreover, our proof of concept implementation described in Section7.2 shows that our approach is not only theoretically interesting, but is functionally working in a CAN network. However, an implementation needs to respect a couple of considerations. One of them is that our approach allows pulse acceleration, hence the counter must be sufficiently long in order to prohibit counter overflow during the lifetime of a car. We consider 58 bits as suggested in Section 7.2.2 adequate. Further, a concrete synchronization mechanism must for example prohibit brute force attacks on truncated MACs of synchronization messages and must ensure a synchronized network as soon as possible after the startup process.In the future, we plan to extend our attack model and address an adversary that can manipulate devices connected to the bus. One possible countermeasure that at least reduces the severity of this attack is to assign specific roles to different ECUs and to enable ECUs to authentically identify the sender of messages. Hence, we plan to investigate how our approach can be extended by sender authentication mechanisms. Further, we will explore whether and how techniques to protect the devices’ integrity can be integrated in order to prohibit manipulation of genuine ECUs.



---

*Source: 9951777-2021-11-30.xml*