Mobile Driver's License (mDL) Verification Tools

This repository contains supplementary materials and code for verifying the mDL protocol, encompassing both formal modeling and dynamic analysis:

• The mdl_modeling directory contains a ProVerif-based framework for generating formal models and verifying security properties.
• The mdl_verif directory contains a tool for dynamic differential analysis of real-world mDL verifier applications.

Model Generation Framework (mdl_modeling)

MDL Authentication Process

Here we use simplified pseudocode to show how the IA, mDL, and Reader interact with each other to ensure an mDL's authenticity.

Initial Setup on IA (Simplified):

issuerSigned = [(randNum1, salt1, itemId1, itemValue1),...,(randNum3, salt3, ItemId3, itemValue3)]
issuerAuth(MSO) = [sign(issuerSigned, issuerPrivateKey),{randNum1: digest(randNum1, salt1, itemId1, itemValue1),...,randNum3: digest(randNum3, salt3, itemId3, itemValue3)}]

IA sends MSO and issuerSigned to Bob

Data Exhchange Phase on Reader (Simplified):

readerAuthentication = (SessionTranscript, ItemsRequest)
readerAuth = sign(readerAuthentication)
deviceRequest = (readerAuth, ItemsRequest)

Reader sends DeviceRequest to mDL (Bob).

Data Exhchange Phase on mDL (Simplified):

deviceAuthentication = (SessionTranscript, DocType, DeviceNameSpace)
deviceAuth = sign(deviceAuthentication)

deviceResponse = (DocType, issuerSigned, deviceAuth, DeviceNameSpace)

Bob sends deviceResponse to Reader.

Verification Phase on mDL (Simplified):

if (verify(readerAuth)){
 	mdoc_reader_authentication = true
}

Verification Phase on Reader (Simplified):

if (verify(deviceAuth)){
 	mdoc_authentication = true
}

if (verify(issuerAuth)){
	issuer_data_authentication = true
}

Formal Model Process

Here are the steps (simplified pseudocode) in our formal model that simulate the authentication process of a mDL.

Step 4:

Issuer Process:
issuer_auth = (sign((doc_type, data, digests of data), secretKey), digests of data)

Step 6:

Reader Process:
reader_signature = sign(mDL request, secretKey)

mDL Process:
reader_authenticated = verify(reader_signature, mDL request , publicKey)

Step 7:

mDL Process:
device_auth = sign(mDL response, secretKey)

Step 9:

Reader Process:
device_authenticated = verify(device_auth, mDL response, secretKey)
issuer_authenticated = verify(issuer_auth, doc_type + data, secretKey)

Formal Model Queries

The following are the queries run by our formal model to verify the basic properties BP1-BP4.

Query for Forgery (BP1):

query event(issuer_authenticated(doc_type, any_data, gen_pk(generate_skey(two(id, device))))) ==> event(ia_sign(doc_type, any_data, gen_pk(generate_skey(two(id, device))))).

Query for Cloning (BP2):

query event(item_accept(doc_type, any_data, show_presence(id, sess_key), sess_key)) ==> event(ia_sign(doc_type, any_data, gen_pk(generate_skey(two(id, device)))))

Query for Eavesdropping (BP3):

query attacker(my_given_name)

Query for Unauthorized Access (BP4):

query event(reader_authenticated(mdl_doc_type, sign(some_reader_auth_bytes, some_reader_skey), gen_pk(some_reader_skey), sess_key)) ==> event(reader_sign(mdl_doc_type, some_reader_auth_bytes, generate_skey(reader_identity), sess_key)).

Open-Sourced Code

The generated/ directory is automatically generated code by running generate.sh.

Within the generated/ directory

• basic_queries/on/ contains ProVerif models for verifying four basic properties using M_mDL
• basic_queries/off/ is verifying four basic properties using M^'_mDL
• extended_queries/on/ is verifying 11 real-world scenarios using M_mDL
• extended_queries/off/ is verifying 11 real-world scenarios using M^'_mDL

The m4/ directory contains the source code of this framework, we have

• m4/basic_queries/ are "scenario modules" used to generate both M_mDL and M^'_mDL for verifying basic properties.
• m4/extended_queries/ are "scenario modules" used to generate both M_mDL and M^'_mDL for verifying 11 real-world scenarios.
• m4/gadgets/ are "component modules" used to reduce duplicate code and improve flexibility.
• m4/mdl.m4 is the "main module" that models the M_mDL, including shared code such as all security mechanisms.

Usage

To illustrate how our framework aids its adaptability, we explain how to extend Scenario 7, "Accessing Federal Buildings" m4/extended_queries/11.7_accessing_federal_buildings.m4, to include Scenarios 4, "Purchasing Alcohol" m4/extended_queries/11.4_purchasing_alcohol.

In this instance, the business question differs: Scenario 7 focuses on authentication, while Scenario 4 concentrates on the mDL holder's age verification. To accommodate this shift, we specialize the component module BUSINESS_QUESTIONS by partially overriding its holder's name authentication to age authentication.

Additionally, the IA issuance procedure differs for the new scenario. To verify Scenario 7, we prohibit the attacker from acquiring an mDL from IA. However, to verify Scenario 4, we need to allow an attacker to obtain an mDL, but not with the data item age_over_21=TRUE. To achieve this, we specialize the component module MDL_SIGNING, and partially override its signing procedure to set age_over_21 to TRUE only if the applicant is not the attacker.

Other procedures also require modification, such as calculating digests for different items. To implement these changes, we import a component module, HASH_CHECK. Specifically, we modify the reader's behavior by customizing the MDL_VERIFY module and invoking HASH_CHECK(age_over_21) within it to verify different items in our formal model.

Dynamic Analysis Tool (mdl_verif)

This tool is used for differential analysis of real-world mDL applications. It allows us to automatically test mDL verifier apps against various security properties and detect potential vulnerabilities.

Tool Components

• main.py: The entry point that coordinates the testing process between holder and reader devices
• security_goals: Defines various security properties and test cases to be verified
• apps: Contains mDL verifier applications that are subject to testing
• lib: Utility libraries for device interaction, verification, and result analysis

mDLVerifWorker

The mDLVerifWorker is an Android-based worker component that facilitates the testing process:

• Provides implementation of both mDL holder and reader functionality
• Supports interaction with real mDL apps through Android's Identity Credential API
• Enables creation of test mDL credentials with modified security properties
• Facilitates communication between the holder device and verifier app

Workflow

1. The tool connects to two Android devices via ADB - one acting as the mDL holder and another as the reader
2. It installs and configures the necessary test applications
3. For each security goal, it creates test credentials with both valid and invalid properties
4. It then conducts differential analysis by comparing how verifier apps respond to these different credentials
5. Results are logged and analyzed to identify potential security vulnerabilities

This dynamic testing complements the formal verification approach, allowing us to validate our theoretical findings against real-world implementations.