dh.psl 2.4 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
/*
    A simple protocol that demonstrates Diffie-Helman public and secret key encryption
    with keys generated using exponents, and the fact that 
    g^(a * b) = (g^a)^b.
*/
spec DIFFIE-HELMAN is
Theory
  types Name Nonce NeNonceSet Gen Exp Key GenvExp Secret .
  subtype Gen Exp < GenvExp .
  subtype Exp < Key .
  subtype Name < Public . // This is quite relevant and necessary
  subtype Gen < Public . // This is quite relevant and necessary

  op sec : Name Fresh -> Secret .

  op n : Name Fresh -> Nonce .

  ops a b i : -> Name .

  op e : Key Msg -> Msg .
  op d : Key Msg -> Msg .

  op exp : GenvExp NeNonceSet -> Exp .

  op g : -> Gen .

  subtype Nonce < NeNonceSet .
  op _*_ : NeNonceSet NeNonceSet -> NeNonceSet [assoc comm] .

  op _;_ : Msg Msg -> Msg [gather (e E)] .

32 33 34 35 36 37 38
  var W : Gen .
  vars Y Z : NeNonceSet .
  var K : Key .
  var M : Msg .
  eq exp(exp(W,Y),Z) = exp(W, Y * Z) .
  eq e(K,d(K,M)) = M .
  eq d(K,e(K,M)) = M .
39 40

Protocol
41
    vars ANAME BNAME ANAME1 : Name .
42 43 44 45
    vars r r' r1 : Fresh .
    vars XEA XEB : Exp .
    var S : Secret .

46 47
    roles A B .

48
    In(A) = ANAME, BNAME .
49
    In(B) = BNAME .
50 51 52

    Def(A) = na := n(ANAME, r), secret := sec(ANAME, r') .
    Def(B) = nb := n(BNAME, r1) .
53

54 55 56 57
    1 . A -> B : ANAME  ; BNAME ; exp(g, na)      
              |- ANAME1 ; BNAME ; XEB .
    2 . B -> A : ANAME1 ; BNAME ; exp(g, nb)      
              |- ANAME  ; BNAME ; XEA .
58 59 60 61 62 63 64
    3 . A -> B : e(exp(XEA, na), secret)     
              |- e(exp(XEB, nb), S) .

    Out(A) = na, exp(g, na), XEB, secret .
    Out(B) = nb, exp(g, nb), XEA, S .

Intruder
65
    vars NAME : Name .
66 67 68 69 70
    var K : Key .
    vars M M1 M2 : Msg .
    vars NS1 NS2 : NeNonceSet .
    var GE : GenvExp .
    var r  : Fresh .
71
             => n(i, r), g, NAME .
72
    M1 ; M2 <=> M1, M2 .
73 74 75
    K, M     => e(K, M), d(K, M) .
    NS1, NS2 => NS1 * NS2 .
    GE, NS1  => exp(GE, NS1) .
76 77 78 79 80 81 82 83 84

Attacks
    /*
        Authentication attack meant to make sure the protocol is implemented
        properly. If this "attack" does not find an initial state, then this
        protocol was implemented incorrectly.
    */
    0 .
        B executes protocol .
85
        Subst(B) = ANAME1 |-> a, BNAME |-> b, S |-> sec(a, r') .
86
        without:
87
            Subst(A) = ANAME |-> a, BNAME |-> b .
88 89 90
            A executes protocol .
    1 .
        B executes protocol .
91
        Subst(B) = ANAME1 |-> a, BNAME |-> b, S |-> sec(a, r') .
92
        Intruder learns sec(a, r') .
93

94
ends