You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
144 lines
3.9 KiB
144 lines
3.9 KiB
// non-repudiation protocol (with malicious recipient with decoder)
|
|
// Markowitch & Roggeman [MR99]
|
|
// POPTA model based on the PTA model in:
|
|
// G. Norman, D. Parker and J. Sproston
|
|
// Model checking for probabilistic timed automata
|
|
// Formal Methods in System Design 43(2):164–190 (2013)
|
|
// dxp/gxn 04/09/14
|
|
|
|
popta
|
|
|
|
// observable variables (N is hidden)
|
|
observables
|
|
last, r, mess, ack, o, x, y
|
|
endobservables
|
|
|
|
// constants
|
|
const K; // range N is chosen over
|
|
const int ad = 1; // min time to send an ack
|
|
const int AD = 4; // deadline (if ack not arrived then end protocol)
|
|
|
|
module originator
|
|
|
|
// location of originator
|
|
o : [0..4];
|
|
// 0 - init
|
|
// 1 - send
|
|
// 2 - waiting
|
|
// 3 - finished
|
|
// 4 - error
|
|
|
|
N : [0..K]; // number of messages
|
|
ack : [0..K]; // number of acks the originator has received
|
|
|
|
x : clock;
|
|
|
|
invariant
|
|
(o=0 => true) &
|
|
(o=1 => x<=0) &
|
|
(o=2 => x<=AD) &
|
|
(o=3 => true) &
|
|
(o=4 => true)
|
|
endinvariant
|
|
|
|
// init
|
|
[req] o=0 & K=1 -> 1/K : (o'=1) & (N'=1);
|
|
[req] o=0 & K=2 -> 1/K : (o'=1) & (N'=1)
|
|
+ 1/K : (o'=1) & (N'=2);
|
|
[req] o=0 & K=3 -> 1/K : (o'=1) & (N'=1)
|
|
+ 1/K : (o'=1) & (N'=2)
|
|
+ 1/K : (o'=1) & (N'=3);
|
|
|
|
[req] o=0 & K=4 -> 1/K : (o'=1) & (N'=1)
|
|
+ 1/K : (o'=1) & (N'=2)
|
|
+ 1/K : (o'=1) & (N'=3)
|
|
+ 1/K : (o'=1) & (N'=4);
|
|
[req] o=0 & K=5 -> 1/K : (o'=1) & (N'=1)
|
|
+ 1/K : (o'=1) & (N'=2)
|
|
+ 1/K : (o'=1) & (N'=3)
|
|
+ 1/K : (o'=1) & (N'=4)
|
|
+ 1/K : (o'=1) & (N'=5);
|
|
[req] o=0 & K=6 -> 1/K : (o'=1) & (N'=1)
|
|
+ 1/K : (o'=1) & (N'=2)
|
|
+ 1/K : (o'=1) & (N'=3)
|
|
+ 1/K : (o'=1) & (N'=4)
|
|
+ 1/K : (o'=1) & (N'=5)
|
|
+ 1/K : (o'=1) & (N'=6);
|
|
[req] o=0 & K=7 -> 1/K : (o'=1) & (N'=1)
|
|
+ 1/K : (o'=1) & (N'=2)
|
|
+ 1/K : (o'=1) & (N'=3)
|
|
+ 1/K : (o'=1) & (N'=4)
|
|
+ 1/K : (o'=1) & (N'=5)
|
|
+ 1/K : (o'=1) & (N'=6)
|
|
+ 1/K : (o'=1) & (N'=7);
|
|
[req] o=0 & K=8 -> 1/K : (o'=1) & (N'=1)
|
|
+ 1/K : (o'=1) & (N'=2)
|
|
+ 1/K : (o'=1) & (N'=3)
|
|
+ 1/K : (o'=1) & (N'=4)
|
|
+ 1/K : (o'=1) & (N'=5)
|
|
+ 1/K : (o'=1) & (N'=6)
|
|
+ 1/K : (o'=1) & (N'=7)
|
|
+ 1/K : (o'=1) & (N'=8);
|
|
|
|
// send
|
|
[message] o=1 & x<=0 -> (o'=2); // send message immediately
|
|
|
|
// waiting
|
|
// ack arrives
|
|
[ack] o=2 & ack<N-1 & x<=AD -> (o'=1) & (ack'=min(ack+1,K)) & (x'=0); // not last
|
|
[ack] o=2 & ack=N-1 & x<=AD -> (o'=3) & (ack'=min(ack+1,K)) & (x'=0); // last
|
|
// no ack arrives within time bound
|
|
[noack] o=2 & x>=AD -> (o'=4) & (x'=0); // ack not arrived within expected interval (stop)
|
|
|
|
endmodule
|
|
|
|
module malicious_recipient
|
|
|
|
r : [0..6];
|
|
// 0 - request
|
|
// 1 - wait
|
|
// 2 - ack
|
|
// 3 - decode1 // decode probabilistically
|
|
// 4 - decode3 // decode correctly
|
|
// 5 - send act (after successfully decoded and not last)
|
|
// 6 - decoded
|
|
|
|
mess : [0..K]; // number of mess the originator has received
|
|
|
|
last : [0..1]; // message is last
|
|
|
|
y : clock;
|
|
|
|
invariant
|
|
(r=0 => y<=0) &
|
|
(r=1 => true) &
|
|
(r=2 => true) &
|
|
(r=3 => y<=4) &
|
|
(r=4 => y<=AD+1) &
|
|
(r=5 => y<=0) &
|
|
(r=6 => true)
|
|
endinvariant
|
|
|
|
[req] r=0 & y=0 -> (r'=1); // initiate protocol
|
|
[message] r=1 -> (r'=2) & (y'=0) & (mess'=min(mess+1,K)); // receive message
|
|
[ack] r=2 & y>=ad -> (r'=1); // send ack
|
|
|
|
// try and decode
|
|
[decp] r=2 -> (r'=3); // decode probabilistically
|
|
[dec] r=2 -> (r'=4); // decode correctly
|
|
|
|
// decoding probabilistically (if fails can try again or send ack)
|
|
[] r=3 & y>=3 -> 0.75 : (r'=2) & (y'=0) + 0.25 : (r'=5) & (y'=0);
|
|
[] r=4 & y>=AD+1 -> (r'=5) & (y'=0);
|
|
|
|
// decode yields message so stop (immediate)
|
|
[] r=5 & mess=N & ack<N & y<=0 -> (r'=6) & (last'=1); // unfair
|
|
[] r=5 & mess=N & ack=N & y<=0 -> (r'=6); // fair
|
|
// decode noes not yield message as not last so continue (immediate)
|
|
[] r=5 & mess<N & y<=0 -> (r'=2); // unfair
|
|
|
|
endmodule
|
|
|
|
// unfair state reached
|
|
label "unfair" = last=1;
|
|
|