BANANA is a tool for the analysis of information leakage in mobile ambient specifications. The language considered is Mobile Ambient calculus, initially proposed by Cardelli and Gordon with the main purpose of explicitly modeling mobility. Sites and agents (i.e., processes) are modeled as nested boxes (i.e., ambients), provided with capabilities for entering, exiting and dissolving other boxes. This specification language provides a very simple framework to reason about information flow and security when mobility is an issue.
Keywords for this software
References in zbMATH (referenced in 3 articles , 1 standard article )
Showing results 1 to 3 of 3.
- Braghin, Chiara; Cortesi, Agostino; Focardi, Riccardo: Information flow security in boundary ambients (2008)
- Braghin, Chiara; Cortesi, Agostino; Focardi, Riccardo; Luccio, Flaminia L.; Piazza, Carla: Nesting analysis of mobile ambients (2004)
- Braghin, Chiara; Cortesi, Agostino; Filippone, Stefano; Focardi, Riccardo; Luccio, Flaminia L.; Piazza, Carla: BANANA -- A tool for boundary ambients nesting analysis (2003)
Further publications can be found at: http://www.dsi.unive.it/~mefisto/BANANA/references.html