Rework the description of key derivation output/verify key

Some of the fallback mechanisms between the entry points were not described
corrrectly.

Signed-off-by: Gilles Peskine <Gilles.Peskine@arm.com>

Author: gilles-peskine-arm

docs/proposed/psa-driver-interface.md

@@ -473,11 +473,22 @@ The core calls a key derivation driver's output entry point when the application
 
 If the key derivation's `PSA_KEY_DERIVATION_INPUT_SECRET` input is in a secure element and the derivation operation is handled by that secure element, the core performs the following steps:
 
-1. For a call to `psa_key_derivation_output_key()` where the derived key is in the same secure element, if the driver has an `"key_derivation_output_key"` entry point, call that entry point. If the driver has no such entry point, or if that entry point returns `PSA_ERROR_NOT_SUPPORTED`, continue with the following steps, otherwise stop.
-1. For a call to `psa_key_derivation_output_key()`, if the driver's capabilities indicate that its `"import_key"` entry point does not support the derived key, stop and return `PSA_ERROR_NOT_SUPPORTED`.
-1. For a call to `psa_key_derivation_verify_key()`, if the driver has a `"key_derivation_verify_key"` entry point, call it and stop.
-1. For a call to `psa_key_derivation_verify_key()` or `psa_key_derivation_verify_bytes()`, if the driver has a `"key_derivation_verify_bytes"` entry point, call the driver's `"export_key"` entry point on the key object that contains the expected value, call the `"key_derivation_verify_bytes"` entry point on the exported material, and stop.
-1. Call the `"key_derivation_output_bytes"` entry point. The core may call this entry point multiple times to implement a single call from the application when deriving a cooked (non-raw) key as described below, or if the output size exceeds some implementation limit.
+* For a call to `psa_key_derivation_output_key()`:
+
+    1. If the derived key is in the same secure element, if the driver has an `"key_derivation_output_key"` entry point, call that entry point. If the driver has no such entry point, or if that entry point returns `PSA_ERROR_NOT_SUPPORTED`, continue with the following steps, otherwise stop.
+    1. If the driver's capabilities indicate that its `"import_key"` entry point does not support the derived key, stop and return `PSA_ERROR_NOT_SUPPORTED`.
+    1. Otherwise proceed as for `psa_key_derivation_output_bytes()`, then import the resulting key material.
+
+* For a call to `psa_key_derivation_verify_key()`:
+    1. For ``psa_key_derivation_verify_key()` only: if the driver has a `"key_derivation_verify_key"` entry point, call it and stop.
+    1. Call the driver's `"export_key"` entry point on the key object that contains the expected value, then proceed as for `psa_key_derivation_verify_bytes()`.
+
+* For a call to `psa_key_derivation_verify_bytes()`:
+    1. If the driver has a `"key_derivation_verify_bytes"` entry point, call the driver's , call the `"key_derivation_verify_bytes"` entry point on the expected output, then stop.
+    1. Otherwise, proceed as for `psa_key_derivation_output_bytes()`, and compare the resulting output to the expected output inside the core..
+
+* For a call to `psa_key_derivation_output_bytes()`:
+    1. Call the `"key_derivation_output_bytes"` entry point. The core may call this entry point multiple times to implement a single call from the application when deriving a cooked (non-raw) key as described below, or if the output size exceeds some implementation limit.
 
 If the key derivation operation is not handled by an opaque driver as described above, the core calls the `"key_derivation_output_bytes"` from the applicable transparent driver (or multiple drivers in succession if fallback applies). In some cases, the core then calls additional entry points in the same or another driver: