AnBx:: Automatic Generation and Verification of Security Protocols Implementations

Paolo Modesti

doi:10.1007/978-3-319-30303-1_10

AnBx: Automatic Generation and Verification of Security Protocols Implementations

Paolo Modesti

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

238 Downloads (Pure)

Abstract

The AnBx compiler is a tool for automatic generation of Java implementations of security protocols specified in a simple and abstract model that can be formally verified. In our model-driven development approach, protocols are described in AnBx, an extension of the Alice & Bob notation. Along with the synthesis of consistency checks, the tool analyses the security goals and produces annotations that allow the verification of the generated implementation with ProVerif.

Original language	English
Title of host publication	Foundations and Practice of Security
Editors	Joaquín García-Alfaro, Evangelos Kranakis, Guillaume Bonfante
Publisher	Springer
Pages	156-173
Number of pages	18
Volume	9482
DOIs	https://doi.org/10.1007/978-3-319-30303-1_10
Publication status	E-pub ahead of print - 25 Feb 2016
Event	8th International Symposium on Foundations and Practice of Security - Clermont-Ferrand, France Duration: 26 Oct 2015 → 28 Oct 2015

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer

Conference

Conference	8th International Symposium on Foundations and Practice of Security
Abbreviated title	FPS 2015
Country/Territory	France
City	Clermont-Ferrand
Period	26/10/15 → 28/10/15

Access to Document

10.1007/978-3-319-30303-1_10Licence: Unspecified

Full textAccepted author manuscript, 512 KBLicence: CC BY-NC-ND

https://doi.org/10.1007/978-3-319-30303-1_10Licence: Unspecified

Cite this

@inproceedings{9dcba500543945e2b04041dbe76b613f,

title = "AnBx:: Automatic Generation and Verification of Security Protocols Implementations",

abstract = "The AnBx compiler is a tool for automatic generation of Java implementations of security protocols specified in a simple and abstract model that can be formally verified. In our model-driven development approach, protocols are described in AnBx, an extension of the Alice & Bob notation. Along with the synthesis of consistency checks, the tool analyses the security goals and produces annotations that allow the verification of the generated implementation with ProVerif.",

author = "Paolo Modesti",

year = "2016",

month = feb,

day = "25",

doi = "10.1007/978-3-319-30303-1_10",

language = "English",

volume = "9482",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "156--173",

editor = "Joaqu{\'i}n Garc{\'i}a-Alfaro and Evangelos Kranakis and Guillaume Bonfante",

booktitle = "Foundations and Practice of Security",

note = "8th International Symposium on Foundations and Practice of Security, FPS 2015 ; Conference date: 26-10-2015 Through 28-10-2015",

}

Modesti, P 2016, AnBx: Automatic Generation and Verification of Security Protocols Implementations. in J García-Alfaro, E Kranakis & G Bonfante (eds), Foundations and Practice of Security . vol. 9482, Lecture Notes in Computer Science, Springer, pp. 156-173, 8th International Symposium on Foundations and Practice of Security, Clermont-Ferrand, France, 26/10/15. https://doi.org/10.1007/978-3-319-30303-1_10

AnBx: Automatic Generation and Verification of Security Protocols Implementations. / Modesti, Paolo.
Foundations and Practice of Security . ed. / Joaquín García-Alfaro; Evangelos Kranakis; Guillaume Bonfante. Vol. 9482 Springer, 2016. p. 156-173 (Lecture Notes in Computer Science).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - AnBx:

T2 - 8th International Symposium on Foundations and Practice of Security

AU - Modesti, Paolo

PY - 2016/2/25

Y1 - 2016/2/25

N2 - The AnBx compiler is a tool for automatic generation of Java implementations of security protocols specified in a simple and abstract model that can be formally verified. In our model-driven development approach, protocols are described in AnBx, an extension of the Alice & Bob notation. Along with the synthesis of consistency checks, the tool analyses the security goals and produces annotations that allow the verification of the generated implementation with ProVerif.

AB - The AnBx compiler is a tool for automatic generation of Java implementations of security protocols specified in a simple and abstract model that can be formally verified. In our model-driven development approach, protocols are described in AnBx, an extension of the Alice & Bob notation. Along with the synthesis of consistency checks, the tool analyses the security goals and produces annotations that allow the verification of the generated implementation with ProVerif.

U2 - 10.1007/978-3-319-30303-1_10

DO - 10.1007/978-3-319-30303-1_10

M3 - Conference contribution

VL - 9482

T3 - Lecture Notes in Computer Science

SP - 156

EP - 173

BT - Foundations and Practice of Security

A2 - García-Alfaro, Joaquín

A2 - Kranakis, Evangelos

A2 - Bonfante, Guillaume

PB - Springer

Y2 - 26 October 2015 through 28 October 2015

ER -