Disciplina
Lógica Cleística
Área
Área Científica de Lógica e Computação > Lógica e Computação
Activa nos planos curriculares
DEASegInf2021 > DEASegInf2021 > 3º Ciclo > Matemática > Lógica e Computação > Lógica Cleística
DEAMat2006 > DEAMat2006 > 3º Ciclo > Lógica e Computação > Lógica Cleística
DEASegInf2007 > DEASegInf2007 > 3º Ciclo > Matemática > Lógica e Computação > Lógica Cleística
Nível
Tipo
Não Estruturante
Regime
Semestral
Carga Horária
1º Semestre
4.0 h/semana
154.0 h/semestre
Objectivos
Dominar os modelos simbólicos 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. 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 verificaçã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
Pré-requisitos
Componente Laboratorial
Princípios Éticos
Componente de Programação e Computação
Componente de Competências Transversais
Bibliografia
Principal
P. Blackburn, M. de Rijke, and Y. Venema
R. Fagin, J. Y. Halpern, Y. Moses, and M. Y. Vardi
On the Security of Public Key Protocols
IEEE Transactions on Information Theory, vol. IT-29(2), pp. 198-208.
M. Burrows, M. Abadi, and R. Needham
ACM Transactions on Computer Systems 8(1), pp. 18-36
Secundária
Metareasoning about security protocols using distributed temporal logic
C. Caleiro, L. Viganò, and D. Basin
Electronic Notes in Theoretical Computer Science, 125(1):67-89
A compositional logic for proving security properties of protocols
N.A. Durgin, J.C. Mitchell, D. Pavlovic
Journal of Computer Security, 11(4), pp. 677-721
Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR
Software - Concepts and Tools 17(3), pp. 93-102.
Strand Spaces: Proving Security Protocols Correct
F. Thayer, J. Herzog, and J. Guttman
Journal of Computer Security, 7(1)