model checking, social networks, prism, information leakage