:comment  DARPI  (Master Thesis by Andrea Di Pasquale)
:comment  Elena Pagani -- Last update: Jan.26, 2018

:comment  SIMULO SOLO LE TRANSIZIONI CON 2 COME OGGETTO
:comment  Simulo solo gestione base Request e 1 malizioso (nodo 1)
:comment  Dimostro che, se cache avvelenata, allora la vittima deve ancora mandare Verify, oppure la cache non è avvelenata 
  
:comment  Modelization with malicious hosts; no cache aging
:comment  All packets are sent broadcast, but processed just by the target
:comment  Any node (but victim) may behave maliciously against the victim.
:comment  Victim is node 2
:comment  "Honest" is any node behaving properly but different from victim

:comment  probe replay signals IP address conflict
:comment  unconfigured nodes can just send Probe and do not process any message

:comment  PROPERTY: safety (no MitM)


:index nat
:smt (define N::nat)

:comment  phi counts the phase of the computation
:global phi nat

:comment  LOCAL CLOCK: new call when TS = 100 (= 1s.)  --> T24
:comment  TS indicates the time elapsed from the last timeout
:local TS nat
:comment  flag for host sending message
:local sm nat
:comment  MAC of victim in caches
:local CM nat
:comment  IP of victim in caches
:local CP nat
:comment  flag for host updating cache
:local cu nat

:comment  all addresses (both MAC and IP) equal the node ID
:comment  target ip address
:global tp nat
:comment  source hardware address
:global sh nat
:comment  source ip address
:global sp nat

:comment  variables to manage the DARPI_cache
:comment  flag remembering execution of Verify on behalf of every node
:local fv nat
:comment  target address in DARPI_cache
:local tD nat
:comment  time (clock) in DARPI_cache
:local cD nat
:comment  target of a (Probe) Reply
:local tg nat

:comment  flag azzeramento DARPI_cache
:global Dr nat


:comment  ------- SYSTEM AXIOMS -------
:comment  none


:comment  ------- SUGGESTED INVARIANTS -------
:suggested_negated_invariants
:var z1
:cnj (not (= CP[z1] 0)) (not (= CP[z1] 2))
:end_of_suggested_negated_invariants

:comment  GLI INVARIANTI QUI SOTTO SONO TUTTI TESTATI E VERI  (13)
:comment  cnj (= fv[z1] 1) (not (= CM[z1] 0)) (not (= CP[z1] 0))
:comment  cnj (= fv[z1] 1) (not (= CM[z1] 0))
:comment  cnj (not (= CP[z1] 0)) (not (= CP[z1] 2))
:comment  cnj (not (= tD[z1] 0)) (not (= tD[z1] 2))
:comment  cnj (not (<= phi 7))
:comment  cnj (not (<= I (+ N 1)))
:comment  cnj (not (<= cD[z1] TS[z1]))
:comment  cnj (not (= sm[z1] 0)) (not (= sm[z1] 1))
:comment  cnj (not (= fv[z1] 0)) (not (= fv[z1] 1))
:comment  cnj (not (= cu[z1] 0)) (not (= cu[z1] 1))
:comment  cnj (> sh N)
:comment  cnj (> CM[z1] N)
:comment  cnj (> tg[z1] N)


:comment  ------- INITIAL & UNSAFE -------

:initial
:var x
:comment  no process has done anything; this includes Clean() policy
:comment  lines 4-5 Algorithm 1
:cnj (= phi 0) (= TS[x] 0) (= sh 0) (= sp 0) (= tp 0) (= sm[x] 0) (= CM[x] 0) (= CP[x] 0) (= cu[x] 0) (= fv[x] 0) (= tD[x] 0) (= cD[x] 0) (= tg[x] 0) (= Dr 0)


:unsafe
:var z1
:var z2
:var z3
:comment  MITM VERIFICATION - uncomment subsequent conjunct
:comment  >=1 process remembers MAC(v)!= v for IP(v)=v
:comment  cnj (not (= CM[z1] 2)) (= CP[z1] 2)
:cnj (= phi 6) (= Dr 0) (not (= CM[z1] CP[z1])) (not (= z1 z2)) (= z2 2) (= sm[z2] 0) (= z3 CM[z1]) (>= sm[z3] 0)


