db.psl 846 Bytes
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21
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

acholewa's avatar
acholewa committed
22
    vars ANAME BNAME  : Name .
23 24 25
    vars N NA : Nonce .
    var r     : Fresh .

acholewa's avatar
acholewa committed
26
    roles A B .
27

acholewa's avatar
acholewa committed
28 29
    In(A) = ANAME, BNAME, N .
    In(B) = ANAME, BNAME, N .
30

acholewa's avatar
acholewa committed
31 32 33 34
    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) .
35 36 37 38 39 40 41 42 43 44 45 46 47
    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 .
acholewa's avatar
acholewa committed
48
        Subst(B) = ANAME |-> a, BNAME |-> b .
49 50

ends