theory Yubikey begin section{* The Yubikey-Protocol *} /* * Protocol: Yubikey Protocol * Modeler: Robert Kunnemann, Graham Steel * Date: August 2012 * * Status: working */ builtins: symmetric-encryption functions: S/1,zero/0 /* We to model the Yubikey protocol, described in * http://www.yubico.com/documentation * http://www.yubico.com/developers-intro * This is simplified version, in particular: * - timestamps are not modelled * - We do not distinguish the session and token counter. We describe them * as one single counter, that represents the pair (session counter, token * counter) with a lexicographical order on the pair. This implies that * a) pressing the button on the Yubikey increases this counter by 1, and * b) a plugin of the Yubikey increases it by an arbitrary amount the * adversary gets to choose (giving him more power). */ /* The following rules model two binary relations between integers. !Succ * is functional. If !Succ(a,b), then the adversary was able to show that b * is the successor of b. Similarly, albeit !Smaller is not functional, if * !Smaller(a,b), then the adversary was able to show that a is smaller * than b. * The Theory() action is used to enforce that this relation (to the extend * it is needed in this trace) has to be build up before running the first * protocol actions. */ rule InitSucc: [In(zero),In(S(zero))] --[Theory(), IsSucc(zero,S(zero)),IsZero(zero)]-> [!Succ(zero,S(zero))] rule StepSucc: [In(y),In(S(y)), !Succ(x,y)] --[Theory(), IsSucc(y,S(y)) ]-> [!Succ(y,S(y))] rule SimpleSmaller: [!Succ(x,y)] --[Theory(), IsSmaller(x,y)]-> [!Smaller(x,y)] rule ZExtendedSmaller: [!Smaller(x,y),!Succ(y,z)] --[Theory(), IsSmaller(x,z)]-> [!Smaller(x,z)] /* A Yubikey is initialised with a zero counter, a key and a public, as well as a * secret identifier, ~pid and ~sid. This information is shared with the * Authentication Server, so we assume a trusted way of installing a * Yubikey */ rule BuyANewYubikey: [Fr(~k),Fr(~pid),Fr(~sid)] //for fresh k, public and secret id.. --[Protocol(), Init(~pid,~k),ExtendedInit(~pid,~sid,~k),IsZero(zero)]-> [!Y(~pid,~sid), Y_counter(~pid,zero), //..store public and secret id along with the starting counter //(zero) on the Yubikey.. Server(~pid,~sid,zero),!SharedKey(~pid,~k), //and on the server Out(~pid)] //and make the public id public //On plugin, the session counter is increased and the token counter reset rule Yubikey_Plugin: [Y_counter(pid,sc),!Smaller(sc, Ssc) ] //The old counter value sc is removed --[ Yubi(pid,Ssc) ]-> [Y_counter(pid, Ssc)] //and substituted by a new counter value, larger, Ssc //If the Button is pressed, the token counter is increased rule Yubikey_PressButton: [!Y(pid,sid), Y_counter(pid,tc),!SharedKey(pid,k), !Succ(tc,Stc),Fr(~npr),Fr(~nonce) ] //The old countervalue tc is removed --[ YubiPress(pid,tc), YubiOTP(pid,senc(,k)), YubiSid(pid,sid,k) ]-> [Y_counter(pid, Stc), //and substituted by its successor Out(,k)>) //in addition, an encrypted otp is output along with a nonce and //the public id of the Yubikey used. ] /* Upon receiving an encrypted OTP, the Server compares the (unencrypted) * public id to his data base to identify the key to decrypt the OTP. After * making sure that the secret id is correct, the Server verifies that the * received counter value is larger than the last one stored. If the Login * is successful, i.e., the previous conditions were fulfilled, the counter * value on the Server that is associated to the Yubikey is updated. */ rule Server_ReceiveOTP_NewSession: [Server(pid,sid,otc), In(,k)>), !SharedKey(pid,k), !Smaller(otc,tc) ] //if the Server receives an OTP encrypted with k that belongs to //the (unencrypted) public id, and the OTP has the right format, //contains the correct secret id as well as a counter tc that is //larger than the current counter otc, then... --[ Login(pid,sid,tc,senc(,k)), LoginCounter(pid,otc,tc) //..the Login is accepted.. ]-> [Server(pid,sid,tc)] //..and the counter value updated. /* The following three axioms are conditions on the traces that make sure * that : */ //a) the !Smaller relation is transitive axiom transitivity: //axiomatic "All #t1 #t2 a b c. IsSmaller(a,b)@t1 & IsSmaller(b,c)@t2 ==> Ex #t3 . IsSmaller(a,c)@t3 " //b) !Smaller implies unequality axiom smaller_implies_unequal: //axiomatic "not (Ex a #t . IsSmaller(a,a)@t)" //c) The protocol runs only after the IsSmaller and IsSuccessor relation is // build up axiom theory_before_protocol: "All #i #j. Theory() @ i & Protocol() @ j ==> i < j" // For sanity: Ensure that a successful login is reachable. lemma Login_reachable: exists-trace "Ex #i pid sid x otp1. Login(pid,sid,x,otp1)@i" // Each succesful login with counter value x was preceeded by a PressButton // event with the same counter value lemma one_count_foreach_login[reuse,use_induction]: "All pid sid x otp #t2 . Login(pid,sid,x,otp)@t2 ==> ( Ex #t1 . YubiPress(pid,x)@#t1 & #t1<#t2 )" // If a succesful Login happens before a second sucesfull Login, the // counter value of the first is smaller than the counter value of the // second lemma slightly_weaker_invariant[reuse, use_induction]: "(All pid otc1 tc1 otc2 tc2 #t1 #t2 . LoginCounter(pid,otc1,tc1)@#t1 & LoginCounter(pid,otc2,tc2)@#t2 ==> ( #t1<#t2 & ( Ex #t3 . IsSmaller(tc1,tc2)@t3 )) | #t2<#t1 | #t1=#t2) " induction case empty_trace by contradiction // from formulas next case non_empty_trace simplify solve( (∀ pid otc1 tc1 otc2 tc2 #t1 #t2. (LoginCounter( pid, otc1, tc1 ) @ #t1) ∧ (LoginCounter( pid, otc2, tc2 ) @ #t2) ⇒ (last(#t2)) ∨ (last(#t1)) ∨ ((#t1 < #t2) ∧ (∃ #t3. (IsSmaller( tc1, tc2 ) @ #t3) ∧ ¬(last(#t3)))) ∨ (#t2 < #t1) ∨ (#t1 = #t2)) ∥ (∃ #t1 #t2 a b c. (IsSmaller( a, b ) @ #t1) ∧ (IsSmaller( b, c ) @ #t2) ∧ (¬(last(#t2))) ∧ (¬(last(#t1))) ∧ (∀ #t3. (IsSmaller( a, c ) @ #t3) ⇒ last(#t3))) ) case case_1 solve( (last(#t2)) ∥ (last(#t1)) ∥ ((#t1 < #t2) ∧ (∃ #t3. (IsSmaller( tc1, tc2 ) @ #t3) ∧ ¬(last(#t3)))) ∥ (#t2 < #t1) ∥ (#t1 = #t2) ) case case_1 solve( Server( pid, sid, otc1 ) ▶₀ #t1 ) case BuyANewYubikey solve( Server( ~pid, sid.1, otc2 ) ▶₀ #t2 ) by sorry next case Server_ReceiveOTP_NewSession_case_1 solve( Server( ~pid, sid.1, otc2 ) ▶₀ #t2 ) by sorry next case Server_ReceiveOTP_NewSession_case_2 solve( Server( ~pid, sid.1, otc2 ) ▶₀ #t2 ) by sorry next case Server_ReceiveOTP_NewSession_case_3 solve( Server( ~pid, sid.1, otc2 ) ▶₀ #t2 ) by sorry next case Server_ReceiveOTP_NewSession_case_4 solve( Server( ~pid, sid.1, otc2 ) ▶₀ #t2 ) by sorry qed next case case_2 by contradiction // cyclic next case case_3 by contradiction // from formulas next case case_4 by contradiction // from formulas next case case_5 by contradiction // from formulas qed next case case_2 by sorry qed qed // It is not possible to have to distinct logins with the same counter // value lemma no_replay: "not (Ex #i #j pid sid x otp1 otp2 . Login(pid,sid,x,otp1)@i & Login(pid,sid,x,otp2)@j & not(#i=#j))" lemma injective_correspondance: "All pid sid x otp #t2 . Login(pid,sid,x,otp)@t2 ==> ( Ex #t1 . YubiPress(pid,x)@#t1 & #t1<#t2 & All otp2 #t3 . Login(pid,sid,x,otp2)@t3 ==> #t3=#t2 )" lemma Login_invalidates_smaller_counters: "All pid otc1 tc1 otc2 tc2 #t1 #t2 #t3 . LoginCounter(pid,otc1,tc1)@#t1 & LoginCounter(pid,otc2,tc2)@#t2 & IsSmaller(tc1,tc2)@t3 ==> #t1<#t2 " end