webAuthWithFix.als

open declarations

/* Model the WebAuth Protocol and the interaction of the following:
  WebKDC: the WebAuth Login Server
  WAS   : a WebAuth-enabled Web Server
  UA    : the user agent, i.e. browser
*/

sig WAToken extends Token {}

// requester credentials
sig WAServiceToken extends WAToken { }
sig WAKrb5Token extends WAToken {}

// subject credentials

// The proxy token allow an application server to 
// retrieve sensitive information (e.g. a user's
// mails or LDAP data) on behalf of the user.
sig WAProxyToken extends WAToken{}

sig WALoginToken extends WAToken{}
sig WACredToken extends WAToken{}

// request token
sig WARequestToken extends Token {
  nonce:WANonce // add a WANonce to fix login CSRF in WebAuth
}

sig WARequest extends Token {
   msgId: lone Int
}

sig WAResponse extends Token {
   causedByMsgId: lone Int
}

sig WAGetTokenReq extends WARequest {
  reqCred:WAToken,
  subjCred:lone WAToken,
  reqToken:lone WARequestToken,
  tokens:set WAToken
}

sig WASessionKey extends Secret {}

sig WAGetTokenResp extends WAResponse {
  respTokens:set WAToken,
  sessionKey:WASessionKey
}

sig WARequestTokenReq extends WARequest {
  reqCred:WAServiceToken,
  proxyTokens:set WAProxyToken,
  loginTokens:WALoginToken,
  reqToken:WARequestToken,
  remoteUser:WebPrincipal
  // optional IP addresses go here
}

sig WAErrorToken extends WAToken {}
sig WAAppToken extends WAToken {} // opaque application token

sig WARequestTokenResp extends WAResponse {
  error:WAErrorToken,
  proxyToken:lone WAProxyToken, // for login request
  returnURL:URL,
  requesterSubject:Principal, // identity of requester
  subject:Principal, // identity in supplied credentials
  requestedToken:lone WAIdToken+WAProxyToken,
  loginCanceledToken:WAErrorToken,
  appState:WAAppToken
}

sig WAProxyData extends WAToken {} // may contain encrypted Krb data

// This command converts an existing Kerberos token 
// into a webkdc-proxy token, for improvied single sign-on.
sig WAProxyTokenReq extends WARequest {
  subjCred:WAToken,
  proxyData:WAProxyData
}

sig WAProxyTokenResp extends WAResponse {
  proxyToken:WAProxyToken,
  subject:WebPrincipal // identity from subject credential in the request
}

// This command extracts info from a proxy token
sig WAProxyTokenInfoReq extends WARequest {
  proxyToken:WAProxyToken
}

sig WAProxyTokenInfoResp extends WAResponse {
  subject:WebPrincipal, // identity from proxy token
  // proxy type
  creation:Time,
  expiration:Time
}

sig WANonce extends Token {}

// HMAC used in WebAuth. We may move them to a generic crypto file after we accumulate enough of them
sig WAHmac extends Token {} 

sig WAAttribute {name:Token, Value:Token}

sig WAEncryptedToken extends WAToken {
// 4-byte UTC time to tell the server which key was used to encrypt this token
  private keyHint:Token, 
  private nonce:WANonce,
  private hmac:WAHmac,
  // private attrs:set WAAttribute,
  private padding:Token
}
  
sig WASCookie extends SecureCookie {}{
  value in WANonce
}

fact WASCookieConstraints {
  all disj c1, c2:WASCookie | c1.value != c2.value
}

sig WAIdToken extends WAEncryptedToken{
  private username: WebPrincipal,
  private wasNonce: WANonce,
  // we don't need Kerberos subject authn data for now
  private creationTime: Time,
  private expirationTime: Time
}{
  // Token should normally expire within 5 minutes based on WebAuth spec. 
  // Simulate using 5 ticks
  expirationTime in creationTime.next.next.next.next.^next
}

// pred WAPossessWASCookie[httpClient:HTTPClient, token:WAIdToken, usageEvent:Event]{}

pred WARemoteScriptingIsPossible {
  1 = 1  // true unless user disables script support
}

sig WASAuthPath extends Path {}
sig WAS extends HTTPServer {}
sig WAWebKDC extends HTTPServer {}

/* On initial access to WAS, WAS creates a host cookie containing a nonce,
   and redirects the user's browser to the WebKDC with the nonce imbedded
   in the query string
*/
pred WARedirectedFromWAS[t2:HTTPTransaction] {
  some t1:t2.^cause, c:WASCookie|{
    t1.req.to in WAS and
    t1.resp.statusCode in RedirectionStatus and
    WAWebKDC in (location & t1.resp.headers ).targetOrigin.dnslabel.resolvesTo  and
    c in (SetCookieHeader & t1.resp.headers).thecookie and
    c.value in (t2.req.queryString.value & WARequestToken).nonce
  }
}

