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