:comment ALTRI INVARIANTI DA PROVARE
:u_cnj (= phi 2) (= cu[z1] 1) (= fv[z1] 1) (not (= CM[z1] 0)) (not (= CP[z1] 0))
:comment  u_cnj (> sp N)
:comment  u_cnj (> tp N)
:comment  u_cnj (= sp 2) (= tp 2)
:comment  u_cnj (= tD[z1] 2) (not (= sp z1)) (not (= sp 2))
:comment  u_cnj (= z2 2) (= tD[z1] 2) (= sm[z2] 1) (not (= tg[z2] z1))
:comment  u_cnj (= tD[z1] 2) (not (= CM[z1] 0)) (not (= CP[z1] 0))
:comment  u_cnj (= z2 2) (= phi 3) (= tp 2) (= tD[z1] 2) (= sh z1) (= sp z1) (>= I N) (= CM[z1] 0) (= CP[z1] 0) (= cu[z2] 1) (not (= sm[z2] 1)) (not (= tg[z2] z1))
:comment  u_cnj (= phi 5) (= sp 2) (= tD[z1] 2) (= cu[z1] 0) (not (= tp z1)) (not (= CM[z1] 0)) (not (= CP[z1] 0))

:comment  u_cnj (< N 3)


:comment  max_domain_cardinality 3


:comment  ------- TRANSITIONS -------

:comment  T1
:comment  byzantine node sends a MALICIOUS unsolicited reply
:comment  go to T4
:transition
:var x
:var y
:var j
:guard (= phi 0) (= x 1) (<= x N) (not (= y 2)) (<= y N) (<= TS[x] 100) (<= 3 N)
:numcases 2
:case (= x j)
:val 2
:val (+ TS[j] 1)
:val sm[j]
:val CM[j]
:val CP[j]
:val 1
:val y
:val x
:val 2
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]
:val Dr
:case (not (= x j))
:val 2
:val (+ TS[j] 1)
:val sm[j]
:val CM[j]
:val CP[j]
:val 0
:val y
:val x
:val 2
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]
:val Dr


:comment ============ END OF REPLY GENERATION ============
:comment ============ REPLY PROCESSING ============


:comment  T2 (5)
:comment  Reply processing when node != target --> skip
:comment  just for configured nodes -- lines 44-46 Algorithm 3
:transition
:var x
:var j
:guard (= phi 2) (= cu[x] 0) (not (= x tp)) (<= TS[x] 100) (<= 3 N)
:numcases 2
:case (= x j)
:val phi
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val 1
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]
:val Dr
:case (not (= x j))
:val phi
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]
:val Dr


:comment  T3 (7)
:comment  Reply processing when target and source!=myIP and source=victim and source not in DARPI_cache
:comment  lines 17-25 Algorithm 3 -- just for configured nodes
:comment  it calls Verify() + Deny(); DARPI_cache updated upon Req generation
:transition
:var x
:var j
:guard (= phi 2) (= cu[x] 0) (= tp x) (= sp 2) (= tD[x] 0) (<= TS[x] 100) (<= 3 N)
:numcases 2
:case (= x j)
:val phi
:val TS[j]
:val sm[j]
:val 0
:val 0
:val 1
:val tp
:val sh
:val sp
:val 1
:val tD[j]
:val cD[j]
:val tg[j]
:val Dr
:case (not (= x j))
:val phi
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]
:val Dr


:comment ============ END OF REPLY PROCESSING ============
:comment ============ GENERATION OF VERIFICATIONS ============


:comment  T4 (9)
:comment  host performs Verify() --> HONEST Request generation
:comment  DARPI_cache updated -- lines 11-13 Algorithm 3
:comment  TS incremented of 1 tick for Request processing and verification generation 
:transition
:var x
:var j
:guard (= phi 2) (= cu[x] 1) (= fv[x] 1) (not (= x 2)) (<= x N) (= fv[2] 0) (<= TS[x] 100) (<= 3 N)
:uguard (= cu[j] 1)
:numcases 2
:case (= x j)
:val 3
:val (+ TS[j] 1)
:val sm[j]
:val CM[j]
:val CP[j]
:val 1
:val 2
:val x
:val x
:val 0
:val 2
:val TS[j]
:val tg[j]
:val Dr
:case (not (= x j))
:val 3
:val (+ TS[j] 1)
:val sm[j]
:val CM[j]
:val CP[j]
:val 0
:val 2
:val x
:val x
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]
:val Dr


:comment ============ END OF VERIFICATION GENERATION ============
:comment ============ VERIFICATION PROCESSING ============


:comment  T5 (11)
:comment  Verify processing when node != target --> skip
:comment  just for configured nodes -- lines 44-46 Algorithm 3
:transition
:var x
:var j
:guard (= phi 3) (= cu[x] 0) (not (= x tp)) (not (= x 2)) (<= TS[x] 100) (<= 3 N)
:numcases 2
:case (= x j)
:val phi
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val 1
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]
:val Dr
:case (not (= x j))
:val phi
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]
:val Dr


