CLOUSEAU: verificación de propiedades de seguridad en protocolos distribuidos con probabilidades

Abstract

Presentamos una herramienta para analizar propiedades de seguridad en protocolos distribuidos. La herramienta está construida sobre los schedulers llamados fuertemente distribuidos, donde el secreto también es considerado. El secreto es presentado como una clase de equivalencia sobre acciones que las componentes no tienen acceso al él; sin embargo estas acciones pueden ser distinguidas por los que tienen autorización apropiada. También presentamos un algoritmo para resolver análisis de alcanzabilidad sobre estos tipos de modelo. El algoritmo codifica apropiadamente el modelo no determinista interpretando las decisiones de los schedulers como parámetros. El problema está en reducirlo a un problema de optimización polinomial.

We present a tool for analyzing security properties in distributed protocols. The tool is built on the so-called strongly distributed schedulers, where secrecy is also considered. The secrecy is presented as an equivalence class over actions that components do not have access to; however these actions can be distinguished by those who have proper authorization. We also present an algorithm for solving reachability analysis over these types of model. The algorithm appropriately encodes the nondeterministic model by interpreting the schedulers' decisions as parameters. The problem is to reduce it to a polynomial optimization problem.