Aggiornamento Repository Istituzionale e dismissione di PORTO.

Formally sound implementations of security protocols with JavaSPI

Tipo di pubblicazione: Articolo su rivista
Tipologia MIUR: Contributo su Rivista > Articolo in rivista
Titolo: Formally sound implementations of security protocols with JavaSPI
Autori: Sisto, Riccardo; Bettassa Copet, Piergiuseppe; Avalle, Matteo; Pironti, Alfredo
Autori di ateneo:
Titolo del periodico: FORMAL ASPECTS OF COMPUTING
Tipo di referee: Esperti anonimi
Editore: Springer
Numero di pagine: 39
ISSN: 0934-5043
Abstract: Designing and coding security protocols is an error prone task. Several flaws are found in protocol implementations and specifications every year. Formal methods can alleviate this problem by backing implementations with rigorous proofs about their behavior. However, formally-based development typically requires domain specific knowledge available only to few experts and the development of abstract formal models that are far from real implementations. This paper presents a Java-based protocol design and implementation framework, where the user can write a security protocol symbolic model in Java, using a well defined subset of the language that corresponds to applied π-calculus. This Java model can be symbolically executed in the Java debugger, formally verified with ProVerif, and further refined to an interoperable Java implementation of the protocol. Soundness theorems are provided to prove that, under some reasonable assumptions, a simulation relation relates the Java refined implementation to the symbolic model verified by ProVerif, so that, for the usual security properties, a property verified by ProVerif on the symbolic model is preserved in the Java refined implementation. The applicability of the framework is evaluated by developing an extensive case study on the popular SSL protocol.
Status: In stampa
Lingua della pubblicazione: Inglese
Parole chiave: security protocols, software, theoretical computer science, formal methods, formal verification, model-driven development
Dipartimenti (originale): NON SPECIFICATO
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: 04 Gen 2018 17:32
Data ultima modifica (IRIS): 08 Gen 2018 09:21:14
Data inserimento (PORTO): 10 Gen 2018 21:58
Numero Identificativo (DOI): 10.1007/s00165-017-0449-8
Permalink: http://porto.polito.it/id/eprint/2695975
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 (AuthorsPostPrint.pdf) - Postprint
Accesso al documento: Visibile (Ad accesso aperto) non prima del 12 Dicembre 2018 (data di embargo).
Licenza: Pubblico - Tutti i diritti riservati.

Download (959Kb (982405 bytes)) | Spedisci una richiesta all'autore per una copia del documento
[img] PDF (10.1007_s00165_017_0449_8.pdf) - Postprint
Accesso al documento: Non visibile (accessibile solo al proprietario del dato)
Licenza: Non pubblico - Accesso privato / Ristretto.

Download (4Mb (4616800 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)