Disciplina
Modelos Computacionais em Segurança
Área
Área Científica de Metodologia e Tecnologias da Programação > Algoritmos
Activa nos planos curriculares
DEASegInf2021 > DEASegInf2021 > 3º Ciclo > Engenharia Informática > Metodologia e Tecnologia da Programação > Modelos Computacionais em Segurança
DEAEIC2006 > DEAEIC2006 > 3º Ciclo > Modelos Computacionais em Segurança
DEASegInf2007 > DEASegInf2007 > 3º Ciclo > Engenharia Informática > Metodologia e Tecnologia da Programação > Modelos Computacionais em Segurança
Nível
Exame + Projecto.
Tipo
Não Estruturante
Regime
Semestral
Carga Horária
1º Semestre
3.0 h/semana
126.0 h/semestre
Objectivos
Dominar os modelos computacionais de concepção e de 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. Análise da correcção e completude das abstracções simbólicas. Ferramentas para verificação de propriedades de segurança, AVISPA, ProVerif, inter alia.
Metodologia de avaliação
Exame + Projecto.
Pré-requisitos
Componente Laboratorial
Princípios Éticos
Componente de Programação e Computação
Componente de Competências Transversais
Bibliografia
Principal
A Calculus for Cryptographic Protocols: The Spi Calculus
ACM Conference on Computer and Communications Security, pp. 36-47.
Reconciling Two Views of Cryptography (The Computational Soundness of Formal Encryption)
Journal Cryptology, 15(2), pp. 103-127
Formal Methods for the Analysis of Security Protocols
Pedro Adão - Supervised by P. Mateus and A. Scedrov
PhD thesis, IST, Universidade Técnica de Lisboa.
On the Security of Public Key Protocols
IEEE Transactions on Information Theory, vol. IT-29(2), pp. 198-208
Multiset rewriting and the complexity of bounded security protocols
N. Durgin, P. Lincoln, J. Mitchell, and A. Scedrov
Journal of Computer Security, 12(2), 247-311
The faithfulness of abstract protocol analysis: message authentication
J. Guttman, F. Thayer, and L. Zuck
ACM Conference on Computer and Communications Security, pp. 186-195
Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR, Software
Concepts and Tools 17(3), pp. 93-102.
Formal Methods for Cryptographic Protocol Analysis: Emerging Issues
IEEE Journal on Selected Areas in Communications 21(1), pp. 44-54.