NAME

ncStateByRedirect4Reachable - Verifying State Machine: Redirect vs. REACHABLE

TARGET

Host only

SYNOPSIS

  ncStateByRedirect4Reachable.seq [-tooloption ...] -p ncStateByRedirect4Reachable.def

INITIALIZATION

Set R1 as the default router by sending RA and NA.
Set TN's Neighbor Cache State to REACHABLE.
Cache either TN's LLA, or a bogus LLA

Cache a LLA of TN

  TN                 NUT
  ----------------------


  State: NONCE (for all)


  ==== unsolicited RA ===>
       src=R1's link-local
       dst=all-node
       M=0, O=0
       RouterLifetime=600
       ReachableTime=0
       RetransTimer=0
       w/ SLLA
       Prefix Option:
           L=1, A=1
           ValidLifetime=2592000
           PreferredLifetime=604800
           Prefix=3ffe:501:ffff:100::/64


  State: STALE (for R1), NONCE (for TN)


  ==== solicited NA ===>
        src=R1's link-local
        dst=NUT's link-local
        R=1, S=1, O=1
        target=R1's link-local
        TLLA=R1's LLA


  State: REACHABLE (for R1), NONCE (for TN)


  Wait (3 sec) for DAD NS


  ==== unsolicited RA ===>
       src=TN's link-local
       dst=all-node
       M=0, O=0
       RouterLifetime=600
       ReachableTime=0
       RetransTimer=0
       w/ SLLA
       Prefix Option:
           L=1, A=1
           ValidLifetime=2592000
           PreferredLifetime=604800
           Prefix=3ffe:501:ffff:100::/64


  State: REACHABLE (for R1), STALE (for TN)


  ==== solicited NA ===>
        src=TN's link-local
        dst=NUT's link-local
        R=1, S=1, O=1
        target=R1's link-local
        TLLA=TN's LLA


  State: REACHABLE (for R1), REACHABLE (for TN)

Cache a bogus LLA

  TN                 NUT
  ----------------------


  State: NONCE (for all)


  ==== unsolicited RA ===>
       src=R1's link-local
       dst=all-node
       M=0, O=0
       RouterLifetime=600
       ReachableTime=0
       RetransTimer=0
       w/ SLLA
       Prefix Option:
           L=1, A=1
           ValidLifetime=2592000
           PreferredLifetime=604800
           Prefix=3ffe:501:ffff:100::/64


  State: STALE (for R1), NONCE (for TN)


  ==== solicited NA ===>
        src=R1's link-local
        dst=NUT's link-local
        R=1, S=1, O=1
        target=R1's link-local
        TLLA=R1's LLA


  State: REACHABLE (for R1), NONCE (for TN)


  Wait (3 sec) for DAD NS


  ==== unsolicited RA ===>
       src=TN's link-local
       dst=all-node
       M=0, O=0
       RouterLifetime=600
       ReachableTime=0
       RetransTimer=0
       w/ SLLA
       Prefix Option:
           L=1, A=1
           ValidLifetime=2592000
           PreferredLifetime=604800
           Prefix=3ffe:501:ffff:100::/64


  State: REACHABLE (for R1), STALE (for TN)


  ==== solicited NA ===>
        src=TN's link-local
        dst=NUT's link-local
        R=1, S=1, O=1
        target=R1's link-local
        TLLA=bogus LLA


  State: REACHABLE (for R1), REACHABLE (for TN)

TEST PROCEDURE

ncStateByRedirect4Reachable verifies that state transition for a NUT in REACHABLE state when receiving a Redirect.

  TN               NUT
  ----------------------


  State: REACHABLE (for R1), REACHABLE (for TN)


  ==== Redirect ===>
      src=R1's link-local
      dst=NUT's link-local
      icmp target=TN's link-local
      icmp dst=H1's global
      w/ or w/o TLL option (i.e. TN's LLA)
      w/ or w/o Redirected header option


  Judgment: Examining NUT's neighbor cache state

JUDGMENT


8.3.  Host Specification


   If the redirect contains a Target Link-Layer Address option the host
   either creates or updates the Neighbor Cache entry for the target.
   In both cases the cached link-layer address is copied from the Target
   Link-Layer Address option.  If a Neighbor Cache entry is created for
   the target its reachability state MUST be set to STALE as specified
   in Section 7.3.3.  If a cache entry already existed and it is updated
   with a different link-layer address, its reachability state MUST also
   be set to STALE.  If the link-layer address is the same as that
   already in the cache, the cache entry's state remains unchanged.

  =====================+=====================+===========+=============================
  IP                   |ICMP                 |Option     |NC state
  ----------+----------+----------+----------+-----+-----+---------+---------+---------
  Src       |Dst       |Target    |Dst       |TLLA |R'ed |Current   |New      |LLA
  ==========+==========+==========+==========+=====+=====+=========+=========+=========
  R1's      |NUT's     |TN's      |H1's      |none |none |REACHABLE|REACHABLE|unchanged
  link-local|link-local|link-local|global    |     |     |         |         |
  ----------+----------+----------+----------+-----+-----+---------+---------+---------
  R1's      |NUT's     |TN's      |H1's      |same |none |REACHABLE|REACHABLE|unchanged
  link-local|link-local|link-local|global    |     |     |         |         |
  ----------+----------+----------+----------+-----+-----+---------+---------+---------
  R1's      |NUT's     |TN's      |H1's      |diff.|none |REACHABLE|STALE    |updated
  link-local|link-local|link-local|global    |     |     |         |         |
  ----------+----------+----------+----------+-----+-----+---------+---------+---------
  R1's      |NUT's     |TN's      |H1's      |diff.|exist|REACHABLE|STALE    |updated
  link-local|link-local|link-local|global    |     |     |         |         |
  ----------+----------+----------+----------+-----+-----+---------+---------+---------
  R1's      |NUT's     |TN's      |H1's      |diff.|exist|REACHABLE|STALE    |updated
  link-local|link-local|link-local|global    |     |>1280|         |         |
  ==========+==========+==========+==========+=====+=====+=========+=========+=========

TERMINATION

  TN               NUT
  ----------------------


  State: any (for TN)


  ==== Redirect ===>
      src=TN's link-local
      dst=NUT's link-local
      icmp target=R1's link-local
      icmp dst=H1's global
      w/o TLL option
      w/o Redirected header option


  ==== RA (at the end of the test) ===>
      src=R1's link-local
      dst=allnode
      RouterLifetime=0

NOTE

  The test does not invoke any remote command.