Programma del Corso

Presentazione del Corso

Un esempio di modellazione formale di protocolli di sicurezza

Introduzione alle Abstract State Machines - ASM:

• Il problema
• Scopo e caratteristiche
• Applicabilità

Concetti di base:

• Richiami sulle Finite State Machine - FSM
• Da FSM a ASM
• Il formalismo delle ASM
• ASM di Bohem-Jacopini:
  • Costrutti di sequenza-iterazione
  • Parametrizzazione di ASM

Il metodo di sviluppo basato sulle ASM:

• Ground model
• Raffinamenti verticali
• Raffinamenti orizzontali

Introduzione alle Distributed ASM - DASM:

• sync_DASM
• async_DASM

Analisi delle Proprietà

Esempi di applicazione:

• Routing Sicuro nelle Mobile Ad-hoc NETwork - MANET
• Kerberos
• Protocolli di sicurezza come open systems

Possibili approfondimenti.