Increasingly pervasive computing throws up scenarios where users may wish to achieve some degree of security in their interaction with other people or equipment, in contexts where the entities involved cannot be confident of the others’ long term identities and where there may be no PKI which can validate entities to each other. We examine the problem of bootstrapping security in an ad-hoc network formed by a group of users. In [3] a number of protocols using low-bandwidth channels involving the human agent(s) “in the loop” to bootstrap secure communication over an untrusted infrastructure were presented, the point being that it is reasonable to suppose that the attacker’s powers are more limited with regard to these empirical channels in one or more respects than in the standard Dolev-Yao view. The two-party protocols proved easy to verify [6] (relative to those weakened powers) by adapting the CSP/FDR-based approach of Casper [9], but the multi-party network-formation proto...