Які протоколи та стандарти пройшли формальну верифікацію в Tamarin Prover і яка вимога NIST та IETF щодо цього?

Question

Answer

TLS 1.3, Signal Double Ratchet, Noise Framework, MLS та WireGuard верифіковані в Tamarin у моделі Dolev-Yao

Answer

Tamarin Prover використовувався для верифікації ISO/IEC 9798, DNP3 Secure Authentication v5 та протоколу PQ3 від Apple iMessage

Answer

NIST та IETF вимагають формального аналізу протоколів саме в парадигмі Dolev-Yao перед їх стандартизацією

Answer

Tamarin є комерційним інструментом, доступним лише для верифікованих урядових організацій

Crowdly