a fragment of a full PIN cracking attack

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