-- I) Base case
open BASE-NSLPK
-- check
  red inv1(init,n) .
close

-- II) Inductive cases

--> 1) sdm1(s,p10,q10,r10)
--> c-sdm1(s,p10,q10,r10), ~(q10 = intruder)
open ISTEP-NSLPK
-- fresh constants
  ops p10 q10 : -> Principal .
  op r10 : -> Random .
-- assumptions
  -- eq c-sdm1(s,p10,q10,r10) = true .
  eq r10 \in rands(s) = false .
  --
  eq (q10 = intruder) = false .
-- successor state
  eq s' = sdm1(s,p10,q10,r10) .
-- check 
  red istep1 .
close
--> c-sdm1(s,p10,q10,r10), q10 = intruder
open ISTEP-NSLPK
-- fresh constants
  ops p10 q10 : -> Principal .
  op r10 : -> Random .
-- assumptions
  -- eq c-sdm1(s,p10,q10,r10) = true .
  eq r10 \in rands(s) = false .
  --
  eq q10 = intruder .
-- successor state
  eq s' = sdm1(s,p10,q10,r10) .
-- check 
  red istep1 .
close
--> ~c-sdm1(s,p10,q10,r10)
open ISTEP-NSLPK
-- fresh constants
  ops p10 q10 : -> Principal .
  op r10 : -> Random .
-- assumptions
  eq c-sdm1(s,p10,q10,r10) = false .
-- successor state
  eq s' = sdm1(s,p10,q10,r10) .
-- check 
  red istep1 .
close

--> 2) sdm2(s,p10,q10,r10,n10)
--> c-sdm2(s,p10,q10,r10,n10), ~(q10 = intruder)
open ISTEP-NSLPK
-- fresh constants
  ops p10 q10 : -> Principal .
  op r10 : -> Random .
  op n10 : -> Nonce .
  op nw10 : -> Network .
-- assumptions
  -- eq c-sdm2(s,p10,q10,r10,n10) = true .
  eq network(s) = enc1(p10,n10,q10) nw10 .
  eq r10 \in rands(s) = false .
  --
  eq (q10 = intruder) = false .
-- successor state
  eq s' = sdm2(s,p10,q10,r10,n10) .
-- check 
  red istep1 .
close
--> c-sdm2(s,p10,q10,r10,n10), q10 = intruder, ~(n = n10)
open ISTEP-NSLPK
-- fresh constants
  ops p10 q10 : -> Principal .
  op r10 : -> Random .
  op n10 : -> Nonce .
  op nw10 : -> Network .
-- assumptions
  -- eq c-sdm2(s,p10,q10,r10,n10) = true .
  eq network(s) = enc1(p10,n10,q10) nw10 .
  eq r10 \in rands(s) = false .
  --
  eq q10 = intruder .
  eq (n = n10) = false .
-- successor state
  eq s' = sdm2(s,p10,q10,r10,n10) .
-- check 
  red istep1 .
close
--> c-sdm2(s,p10,q10,r10,n10), q10 = intruder, n = n10
open ISTEP-NSLPK
-- fresh constants
  ops p10 q10 : -> Principal .
  op r10 : -> Random .
  op n10 : -> Nonce .
  op nw10 : -> Network .
-- assumptions
  -- eq c-sdm2(s,p10,q10,r10,n10) = true .
  eq network(s) = enc1(p10,n10,q10) nw10 .
  eq r10 \in rands(s) = false .
  --
  eq q10 = intruder .
  eq n = n10 .
-- successor state
  eq s' = sdm2(s,p10,q10,r10,n10) .
-- check 
  red inv2(s,p10,n) implies istep1 .
close
--> ~c-sdm2(s,p10,q10,r10,n10)
open ISTEP-NSLPK
-- fresh constants
  ops q10? p10 q10 : -> Principal .
  op r10 : -> Random .
  op n10 : -> Nonce .
-- assumptions
  eq c-sdm2(s,p10,q10,r10,n10) = false .
-- successor state
  eq s' = sdm2(s,p10,q10,r10,n10) .
-- check 
  red istep1 .
close

--> 3) sdm3(s,p10,q10,n10,n20)
--> c-sdm3(s,p10,q10,n10,n20), ~(q10 = intruder)
open ISTEP-NSLPK
-- fresh constants
  ops p10 q10 : -> Principal .
  ops n10 n20 : -> Nonce .
  op nw10 : -> Network .
-- assumptions
  -- eq c-sdm3(s,p10,q10,n10,n20) = true .
  eq network(s) = enc1(q10,n10,p10) enc2(p10,n10,n20,q10) nw10 .
  --
  eq (q10 = intruder) = false .
