Safe abstractions of data encodings in formal security protocol models

Tipo di pubblicazione: Articolo su rivista
Tipologia MIUR: Contributo su Rivista > Articolo in rivista
Titolo: Safe abstractions of data encodings in formal security protocol models
Autori: 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. 125-167
Numero di pagine: 43
ISSN: 0934-5043
Abstract: When using formal methods, security protocols are usually modeled at a high level of abstraction. In particular, data encoding and decoding transformations are often abstracted away. However, if no assumptions at all are made on the behavior of such transformations, they could trivially lead to security faults, for example leaking secrets or breaking freshness by collapsing nonces into constants. In order to address this issue, this paper formally states sufficient conditions, checkable on sequential code, such that if an abstract protocol model is secure under a Dolev-Yao adversary, then a refined model, which takes into account a wide class of possible implementations of the encoding/decoding operations, is implied to be secure too under the same adversary model. The paper also indicates possible exploitations of this result in the context of methods based on formal model extraction from implementation code and of methods based on automated code generation from formally verified models
Data: 2014
Status: Pubblicato
Lingua della pubblicazione: Inglese
Parole chiave: security protocols, refinement, model abstraction
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: 14 Nov 2012 12:54
    Data ultima modifica (IRIS): 09 Mag 2016 16:06:49
    Data inserimento (PORTO): 22 Mag 2016 02:38
    Numero Identificativo (DOI): 10.1007/s00165-012-0267-y
    Permalink: http://porto.polito.it/id/eprint/2504212
    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 (730Kb (748542 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...