Critical security-related infrastructure often makes use of both \emph{probability} and \emph{concurrency} features and there is a need to develop mathematical tools to reason about programs consisting of both features. In my research, I aim to develop expressive and modular separation logics for reasoning about concurrent probabilistic programs using the Rocq proof assistant and the Iris separation logic framework. These program logics will enable us to formally verify correctness and security properties of security-related software systems.