Otway-Rees.psl 2.81 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104
spec Otway-Rees is
Theory
     types UName SName Name Key Nonce Masterkey 
        Sessionkey .
     subtypes Masterkey Sessionkey < Key .
     subtypes SName UName < Name < Public .
     op n : Name Fresh -> Nonce .
     ops a b i : -> UName .
     op s : ->  SName . 
     op mkey : Name Name -> Masterkey .
     op seskey : Name Name Nonce -> Sessionkey .  
     op e  : Key Msg -> Msg . //encryption
     op d : Key Msg -> Msg . //decryption
     op _;_ : Msg Msg -> Msg [gather (e E)] .

     var K : Key .
     var Z : Msg .
     eq d(K, e(K, Z)) = Z .
     eq e(K, d(K, Z)) = Z .
     
      
Protocol
    vars ANAME BNAME : UName .
    var SNAME : SName .
    vars r r' r'' rM : Fresh .
    vars RA CB CS RB : Nonce .
    vars M1 MA : Msg . 
    var KCA KCB : Sessionkey . 

    roles A B S .

    Def(A) = c   := n(ANAME, rM), ra := n(ANAME, r), 
             skA := mkey(ANAME, SNAME) .
    Def(B) = rb  := n(BNAME, r'), 
             skB := mkey(BNAME, SNAME) .
    Def(S) = skA := mkey(ANAME, SNAME), 
             skB := mkey(BNAME, SNAME), 
              kc := seskey(ANAME, BNAME, 
                                  n(SNAME, r'')) .
              

    In(A) = ANAME, BNAME, SNAME .
    In(B) = ANAME, BNAME, SNAME .
    In(S) = ANAME, BNAME, SNAME .

    1 . A -> B :  c  ; ANAME ; BNAME ; e(skA, ra ; c ; 
                                        ANAME ; BNAME) 
               |- CB ; ANAME ; BNAME ; M1 .
              

    2 . B -> S :  CB ; ANAME ; BNAME ; 
                    M1 ; 
                    e(skB, rb ; CB ; ANAME ; BNAME)
               |- CS ; ANAME ; BNAME ; 
                    e(skA, RA ; CS ; ANAME ; BNAME) ;
                    e(skB, RB ; CS ; ANAME ; BNAME) .
              

    3 . S -> B :  CS ; e(skA, RA ; kc) ; 
                    e(skB, RB ; kc) 
               |- CB ; MA ; 
                    e(skB, rb ; KCB) .
              

    4 . B -> A :  CB ; MA 
               |- c  ; e(skA, ra ; KCA) .

    Out(A) = c, ra, KCA .
    Out(B) = rb, KCB, MA, M1, CB .
    Out(S) = kc, RA, RB, CS .

Intruder 
    vars P : UName .
    var S : SName .
    vars K : Key .
    vars N M : Msg .

    => s, P, mkey(i, s) .
    M, N <=> M ; N .
    K, M => d(K, M), e(K, M) .
    P => mkey(P, i), mkey(i, P) .
    

Attacks
   0 .
         A executes protocol .
         Subst(A) = ANAME |-> a, BNAME |-> b, 
            SNAME |-> s .
   1 .
         A executes protocol .
         Subst(A) = ANAME |-> a, BNAME |-> b, 
            SNAME |-> s .
         Intruder learns KCA .
   2 .
         A executes protocol .
         Subst(A) = ANAME |-> a, BNAME |-> b, 
            SNAME |-> s .
         without:
             B executes protocol .
             Subst(B) = M1 |-> e(skA, c ; ra ; ANAME ; 
                                 BNAME),  
                        ANAME |-> a, BNAME |-> b, 
                        SNAME |-> s .
ends