tamarin-prover 0.8.5.0 → 0.8.5.1
raw patch · 9 files changed
+346/−18 lines, 9 filesdep ~aesondep ~tamarin-prover-termdep ~tamarin-prover-theory
Dependency ranges changed: aeson, tamarin-prover-term, tamarin-prover-theory, tamarin-prover-utils, yesod-core, yesod-json, yesod-static
Files
- data/CHANGES +6/−0
- data/etc/spthy.vim +1/−0
- data/examples/Tutorial.spthy +1/−1
- data/examples/csf12/KEA_plus_AdvKey-fix.spthy +159/−0
- data/examples/csf12/KEA_plus_AdvKey.spthy +159/−0
- src/Web/Hamlet.hs +1/−1
- src/Web/Handler.hs +5/−5
- src/Web/Types.hs +3/−3
- tamarin-prover.cabal +11/−8
data/CHANGES view
@@ -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
data/etc/spthy.vim view
@@ -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 "\<h("he=e-1
data/examples/Tutorial.spthy view
@@ -416,7 +416,7 @@ Benedikt Schmidt benedikt.schmidt@inf.ethz.ch Simon Meier iridcode@gmail.com- Cas Cremers cas.cremers@inf.ethz.ch+ Cas Cremers cas.cremers@cs.ox.ac.uk BTW, every security protocol theory must be delimited with 'end'.
+ data/examples/csf12/KEA_plus_AdvKey-fix.spthy view
@@ -0,0 +1,159 @@+theory KEA_plus_AdvKey_fix+begin++builtins: hashing, diffie-hellman++section{* KEA+ with adversarial key registration with fix *}+/*+ * 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( <Y^~lkI, (pkR)^~ekI, $I, $R, pkI, pkR > )+ 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
+ data/examples/csf12/KEA_plus_AdvKey.spthy view
@@ -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( <Y^~lkI, (pkR)^~ekI, $I, $R > )+ 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
src/Web/Hamlet.hs view
@@ -266,7 +266,7 @@ \ <a href="http://people.inf.ethz.ch/meiersi">Simon Meier</a>, \ <a href="https://www1.ethz.ch/infsec/people/benschmi">Benedikt Schmidt</a><br> Contributors:- \ <a href="http://people.inf.ethz.ch/cremersc/index.html">Cas Cremers</a>,+ \ <a href="http://www.cs.ox.ac.uk/people/cas.cremers/">Cas Cremers</a>, \ <a href="http://cssx.ch">Cedric Staub</a> <p> <span class="tamarin">Tamarin</span> was developed at the
src/Web/Handler.hs view
@@ -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
src/Web/Types.hs view
@@ -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 !!! <html>
tamarin-prover.cabal view
@@ -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: