Provably correct Java implementations of Spi Calculus security protocols specifications

Tipo di pubblicazione: Articolo su rivista
Tipologia MIUR: Contributo su Rivista > Articolo in rivista
Titolo: Provably correct Java implementations of Spi Calculus security protocols specifications
Autori: Pironti A.; Sisto R.
Autori di ateneo:
Titolo del periodico: COMPUTERS & SECURITY
Tipo di referee: Tipo non specificato
Editore: Elsevier
Volume: 29(3)
Numero: 3
Intervallo pagine: pp. 302-314
Numero di pagine: 13
ISSN: 0167-4048
Abstract: Spi Calculus is an untyped high level modeling language for security protocols, used for formal protocols specification and verification. In this paper, a type system for the Spi Calculus and a translation function are formally defined, in order to formalize the refinement of a Spi Calculus specification into a Java implementation. The Java implementation generated by the translation function uses a custom Java library. Formal conditions on such library are stated, so that, if the library implementation code satisfies such conditions, then the generated Java implementation correctly simulates the Spi Calculus specification. A verified implementation of part of the custom library is further presented
Data: 2010
Status: Pubblicato
Lingua della pubblicazione: Inglese
Parole chiave: model-based software development, correctness preserving code generation, code verification, formal methods, security protocols
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: 02 Nov 2009 12:24
    Data ultima modifica (IRIS): 17 Ott 2016 10:44:01
    Data inserimento (PORTO): 02 Nov 2016 12:07
    Numero Identificativo (DOI): 10.1016/j.cose.2009.08.001
    Permalink: http://porto.polito.it/id/eprint/2284514
    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] PDF (cose2009_author_postprint.pdf) - Postprint
    Accesso al documento: Visibile (Ad accesso aperto)
    Licenza: Pubblico - Tutti i diritti riservati.

    Download (217Kb (222885 bytes))
    [img] PDF (1_s2.0_S0167404809000832_main.pdf) - Altro
    Accesso al documento: Non visibile (accessibile solo al proprietario del dato)
    Licenza: Non pubblico - Accesso privato / Ristretto.

    Download (1488Kb (1524185 bytes)) | Spedisci una richiesta all'autore per una copia del documento

    Azioni (richiesto il login)

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

    Statistiche sul Download degli allegati

    Altre statistiche su questa pubblicazione...