:comment  T6 (12)
:comment  Victim processing when target and source!=myIP and source!=victim
:comment  lines 44-46 Algorithm 3 -- just for configured nodes
:comment  this is the victim; it would generate a Reply and call SARPI
:transition
:var x
:var j
:guard (= phi 3) (= cu[x] 0) (= tp x) (= x 2) (not (= sp x)) (<= TS[x] 100) (<= 3 N)
:numcases 2
:case (= x j)
:val phi
:val TS[j]
:val 1
:val CM[j]
:val CP[j]
:val 1
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val sp
:val Dr
:case (not (= x j))
:val phi
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]
:val Dr


:comment  T7 (13)
:comment  Verification processing terminated
:transition
:var x
:var j
:guard (= phi 3) (= cu[x] 1) (<= 3 N)
:uguard (= cu[j] 1)
:numcases 2
:case (= x j)
:val 4
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val 0
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]
:val Dr
:case (not (= x j))
:val 4
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val 0
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]
:val Dr


:comment ============ END OF VERIFICATION PROCESSING ============
:comment ============ REPLY GENERATION ============


:comment  T8 (16)
:comment  malicious generates MALICIOUS UNSOLICITED Reply (broadcast)
:comment  neither target nor Request source are the victim
:comment  TS incremented of 1 tick for Request processing and Reply generation 
:transition
:var x
:var y
:var j
:guard (= phi 4) (= x 1) (= sm[x] 0) (= tD[y] 2) (not (= y 2)) (= sm[2] 0) (<= x N) (<= y N) (<= TS[x] 100) (<= 3 N)
:numcases 2
:case (= x j)
:val 5
:val (+ TS[j] 1)
:val sm[j]
:val CM[j]
:val CP[j]
:val 1
:val y
:val x
:val 2
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]
:val Dr
:case (not (= x j))
:val 5
:val (+ TS[j] 1)
:val sm[j]
:val CM[j]
:val CP[j]
:val 0
:val y
:val x
:val 2
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]
:val Dr


:comment  T8.1 (14)
:comment  victim generates HONEST Reply (broadcast)
:comment  TS incremented of 1 tick for Request processing and Reply generation 
:transition
:var x
:var j
:guard (= phi 4) (= sm[x] 1) (= x 2) (<= x N) (<= tg[x] N) (<= TS[x] 100) (<= 3 N)
:numcases 2
:case (= x j)
:val 5
:val (+ TS[j] 1)
:val 0
:val CM[j]
:val CP[j]
:val 1
:val tg[x]
:val 2
:val 2
:val fv[j]
:val tD[j]
:val cD[j]
:val 0
:val Dr
:case (not (= x j))
:val 5
:val (+ TS[j] 1)
:val sm[j]
:val CM[j]
:val CP[j]
:val 0
:val tg[x]
:val 2
:val 2
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]
:val Dr


:comment ============ END OF REPLY GENERATION ============
:comment ============ REPLY PROCESSING ============


:comment  T9 (17)
:comment  Reply processing when node != target --> skip
:comment  just for configured nodes
:transition
:var x
:var j
:guard (= phi 5) (= cu[x] 0)(not (= x tp)) (not (= tp 2))  (<= TS[x] 100) (<= 3 N)
:numcases 2
:case (= x j)
:val phi
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val 1
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]
:val Dr
:case (not (= x j))
:val phi
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]
:val Dr


:comment  T10 (19)
:comment  Reply processing when node=target and source!=myIP and source=victim and source in DARPI_cache
:comment  lines 36-39 Algorithm 3 -- just for configured nodes
:comment  it calls Allow() and resets DARPI_cache
:transition
:var x
:var j
:guard (= phi 5) (= cu[x] 0) (= x tp) (not (= sp x)) (= sp 2) (= tD[x] 2) (<= TS[x] 100) (<= 3 N)
:numcases 2
:case (= x j)
:val phi
:val TS[j]
:val sm[j]
:val sh
:val sp
:val 1
:val tp
:val sh
:val sp
:val fv[j]
:val 0
:val 0
:val tg[j]
:val Dr
:case (not (= x j))
:val phi
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]
:val Dr


:comment  T11 (21)
:comment  all hosts processed Reply --> decide what to do
:transition
:var x
:var j
:guard (= phi 5) (= cu[x] 1) (<= 3 N)
:uguard (= cu[j] 1)
:numcases 2
:case (= x j)
:val 6
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]
:val Dr
:case (not (= x j))
:val 6
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]
:val Dr


