diff --git a/1.0/openid-4-verifiable-presentations-1_0.md b/1.0/openid-4-verifiable-presentations-1_0.md
index 915752f7..44169951 100644
--- a/1.0/openid-4-verifiable-presentations-1_0.md
+++ b/1.0/openid-4-verifiable-presentations-1_0.md
@@ -1769,6 +1769,10 @@ While breaking changes to the specifications referenced in this specification ar
# Security Considerations {#security_considerations}
+## Formal Security Analysis
+
+The security properties of the OpenID for Verifiable Credentials family of specifications have been formally analyzed, see [@secanalysis.openid4vc].
+
## Preventing Replay of Verifiable Presentations {#preventing-replay}
An attacker could try to inject Presentations obtained from (for example) a previous Authorization Response into another Authorization Response, thus impersonating the End-User that originally presented the respective Verifiable Presentation. Holder Binding aims to prevent such attacks.
@@ -2357,7 +2361,6 @@ Ecosystems intending to use trusted authority mechanisms SHOULD ensure that the
-
Named Information Hash Algorithm Registry
@@ -2367,6 +2370,26 @@ Ecosystems intending to use trusted authority mechanisms SHOULD ensure that the
+
+
+ Formal Security Analysis of the OpenID for Verifiable Presentations Specification (with DC API)
+
+
+
+
+
+
+
+
+
+
+ OpenID for Verifiable Credentials: Formal Security Analysis using the Web Infrastructure Model
+
+
+
+
+
+
# OpenID4VP over the Digital Credentials API {#dc_api}
This section defines how to use OpenID4VP with the Digital Credentials API.
@@ -2544,13 +2567,15 @@ The audience for the response (for example, the `aud` value in a Key Binding JWT
## Security Considerations {#dc_api_security_considerations}
+The security properties of the OpenID4VP protocol, when used in conjunction with the Digital Credentials API (DC API) [@!W3C.Digital_Credentials_API], have been formally analyzed, see [@secanalysis.openid4vp.dc].
+
The following security considerations from OpenID4VP apply:
* Preventing Replay of Verifiable Presentations as described in (#preventing-replay), with the difference that the origin is used instead of the Client Identifier to bind the response to the Client.
* End-User Authentication using Credentials as described in (#end-user-authentication-using-credentials).
* Encrypting an Unsigned Response as described in (#encrypting_unsigned_response).
* TLS Requirements as described in (#tls-requirements).
-* Always Use the Full Client Identifier as described in (#full-client-identifier) for signed requests.
+* Always use the Full Client Identifier as described in (#full-client-identifier) for signed requests.
* Security Checks on the Returned Credentials and Presentations as described in (#dcql_query_security).
* DCQL Value Matching as described in (#dcql-value-matching).
@@ -3570,4 +3595,4 @@ The technology described in this specification was made available from contribut
-final
- * https://openid.net/specs/openid-4-verifiable-presentations-1_0-final.html
\ No newline at end of file
+ * https://openid.net/specs/openid-4-verifiable-presentations-1_0-final.html
diff --git a/1.1/openid-4-verifiable-presentations-1_1.md b/1.1/openid-4-verifiable-presentations-1_1.md
index a6c783a3..2b124ff8 100644
--- a/1.1/openid-4-verifiable-presentations-1_1.md
+++ b/1.1/openid-4-verifiable-presentations-1_1.md
@@ -1765,6 +1765,10 @@ While breaking changes to the specifications referenced in this specification ar
# Security Considerations {#security_considerations}
+## Formal Security Analysis
+
+The security properties of the OpenID for Verifiable Credentials family of specifications have been formally analyzed, see [@secanalysis.openid4vc].
+
## Preventing Replay of Verifiable Presentations {#preventing-replay}
An attacker could try to inject Presentations obtained from (for example) a previous Authorization Response into another Authorization Response, thus impersonating the End-User that originally presented the respective Verifiable Presentation. Holder Binding aims to prevent such attacks.
@@ -2357,7 +2361,6 @@ Ecosystems intending to use trusted authority mechanisms SHOULD ensure that the
-
Named Information Hash Algorithm Registry
@@ -2367,6 +2370,26 @@ Ecosystems intending to use trusted authority mechanisms SHOULD ensure that the
+
+
+ Formal Security Analysis of the OpenID for Verifiable Presentations Specification (with DC API)
+
+
+
+
+
+
+
+
+
+
+ OpenID for Verifiable Credentials: Formal Security Analysis using the Web Infrastructure Model
+
+
+
+
+
+
# OpenID4VP over the Digital Credentials API {#dc_api}
This section defines how to use OpenID4VP with the Digital Credentials API.
@@ -2544,6 +2567,8 @@ The audience for the response (for example, the `aud` value in a Key Binding JWT
## Security Considerations {#dc_api_security_considerations}
+The security properties of the OpenID4VP protocol, when used in conjunction with the Digital Credentials API (DC API) [@!W3C.Digital_Credentials_API], have been formally analyzed, see [@secanalysis.openid4vp.dc].
+
The following security considerations from OpenID4VP apply:
* Preventing Replay of Verifiable Presentations as described in (#preventing-replay), with the difference that the origin is used instead of the Client Identifier to bind the response to the Client.
@@ -2551,7 +2576,7 @@ The following security considerations from OpenID4VP apply:
* VP Token abuse (#vp-token-abuse).
* Encrypting an Unsigned Response as described in (#encrypting_unsigned_response).
* TLS Requirements as described in (#tls-requirements).
-* Always Use the Full Client Identifier as described in (#full-client-identifier) for signed requests.
+* Always use the Full Client Identifier as described in (#full-client-identifier) for signed requests.
* Security Checks on the Returned Credentials and Presentations as described in (#dcql_query_security).
* DCQL Value Matching as described in (#dcql-value-matching).