Dissertação

Tableaux for Distributed Temporal Logic: Applications to Security Protocols EVALUATED

A lógica temporal distribuída DTL é uma lógica expressiva para formalizar e raciocinar sobre propriedades temporais de sistemas distribuídos, sob o ponto de vista local dos agentes do sistema, e sobre propriedades globais de processos de comunicação distribuídos por estes agentes, que interagem por partilha de eventos sincronizados. A DTL é apropriada para formalizar e raciocinar sobre modelos de protocolos de segurança. Pode ser usada tanto como uma "lógica objecto", para formalizar modelos de protocolos específicos e provar propriedades dos protocolos com respeito a esses modelos, ou como uma metalógica, para estudar o relacionamento entre modelos em diferentes níveis de abstracção. A DTL possui um sistema de tableaux correcto e completo. Mas este sistema de tableaux foi originalmente definido para uma linguagem de DTL ligeiramente diferente. O principal objectivo nesta dissertação é provar certos resultados acerca de protocolos de segurança e dos seus modelos recorrendo a este sistema de tableaux. Para atingir este objectivo, enriquecemos o sistema de tableaux, introduzimos um novo conceito para permitir que informação necessária seja incluída num meta-nível externo ao sistema de tableaux, introduzimos regras específicas para os modelos considerados e derivámos regras para simplificar os tableaux.
Lógica Temporal Distribuída, Sistema de Tableaux, Protocolos de Segurança, Provas por Tableaux

Dezembro 9, 2011, 9:30

Documentos da dissertação ainda não disponíveis publicamente

Orientação

CO-ORIENTADOR

Jaime Arsénio de Brito Ramos

Departamento de Matemática (DM)

Professor Auxiliar

ORIENTADOR

Carlos Manuel Costa Lourenço Caleiro

Departamento de Matemática (DM)

Professor Associado