diff --git a/openid-4-verifiable-presentations-1_0.md b/openid-4-verifiable-presentations-1_0.md
index e59dd4fa..8a6c849f 100644
--- a/openid-4-verifiable-presentations-1_0.md
+++ b/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.
@@ -2367,6 +2371,27 @@ 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 +2569,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).