diff --git a/data/CHANGES b/data/CHANGES --- a/data/CHANGES +++ b/data/CHANGES @@ -1,3 +1,9 @@ +* 0.8.5.1 + - Added KEA+ models with adversarial key registration. + - Make case splitting more extensive. This possibly increases precomputation + time, but in some cases it enables proving more properties. + - fix: restrict aeson depedency to 0.6.* + * 0.8.5 Dropped support for GHC 7.0.x and GHC 7.2.x in favor of GHC 7.6.x - fix: faster and simpler variant computation diff --git a/data/etc/spthy.vim b/data/etc/spthy.vim --- a/data/etc/spthy.vim +++ b/data/etc/spthy.vim @@ -37,6 +37,7 @@ syn match spthyLAtom "=" syn match spthyLAtom "@" syn match spthyLAtom "<" +syn match spthyLAtom ">" syn keyword spthyConstr aenc sdec senc sdec sign verify hashing signing syn match spthyConstr "\ + [ !Ltk( $A, ~lk ), !Pk( $A, pk ), Out( pk ) ] + +rule generate_ltk_adv: + [ In(< $A, pk> ) ] + --[ AdvKey(pk), LtkRev(pk) ]-> + [ !Pk( $A, pk ) ] + +rule Init_1: + let epkI = 'g'^~ekI + in + [ Fr( ~ekI ), !Ltk( $I, ~lkI ) ] + --[ SidI_1(~ekI,$I,$R, epkI ) ]-> + [ Init_1( ~ekI, $I, $R, ~lkI, epkI ), + !Ephk(~ekI), + Out( epkI ) ] + +rule Init_2: + let epkR = 'g'^~ekR + pkI = 'g'^~lkI + sesk = h( ) + in + [ Init_1( ~ekI, $I, $R, ~lkI , hkI), In( Y ), !Pk( $R,pkR ) ] + --[SidI_2( ~ekI, $I, $R, hkI, Y, sesk, pkI, pkR ) ]-> + [ !Sessk( ~ekI, sesk ) ] + +rule Resp_1: + let pkR = 'g'^~lkR + sesk = h( <(pkI)^~ekR, X^~lkR, $I, $R, pkI, pkR > ) + in + [ In( X ), Fr( ~ekR ), !Ltk($R, ~lkR), !Pk($I, pkI) ] + --[ SidR_1( ~ekR, $I, $R, X, 'g'^~ekR, sesk, pkI, pkR ) ]-> + [ Out( 'g'^~ekR ), !Ephk(~ekR), !Sessk( ~ekR, sesk) ] + +rule Sessk_reveal: + [ !Sessk(~tid, k) ] + --[ SesskRev(~tid) ]-> + [ Out(k) ] + +rule Ephk_reveal: + [ !Ephk(~ekI) ] + --[ EphkRev(~ekI) ]-> + [ Out(~ekI) ] + +rule Ltk_reveal: + [ !Ltk($A, k) ] + --[ LtkRev('g'^k) ]-> + [ Out(k) ] + + +/* Security properties */ + +/* +lemma key_agreement_reachable: + "not (Ex #i1 #i2 ekI ekR I R k hkI hkR. + SidI_2(ekI, I, R, hkI, hkR, k) @ i1 & SidR_1(ekR, I, R, hkI, hkR, k) @ i2)" +*/ + +/* Security notion. + * + * This is the "core" KEA+ security definition without (w)PFS or KCI. + * + * We model ephemeral key reveals for non-partner threads. This + * corresponds to a session-state-reveal analysis where the + * session-state is defined as the randomness generated by the parties. + * This property is not implied by the proof (sketch) in the KEA+ paper. + */ + +/* An attack is valid in the security notion if the session key of the test session is deduced and + the test session is clean. +*/ +lemma keaplus_initiator_key: + "not (Ex #i1 #i2 ttest I R k hkI hkR kI kR. + SidI_2(ttest, I, R, hkI, hkR, k, kI, kR ) @ i1 & K( k ) @ i2 + + /* No ephemeral-key-reveal of test thread */ + & (All #i3. EphkRev( ttest ) @ i3 ==> F) + + /* Not session-key-reveal of test thread. */ + & (All #i3. SesskRev( ttest ) @ i3 ==> F) + + /* Not ephemeral-key-reveal of partner thread. */ + & (All #i3 #i4 tpartner kpartner kI2 kR2 . + SidR_1( tpartner,I,R,hkI,hkR,kpartner,kI2,kR2 ) @i3 + & EphkRev( tpartner ) @ i4 ==> F) + + /* Not session-key-reveal of partner thread. */ + & (All #i3 #i4 tpartner kpartner kI2 kR2 . + SidR_1( tpartner,I,R,hkI,hkR,kpartner,kI2,kR2 ) @i3 + & SesskRev( tpartner ) @ i4 ==> F) + + /* Not longterm-key-reveal of actor or intended peer. */ + & (All #i3. LtkRev( kI ) @ i3 ==> F) + & (All #i3. LtkRev( kR ) @ i3 ==> F) + )" + +/* An attack is valid in the security notion if the session key of the test session is deduced and + the test session is clean. +*/ +lemma keaplus_responder_key: + "not (Ex #i1 #i2 ttest I R k hkI hkR kI kR. + SidR_1(ttest, I, R, hkI, hkR, k, kI, kR) @ i1 & K( k ) @ i2 + + /* Not ephemeral-key-reveal of test thread. */ + & (All #i3. EphkRev( ttest ) @ i3 ==> F) + + /* Not session-key-reveal of test thread. */ + & (All #i3. SesskRev( ttest ) @ i3 ==> F) + + /* Not ephemeral-key-reveal of partner thread. */ + /* Note we distinguish explicitly between an incomplete + * and complete partner thread case. + */ + & (All #i3 #i4 tpartner lki. + SidI_1( tpartner,I,R,lki ) @i3 + & EphkRev( tpartner ) @ i4 ==> F) + & (All #i3 #i4 tpartner kpartner kI2 kR2 . + SidI_2( tpartner,I,R,hkI,hkR,kpartner,kI2,kR2 ) @i3 + & EphkRev( tpartner ) @ i4 ==> F) + + /* Not session-key-reveal of partner thread. Note that we use SidI_2 here. + A session key reveal can only happen after SidI_2 is logged anyways. + */ + & (All #i3 #i4 tpartner kpartner kI2 kR2 . + SidI_2( tpartner,I,R,hkI,hkR,kpartner,kI2,kR2 ) @i3 + & SesskRev( tpartner ) @ i4 ==> F) + + /* Not longterm-key-reveal of actor or intended peer. */ + & (All #i3. LtkRev( kR ) @ i3 ==> F) + & (All #i3. LtkRev( kI ) @ i3 ==> F) + )" + +end diff --git a/data/examples/csf12/KEA_plus_AdvKey.spthy b/data/examples/csf12/KEA_plus_AdvKey.spthy new file mode 100644 --- /dev/null +++ b/data/examples/csf12/KEA_plus_AdvKey.spthy @@ -0,0 +1,159 @@ +theory KEA_plus_AdvKey +begin + +builtins: hashing, diffie-hellman + +section{* KEA+ with adversarial key registration *} +/* + * Protocol: KEA+ + * Modeler: Cas Cremers + * Date: January 2012, June 2013 + * Source: "Security Analysis of KEA Authenticated Key Exchange Protocol" + * Lauter, Mityagin, 2006 + * + * Adapted the security model in the context of the ASICS + * work, in order to be able to model the attack previously + * found manually by Michele Feltz on KEA+. + * + * Status: Working + */ + + +/* Protocol rules */ + +rule generate_ltk: + let pk = 'g'^~lk + in + [ Fr(~lk) ] --> + [ !Ltk( $A, ~lk ), !Pk( $A, pk ), Out( pk ) ] + +rule generate_ltk_adv: + [ In(< $A, pk> ) ] + --[ AdvKey(pk), LtkRev(pk) ]-> + [ !Pk( $A, pk ) ] + +rule Init_1: + let epkI = 'g'^~ekI + in + [ Fr( ~ekI ), !Ltk( $I, ~lkI ) ] + --[ SidI_1(~ekI,$I,$R, epkI ) ]-> + [ Init_1( ~ekI, $I, $R, ~lkI, epkI ), + !Ephk(~ekI), + Out( epkI ) ] + +rule Init_2: + let epkR = 'g'^~ekR + pkI = 'g'^~lkI + sesk = h( ) + in + [ Init_1( ~ekI, $I, $R, ~lkI , hkI), In( Y ), !Pk( $R,pkR ) ] + --[SidI_2( ~ekI, $I, $R, hkI, Y, sesk, pkI, pkR ) ]-> + [ !Sessk( ~ekI, sesk ) ] + +rule Resp_1: + let pkR = 'g'^~lkR + sesk = h( <(pkI)^~ekR, X^~lkR, $I, $R > ) + in + [ In( X ), Fr( ~ekR ), !Ltk($R, ~lkR), !Pk($I, pkI) ] + --[ SidR_1( ~ekR, $I, $R, X, 'g'^~ekR, sesk, pkI, pkR ) ]-> + [ Out( 'g'^~ekR ), !Ephk(~ekR), !Sessk( ~ekR, sesk) ] + +rule Sessk_reveal: + [ !Sessk(~tid, k) ] + --[ SesskRev(~tid) ]-> + [ Out(k) ] + +rule Ephk_reveal: + [ !Ephk(~ekI) ] + --[ EphkRev(~ekI) ]-> + [ Out(~ekI) ] + +rule Ltk_reveal: + [ !Ltk($A, k) ] + --[ LtkRev('g'^k) ]-> + [ Out(k) ] + + +/* Security properties */ + +/* +lemma key_agreement_reachable: + "not (Ex #i1 #i2 ekI ekR I R k hkI hkR. + SidI_2(ekI, I, R, hkI, hkR, k) @ i1 & SidR_1(ekR, I, R, hkI, hkR, k) @ i2)" +*/ + +/* Security notion. + * + * This is the "core" KEA+ security definition without (w)PFS or KCI. + * + * We model ephemeral key reveals for non-partner threads. This + * corresponds to a session-state-reveal analysis where the + * session-state is defined as the randomness generated by the parties. + * This property is not implied by the proof (sketch) in the KEA+ paper. + */ + +/* An attack is valid in the security notion if the session key of the test session is deduced and + the test session is clean. +*/ +lemma keaplus_initiator_key: + "not (Ex #i1 #i2 ttest I R k hkI hkR kI kR. + SidI_2(ttest, I, R, hkI, hkR, k, kI, kR ) @ i1 & K( k ) @ i2 + + /* No ephemeral-key-reveal of test thread */ + & (All #i3. EphkRev( ttest ) @ i3 ==> F) + + /* Not session-key-reveal of test thread. */ + & (All #i3. SesskRev( ttest ) @ i3 ==> F) + + /* Not ephemeral-key-reveal of partner thread. */ + & (All #i3 #i4 tpartner kpartner kI2 kR2 . + SidR_1( tpartner,I,R,hkI,hkR,kpartner,kI2,kR2 ) @i3 + & EphkRev( tpartner ) @ i4 ==> F) + + /* Not session-key-reveal of partner thread. */ + & (All #i3 #i4 tpartner kpartner kI2 kR2 . + SidR_1( tpartner,I,R,hkI,hkR,kpartner,kI2,kR2 ) @i3 + & SesskRev( tpartner ) @ i4 ==> F) + + /* Not longterm-key-reveal of actor or intended peer. */ + & (All #i3. LtkRev( kI ) @ i3 ==> F) + & (All #i3. LtkRev( kR ) @ i3 ==> F) + )" + +/* An attack is valid in the security notion if the session key of the test session is deduced and + the test session is clean. +*/ +lemma keaplus_responder_key: + "not (Ex #i1 #i2 ttest I R k hkI hkR kI kR. + SidR_1(ttest, I, R, hkI, hkR, k, kI, kR) @ i1 & K( k ) @ i2 + + /* Not ephemeral-key-reveal of test thread. */ + & (All #i3. EphkRev( ttest ) @ i3 ==> F) + + /* Not session-key-reveal of test thread. */ + & (All #i3. SesskRev( ttest ) @ i3 ==> F) + + /* Not ephemeral-key-reveal of partner thread. */ + /* Note we distinguish explicitly between an incomplete + * and complete partner thread case. + */ + & (All #i3 #i4 tpartner lki. + SidI_1( tpartner,I,R,lki ) @i3 + & EphkRev( tpartner ) @ i4 ==> F) + & (All #i3 #i4 tpartner kpartner kI2 kR2 . + SidI_2( tpartner,I,R,hkI,hkR,kpartner,kI2,kR2 ) @i3 + & EphkRev( tpartner ) @ i4 ==> F) + + /* Not session-key-reveal of partner thread. Note that we use SidI_2 here. + A session key reveal can only happen after SidI_2 is logged anyways. + */ + & (All #i3 #i4 tpartner kpartner kI2 kR2 . + SidI_2( tpartner,I,R,hkI,hkR,kpartner,kI2,kR2 ) @i3 + & SesskRev( tpartner ) @ i4 ==> F) + + /* Not longterm-key-reveal of actor or intended peer. */ + & (All #i3. LtkRev( kR ) @ i3 ==> F) + & (All #i3. LtkRev( kI ) @ i3 ==> F) + )" + +end diff --git a/src/Web/Hamlet.hs b/src/Web/Hamlet.hs --- a/src/Web/Hamlet.hs +++ b/src/Web/Hamlet.hs @@ -266,7 +266,7 @@ \ Simon Meier, \ Benedikt Schmidt
Contributors: - \ Cas Cremers, + \ Cas Cremers, \ Cedric Staub

Tamarin was developed at the diff --git a/src/Web/Handler.hs b/src/Web/Handler.hs --- a/src/Web/Handler.hs +++ b/src/Web/Handler.hs @@ -320,7 +320,7 @@ -- | The root handler lists all theories by default, -- or load a new theory if the corresponding form was submitted. -getRootR :: Handler RepHtml +getRootR :: Handler Html getRootR = do theories <- getTheories defaultLayout $ do @@ -330,7 +330,7 @@ data File = File T.Text deriving Show -postRootR :: Handler RepHtml +postRootR :: Handler Html postRootR = do result <- lookupFile "uploadedTheory" case result of @@ -357,7 +357,7 @@ -- | Show overview over theory (framed layout). -getOverviewR :: TheoryIdx -> TheoryPath -> Handler RepHtml +getOverviewR :: TheoryIdx -> TheoryPath -> Handler Html getOverviewR idx path = withTheory idx $ \ti -> do renderF <- getUrlRender defaultLayout $ do @@ -456,7 +456,7 @@ {- -- | Show a given path within a theory (debug view). -getTheoryPathDR :: TheoryIdx -> TheoryPath -> Handler RepHtml +getTheoryPathDR :: TheoryIdx -> TheoryPath -> Handler Html getTheoryPathDR idx path = withTheory idx $ \ti -> ajaxLayout $ do -- let maybeDebug = htmlThyDbgPath (tiTheory ti) path -- let maybeWidget = wrapHtmlDoc <$> maybeDebug @@ -700,7 +700,7 @@ {- -- | Show a list of all currently running threads. -getThreadsR :: Handler RepHtml +getThreadsR :: Handler Html getThreadsR = do threads <- getThreads defaultLayout $ do diff --git a/src/Web/Types.hs b/src/Web/Types.hs --- a/src/Web/Types.hs +++ b/src/Web/Types.hs @@ -328,12 +328,12 @@ -- belong in the "types" module in order to avoid mutually recursive modules. -- defaultLayout' :: (Yesod master, Route master ~ WebUIRoute) -- => Widget master () -- ^ Widget to embed in layout --- -> Handler master RepHtml -defaultLayout' :: Widget -> Handler RepHtml +-- -> Handler master Html +defaultLayout' :: Widget -> Handler Html defaultLayout' w = do page <- widgetToPageContent w message <- getMessage - hamletToRepHtml [hamlet| + giveUrlRenderer [hamlet| $newline never !!! diff --git a/tamarin-prover.cabal b/tamarin-prover.cabal --- a/tamarin-prover.cabal +++ b/tamarin-prover.cabal @@ -1,7 +1,7 @@ cabal-version: >= 1.8 build-type: Simple name: tamarin-prover -version: 0.8.5.0 +version: 0.8.5.1 license: GPL license-file: LICENSE category: Theorem Provers @@ -166,6 +166,9 @@ examples/csf12/JKL_TS3_2004_KI_wPFS.spthy_nonterm examples/csf12/JKL_TS3_2008_KI_wPFS.spthy_nonterm + examples/csf12/KEA_plus_AdvKey-fix.spthy + examples/csf12/KEA_plus_AdvKey.spthy + extra-source-files: .ghci interactive-only-src/Paths_tamarin_prover.hs @@ -229,16 +232,16 @@ , blaze-html >= 0.5 , http-types >= 0.7 , blaze-builder >= 0.3 - , yesod-core >= 1.1 - , yesod-json >= 1.1 - , yesod-static >= 1.1 + , yesod-core >= 1.2.6.6 + , yesod-json >= 1.2 + , yesod-static >= 1.2 , conduit >= 0.5 -- , yesod-form == 0.4.* -- required once we reactivate editing , text == 0.11.* , wai >= 1.3 , hamlet >= 1.1 , warp >= 1.3 - , aeson >= 0.6 + , aeson == 0.6.* , old-locale == 1.* , monad-control == 0.* , lifted-base >= 0.2.0.5 @@ -268,9 +271,9 @@ , parallel == 3.2.* , HUnit == 1.2.* - , tamarin-prover-utils >= 0.8.5 && < 0.9 - , tamarin-prover-term >= 0.8.5 && < 0.9 - , tamarin-prover-theory >= 0.8.5 && < 0.9 + , tamarin-prover-utils >= 0.8.5.1 && < 0.9 + , tamarin-prover-term >= 0.8.5.1 && < 0.9 + , tamarin-prover-theory >= 0.8.5.1 && < 0.9 other-modules: