Facultatea de Informatica IasiUniversitatea A.I.Cuza

Home Page Coordonates About Me Useful links What I teach

in Romanian

Logici de încredere în securitatea informației

Cod
: MSI2102
Semestrul : 4   Master Securitatea Informaţiei
Credite : 8 Tip : opțional
Titular: Cristian Masalagiu
Asistent: Cristian Masalagiu
Ore/sapt:
Curs: 2 , Seminar/Laborator: 2
Evaluare
:
  • Conform Fișelor oficiale


 


Obiective (vezi și Fișele oficiale)

  1. Capacitatea de a analiza și de a demonstra corectitudinea funcționării cu ajutorul logicii formale a oricărui protocol criptografic de securitate, utilizat pentru comunicare într-un sistem multiagent.
  2. Explicarea diferențelor dintre diverse logici care pot fi utilizate în scopul amintit (de exemplu GNY și SvO).
  3. Depistarea, cu ajutorul unei logici specifice, a vulnerabilităților unor protocoale existente; crearea de noi protocoale, având mai puține vulnerabilități, sau chiar a unor noi logici pentru analiza acestora.
  4. Utilizarea unor demonstratoare automate, model-checker-e, SMT-solver-e comerciale existente, pentru a efectua raționamente specifice logicilor de încredere trecute în revistă.
  5. Traducerea din limbaj natural într-un limbaj intermediar (și apoi într-un limbaj abstract, adică într-o logică precizată) a prezentării unui protocol de securitate (incluzând specificațiile funcționării corecte a acestuia).
Tematica generală (vezi și Fișele oficiale)
  1. Recapitulare (logica clasică bivalentă, logici neclasice, criptografie, protocoale de securitate în sisteme multiagent și mediu Internet, logica BAN).
  2. Logici epistemice, cunoștințe/knoledge (K) și credințe/beliefs (B).
  3. Vulnerabilitățile logicii BAN. Posibilitatea efectuării unor atacuri prin reluare.
  4. Logica GNY și sistemul deductiv SD-GNY.
  5. Analiza logicii GNY și tratarea unor protocoale specifice.
  6. Logica SvO.
  7. Demonstrare automată - Isabelle.
Tematică (vezi și Fișele oficiale)
Tematica seminariilor/laboratoarelor va fi fixată, în principiu, la prima întâlnire. Ea va cuprinde exemplificări ale cursurilor deja predate, teme imediate pentru acasă şi proiecte de durată mai îndelungată (referate). Se vor folosi metodele clasice de predare-învățare (Expunerea sistematică a cunostintelor, Conversaţia, Problematizarea şi învăţarea prin descoperire, Modelarea etc.). Cursurile şi Seminariile vor fi predate/organizate on-line folosind Zoom şi Discord (detalii pe e-mail). Seminariile sau Laboratoarele vor fi axate pe învăţarea unui limbaj comercial existent (unul dintre Isabelle, HOL, MCMAS, TLC etc.).

Cursuri anterioare benefic a fi fost făcute (la care se adaugă, desigur, cursurile anterioare tematice de la acest master):
  • Logica pentru informatică.
  • Securitatea informaţiei.
  • Programare logică (opţional).
  • Programare funcțională (opțional).
  • Fundamentele algebrice ale informaticii.
  • Limbaje formale și automate.
  • Calculabilitate, decidabilitate şi complexitate (opţional).

Bibliografie principală recomandată și link-uri INTERNET
  1. C. Masalagiu - Fundamentele logice ale Informaticii, Ed. Universitatii "Al. I. Cuza", Iasi, 2004, ISBN 973-703-015-X
  2. M. Huth, M. Ryan - Logic in Computer Science: Modelling and Reasoning about Systems, Cambridge University Press, England, 2000, ISBN 0-521-65200-6
  3. R. Stalnaker – On Logic of Knoledge and Belief, Springer Verlag, 2006
  4. P.C. van Oorschot – Handbook of Applied Cryptography, Carleton University, 2002
  5. T. Kwon, S. Lim – Automation-Considered Logic of Authentication and Key Distibution, Spinger Verlag, 2003
  6. D. Yiqiang – An Improvement of GNY Logic for the Reflection Attacks, Springer Verlag, 1999
  7. M. Benerecetti, et al. – A Logic of Belief and a Model Checking Algoritm for Security Protocols, 2000
  8. D. Monniaux – Analysis of Cryprographic Protocols Using Logics of Belief: An Overview, J. T. I.T., 2006
  9. R. Fagin, et al. – Reasoning about Knoledge, M. I. T. Press, 2003
  10. J.J. Ch. Meyer, W. van der Hoek, Epistemic Logic for AI and Computer Science, Cambridge Univ. Press, 2004
  11. Fisa oficiala RO
  12. Fisa oficiala EN
  13. Slide-uri curs
  14. Cerinte referate
  15. Protocoale in GNY (exercitii)
  16. Sintaxa GNY in BNF
  17. Operatori, axiome (formule, afirmatii) si reguli in GNY
  18. Decidabilitate si complexitate pentru protocoale
  19. GNY Articolul original
  20. Altă carte protocoale
  21. Idei (extinse) despre Logica BAN
  22. Conceptul de mutual-belief revizuit
  23. Anonimitatea de grup pentru protocoalele de securitate
  24. Carte SMT-Solvers, C. Barrett
  25. Carte SMT-Solvers, L. de Moura
  26. Manual Isabelle-HOL
  27. Isabelle - Verificarea unui protocol de securitate
  28. Zhang - Protocoale LCAP si OHLCAP
  29. Protocolul Aydos
  30. Analiza protocoalelor de securitate
  31. Automatizarea logicii GNY
  32. Job in securitatea informatiei
Modalităţi de evaluare (cerinţele sunt conform Fișelor oficiale)
  • Prezenţa este necesară și va fi cumva contabilizată.
  • Se vor da exerciții pentru acasă sau direct la seminarii. Media notelor obținute aici va conta în proporţie de 25% din nota finală.
  • Nota/media de la lucrarea/lucrările de evaluare (săptămâna a 8-a, sau, eventual, la sfârșit) va conta 50% din nota finală.
  • Restul de 25% din nota finală se va obține din aprecierea proiectului/referatului ales/finalizat și prezentat cu Zoom (Alte detalii pe e-mail).

Designed by Adrian Mironescu