:comment  DARPI  (Master Thesis by Andrea Di Pasquale)
:comment  Elena Pagani -- Last update: Feb.20, 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 int
:smt (define N::nat)

:comment  phi counts the phase of the computation
:global phi 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  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  switch for checking poisoning
:global ww 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  target of a (Probe) Reply
:local tg nat


:comment  ------- SYSTEM AXIOMS -------
:system_axiom
:var x
:cnj (>= x 0)


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

:comment  cnj (= fv[z1] 1) (not (= CM[z1] 0)) (not (= CP[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 (<= 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  cnj (not (= Dr 0)) (not (= Dr 1))


: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) (= sh 0) (= sp 0) (= tp 0) (= ww 0) (= sm[x] 0) (= CM[x] 0) (= CP[x] 0) (= fv[x] 0) (= tD[x] 0) (= tg[x] 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) (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) (= fv[z1] 1) (not (= CM[z1] 0)) (not (= CP[z1] 0))
:comment  u_cnj (= phi 4) (= sm[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) (= 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  max_domain_cardinality 10


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

:comment  T1
:comment  node V sends a HONEST base Request
:comment  go to T4
:transition
:var x
:var y
:var j
:guard (= phi 0) (= x 2) (<= x N) (not (= y 2)) (<= y N) (<= 3 N)
:numcases 2
:case (= x j)
:val 1
:val sm[j]
:val CM[j]
:val CP[j]
:val y
:val 2
:val 2
:val ww
:val fv[j]
:val tD[j]
:val tg[j]
:case (not (= x j))
:val 1
:val sm[j]
:val CM[j]
:val CP[j]
:val y
:val 2
:val 2
:val ww
:val fv[j]
:val tD[j]
:val tg[j]


:comment  T2
:comment  node sends a HONEST base Request to V
:comment  update DARPI_cache -- go to T4
:transition
:var x
:var y
:var j
:guard (= phi 0) (not (= x 2)) (<= x N) (= y 2) (<= y N) (<= 3 N)
:numcases 2
:case (= x j)
:val 1
:val sm[j]
:val CM[j]
:val CP[j]
:val 2
:val x
:val x
:val ww
:val fv[j]
:val 2
:val tg[j]
:case (not (= x j))
:val 1
:val sm[j]
:val CM[j]
:val CP[j]
:val 2
:val x
:val x
:val ww
:val fv[j]
:val tD[j]
:val tg[j]


:comment  T3
:comment  host sends a MALICIOUS base Request (broadcast)
:comment  source != victim and configured; target chosen different from victim
:comment  goto T8 and successive
:transition
:var x
:var y
:var j
:guard (= phi 0) (= x 1) (not (= y 2)) (<= x N) (<= y N) (<= 3 N)
:numcases 2
:case (= x j)
:val 1
:val 3
:val CM[j]
:val CP[j]
:val y
:val x
:val 2
:val ww
:val fv[j]
:val tD[j]
:val tg[j]
:case (not (= x j))
:val 1
:val sm[j]
:val CM[j]
:val CP[j]
:val y
:val x
:val 2
:val ww
:val fv[j]
:val tD[j]
:val tg[j]


:comment  T4
:comment  host sends a MALICIOUS unsolicited Reply (broadcast)
:comment  source != victim and configured; target chosen different from victim
:comment  go to T27 and successive
:transition
:var x
:var y
:var j
:guard (= phi 0) (= x 1) (not (= y 2)) (<= x N) (<= y N) (<= 3 N)
:numcases 2
:case (= x j)
:val 8
:val 3
:val CM[j]
:val CP[j]
:val y
:val x
:val 2
:val ww
:val fv[j]
:val tD[j]
:val tg[j]
:case (not (= x j))
:val 8
:val sm[j]
:val CM[j]
:val CP[j]
:val y
:val x
:val 2
:val ww
:val fv[j]
:val tD[j]
:val tg[j]


:comment ============ END OF REQUEST GENERATION ============
:comment ============ REQUEST PROCESSING ============


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


:comment  T6
:comment  Base Request 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 generates a Reply and calls Verify() + Deny(); DARPI_cache updated upon Req generation
:transition
:var x
:var j
:guard (= phi 1) (= tp x) (= sp 2) (= tD[x] 0) (<= 3 N)
:numcases 2
:case (= x j)
:val 2
:val 1
:val 0
:val 0
:val tp
:val sh
:val sp
:val ww
:val 1
:val tD[j]
:val 2
:case (not (= x j))
:val 2
:val sm[j]
:val CM[j]
:val CP[j]
:val tp
:val sh
:val sp
:val ww
:val fv[j]
:val tD[j]
:val tg[j]


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


:comment  T7
: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) (= fv[x] 1) (not (= x 2)) (<= x N) (<= 3 N)
:numcases 2
:case (= x j)
:val 3
:val sm[j]
:val CM[j]
:val CP[j]
:val 2
:val x
:val x
:val ww
:val 0
:val 2
:val tg[j]
:case (not (= x j))
:val 3
:val sm[j]
:val CM[j]
:val CP[j]
:val 2
:val x
:val x
:val ww
:val fv[j]
:val tD[j]
:val tg[j]


:comment  T8
:comment  no host has verifications to send --> goto Reply generation
:transition
:var x
:var j
:guard (= phi 2) (= fv[x] 0) (<= 3 N)
:uguard (= fv[j] 0)
:numcases 2
:case (= x j)
:val 7
:val sm[j]
:val CM[j]
:val CP[j]
:val tp
:val sh
:val sp
:val ww
:val fv[j]
:val tD[j]
:val tg[j]
:case (not (= x j))
:val 7
:val sm[j]
:val CM[j]
:val CP[j]
:val tp
:val sh
:val sp
:val ww
:val fv[j]
:val tD[j]
:val tg[j]


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


:comment  T9
:comment  Verification Request processing when target and source!=myIP and source!=victim
:comment  lines 44-46 Algorithm 3 -- just for configured nodes
:comment  it is the victim: it would generate a Reply
:transition
:var x
:var j
:guard (= phi 3) (= tp x) (= x 2) (not (= sp x)) (<= 3 N)
:numcases 2
:case (= x j)
:val 4
:val 2
:val CM[j]
:val CP[j]
:val tp
:val sh
:val sp
:val ww
:val fv[j]
:val tD[j]
:val sp
:case (not (= x j))
:val 4
:val sm[j]
:val CM[j]
:val CP[j]
:val tp
:val sh
:val sp
:val ww
:val fv[j]
:val tD[j]
:val tg[j]


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


:comment  T10
:comment  target (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] 2) (= x 2) (<= x N) (<= tg[x] N) (<= 3 N)
:numcases 2
:case (= x j)
:val 5
:val 0
:val CM[j]
:val CP[j]
:val tg[x]
:val x
:val x
:val ww
:val fv[j]
:val tD[j]
:val 0
:case (not (= x j))
:val 5
:val sm[j]
:val CM[j]
:val CP[j]
:val tg[x]
:val x
:val x
:val ww
:val fv[j]
:val tD[j]
:val tg[j]


:comment  T11
: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) (not (= sm[x] 3)) (= tD[y] 2) (not (= y 2)) (<= x N) (<= y N) (<= 3 N)
:numcases 2
:case (= x j)
:val 5
:val 3
:val CM[j]
:val CP[j]
:val y
:val x
:val 2
:val ww
:val fv[j]
:val tD[j]
:val tg[j]
:case (not (= x j))
:val 5
:val sm[j]
:val CM[j]
:val CP[j]
:val y
:val x
:val 2
:val ww
:val fv[j]
:val tD[j]
:val tg[j]


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


:comment  T12
: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) (= x tp) (not (= sp x)) (= sp 2) (= tD[x] 2) (<= 3 N)
:numcases 2
:case (= x j)
:val 6
:val sm[j]
:val sh
:val sp
:val tp
:val sh
:val sp
:val ww
:val fv[j]
:val 0
:val tg[j]
:case (not (= x j))
:val 6
:val sm[j]
:val CM[j]
:val CP[j]
:val tp
:val sh
:val sp
:val ww
:val fv[j]
:val tD[j]
:val tg[j]


:comment  T13
:comment  go on to Reply generation (victim reply to verify may still be pending)
:comment  just to check unsafe condition
:transition
:var x
:var j
:guard (= phi 6) (= ww 0) (<= x N) (<= 3 N)
:numcases 2
:case (= x j)
:val 7
:val sm[j]
:val CM[j]
:val CP[j]
:val tp
:val sh
:val sp
:val ww
:val fv[j]
:val tD[j]
:val tg[j]
:case (not (= x j))
:val 7
:val sm[j]
:val CM[j]
:val CP[j]
:val tp
:val sh
:val sp
:val ww
:val fv[j]
:val tD[j]
:val tg[j]


:comment  ============ END OF PROCESSING OF VERIFICATION REPLY ============
:comment  ============ GENERATION OF BASE REPLY TO INITIAL BASE REQ ============


:comment  T14
:comment  victim generates Reply to verify
:comment  TS incremented of 1 tick for Request processing and Reply generation 
:transition
:var x
:var j
:guard (= phi 7) (= sm[x] 2) (= x 2) (<= x N) (<= tg[x] N) (<= 3 N)
:numcases 2
:case (= x j)
:val 8
:val 0
:val CM[j]
:val CP[j]
:val tg[x]
:val x
:val x
:val ww
:val fv[j]
:val tD[j]
:val 0
:case (not (= x j))
:val 8
:val sm[j]
:val CM[j]
:val CP[j]
:val tg[x]
:val x
:val x
:val ww
:val fv[j]
:val tD[j]
:val tg[j]


:comment  T15
:comment  target generates HONEST Reply (broadcast)
:comment  TS incremented of 1 tick for Request processing and Reply generation 
:transition
:var x
:var j
:guard (= phi 7) (= sm[x] 1) (<= x N) (<= tg[x] N) (<= 3 N)
:numcases 2
:case (= x j)
:val 8
:val 0
:val CM[j]
:val CP[j]
:val tg[x]
:val x
:val x
:val ww
:val fv[j]
:val tD[j]
:val 0
:case (not (= x j))
:val 8
:val sm[j]
:val CM[j]
:val CP[j]
:val tg[x]
:val x
:val x
:val ww
:val fv[j]
:val tD[j]
:val tg[j]


:comment  T16
:comment  malicious generates MALICIOUS UNSOLICITED Reply a target della vittima
: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 7) (= x 1) (not (= sm[x] 3)) (not (= y 2)) (= sm[y] 1) (= tg[y] 2) (= tD[y] 0) (<= x N) (<= y N) (<= 3 N)
:numcases 2
:case (= x j)
:val 8
:val 3
:val CM[j]
:val CP[j]
:val y
:val x
:val 2
:val ww
:val fv[j]
:val tD[j]
:val tg[j]
:case (not (= x j))
:val 8
:val sm[j]
:val CM[j]
:val CP[j]
:val y
:val x
:val 2
:val ww
:val fv[j]
:val tD[j]
:val tg[j]


