Design & Verif. of a LAKE Process for Secure M2M Communication

Meta-Information

Origin: Sibylle Fröschle / OFFIS, Marlon Gräfing / OFFIS

Written: April 2019

Purpose: Pattern for design and verification of a location-based authentication and key establishment (LAKE) process for secure M2M communication.
Many processes of ACPS’ require a secure channel for M2M communication, and hence, a secure authentication and key establishment (AKE) process that sets up a shared secret between the communicating parties. In the context of M2M communication one can often make use of the location of the parties, and thereby obtain a simple and yet highly resilient AKE process.
This pattern supports the development of a location-based AKE (LAKE) process. The pattern builds on a systematization of aspects common to LAKE processes and previously identified designs and verification templates. These can either be used directly or adapted to a new situation.

To consider: this V&V pattern needs a significant number of human experts (see “participants”).

Structure

Adaption & Verification:

Participants and Important Artefacts

Participants:

ACPS Process Engineer: Expert on the process that is to be automatized with the help of M2M communication.

Risk Analyst: Expert on the security risks and their safety impact.

Systems Engineer: Responsible for overall design and verification.

Artefacts:

High-Level Attack Goals: Given a setting with two machines of different type to be paired there are five categories of attacks the attacker can aim for : Man-in-the-Middle attack, Impersonation to first machine, Impersonation to second machine, Mismatch of first machine, Mismatch of second machine. There are also several sub-categories of mismatch attacks such as location and service mismatch. Combinations are also possible. These high-level attack categories provide the interface to safety analysis.

Criticality Mapping: It is decided and documented which of the high-level attack goals are critical. For example, in UC7 it is highly safety-critical if the attacker achieves „Impersonation to ground unit“ but less critical if the attacker achieves „Impersonation to airplane“. The reason is that the physical control lies with the ground unit, which will act based on sensor values sent over the communication channel.

Requirements Pattern: These patterns concern correctness, security, and resilience against attacks. The pattern structure is as follows: There is a top-level requirement for correctness of the setup of the two machines to be paired. This is refined into requirements on the physical setup and requirements on the LAKE process. The LAKE requirements are refined into requirements on the underlying security protocol, the underlying channel (e.g. the NFC system in UC7) and constraints on actions of human operators and the operational environment. In addition, there are requirements patterns that address resilience against parallel escalation of attacks, and resilience against compromise of long-term keys.

Performance & other Criteria: For example, timing constraints on the duration of the key establishment process.

Requirements: This is the identified set of necessary requirements from the last two categories.

LAKE Verified Design Patterns: LAKE is very generic. Hence, it is likely that a previous design matches the requirements of the new ACPS process. Currently, there are several verified designs for the TAGA use case. Moreover, we expect that they are exhaustive wrt an abstraction of TAGA and the criteria of LAKE.

Verification Results: The collection of models and proofs that establish that an element satisfies the requirements as prescribed by the requirements pattern.

Derived Tests: Some models and tools will allow the derivation of tests to be run against a higher-level model or the implementation.

Actions/Collaborations

(1) Safety Impact Analysis: ACPS Expert and Risk Analyst work through the list of systematized LAKE attack goals and assign a criticality to each attack goal relative to the new ACPS process.

(2) Derivation of Requirements: ACPS Expert, Risk Analyst and Systems Engineer derive requirements from this criticality map and other criteria such as constraints concerning performance and resources. (E.g. at most one operator, at most t time.) The requirements pattern help to tune and express this in a way suitable for the next step.

(3) Match to Design Pattern: Systems Engineer checks whether there is already an existing pattern that matches the requirements of the new ACPS process. If this is the case go to step 5.

(4) Adaptation & Verification: Systems Engineer (in collaboration with suitable experts) identifies process elements that need to be adapted or newly developed. We distinguish between several types of process elements: security protocols & APIs, mechanisms built-in/based on the ACPS process itself, procedures do to with the course of the pairing and preparing the „machines“ for the process (often involving humans), technical artefacts supporting some procedure. Each of these elements goes through their own D&V process carried out by corresponding experts.

(5) High-Level Verification: Systems Engineer with verification experts carry out a high-level verification. This verifies that a model of the overall process (including resilience measures and IDS) satisfies the high-level requirements. Examples are timing aspects (detection of impersonation within a certain time, overall performance), resilience under attack injection including denial-of-service, etc. based on properties of elements verified in Step 4 or from the database of verified patterns. This could involve formal verification and/or simulative evaluation of an executable model.

Discussion

Notes on experts:

– The roles „ACPS Process Engineer“ and „Systems Engineer“ can be assumed by the same person.

– When an existing LAKE design is used no more experts are needed.

– When new elements need to be introduced other experts might need to be involved: e.g. expert for security protocols, expert for formal verification of timing experts.

Benefits/Limitations: If a new situation is encountered, and there is no good match with an existing pattern then considerable manual effort might be required. However, there are probably not that many patterns so that there might be a point of complete coverage.

Comments: We expect that step 2 and 3 can be fully automated.

Application Example

ENABLE-S3 UC7 “Touch and Go Assistant (TAGA)”: The first LAKE design patterns and verification templates are developed bottom-up by analysis of the TAGA use case: a shared key for M2M communication between an Aircraft and a Gound Unit for efficient ground services is established using local trust anchors and a mobile unit with NFC interface.

Comments:

– High-Level Verification is currently available by manual proofs that establish how the top-level correctness goals follow from requirements on the protocols, the NFC system, and further process measures.

– For the properties on protocols the protocol verifier TAMARIN is used.

– Tool-support for High-Level Verification could e.g. be provided by EventB.

Relations to other Patterns

Pattern Name	Relation
Formalized Analysis and Verification	Uses (also) formal methods; application example uses also EventB
Scenario-based Safety & Security Analysis	Can help in steps 1 and 2