Home

Projects

  • warning: Declaration of views_plugin_style_default::options(&$options) should be compatible with views_object::options() in /home/alfredo/Public/alfredo.pironti.eu/research/sites/all/modules/views/plugins/views_plugin_style_default.inc on line 0.
  • warning: preg_replace(): The /e modifier is no longer supported, use preg_replace_callback instead in /home/alfredo/Public/alfredo.pironti.eu/research/includes/unicode.inc on line 349.
  • warning: preg_replace(): The /e modifier is no longer supported, use preg_replace_callback instead in /home/alfredo/Public/alfredo.pironti.eu/research/includes/unicode.inc on line 349.
  • warning: preg_replace(): The /e modifier is no longer supported, use preg_replace_callback instead in /home/alfredo/Public/alfredo.pironti.eu/research/includes/unicode.inc on line 349.
  • warning: preg_replace(): The /e modifier is no longer supported, use preg_replace_callback instead in /home/alfredo/Public/alfredo.pironti.eu/research/includes/unicode.inc on line 349.

miTLS

Mon, 03/04/2013 - 11:42 — alfredo

miTLS is a verified reference implementation of the TLS protocol. Our code fully supports its wire formats, ciphersuites, sessions and connections, re-handshakes and resumptions, alerts and errors, and data fragmentation, as prescribed in the RFCs; it interoperates with mainstream web browsers and servers.

Spi2Java

Wed, 12/16/2009 - 17:59 — alfredo

Spi2Java is a model driven development (MDD) framework to semi-automatically generate Java security protocol implementations from verified Spi Calculus formal specifications of such protocols. The aim of the framework is to provide high correctness confidence on the generated code, thus making a step towards bridging the gap between the verified abstract formal models, and their concrete implementations.

Get more details on the Spi2Java home page.

Monitoring

Wed, 12/16/2009 - 18:02 — alfredo

Online Resources about Black-Box Monitoring and Monitorability

On this page you can find online material regarding the black-box monitoring approach for security protocol implementations.

Monitorability Measure

Download: monPV tool, along with SSL and SSH-TLP examples. Contains a README file with furhter instructions on compilation and usage.

Black-Box Monitoring

Manuscript

Pironti, A., and J. Jürjens, Black-Box Monitoring of Security Protocols, Revision 1, : Politecnico di Torino (Italy), Microsoft Research Cambridge (UK) and Open University (UK), 2009.