Disciplina Curricular
Métodos Formais em Segurança MFS
Mestrado Bolonha em Matemática e Aplicações e Computação - MMA 2006
Peso
7.5 (para cálculo da média)
Objectivos
Dominar os métodos formais de concepção e análise de protocolos de segurança e perspectivar desenvolvimentos futuros.
Programa
Cenários básicos de formalização: criptografia perfeita, intruso de Dolev-Yao, álgebra livre de mensagens. Revisão dos objectivos e protocolos de segurança. Protocolos de segurança como sistemas concorrentes. Traços, álgebras de processos e CSP, reescrita, cálculos pi e spi, estruturas de eventos, tranças, modelos computacionais e máquinas de Turing interactivas. Resultados de (in)decidibilidade e complexidade. Lógicas cleísticas: lógicas epistémicas, sistemas de agentes, conhecimento partilhado, lógica BAN e lógicas temporais. Aplicações. Teorias de segurança em sistemas lógicos computacionais: teorias indutivas, programação em lógica. Verificação semântica de protocolos: limitações dos modelos finitos, técnicas de abstracção e verficação simbólica. Cenários avançados de formalização: ataques probabilísticos, extensões ao intruso de Dolev-Yao, álgebras de mensagens. Resultados de fidelidade da representação.
Metodologia de avaliação
Projecto (20%) e exame final (80%).