One of our principal aims in this work is to extend the reliable derivation of implementations from specifications –so long pursued in other areas like functionality, concurrency and probability– to include security as well, and in particular quantitative security.
