Verification of security protocols based on multicast communication/
Abstract: Over an insecure network, agents need means to communicate securely. To these means we often call security protocols. Security protocols, although constructed over the ar- rangement of simple security blocks, normally target the yielding of complex goals. They seem simple at a first glance...
Na minha lista:
| Principais autores: | , , |
|---|---|
| Formato: | Tese |
| Publicado em: |
|
| Assuntos: | |
| Endereço do item: | https://app.bczm.ufrn.br/home/#/item/215906 |
| Tags: |
Adicionar Tag
Sem tags, seja o primeiro a adicionar uma tag!
|
| Resumo: | Abstract: Over an insecure network, agents need means to communicate securely. To these means we often call security protocols. Security protocols, although constructed over the ar- rangement of simple security blocks, normally target the yielding of complex goals. They seem simple at a first glance, but hide subtleties that allow them to be exploited. One way of trying to systematically capture such subtleties is through the usage of formal methods. The maturity of some methods for protocol verification is a fact today. But these methods are still not able to capture the whole set of security protocols being designed. With the convergence to an on-line world, new security goals are proposed and new protocols need to be designed. The evolution of formal verification methods becomes a necessity to keep the pace with this ongoing development. This thesis covers the Inductive Method and its extensions. The Inductive Method is a formalism to specify and verify security protocols based on structural induction and higher-order logic proofs. The account of our extensions comes to enable the Inductive Method to reason about non-Unicast communication and threshold cryptography. We developed a new set of theories capable of representing the entire known message casting frameworks, Our theories enable the Inductive Method to reason about a whole new set of protocols. We also specified a basic abstraction of threshold cryptography as a way of proving the extensibility of the method regarding new cryptographic primitives. We shown the feasibility of our specitications by revisiting a classic protocol, now veritied under our framework. Secrecy verification under a mixed environment of Multicast and Unicast was also done. |
|---|