{"data":{"id":2752,"lang":"cs","title":"Google DeepMind formálně ověřil protokol Signal pomocí AI: 6,5 milionu řádků důkazů za čtyři týdny","summary":"AlphaProof Code od DeepMindu vytvořil strojově ověřené důkazy klíčových bezpečnostních vlastností Signalu, zatím jen pro konverzace mezi dvěma lidmi.","category":"ai","category_label":"AI","published_at":"2026-11-12T15:01:26Z","updated_at":"2026-11-12T15:01:26Z","url":"https://techtools.cz/tools/news/clanek/2752-google-deepmind-formalne-overil-protokol-signal-pomoci-ai-6-5-milionu-radku","api_url":"https://techtools.cz/news-api/v1/articles/2752?lang=cs","markdown_url":"https://techtools.cz/news-api/v1/articles/2752.md?lang=cs","image_url":"https://images.unsplash.com/photo-1677442136019-21780ecad995?w=800","word_count":123,"reading_time_minutes":1,"sources":[{"url":"https://www.theneuron.ai/news/google-ai-math-signal-security-verification/","domain":"theneuron.ai"},{"url":"https://github.com/google-deepmind/code-verification","domain":"github.com"}],"translation":{"lang":"en","id":2678,"title":"Google DeepMind Uses AI to Formally Verify the Signal Protocol, Producing 6.5 Million Lines of Proofs in Four Weeks","url":"https://techtools.cz/tools/news/article/2678-google-deepmind-uses-ai-to-formally-verify-the-signal-protocol-producing-6-5","api_url":"https://techtools.cz/news-api/v1/articles/2678?lang=en"},"content":"Google DeepMind pomocí nového systému AlphaProof Code vytvořil strojově ověřené matematické důkazy bezpečnostních vlastností protokolu Signal. Práce oznámená 10. listopadu pokrývá důvěrnost zpráv, autentizaci, forward secrecy a post-compromise security a důkazy kontroluje nástroj Lean, včetně zhruba 140 000 instrukcí přeloženého strojového kódu.\n\nPět výzkumníků za čtyři týdny vygenerovalo přibližně 6,5 milionu řádků důkazů, což dříve trvalo specializovaným týmům roky. Pro ověření metody DeepMind vrátil do testovacích verzí dvě dříve opravené zranitelnosti Signalu a systém vytvořil důkazy, že obě upravené verze porušují bezpečnostní požadavky.\n\nRozsah je omezený: pokryty byly jen konverzace mezi dvěma lidmi, nikoli skupinové zprávy, více zařízení ani celá mobilní aplikace, a důkaz ověřuje jen zadané požadavky. Google zveřejnil důkazy a specifikace na GitHubu a uvádí, že komerční služba zatím neexistuje."}}