Disciplina

Área

Área Científica de Metodologia e Tecnologia da Programação > Algoritmos

Activa nos planos curriculares

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.

Bibliografia

Principal

A Calculus for Cryptographic Protocols: The Spi Calculus

M. Abadi, A. Gordon.

1997

ACM Conference on Computer and Communications Security, pp. 36-47.


Reconciling Two Views of Cryptography (The Computational Soundness of Formal Encryption)

M. Abadi, P. Rogaway

2002

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

2006

PhD thesis, IST, Universidade Técnica de Lisboa.


On the Security of Public Key Protocols

D. Dolev, and A. Yao

1983

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

2004

Journal of Computer Security, 12(2), 247-311


The faithfulness of abstract protocol analysis: message authentication

J. Guttman, F. Thayer, and L. Zuck

2001

ACM Conference on Computer and Communications Security, pp. 186-195


Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR, Software

G. Lowe

1996

Concepts and Tools 17(3), pp. 93-102.


Formal Methods for Cryptographic Protocol Analysis: Emerging Issues

C. Meadows

2003

IEEE Journal on Selected Areas in Communications 21(1), pp. 44-54.