signal-oidc.spthy

theory MessagingOIDC
begin

heuristic: o "./oracle.py"

#include "src/header.spthy"
#include "src/tls.spthy"
#include "src/idp.spthy"
#include "src/messaging.spthy"

rule Client:
  []
  -->
  [ !Client($App) ]

rule MessagingApp:
  [ !Client($App) ]
  --[ IsMessagingApp($App)
    , OnlyOnce('messaging_app_client') ]->
  [ !MessagingApp($App) ]

rule RedirectURL:
  [ !IdP($IdP), !Client($App), !Domain($RedirectURL) ]
  --[ IsRedirectURL($IdP, $App, $RedirectURL) ]->
  [ !RedirectURL($IdP, $App, $RedirectURL) ]

// NOTE: This restriction might seem overly strict. This practically means that:
// We require the messaging app uses unique redirect URLs per IdP, and that any
// usage of the messaging app's redirect URL in other contexts counts as
// malicious. (Honest other apps cannot do that.)
restriction UniqueRedirectURLs:
  "All idp1 idp2 app1 app2 url #t1 #t2 #t3.
        ( IsMessagingApp(app1) @ #t1
        & IsRedirectURL(idp1, app1, url) @ #t2
        & IsRedirectURL(idp2, app2, url) @ #t3)
    ==> (idp1 = idp2 & app1 = app2)"

// Clients need to memorize which query they issued last. We prefix rule name
// with 0_ s.t. it comes first in case ordering (which is alphabetical) of the
// executability lemma. Otherwise, there is an infinite loop.
rule 0_InitSessionStore:
  []
  --[ OnlyOnce(<'init_session_store', $User>) ]->
  [ SessionStore($User, 'null', 'null') ]

rule ClearSessionStore:
  [ SessionStore($User, x, y) ]
  -->
  [ SessionStore($User, 'null', 'null') ]

// It is necessary handle forwards from the adversary dedicatedly, because
// otherwise, the adversary can choose the session they forward to. This would
// be unrealistic.
rule LinkClick[color=#FF6961]:
  [ Fr(~sess), In(m), !Domain($Domain) ]
  --[ AdversaryActivity() ]->
  [ TLSClient_Out('GET', ~sess, $Domain, m)
  , !Browser($Prover, ~sess) ]

// OpenID Connect Auth code + PKCE flow
rule OIDCAppLaunchBrowser[color=#B4D9EF]:
  let fp = fingerprint(<pk(skProver), pkVerifier>)
      hash = h(fp, salt)
      code_challenge = s256(code_verifier)
  in
  [ !IdP($IdP), !MessagingApp($App)
  , !RedirectURL($IdP, $App, $RedirectURL)
  , !MessagingLtkUser($Prover, $ProverPhone, skProver)[no_precomp]
  , !UseMessagingKeyFor($Prover, $VerifierPhone, pkVerifier)[no_precomp]
  , SessionStore($Prover, drop1, drop2)
  , Fr(salt), Fr(nonce), Fr(code_verifier), Fr(~sess) ]
  --[ IsNonce(nonce)
    , GenerateCodeVerifierFor(code_verifier, $IdP)
    , SOAPStart($Prover, nonce)
    , SOAPMessaging($Prover, nonce, pkVerifier, pk(skProver)) ]->
  [ TLSClient_Out('GET', ~sess, $IdP, <'oidc_req', $App, hash, nonce, code_challenge, $RedirectURL>)
  // This Out fact models that the adversary can access authorization requests.
  , Out(<hash, nonce, code_challenge>)
  , SessionStore($Prover, nonce, <$IdP, $VerifierPhone, hash, salt, code_verifier>)
  , !Browser($Prover, ~sess) ]

rule OIDCIdPInit[color=#B4D9EF]:
  [ !IdP($IdP)
  , !RedirectURL($IdP, $Client, $RedirectURL)
  , TLSServer_In('GET', ~sess, $IdP, <'oidc_req', $Client, hash, nonce, code_challenge, $RedirectURL>) ]
  --[ MustBeNonce(nonce) ]->
  [ TLSServer_Out('GET', ~sess, $IdP, 'auth_req')
  , St_OIDCServer_Auth($IdP, $Client, $RedirectURL, ~sess, hash, nonce, code_challenge) ]

rule OIDCAppLogin[color=#B4D9EF]:
  [ !Browser($Prover, ~sess)
  , !IdP($IdP)
  , TLSClient_In('GET', ~sess, $IdP, 'auth_req')
  , !IdPAccount($Prover, $IdP, $Username, ~pw) ]
  -->
  [ TLSClient_Out('GET', ~sess, $IdP, <'login', $Username, ~pw>) ]

lemma PasswordsConfidential[reuse]:
  "All user idp username pw #t1 #t2.
        ( Username(user, idp, username, pw) @ #t1
        & KU(pw) @ #t2)
    ==> ( (Ex #x. CompromisedDomain(idp) @ #x)
        | (Ex someone #x. CompromisedAccount(someone, idp, username) @ #x))"

lemma MessagingKeysUnique[reuse]:
  "All userA userB phoneA phoneB sk #a #b.
        ClaimMessagingKey(userA, phoneA, sk) @ #a
      & ClaimMessagingKey(userB, phoneB, sk) @ #b
  ==> (#a = #b & userA = userB & phoneA = phoneB)
      | KeyServerCompromise()"

rule OIDCIdPIssueCode[color=#B4D9EF]:
  [ !IdP($IdP)
  , !IdPAccount($User, $IdP, $Username, pw)
  , Fr(~code)
  , St_OIDCServer_Auth($IdP, $Client, $RedirectURL, ~sess, hash, nonce, code_challenge)
  , TLSServer_In('GET', ~sess, $IdP, <'login', $Username, pw>) ]
  --[ IsCode(~code)
    , MustBeNonce(nonce)
    , SOAPIdP($User, nonce, $IdP, $Username) ]->
  [ TLSClient_Out('GET', ~sess, $RedirectURL, <'code', ~code, nonce>)
  , St_OIDCIdP_Code($IdP, $Username, $Client, $RedirectURL, ~code, hash, nonce, code_challenge) ]

rule OIDCAppCodeRedirect[color=#B4D9EF]:
  [ !RedirectURL($IdP, $App, $RedirectURL), !IdP($IdP)
  , !MessagingApp($App)
  , Fr(~sessPost)
  , SessionStore($Prover, nonce, <$IdP, $VerifierPhone, hash, salt, code_verifier>)
  , !Browser($Prover, ~sess)
  , TLSServer_In('GET', ~sess, $RedirectURL, <'code', code, nonce>) ]
  --[ SelfIssued($Prover, nonce)
    , Neq(nonce, 'null')
    , MustBeCode(code) ]->
  [ TLSClient_Out('POST', ~sessPost, $IdP, <'token_req', code, code_verifier, $RedirectURL>)
  , St_OIDCApp_CodeReq($Prover, $IdP, $VerifierPhone, ~sessPost, hash, salt, code)
  , SessionStore($Prover, 'null', 'null') ]

rule OIDCIdPTokenIssue[color=#B4D9EF]:
  let tokenBody = <$IdP, $Client, $Username, nonce, hash>
      token = <tokenBody, sign(tokenBody, idpSk)>
  in
  [ !IdPLtk($IdP, idpSk)
  , St_OIDCIdP_Code($IdP, $Username, $Client, $RedirectURL, code, hash, nonce, code_challenge)
  , TLSServer_In('POST', ~sess, $IdP, <'token_req', code, code_verifier, $RedirectURL>) ]
  --[ Eq(s256(code_verifier), code_challenge)
    , IssueTokenForCode($IdP, ~sess, code)
    , MustBeToken(token)
    , UseCode($IdP, $Client, code)
    , UseCodeVerifierFor($IdP, code_verifier) ]->
  [ TLSServer_Out('POST', ~sess, $IdP, <'token', token>) ]

lemma CodeSecrecy[reuse]:
  "All idp client code #t1 #t2 #t3.
        ( UseCode(idp, client, code) @ #t1
        & IsMessagingApp(client) @ #t2
        & KU(code) @ #t3)
    ==> ( (Ex #x. UsedCode(idp, code) @ #x & #x < #t3)
        | (Ex url #x #y. IsRedirectURL(idp, client, url) @ #x & CompromisedDomain(url) @ #y)
        | (Ex #x. CompromisedDomain(idp) @ #x))"

lemma CodeVerifierSecrecy[reuse]:
  "   All verifier idp #x #y.
        UseCodeVerifierFor(idp, verifier) @ #x
        & GenerateCodeVerifierFor(verifier, idp) @ #y
  ==> not (Ex #z. KU(verifier) @ #z)
      | (Ex #z. CompromisedDomain(idp) @ #z)"

// This sources lemma combines multiple in spirit, but they need to assist each
// other in the proof, hence, they are combined.
lemma TokenFormatAndOTPLearning[sources]:
  "(All token #i.
        MustBeToken(token) @ #i
    ==> (Ex first second user idp client nonce hashed sk.
            token = <first, second>
          & first = <idp, client, user, nonce, hashed>
          & ((Ex #h. KU(nonce) @ #h & #h < #i) | (Ex #h. IsNonce(nonce) @ #h))
          & ((Ex #h. KU(hashed) @ #h & #h < #i) | (Ex fp salt. hashed = h(fp, salt)))
          & second = sign(first, sk))
  ) & (All nonce #i.
        MustBeNonce(nonce) @ #i
    ==> ( (Ex #h. KU(nonce) @ #h & #h < #i)
        | (Ex #h. IsNonce(nonce) @ #h)))
  & (All code #i.
        MustBeCode(code) @ #i
    ==> ( (Ex #h. KU(code) @ #h & #h < #i)
        | (Ex #h. IsCode(code) @ #h)))
  & (All chall #i.
        MustBeOTP(chall) @ #i
    ==> ( (Ex #j. IsOTP(chall) @ #j & #j < #i)
      | (Ex #j. KU(chall) @ #j & #j < #i)))
  & (All ltk #i.
        MustBeMessagingKey(ltk) @ #i
    ==> ( (Ex sk #j. IsMessagingKey(sk) @ #j & ltk = pk(sk))
      | (Ex #j. KU(ltk) @ #j & #j < #i)))"

rule OIDCTokenForward[color=#B4D9EF]:
  let body = <$IdP, $App, $Username, nonce, hash>
      fp = fingerprint(<pk(skProver), pkVerifier>)
      token = <body, signature>
  in
  [ !IdP($IdP), !MessagingApp($App)
  , !UseMessagingKeyFor($Prover, $VerifierPhone, pkVerifier)[no_precomp]
  , !UseIdPKey($Prover, $IdP, pkIdP)
  , !MessagingLtkUser($Prover, $ProverPhone, skProver)[no_precomp]
  , St_OIDCApp_CodeReq($Prover, $IdP, $VerifierPhone, ~sessPost, hash, salt, code)
  // We do not check the nonce in the ID token. This is to highlight that the
  // inclusion of a true nonce in the ID token is not strictly necessary in the
  // protocols design.
  , TLSClient_In('POST', ~sessPost, $IdP, <'token', <<$IdP, $App, $Username, nonce, hash>, signature>>) ]
  --[ Eq(h(fp, salt), hash)
    , Eq(verify(signature, body, pkIdP), true)
    , GetTokenForCode($IdP, ~sessPost, code)
    , MustBeToken(token)
    , MustBeCode(code)
    , UsedCode($IdP, code) ]->
  [ SendAsTo($Prover, $VerifierPhone, <'fwd_token', token, salt>)
  // Sending the code models that the adversary can access the authorization
  // response after the OpenID Connect protocol termianted successfully.
  , Out(code) ]

lemma CodeAgreement[use_induction,reuse]:
  "All idp sess codeClient codeIdP #t1 #t2.
          GetTokenForCode(idp, sess, codeClient) @ #t1
        & IssueTokenForCode(idp, sess, codeIdP) @ #t2
    ==> ( (codeClient = codeIdP)
        | (Ex #x. CompromisedDomain(idp) @ #x))"

lemma CodeIsSingleUse[reuse]:
  "All idp code #a #b.
        (UsedCode(idp, code) @ #a & UsedCode(idp, code) @ #b)
    ==> ( #a = #b
        | (Ex #x. CompromisedDomain(idp) @ #x)
        | (Ex app url #x #y.
              IsRedirectURL(idp, app, url) @ #x
            & CompromisedDomain(url) @ #y))"

rule OIDCTokenReceive[color=#B4D9EF]:
  let body = <$IdP, $App, $Username, nonce, hash>
      fp = fingerprint(<pk(skProver), pk(skVerifier)>)
  in
  [ !MessagingLtkUser($Verifier, $VerifierPhone, skVerifier)[no_precomp]
  , !UseMessagingKeyFor($Verifier, $ProverPhone, pk(skProver))[no_precomp]
  , !MessagingApp($App)
  , !UseIdPKey($Verifier, $IdP, pkIdP)
  , In(e2ee(skProver, pk(skVerifier), <'fwd_token', <body, signature>, salt>)) ]
  --[ Eq(h(fp, salt), hash)
    , Eq(verify(signature, body, pkIdP), true)
    , DidNotIssueSelf($Verifier, nonce)
    , ReceivingKey(pk(skVerifier))
    , Correspond($Verifier, pk(skProver), $IdP, $Username) ]->
  []

restriction CheckNonceReplay:
  "All verifier nonce #t1.
      DidNotIssueSelf(verifier, nonce) @ #t1
  ==> (not Ex #t2. SelfIssued(verifier, nonce) @ #t2)"

lemma Executability:
  exists-trace
  "Ex verifier proverKey idp acc verifierKey m1 m2 s1 s2
    #t1 #t2 #t3 #t4 #t5.
      Correspond(verifier, proverKey, idp, acc) @ #t1
    & ReceiveMessaging(proverKey, verifierKey, m1) @ #t2
    & ReceiveIdP(idp, acc, m2) @ #t3
    & SendMessaging(proverKey, verifierKey, m1) @ #t4
    & Sender(s1) @ #t4
    & SendIdP(idp, acc, m2) @ #t5
    & Sender(s2) @ #t5
    & s1 = s2
    & (not Ex #x. AdversaryActivity() @ #x)"

lemma SOAPAgreement[reuse]:
  "All v proverKey idp acc verifierKey #t1.
        ( Correspond(v, proverKey, idp, acc) @ #t1
        & ReceivingKey(verifierKey) @ #t1)
    ==>   (Ex prover nonce #x1 #x2.
              SOAPStart(prover, nonce) @ #x1
            & SOAPMessaging(prover, nonce, verifierKey, proverKey) @ #x1
            & SOAPIdP(prover, nonce, idp, acc) @ #x2)
        | (Ex #x. CompromisedIdP(idp) @ #x)
        | (Ex #x. CompromisedDomain(idp) @ #x)
        | (Ex app redirectURL #x #y #z.
              IsMessagingApp(app) @ #x
            & IsRedirectURL(idp, app, redirectURL) @ #y
            & CompromisedDomain(redirectURL) @ #z)
        | (Ex p #x. CompromisedAccount(p, idp, acc) @ #x)
        | (Ex p #x. CompromisedMessaging(p, proverKey) @ #x)"

lemma SocialAuthentication:
  "All v sendKey rcvKey m1 idp acc m2 #t #r1 #r2.
        ( Correspond(v, sendKey, idp, acc) @ #t
        & ReceiveMessaging(sendKey, rcvKey, m1) @ #r1
        & ReceiveIdP(idp, acc, m2) @ #r2)
    ==> ( (Ex s #x1 #x2.
          ( SendMessaging(sendKey, rcvKey, m1) @ #x1 & Sender(s) @ #x1 & #x1 < #r1
          & SendIdP(idp, acc, m2) @ #x2 & Sender(s) @ #x2 & #x2 < #r2))
        | (Ex #x. CompromisedIdP(idp) @ #x)
        | (Ex #x. CompromisedDomain(idp) @ #x)
        | (Ex app redirectURL #x #y #z.
              IsMessagingApp(app) @ #x
            & IsRedirectURL(idp, app, redirectURL) @ #y
            & CompromisedDomain(redirectURL) @ #z)
        | (Ex p #x. CompromisedAccount(p, idp, acc) @ #x)
        | (Ex p #x. CompromisedMessaging(p, sendKey) @ #x))"

end