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.

Formally sound implementations of security protocols with JavaSPI / Sisto, Riccardo; Bettassa Copet, Piergiuseppe; Avalle, Matteo; Pironti, Alfredo. - In: FORMAL ASPECTS OF COMPUTING. - ISSN 0934-5043. - STAMPA. - 30:2(2018), pp. 279-317. [10.1007/s00165-017-0449-8]

Formally sound implementations of security protocols with JavaSPI

Sisto, Riccardo;Bettassa Copet, Piergiuseppe;Avalle, Matteo;
2018

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.
File in questo prodotto:
File Dimensione Formato  
AuthorsPostPrint.pdf

Open Access dal 13/12/2018

Descrizione: Articolo principale
Tipologia: 2. Post-print / Author's Accepted Manuscript
Licenza: PUBBLICO - Tutti i diritti riservati
Dimensione 959.38 kB
Formato Adobe PDF
959.38 kB Adobe PDF Visualizza/Apri
10.1007_s00165-017-0449-8.pdf

non disponibili

Descrizione: Articolo principale
Tipologia: 2a Post-print versione editoriale / Version of Record
Licenza: Non Pubblico - Accesso privato/ristretto
Dimensione 4.51 MB
Formato Adobe PDF
4.51 MB Adobe PDF   Visualizza/Apri   Richiedi una copia
Pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11583/2695975
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo