A Security Calculus of Concurrent Objects for Verifying Ad Hoc Network Protocols

We present a calculus of concurrent objects for specification and security analysis of ad hoc security protocols. The communicating nodes and the network are modeled by objects, while the interactions between them are modeled by asynchronous method invocations. The internal state of an object is represented by a constant method which can be overridden. The approach is complemented by a control flow analysis which can be used to automatically check properties such as security routing. The attacker model is integrated into the analysis as set values containing the knowledge of the attacker.