/* On successful user authentication, WebKDC sends the Id Token to WAS.
   The ID token contains the nonce originally created by WAS.
*/
pred WAPossessTokenViaLogin[httpClient:HTTPClient, token:WAIdToken, usageEvent:Event]{
  some t1:HTTPTransaction|{
    happensBeforeOrdering[t1.req, usageEvent] and
    WARedirectedFromWAS[t1] and
    t1.req.path = LOGIN and 
    t1.req.to in WAWebKDC and
    t1.req.from in httpClient and
    t1.resp.statusCode in RedirectionStatus and
    WAContainsIdToken[t1.resp, token] and
    token.creationTime = t1.resp.post and
    token.username in httpClient.owner and
    // IDToken includes the nonce created by WAS
    token.wasNonce in (t1.req.queryString.value & WARequestToken).nonce
  }
}

pred WAContainsIdToken [resp:HTTPResponse, token:WAIdToken] {
  one (LocationHeader & resp.headers) and
  some locHdr: LocationHeader  |
    locHdr in resp.headers and
    locHdr.targetPath in WASAuthPath and
    token in locHdr.params.value
}

/* The WAS accepts an ID Token in the query string only if 
   it is corroborated with a host cookie set by the WAS
*/
pred WAContainsIdToken [req:HTTPRequest, token:WAIdToken] {
  token in req.queryString.value 
  some c:WASCookie| {
    c in (CookieHeader & req.headers).thecookie
    c.value = token.wasNonce
  }
}

pred WAPossessTokenViaRemoteScripting [httpClient1:HTTPClient, token:WAIdToken, usageEvent:Event]{
  // Through remote scripting, some user2(say, Mallory) can pass information to user1(say, Alice)'s browser
  some t1:HTTPTransaction, httpClient2:HTTPClient|let user2=httpClient2.owner|
  {
    // Mallory possesses the token
    WAPossessTokenViaLogin[httpClient2, token, usageEvent] and
    // user1 (Alice) has a connection to user2(Mallory)'s web server
    happensBefore[t1.req, usageEvent] and 
    t1.req.from in httpClient1 and
    t1.req.to in (user2.servers & HTTPServer)
  } and {
    WARemoteScriptingIsPossible 
  }
}

fact WABeforeUsingTokenYouNeedToPossessIt{
  all httpClient:HTTPClient, req:HTTPRequest, token:WAIdToken | 
  {
    req.from in httpClient and 
    WAContainsIdToken [req, token]
  } implies
    WAPossessToken[httpClient, token, req]
}

pred WAPossessToken[httpClient:HTTPClient, token:WAIdToken, usageEvent:Event]{
  WAPossessTokenViaLogin [httpClient, token, usageEvent] or
  WAPossessTokenViaRemoteScripting [httpClient, token, usageEvent] 
}

// Constrain the web model in this module for better illustration.
fact WAHTTPFacts{
  all req:HTTPRequest | {req.from in HTTPClient and req.to in HTTPServer}
  all user:WebPrincipal | user.servers in HTTPServer
  all t1:HTTPTransaction | some (t1.resp) implies (t1.req.from = t1.resp.to ) and (t1.req.to = t1.resp.from)
  Mallory.servers in (HTTPServer - (WAS+WAWebKDC))
}

pred WALoginCSRF [t1:HTTPTransaction]{
  some token:WAIdToken|{
    t1.req.from in Alice.httpClients and
    t1.req.path in WASAuthPath and
    t1.req.to in WAS and
    WAContainsIdToken [t1.req, token] and
    token.username in Mallory
  }
}

fun WAFindAttacks: HTTPTransaction{
  {
    t1:HTTPTransaction |
      WALoginCSRF[t1]
  }
}

// run WAFindAttacks for 8 but exactly 0 ACTIVEATTACKER, exactly 0 PASSIVEATTACKER
check WANoLoginCSRF {
  no WAFindAttacks
}
for 8 but exactly 0 ACTIVEATTACKER, exactly 0 PASSIVEATTACKER

/*
Executing "Check WANoLoginCSRF for 8 but exactly 0 ACTIVEATTACKER, exactly 0 PASSIVEATTACKER"
Run 1:
======
Generating facts...
   Simplifying the bounds...
   Solver=sat4j Bitwidth=4 MaxSeq=7 SkolemDepth=1 Symmetry=20
   Generating CNF...
   Generating the solution...
   Begin solveAll()
   209396 vars. 6897 primary vars. 412890 clauses. 6058505ms.
   Solving...
   End solveAll()
   No counterexample found. Assertion may be valid. 1612370ms.
Run 2:
======
   Solver=sat4j Bitwidth=4 MaxSeq=7 SkolemDepth=1 Symmetry=20
   Generating CNF...
   Generating the solution...
   Begin solveAll()
   209396 vars. 6897 primary vars. 412890 clauses. 4285089ms.
   Solving...
   End solveAll()
   No counterexample found. Assertion may be valid. 1981270ms.
Run 3:
====
   Solver=sat4j Bitwidth=4 MaxSeq=7 SkolemDepth=1 Symmetry=20
   Generating CNF...
   Generating the solution...
   Begin solveAll()
   209396 vars. 6897 primary vars. 412890 clauses. 4412958ms.
   Solving...
   End solveAll()
   No counterexample found. Assertion may be valid. 2087697ms.
*/