const int T; // Maximum probability that malicious recepient gains information Pmax=? [ F "gains_information" ] // Maximum probability that malicious recepient gains information by deadline T Pmax=? [ F<=T "gains_information" ]