// Model for PIN Block attack analysis // Auto generated by AnaBlock // Author G. Steel, Aug 2005 // This file contains just a fragment of a full PIN cracking attack // It is intended to illustrate the representation used for PIN ranges // and corresponds to tree fragment shown in the final figure at // http://www.prismmodelchecker.org/casestudies/pincracking.php mdp module M1 P3_could_be0 : bool init true; P3_could_be1 : bool init true; P3_could_be2 : bool init true; P3_could_be3 : bool init true; P3_could_be4 : bool init true; P3_could_be5 : bool init true; P3_could_be6 : bool init true; P3_could_be7 : bool init true; P3_could_be8 : bool init true; P3_could_be9 : bool init true; P3_guessed : bool init false; PIN_Digit3 : [0..10] init 10; Digit_Count : [1..5] init 3; // xor_in(2) [] !P3_guessed & Digit_Count=3 & P3_could_be0& P3_could_be1& P3_could_be2& P3_could_be3& P3_could_be4& P3_could_be5& P3_could_be6& P3_could_be7& P3_could_be8& P3_could_be9 -> // error case 2/10: (Digit_Count'=4)&(P3_could_be0'=false) & (P3_could_be1'=false) & (P3_could_be2'=false) & (P3_could_be3'=false) & (P3_could_be4'=false) & (P3_could_be5'=false) & (P3_could_be6'=false) & (P3_could_be7'=false) + 8/10: (Digit_Count'=3)&(P3_could_be8'=false) & (P3_could_be9'=false) ; // xor_in(8) [] !P3_guessed & Digit_Count=3 & P3_could_be0& P3_could_be1& P3_could_be2& P3_could_be3& P3_could_be4& P3_could_be5& P3_could_be6& P3_could_be7& P3_could_be8& P3_could_be9 -> // error case 6/10: (Digit_Count'=3)&(P3_could_be0'=false) & (P3_could_be1'=false) & (P3_could_be8'=false) & (P3_could_be9'=false) + 4/10: (Digit_Count'=3)&(P3_could_be2'=false) & (P3_could_be3'=false) & (P3_could_be4'=false) & (P3_could_be5'=false) & (P3_could_be6'=false) & (P3_could_be7'=false) ; // xor_in(10) [] !P3_guessed & Digit_Count=3 & P3_could_be0& P3_could_be1& P3_could_be2& P3_could_be3& P3_could_be4& P3_could_be5& P3_could_be6& P3_could_be7& P3_could_be8& P3_could_be9 -> // error case 6/10: (Digit_Count'=3)&(P3_could_be2'=false) & (P3_could_be3'=false) & (P3_could_be8'=false) & (P3_could_be9'=false) + 4/10: (Digit_Count'=3)&(P3_could_be0'=false) & (P3_could_be1'=false) & (P3_could_be4'=false) & (P3_could_be5'=false) & (P3_could_be6'=false) & (P3_could_be7'=false) ; endmodule rewards [] true : 1; endrewards