Formal Verification of Security Protocol Implementations: A Survey

Tipo di pubblicazione: Articolo su rivista
Tipologia MIUR: Contributo su Rivista > Articolo in rivista
Titolo: Formal Verification of Security Protocol Implementations: A Survey
Autori: Avalle M. ; Pironti A. ; Sisto R.
Autori di ateneo:
Titolo del periodico: FORMAL ASPECTS OF COMPUTING
Tipo di referee: Esperti anonimi
Editore: Springer
Volume: 26
Numero: 1
Intervallo pagine: pp. 99-123
Numero di pagine: 25
ISSN: 0934-5043
Abstract: Automated formal verification of security protocols has been mostly focused on analyzing high-level abstract models which, however, are significantly different from real protocol implementations written in programming languages. Recently, some researchers have started investigating techniques that bring automated formal proofs closer to real implementations. This paper surveys these attempts, focusing on approaches that target the application code that implements protocol logic, rather than the libraries that implement cryptography. According to these approaches, libraries are assumed to correctly implement some models. The aim is to derive formal proofs that, under this assumption, give assurance about the application code that implements the protocol logic. The two main approaches of model extraction and code generation are presented, along with the main techniques adopted for each approach
Data: 2014
Status: Pubblicato
Lingua della pubblicazione: Inglese
Parole chiave: security protocols, automated formal verification, software verification, sound refinement
Dipartimenti (originale): DAUIN - Dipartimento di Automatica Informatica
Dipartimenti: DAUIN - Dipartimento di Automatica e Informatica
URL correlate:
    Area disciplinare: Area 09 - Ingegneria industriale e dell'informazione > SISTEMI DI ELABORAZIONE DELLE INFORMAZIONI
    Data di deposito: 27 Nov 2012 17:06
    Data ultima modifica (IRIS): 22 Apr 2016 13:52:37
    Data inserimento (PORTO): 24 Apr 2016 07:12
    Numero Identificativo (DOI): 10.1007/s00165-012-0269-9
    Permalink: http://porto.polito.it/id/eprint/2505029
    Link resolver URL: Link resolver link
    Citazioni:

    Il campo presenta il numero di citazioni presenti sulle banche dati Scopus e Web of Science e permette di accedere ai relativi record. Visualizza inoltre il link al record presente su Google Scholar.

    Possono verificarsi discrepanze rispetto ai dati presenti sulle banche dati per i seguenti motivi:

    • Differenze tra i dati riportati su IRIS e quelli presenti nelle banche dati.
    • Il numero di citazioni riportate su PORTO viene estratto mensilmente. Il dato citazionale presente sulle singole banche dati è aggiornato in tempo reale
    • Il numero di citazioni per WoS viene calcolato sulla base delle collezioni in abbonamento (Science citation index Expanded e Conference Proceedings Citation Index)

    Per informazioni o segnalazioni contattare scrivia/porto

    +
    -

    Allegati

    [img]
    Preview
    PDF (article.pdf) - Postprint
    Accesso al documento: Visibile (Ad accesso aperto)
    Licenza: Pubblico - Tutti i diritti riservati.

    Download (425Kb (435362 bytes)) | Preview

    Azioni (richiesto il login)

    Visualizza il documento (riservato amministratori) Visualizza il documento (riservato amministratori)

    Statistiche sul Download degli allegati

    Altre statistiche su questa pubblicazione...