:comment  T17
:comment  no reply (of any kind) to generate --> goto end 
:transition
:var x
:var j
:guard (= phi 7) (not (= sm[x] 2)) (not (= sm[x] 1)) (<= x N) (<= 3 N)
:uguard (not (= sm[j] 2)) (not (= sm[j] 1))
:numcases 2
:case (= x j)
:val 11
:val sm[j]
:val CM[j]
:val CP[j]
:val tp
:val sh
:val sp
:val ww
:val fv[j]
:val tD[j]
:val tg[j]
:case (not (= x j))
:val 11
:val sm[j]
:val CM[j]
:val CP[j]
:val tp
:val sh
:val sp
:val ww
:val fv[j]
:val tD[j]
:val tg[j]


:comment  ============ END OF GENERATION OF BASE REPLY ============
:comment  ============ PROCESSING OF BASE REPLY TO INITIAL BASE REQ ============


:comment  T18
:comment  Reply processing when node=target and source!=myIP and source!=victim
:comment  lines 40-43 Algorithm 3 -- just for configured nodes
:comment  node is the victim --> it would call SARPI
:transition
:var x
:var j
:guard (= phi 8) (= x tp) (not (= sp 2)) (= x 2) (<= x N) (<= 3 N)
:numcases 2
:case (= x j)
:val 9
:val sm[j]
:val CM[j]
:val CP[j]
:val tp
:val sh
:val sp
:val ww
:val fv[j]
:val tD[j]
:val tg[j]
:case (not (= x j))
:val 9
:val sm[j]
:val CM[j]
:val CP[j]
:val tp
:val sh
:val sp
:val ww
:val fv[j]
:val tD[j]
:val tg[j]


