Reasoning about Security in Mobile Ambients