Rewrite formal analysis section

As discussed in the editor's call, the formal analysis section (5.3. Foundational Pillars) should be rewritten from its current form to include recent analysis efforts, including the following:

The DY* analysis ongoing in Stuttgart - first results available no earlier than November
The OpenID4VC analysis performed by Fabian - first public version no earlier than ~November
https://elib.uni-stuttgart.de/handle/11682/12417 (mitigation: cross-device stub)
https://elib.uni-stuttgart.de/handle/11682/12220 (to solve the issue, assumed that user is careful and can detect the attack)
https://doi.org/10.1145/3374664.3375727 ("we formally analysed a protocol relying on push notifications delivered to an out-of-band device to approve the authentication attempt on the primary device (defined as Backchannel-Transferred Session Pattern in the draft)")
https://doi.org/10.1109/TDSC.2023.3296210 ("we formally analysed a protocol relying on a QR code to be read by the secondary device to approve the authentication attempt on the primary device (defined as User-Transferred Session Data Pattern in the draft)")

oauth-wg / oauth-cross-device-security

Rewrite formal analysis section #97