:comment  T19
: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()
:transition
:var x
:var j
:guard (= phi 8) (= x tp) (not (= sp x)) (= sp 2) (not (= tD[x] 2)) (<= x N) (<= 3 N)
:numcases 2
:case (= x j)
:val 9
:val sm[j]
:val 0
:val 0
:val tp
:val sh
:val sp
:val ww
:val 1
:val tD[j]
:val tg[j]
:case (not (= x j))
:val 9
:val sm[j]
:val CM[j]
:val CP[j]
:val tp
:val sh
:val sp
:val ww
:val fv[j]
:val tD[j]
:val tg[j]


:comment  T20
:comment  Reply processing when node=target and source!=myIP and source=victim and source in DARPI_cache
:comment  lines 40-43 Algorithm 3 -- just for configured nodes
:comment  it calls Allow() and resets DARPI_cache
:transition
:var x
:var j
:guard (= phi 8) (= x tp) (not (= sp x)) (= sp 2) (= tD[x] 2) (<= x N) (<= 3 N)
:numcases 2
:case (= x j)
:val 6
:val sm[j]
:val sh
:val sp
:val tp
:val sh
:val sp
:val 1
:val fv[j]
:val 0
:val tg[j]
:case (not (= x j))
:val 6
:val sm[j]
:val CM[j]
:val CP[j]
:val tp
:val sh
:val sp
:val 1
:val fv[j]
:val tD[j]
:val tg[j]


