-
Notifications
You must be signed in to change notification settings - Fork 0
/
NetBill.smv
127 lines (98 loc) · 3.21 KB
/
NetBill.smv
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
------------------------
-- Progetto MVSS --
-- Davide Cortellucci --
-- Matricola #260321 --
------------------------
--------------------------------------
-- Model Checking: --
-- The NetBill Transaction Protocol --
--------------------------------------
------------------------------------------------------
-- Specifiche del protocollo: --
-- http://www.sti.uniurb.it/aldini/mvss/2016s2a.pdf --
------------------------------------------------------
MODULE main
--------------------
-- Lista di stati --
--------------------
-- pr: "Price Request"
-- pq: "Price Quote"
-- gr: "Goods Request"
-- eg: "Encrypted Goods"
-- epo: "Electronic Payment Order"
-- eepo: "Endorsed EPO"
-- sr_nm: "Signed Result" (da NetBill a mercante)
-- sr_mc: "Signed Result" (da mercante a cliente)
-- ok: Transazione andata a buon fine
-- error: Transazione non completata
VAR
-- Accordo sul prezzo dei beni
bid : boolean;
-- Decisione di NetBill sulla transazione
nb_decision : boolean;
-- Identifica univocamente la transazione, evita replay attacks
epoid : boolean;
-- Checksum sui beni da mercante a cliente
cc : boolean;
-- Stati delle parti coinvolte nella transazione
cliente : {pr, gr, epo, ok, error};
mercante : {idle, pq, eg, eepo, sr_mc, error};
netbill : {idle, sr_nm, error};
ASSIGN
-- Inizializzazione
init (cliente) := pr;
init (mercante) := idle;
init (netbill) := idle;
init (bid) := {TRUE, FALSE};
init (nb_decision) := {TRUE, FALSE};
init (epoid) := {TRUE, FALSE};
init (cc) := {TRUE, FALSE};
next (bid) := bid;
next (cc) := cc;
next (nb_decision) := nb_decision;
next (epoid) := epoid;
-- Cliente
next (cliente) :=
case
cliente = pr & mercante = pq : gr;
mercante = eg & cc = FALSE : error;
mercante = eg & cc = TRUE : epo;
mercante = sr_mc : ok;
mercante = error : error;
TRUE : cliente;
esac;
-- Mercante
next (mercante) :=
case
cliente = pr & bid = FALSE : error;
cliente = pr & bid = TRUE : pq;
cliente = gr : eg;
cliente = epo : eepo;
netbill = error : error;
netbill = sr_nm : sr_mc;
TRUE : mercante;
esac;
-- NetBill
next (netbill) :=
case
mercante = eepo &
(epoid = FALSE | nb_decision = FALSE) : error;
mercante = eepo &
(epoid = TRUE & nb_decision = TRUE) : sr_nm;
TRUE : netbill;
esac;
--------------------
-- Model Checking --
--------------------
-- Per qualsiasi cammino, alla fine la transazione termina
CTLSPEC AF (cliente = ok | cliente = error);
CTLSPEC EF (cliente = ok | cliente = error);
CTLSPEC EG (netbill = error -> AX mercante = error);
-- Se la transazione è avvenuta con successo, non può essere segnalato errore e viceversa
CTLSPEC EF (cliente = ok <-> !(cliente = error));
-- Se Netbill o il mercante segnalano un qualsiasi errore, la transazione non andrà mai a buon fine
CTLSPEC AF ((netbill = error | mercante = error) -> cliente = error);
-- Se cliente e mercante non si accordano sul prezzo, la transazione non va a buon fine
CTLSPEC EF ((bid = FALSE | nb_decision = FALSE | cc = FALSE) -> cliente = error);
-- Se NetBill segnala un errore qualsiasi, il cliente non riceve la chiave e la transazione non va a buon fine
CTLSPEC AF ((cliente = eepo & nb_decision = FALSE) -> !(cliente = ok));