If you're prepared to look beyond model checking you could start with
McIver & Morgan's monograph. Probabilistic aspects as those described formally in the book become quite important when investigating the presence of covert channels in systems that are meant to protect secrets. There's quite an active area of research around that. You could look for
quantitative information flow if you wanted to learn more.