Routers in wireless mesh networks route traffic within the mesh as well as towards the Internet via mesh gateways. Such routers cannot be trusted as they may be in physically insecure locations and may be operated by different operators mutually distrusting each other. The goal of a secure distributed accounting protocol is to reward each operator for the amount of traffic their routers forwarded. The challenge in such protocols is to detect routers that claim to have forwarded a larger amount of traffic than they did. This requires determining the exact attack scenarios that need to be detectable, and taking into account that attackers may adapt their behavior based on knowledge of the accounting protocol used. The protocol also should create as little extra traffic in the network as possible.

Secure accounting in mobile ad-hoc, wireless mesh and multi-hop cellular networks is well studied. Most works use a deterministic approach and require additional information in packets or add explicit acknowledgements introducing a substantial overhead. Based on securely deployed mesh networks, probabilistic distributed accounting protocols are currently being developed. These probabilistic protocols exchange accounting information between neighbouring nodes and send data to a central accounting entity that combines and correlates the data from routers through the entire network. The protocol identifies routers making false claims with high probability based on the overall collected routing information. Randomising the point in time at which the accounting entity requests information from the routers will improve the load balancing, thwarting adaptive malicious behavior, and reducing the overall load.

These protocols are inherently complex, and their correctness guarantees are hard to establish. Randomised distributed algorithms are one of the key application areas of probabilistic model checking. Protocols for wireless networks such as leader election, a medium access protocol for machine-2-machine and channel access protocols have been successfully analysed using probabilistic model- checking techniques. These studies have resulted in more insight into the protocol mechanisms (such as recovery) and have led to several protocol amendments. This dissertation project aims at formally modelling probabilistic distributed accounting protocols and verifying their correctness guarantees using probabilistic model checkers such as PRISM and MRMC. We expect that the result of the probabilistic model checking will provide valuable feedback for the protocol design itself as well as the optimisation of the various parameters involved in the protocol.