NAME

ncStateByRedirect4Nonce - Verifying State Machine: Redirect vs. NONCE

TARGET

Host only

SYNOPSIS

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

INITIALIZATION

Clear NC state for TN.
Set R1 as the default router by sending RA and NA.

  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

TEST PROCEDURE

ncStateByRedirect4Nonce verifies that state transition for a NUT in NONCE state when receiving a Redirect.

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


  State: REACHABLE (for R1), NONCE (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
      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 |Cur. |New             |LLA      
  ==========+==========+==========+==========+=====+=====+=====+================+=========
  R1's      |NUT's     |TN's      |H1's      |none |none |NONCE|NONCE/INCOMPLETE|unchanged
  link-local|link-local|link-local|link-local|     |     |     |                |         
  ----------+----------+----------+----------+-----+-----+-----+----------------+---------
  R1's      |NUT's     |TN's      |H1's      |exist|none |NONCE|STALE           |updated
  link-local|link-local|link-local|link-local|     |     |                      |         
  ----------+----------+----------+----------+-----+-----+-----+----------------+---------
  R1's      |NUT's     |TN's      |H1's      |exist|exist|NONCE|STALE           |updated
  link-local|link-local|link-local|link-local|     |     |     |                |         
  ----------+----------+----------+----------+-----+-----+-----+----------------+---------
  R1's      |NUT's     |TN's      |H1's      |exist|exist|NONCE|STALE           |updated
  link-local|link-local|link-local|link-local|     |>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.