Behind BANANA: Design and Implementation of a Tool for Nesting Analysis of Mobile Ambients