theory Keyserver begin

/*
 * Protocol:	The keyserver example from [1]
 * Modeler: 	Simon Meier
 * Date: 	June 2012
 *
 * Status: 	working

 [1] Sebastian Moedersheim: Abstraction by set-membership: verifying security
 protocols and web services with databases. ACM Conference on Computer and
 Communications Security 2010: 351-360
 */

/* Original input file from [1]

Problem: zebsKeyserver;

Types:
Agent  : {a,b,c,i,s};
U      : {a,b,c};
S      : {s};
H      : {a,b};
D      : {c,i};
DU     : {c};
Sts    : {valid,revoked};
PK,NPK : value;
M1,M2  : untyped;

Sets:
ring(U), db(S,U,Sts);

Functions:
public sign/2, pair/2;
private inv/1;

Facts:
iknows/1, attack/0;

Rules:

\Agent. => iknows(Agent);
iknows(sign(M1,M2)) => iknows(M2);
iknows(M1).iknows(M2) => iknows(sign(M1,M2));
iknows(pair(M1,M2)) => iknows(M1).iknows(M2);
iknows(M1).iknows(M2) => iknows(pair(M1,M2));
*/

builtins: signing

// The non-deterministic choice between the rules SetupHonestKey and
// SetupDishonestKey determines whether an agent is honest or not.

// \H,S. =[PK]=>iknows(PK).PK in ring(H).PK in db(S,H,valid);
rule SetupHonestKey:
    [ Fr(~sk) ]
  --[ HonestKey(~sk) ]->
    [ Out(pk(~sk)), ClientKey($A, ~sk), ServerDB($A, ~sk) ]

// \S,DU. =[PK]=>iknows(PK).iknows(inv(PK)).PK in db(S,DU,valid);
rule SetupDishonestKey:
    [ In(sk) ]
  -->
    [ ServerDB($A, sk) ]

// \H.
// iknows(PK).PK in ring(H)
// =[NPK]=>NPK in ring(H).iknows(sign(inv(PK),pair(H,NPK)));
rule RequestRenewKey:
    [ ClientKey($A, sk), Fr(~skNew) ]
  --[ HonestKey(~skNew) ]->
    [ Out( sign{'renew', $A, pk(~skNew)}sk )
    , ClientKey($A, ~skNew)
    ]

// \S,U.
// iknows(sign(inv(PK),pair(U,NPK))).PK in db(S,U,valid).
// forall U,Sts. NPK notin db(S,U,Sts)
// =>PK in db(S,U,revoked).NPK in db(S,U,valid).iknows(inv(PK));
rule RenewKey:
    [ In( sign{'renew', A, pk(skNew)}sk )
    , ServerDB(A, sk)
    ]
  --[ Revoked(sk) ]->
    [ ServerDB(A, skNew)
    , Out( sk )
    ]

// Typing lemma: it can be proven, but not with the current heuristic. It
// focuses too much on the first-order part and neglects solving the
// signature. Moreover, it should use an age-based strategy for the goals to
// ensure that it always makes at least some progress.
lemma types [typing]:
  "All sk #i. Revoked(sk) @ i ==>
     ( (Ex f #j. KU(f,sk) @ j & j < i)
     | (Ex #j. HonestKey(sk) @ j & j < i)
     )
  "
/*
The following property proven in Moedersheim's paper is rather easy to
prove, as it depends only on the fact that secret keys are not leaked by
any other means than the "RenewKey" rule. The "RenewKey" rule always log's
that the key is "Revoked", which directly implies the lemma below.

TODO: Prove property that depends on ordering of revocation. For example,
DH-key exchange always succeeds for a protocol with an online key-server. This
crucially depends on the client not sending a renewal message while he's
waiting for the key confirmation.
*/


// \S,H.
// iknows(inv(PK)).PK in db(S,H,valid)
// =>attack;
lemma In_Honest_Key_imp_Revoked:
  "All sk #i #d. HonestKey(sk) @ i & K(sk) @ d ==>
      (Ex #r. Revoked(sk) @ r)
  "


end