MacMusic  |  PcMusic  |  440 Software  |  440 Forums  |  440TV  |  Zicos
formal
Recherche

A formal analysis of Apple’s iMessage PQ3 protocol

samedi 10 mai 2025, 00:42 , par OS News
We present the formal verification of Apple’s iMessage PQ3, a highly performant, device-to-device messaging protocol offering strong security guarantees even against an adversary with quantum computing capabilities. PQ3 leverages Apple’s identity services together with a custom, post-quantum secure initialization phase and afterwards it employs a double ratchet construction in the style of Signal, extended to provide post-quantum, post-compromise security.

We present a detailed formal model of PQ3, a precise specification of its fine-grained security properties, and machine-checked security proofs using the TAMARIN prover. Particularly novel is the integration of post-quantum secure key encapsulation into the relevant protocol phases and the detailed security claims along with their complete formal analysis. Our analysis covers both key ratchets, including unbounded loops, which was believed by some to be out of scope of symbolic provers like TAMARIN (it is not!).
↫ Felix Linker and Ralf Sasse

Weekend, light reading, you know how this works by now. Light some candles, make some tea, get comfy.
https://www.osnews.com/story/142328/a-formal-analysis-of-apples-imessage-pq3-protocol/

Voir aussi

News copyright owned by their original publishers | Copyright © 2004 - 2025 Zicos / 440Network
Date Actuelle
sam. 10 mai - 02:51 CEST