4 papers
Automated Proof of Bell-LaPadula Security Properties
Maximiliano Cristia, Gianfranco Rossi
Almost fifty years ago, D.E. Bell and L. LaPadula published the first formal model of a secure system, known today as the Bell-LaPadula (BLP) model. BLP is described as a state mac…
Automated Reasoning with Restricted Intensional Sets
Maximiliano Cristiá, Gianfranco Rossi
Intensional sets, i.e., sets given by a property rather than by enumerating elements, are widely recognized as a key feature to describe complex problems (see, e.g., specification…
Set-Based Models for Cryptocurrency Software
Gustavo Betarte, Maximiliano Cristiá, Carlos Luna +2
Emin Gün Sirer once said: It's clear that writing a robust, secure smart contract requires extreme amounts of diligence. It's more similar to writing code for a nuclear power react…
Towards a formally verified implementation of the MimbleWimble cryptocurrency protocol
Gustavo Betarte, Maximiliano Cristiá, Carlos Luna +2
MimbleWimble is a privacy-oriented cryptocurrency technology encompassing security and scalability properties that distinguish it from other protocols of the kind. In this paper we…