Noise Explorer: Fully Automated Modeling and Verification for Arbitrary Noise Protocols
| Autor: | Nadim Kobeissi, Karthikeyan Bhargavan, Georgio Nicolas |
|---|---|
| Přispěvatelé: | Programming securely with cryptography (PROSECCO), Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Symbolic Software, Kobeissi, Nadim, Programming securely with cryptography (PROSECCO ) |
| Rok vydání: | 2019 |
| Předmět: |
Handshake
Computer science Noise protocol framework Cryptographic protocols 0102 computer and information sciences 02 engineering and technology [INFO] Computer Science [cs] Encryption 01 natural sciences [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR] [INFO.INFO-NI]Computer Science [cs]/Networking and Internet Architecture [cs.NI] Forward secrecy 0202 electrical engineering electronic engineering information engineering [INFO]Computer Science [cs] Message authentication code Concrete security Formal verification [INFO.INFO-CR] Computer Science [cs]/Cryptography and Security [cs.CR] [INFO.INFO-NI] Computer Science [cs]/Networking and Internet Architecture [cs.NI] business.industry Cryptographic protocol Noise Computer engineering 010201 computation theory & mathematics 020201 artificial intelligence & image processing business |
| Zdroj: | EuroS&P EuroS&P 2019-4th IEEE European Symposium on Security and Privacy EuroS&P 2019-4th IEEE European Symposium on Security and Privacy, Jun 2019, Stockholm, Sweden HAL 2019 IEEE European Symposium on Security and Privacy (EuroS&P) |
| Popis: | International audience; The Noise Protocol Framework, introduced recently, allows for the design and construction of secure channel protocols by describing them through a simple, restricted language from which complex key derivation and local state transitions are automatically inferred. Noise "Handshake Patterns" can support mutual authentication, forward secrecy, zero round-trip encryption, identity hiding and other advanced features. Since the framework's release, Noise-based protocols have been adopted by WhatsApp, WireGuard and other high-profile applications.We present Noise Explorer, an online engine for designing, reasoning about, formally verifying and implementing arbitrary Noise Handshake Patterns. Based on our formal treatment of the Noise Protocol Framework, Noise Explorer can validate any Noise Handshake Pattern and then translate it into a model ready for automated verification and also into a production-ready software implementation written in Go or in Rust. We use Noise Explorer to analyze more than 57 handshake patterns. We confirm the stated security goals for 12 fundamental patterns and provide precise properties for the rest. We also analyze unsafe handshake patterns and document weaknesses that occur when validity rules are not followed. All of this work is consolidated into a usable online tool that presents a compendium of results and can parse formal verification results to generate detailed-but-pedagogical reports regarding the exact security goals of each message of a Noise Handshake Pattern with respect to each party, under an active attacker and including malicious principals. Noise Explorer evolves alongside the standard Noise Protocol Framework, having already contributed new security goal verification results and stronger definitions for pattern validation and security parameters. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|