spec DB is 

Theory
    types Name Key Nonce .
    subtype Name < Key .
    subtype Name < Public .

    ops a b i : -> Name .

    op 0 : -> Msg .
    op n : Name Fresh -> Nonce .

    op _*_ : Msg Msg -> Msg [assoc comm] .

    vars X Y : Msg .
    eq X * X = 0 .
    eq X * 0 = X .
    eq X * X * Y = Y .

Protocol

    vars ANAME BNAME  : Name .
    vars N NA : Nonce .
    var r     : Fresh .

    roles A B .

    In(A) = ANAME, BNAME, N .
    In(B) = ANAME, BNAME, N .

    1 . A -> B : n(ANAME, r) |- NA .
    2 . B -> A : N * NA  |- N * n(ANAME, r) .

    Out(A) = n(ANAME, r), N * n(ANAME, r) .
    Out(B) = NA, N * NA .

Intruder
    var C : Name .
    vars X Y : Msg .
    var r : Fresh .

         => C, n(i, r) .
    X, Y => X * Y .

Attacks
    0 .
        B executes protocol .
        Subst(B) = ANAME |-> a, BNAME |-> b .

ends