:comment  T12 (14)
:comment  victim generates HONEST Reply (broadcast)
:comment  TS incremented of 1 tick for Request processing and Reply generation 
:transition
:var x
:var j
:guard (= phi 6) (= sm[x] 1) (= x 2) (<= x N) (<= tg[x] N) (<= TS[x] 100) (<= 3 N)
:numcases 2
:case (= x j)
:val 7
:val (+ TS[j] 1)
:val 0
:val CM[j]
:val CP[j]
:val 1
:val tg[x]
:val 2
:val 2
:val fv[j]
:val tD[j]
:val cD[j]
:val 0
:val Dr
:case (not (= x j))
:val 7
:val (+ TS[j] 1)
:val sm[j]
:val CM[j]
:val CP[j]
:val 0
:val tg[x]
:val 2
:val 2
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]
:val Dr


:comment  T12.1 (14)
:comment  victim has no reply to generate --> go to last check
:transition
:var x
:var j
:guard (= phi 6) (= sm[x] 0) (= x 2) (<= x N) (= tg[x] 0) (<= TS[x] 100) (<= 3 N)
:numcases 2
:case (= x j)
:val 7
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val 1
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]
:val Dr
:case (not (= x j))
:val 7
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val 1
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]
:val Dr


:comment  T13 (17)
:comment  Reply processing when node != target --> skip
:comment  just for configured nodes
:transition
:var x
:var j
:guard (= phi 7) (= cu[x] 0) (not (= x tp)) (not (= tp 2))  (<= TS[x] 100) (<= 3 N)
:numcases 2
:case (= x j)
:val phi
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val 1
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]
:val Dr
:case (not (= x j))
:val phi
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]
:val Dr


:comment  T14 (20)
:comment  Reply processing when node=target and source!=myIP and source=victim and source not in DARPI_cache
:comment  lines 40-43 Algorithm 3 -- just for configured nodes
:comment  it calls Verify()+Deny() and resets DARPI_cache
:transition
:var x
:var j
:guard (= phi 7) (= cu[x] 0) (= x tp) (not (= sp x)) (= sp 2) (not (= tD[x] 2)) (<= TS[x] 100) (<= 3 N)
:numcases 2
:case (= x j)
:val phi
:val TS[j]
:val sm[j]
:val 0
:val 0
:val 1
:val tp
:val sh
:val sp
:val 1
:val tD[j]
:val cD[j]
:val tg[j]
:val Dr
:case (not (= x j))
:val phi
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]
:val Dr


:comment  T15 (9)
:comment  host performs Verify() --> HONEST Request generation
:comment  DARPI_cache updated -- lines 11-13 Algorithm 3
:comment  TS incremented of 1 tick for Request processing and verification generation 
:transition
:var x
:var j
:guard (= phi 7) (= cu[x] 1) (= fv[x] 1) (not (= x 2)) (<= x N) (= fv[2] 0) (<= TS[x] 100) (<= 3 N)
:uguard (= cu[j] 1)
:numcases 2
:case (= x j)
:val 3
:val (+ TS[j] 1)
:val sm[j]
:val CM[j]
:val CP[j]
:val 1
:val 2
:val x
:val x
:val 0
:val 2
:val TS[j]
:val tg[j]
:val Dr
:case (not (= x j))
:val 3
:val (+ TS[j] 1)
:val sm[j]
:val CM[j]
:val CP[j]
:val 0
:val 2
:val x
:val x
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]
:val Dr


:comment  T15.1 (9)
:comment  host has not to perform Verify() --> goto END
:transition
:var x
:var j
:guard (= phi 7) (= cu[x] 1) (= fv[x] 0) (not (= x 2)) (<= x N) (= fv[2] 0) (<= TS[x] 100) (<= 3 N)
:uguard (= cu[j] 1)
:numcases 2
:case (= x j)
:val 11
:val (+ TS[j] 1)
:val sm[j]
:val CM[j]
:val CP[j]
:val 1
:val 2
:val x
:val x
:val 0
:val 2
:val TS[j]
:val tg[j]
:val Dr
:case (not (= x j))
:val 11
:val (+ TS[j] 1)
:val sm[j]
:val CM[j]
:val CP[j]
:val 0
:val 2
:val x
:val x
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]
:val Dr


:comment ============ END OF REPLY PROCESSING ============
:comment ============ TIMEOUT: CLEANING OF DARPI_CACHE ============


:comment  T16 (25)
:comment  lines 5-7 Algorithm 3 -- cleaning of DARPI_cache
:comment  performed just for configured nodes; the other nodes can only execute T1
:transition
:var x
:var j
:guard (>= TS[x] 100) (<= 3 N)
:numcases 2
:case (= x j)
:val phi
:val 0
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val tp
:val sh
:val sp
:val fv[j]
:val 0
:val 0
:val tg[j]
:val 1
:case (not (= x j))
:val phi
:val TS[j]
:val sm[j]
:val CM[j]
:val CP[j]
:val cu[j]
:val tp
:val sh
:val sp
:val fv[j]
:val tD[j]
:val cD[j]
:val tg[j]
:val 1