Merge pull request #46 from felixlinker/master

2 approvals by the editors. open for more than a week.

Formal Analysis Results

main.md

@@ -68,7 +68,7 @@ This draft uses the terms and definitions from [@!OpenID4VP], section 2.
 
 ## Admission control at a venue 
 
-The user needs to present her electronic ticket (represented by a verifiable credentioal) when entering a venue. She opens her wallet and authenticates towards the wallet. She then scans the QR code at the entrance with her wallet. The wallet determines the credential (the ticket) required by the verifier and asks for consent to share the respective credential. The credential is then transmitted to the verifier, which, after validation, allows her to enter the venue, e.g. by opening the turnstile.  
+The user needs to present her electronic ticket (represented by a verifiable credential) when entering a venue. She opens her wallet and authenticates towards the wallet. She then scans the QR code at the entrance with her wallet. The wallet determines the credential (the ticket) required by the verifier and asks for consent to share the respective credential. The credential is then transmitted to the verifier, which, after validation, allows her to enter the venue, e.g. by opening the turnstile.
 
 # Overview 
 
@@ -85,14 +85,14 @@ Wallet and the Verifier MUST implement BLE according to the [@!Bluetooth.4.2.Cor
 
 ## Limitations
 
-The following limitations in BLE stack 4.2 need to be considerate: 
+The following limitations in BLE stack 4.2 need to be considered:
 
 1. Advertisement
     * The advertisement message can contain only a max. of 23 bytes in the request and 27 bytes in response.
     * The advertisement scan request can not have any custom data.
     * The scan response can have custom data. 
 2. Timing
-    * BLE Scanning and advertising are discrete events, so not every advertisement is received (an advertisment is sent for at most 30s) 
+    * BLE Scanning and advertising are discrete events, so not every advertisement is received (an advertisement is sent for at most 30s)
 3. Throughput
     * The data rate, which can be expected, is about 0.10 Mbps. 
     * The calculation is as follows: 
@@ -140,7 +140,7 @@ Note: The arrow mark indicates a read or write by the wallet.
    * "-->" Read by wallet
    * "<--" Write by wallet
 
-1. Verifier and the Wallet establish the connection. This specification defines two mechanisms to do so: A QR code displayed by the Verifier and BLE Advertisement initiated by the Verifier. The Wallet obtains the advertisment data, including the Verifier's ephemeral key, using one of those messages. It then creates its own ephemeral key and derives the session secret key as defined in (#encryption). 
+1. Verifier and the Wallet establish the connection. This specification defines two mechanisms to do so: A QR code displayed by the Verifier and BLE Advertisement initiated by the Verifier. The Wallet obtains the advertisement data, including the Verifier's ephemeral key, using one of those messages. It then creates its own ephemeral key and derives the session secret key as defined in (#encryption).
 2. The Wallet sends its identification information to the Verifier, which also derives the session secret key as defined in (#encryption). All sub-sequent communication is encrypted using this session key.  
 3. The Wallet reads the Presentation Request from the Verifier. 
 4. The Wallet authenticates the user and obtains consent to share the Credential(s) with the Verifier.
@@ -182,8 +182,8 @@ The following figure shows the message exchange.
 
 Pre-requisites: The Verifier has opened it's application and started the mode that accepts OpenID4VP.
 
-1. The Verifier starts the BLE advertisement (`PDU ADV_IND`) using the service UUID `00000001-5026-444A-9E0E-D6F2450F3A77`. The advertisment message starts with the prefix `OVP` (see below) and includes the first 5 bytes of the verifier's ephemeral key.
-2. The Wallet scans the BLE layer and sends a `SCAN_REQ` to the Verifier acknowledging the advertisment. If there is only a single Verifier sending an advertisment message with the `OVP` prefix, the Wallet may automatically select this Verifier. Otherwise, if there are multiple verifiers the user is asked to choose. 
+1. The Verifier starts the BLE advertisement (`PDU ADV_IND`) using the service UUID `00000001-5026-444A-9E0E-D6F2450F3A77`. The advertisement message starts with the prefix `OVP` (see below) and includes the first 5 bytes of the verifier's ephemeral key.
+2. The Wallet scans the BLE layer and sends a `SCAN_REQ` to the Verifier acknowledging the advertisement. If there is only a single Verifier sending an advertisement message with the `OVP` prefix, the Wallet may automatically select this Verifier. Otherwise, if there are multiple verifiers the user is asked to choose.
 3. On Receiving the `SCAN_REQ`, the verifier sends a `SCAN_RESP` to the particular Wallet using the service UUID `00000002-5026-444A-9E0E-D6F2450F3A77`. This request contains the remaining 27 byte of the Verifier's ephemeral key.
 4. The Wallet generates its ephemeral key pair and combines both keys to create a DHE secret key as described in (#encryption). The Wallet then sends an identify request (`IDENTIFY_REQ`, see (#identify-ble-request)) and submits its public key to the verifier in plain text. The Verifier calculates the DHE secret key based on its key pair and the wallet's public key as described in (#encryption).
 
@@ -384,9 +384,12 @@ MUST not be present if a 'scope' parameter is present.
 * `scope`: CONDITIONAL. The scope value MUST represent a credential presentation request. This parameter MUST NOT be present if a `presentation_definition` parameter is present. 
 * `nonce`: REQUIRED. This value is used to securely bind the verifiable presentation(s) provided by the wallet to the particular transaction.
 * `aud`: OPTIONAL. This value identifies the wallet issuer (as intended recipient of the presentation request).
+* `ble_key`: REQUIRED. A hash of the verifier's ephemeral key used in this connection.
 
 The parameters `response_type` and `redirect_uri` MUST NOT be present in the request.
 
+When a wallet receives such a request, it MUST verify that it was sent over a BLE channel established with the ephemeral key provided in the request, and it MUST verify the request's signature.
+
 The following is a non normative example of a request before signing:
 ```json
 {
@@ -439,6 +442,9 @@ On the BLE layer, the transmission of the payload is performed as described in (
 
 The response contains the parameters as defined in Section 6 of [!@OpenID4VP] in JSON encoding. 
 
+The nonce signed as part of the `vp_token` MUST be computed by computing the hash of the nonce provided in the OpenID4VP request (see (#identify-request)) and the wallet's ephemeral key used to establish the BLE channel.
+Naturally, when the verifier receives the token, they MUST compute the nonce themselves and verify that they received it over the correct BLE channel.
+
 The following is a non normative example of a response before signing:
 
 ```json
@@ -510,17 +516,29 @@ Verifier Service UUID for SCAN_RESP MUST be `00000002-5026-444A-9E0E-D6F2450F3A7
 
 # Security Considerations {#security}
 
+## Desired Security Properties
+
+This specification aims to provide three security properties:
+
+* Secrecy: Wallets never leak verifiable presentation tokens sent.
+* Authentication: Whenever a verifier accepts a verifiable presentation token, it was sent by an honest wallet and that wallet sent the token to that verifier.
+* Replay protection: Every verifiable presentation token is accepted exactly once.
+
 ## Session Information
 
 Both wallet and the Verifier MUST remove all the information about the session after its termination.
 
 ## Verifier Authentication
 
-How does the wallet authenticate the Verifier? The verifier signs the presentation request. 
+The wallet authenticates the verifier by verifying the signature of the presentation request.
+We assume that the wallet has been configured with an authentic public key of the verifier in advance.
+This could be achieved via cached public keys or trust chains of the verifier.
 
 ## Session Binding
 
-How does the Verifier know a particular response is tied to a particular request? It evaluates the nonce and aud value of the presentation to match the nonce of the request and its client id. 
+The wallet can authenticate the BLE channel by verifying that they established the connection with the ephemeral key contained in the request's `ble_key` field (see (#identify-request)).
+The verifier can authenticate the BLE channel by verifying `aud` and the nonce of the verifiable presentation token (see (#identify-response)).
+Namely, the verifier checks that the `aud` value matches its client ID, and that the nonce contained in the token is a hash of the wallet's ephemeral key, and the nonce provided in the request by the verifier.
 
 {backmatter}