Name
Abstract | ||
|---|---|---|
This paper presents an experiment in which an implementation of the client side of the SSH Transport Layer Protocol (SSH-TLP) was semi-automatically derived according to a model-driven development paradigm that leverages formal methods in order to obtain high correctness assurance. The approach used in the experiment starts with the formalization of the protocol at an abstract level. This model is then formally proved to fulfill the desired secrecy and authentication properties by using the ProVerif prover. Finally, a sound Java implementation is semi-automatically derived from the verified model using an enhanced version of the Spi2Java framework. The resulting implementation correctly interoperates with third party servers, and its execution time is comparable with that of other manually developed Java SSH-TLP client implementations. This case study demonstrates that the adopted model-driven approach is viable even for a real security protocol, despite the complexity of the models needed in order to achieve an interoperable implementation. |
Year | DOI | Venue |
|---|---|---|
2012 | 10.1016/j.jss.2011.10.052 | Journal of Systems and Software |
Keywords | Field | DocType |
semi-automatic implementation,proverif prover,open security protocol,model-driven approach,ssh transport layer protocol,real security protocol,client side,interoperable implementation,resulting implementation,java ssh-tlp client implementation,model-driven development paradigm,sound java implementation,security protocols | Client-side,Programming language,Authentication,Cryptographic protocol,Computer science,Server,Correctness,Real-time computing,Implementation,Formal methods,Java | Journal |
Volume | Issue | ISSN |
85 | 4 | 0164-1212 |
Citations | PageRank | References |
6 | 0.49 | 35 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Alfredo Pironti | 1 | 330 | 27.47 |
| Davide Pozza | 2 | 105 | 7.45 |
| Riccardo Sisto | 3 | 556 | 56.79 |