// 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