-- successor state
  eq s' = sdm3(s,p10,q10,n10,n20) .
-- check 
  red istep1 .
close
--> c-sdm3(s,p10,q10,n10,n20), q10 = intruder, ~(n = n20)
open ISTEP-NSLPK
-- fresh constants
  ops p10 q10 : -> Principal .
  ops n10 n20 : -> Nonce .
  op nw10 : -> Network .
-- assumptions
  -- eq c-sdm3(s,p10,q10,n10,n20) = true .
  eq network(s) = enc1(q10,n10,p10) enc2(p10,n10,n20,q10) nw10 .
  --
  eq q10 = intruder .
  eq (n = n20) = false .
-- successor state
  eq s' = sdm3(s,p10,q10,n10,n20) .
-- check 
  red istep1 .
close
--> c-sdm3(s,p10,q10,n10,n20), q10 = intruder, n = n20
open ISTEP-NSLPK
-- fresh constants
  ops p10 q10 : -> Principal .
  ops n10 n20 : -> Nonce .
  op nw10 : -> Network .
-- assumptions
  -- eq c-sdm3(s,p10,q10,n10,n20) = true .
  eq network(s) = enc1(q10,n10,p10) enc2(p10,n10,n20,q10) nw10 .
  --
  eq q10 = intruder .
  eq n = n20 .
-- successor state
  eq s' = sdm3(s,p10,q10,n10,n20) .
-- check 
  red inv3(s,p10,n10,n20) implies istep1 .
close
--> ~c-sdm3(s,p10,q10,n10,n20)
open ISTEP-NSLPK
-- fresh constants
  ops p10 q10 : -> Principal .
  ops n10 n20 : -> Nonce .
-- assumptions
  eq c-sdm3(s,p10,q10,n10,n20) = false .
-- successor state
  eq s' = sdm3(s,p10,q10,n10,n20) .
-- check 
  red istep1 .
close

--> 4) fkm1(s,p10,q10,n10)
--> c-fkm1(s,p10,q10,n10)
open ISTEP-NSLPK
-- fresh constants
  ops p10 q10 : -> Principal .
  op n10 : -> Nonce .
  op ns10 : -> NonceBag .
-- assumptions
  -- eq c-fkm1(s,p10,q10,n10) = true .
  eq nonces(s) = n10 ns10 .
  --
-- successor state
  eq s' = fkm1(s,p10,q10,n10) .
-- check 
  red istep1 .
close
--> ~c-fkm1(s,p10,q10,n10)
open ISTEP-NSLPK
-- fresh constants
  ops p10 q10 : -> Principal .
  op n10 : -> Nonce .
-- assumptions
  eq c-fkm1(s,p10,q10,n10) = false .
-- successor state
  eq s' = fkm1(s,p10,q10,n10) .
-- check 
  red istep1 .
close

--> 5) fkm2(s,p10,q10,n10,n20)
--> c-fkm2(s,p10,q10,n10,n20)
open ISTEP-NSLPK
-- fresh constants
  ops p10 q10 : -> Principal .
  ops n10 n20 : -> Nonce .
  op ns10 : -> NonceBag .
-- assumptions
  -- eq c-fkm2(s,p10,q10,n10,n20) = true .
  eq nonces(s) = n10 n20 ns10 .
  --
-- successor state
  eq s' = fkm2(s,p10,q10,n10,n20) .
-- check 
  red istep1 .
close
--> ~c-fkm2(s,p10,q10,n10,n20)
open ISTEP-NSLPK
-- fresh constants
  ops p10 q10 : -> Principal .
  ops n10 n20 : -> Nonce .
-- assumptions
  eq c-fkm2(s,p10,q10,n10,n20) = false .
-- successor state
  eq s' = fkm2(s,p10,q10,n10,n20) .
-- check 
  red istep1 .
close

--> 6) fkm3(s,q10,n10)
--> c-fkm3(s,q10,n10)
open ISTEP-NSLPK
-- fresh constants
  op q10 : -> Principal .
  op n10 : -> Nonce .
  op ns10 : -> NonceBag .
-- assumptions
  -- eq c-fkm3(s,q10,n10) = true .
  eq nonces(s) = n10 ns10 .
  --
-- successor state
  eq s' = fkm3(s,q10,n10) .
-- check 
  red istep1 .
close
--> ~c-fkm3(s,q10,n10)
open ISTEP-NSLPK
-- fresh constants
  op q10 : -> Principal .
  op n10 : -> Nonce .
-- assumptions
  eq c-fkm3(s,q10,n10) = false .
-- successor state
  eq s' = fkm3(s,q10,n10) .
-- check 
  red istep1 .
close

-- Q.E.D.