:comment  T21
:comment  go on to Reply generation (victim reply to verify may still be pending)
:comment  just to check unsafe condition
:transition
:var x
:var j
:guard (= phi 6) (= ww 1) (<= x N) (<= 3 N)
:numcases 2
:case (= x j)
:val 9
:val sm[j]
:val CM[j]
:val CP[j]
:val tp
:val sh
:val sp
:val 0
:val fv[j]
:val tD[j]
:val tg[j]
:case (not (= x j))
:val 9
:val sm[j]
:val CM[j]
:val CP[j]
:val tp
:val sh
:val sp
:val 0
:val fv[j]
:val tD[j]
:val tg[j]


:comment  ============ END OF PROCESSING OF BASE REPLY ============
:comment  ============ DECIDE WHAT TO DO ============


:comment  T22
:comment  all hosts processed Reply and someone must Verify() --> go back to Verify() loop (T8)
:transition
:var x
:var j
:guard (= phi 9) (= fv[x] 1) (not (= x 2)) (<= x N) (<= 3 N)
:numcases 2
:case (= x j)
:val 2
:val sm[j]
:val CM[j]
:val CP[j]
:val tp
:val sh
:val sp
:val ww
:val fv[j]
:val tD[j]
:val tg[j]
:case (not (= x j))
:val 2
:val sm[j]
:val CM[j]
:val CP[j]
:val tp
:val sh
:val sp
:val ww
:val fv[j]
:val tD[j]
:val tg[j]


:comment  T23
:comment  all hosts processed Reply and someone must Reply but none needs to Verify() --> go back to Reply loop (T20)
:transition
:var x
:var j
:guard (= phi 9) (= fv[x] 0) (<= sm[x] 2) (>= sm[x] 1) (<= x N) (<= 3 N)
:uguard (= fv[j] 0)
:numcases 2
:case (= x j)
:val 7
:val sm[j]
:val CM[j]
:val CP[j]
:val tp
:val sh
:val sp
:val ww
:val fv[j]
:val tD[j]
:val tg[j]
:case (not (= x j))
:val 7
:val sm[j]
:val CM[j]
:val CP[j]
:val tp
:val sh
:val sp
:val ww
:val fv[j]
:val tD[j]
:val tg[j]


:comment  T24
:comment  all hosts processed Reply and none must Verify() nor reply --> goto end
:comment  re-set everything but caches before new iteration
:transition
:var x
:var j
:guard (= phi 9) (= fv[x] 0) (not (= sm[x] 2)) (not (= sm[x] 1)) (<= x N) (<= 3 N)
:uguard (= fv[j] 0) (not (= sm[j] 2)) (not (= sm[j] 1))
:numcases 2
:case (= x j)
:val 11
:val sm[j]
:val CM[j]
:val CP[j]
:val tp
:val sh
:val sp
:val ww
:val fv[j]
:val tD[j]
:val tg[j]
:case (not (= x j))
:val 11
:val sm[j]
:val CM[j]
:val CP[j]
:val tp
:val sh
:val sp
:val ww
:val fv[j]
:val tD[j]
:val tg[j]


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