Checking the deffinitions of OW-CCA

[Choro Ulan uulu]

Hi,

for my university project i need to understand how tamarin-prover works. I want to check the definitions of OW-CCA. For that i have written this code: 

theory symmEncOracles

begin

/* senc and sdec take 2 inputs, resp. */

functions: senc/2, sdec/2

/* decryption of encryption of m is m */

equations: sdec(k,senc(k,m))=m

/* ORACLES */

rule OracleInit:

  [ Fr(~challKey) ]

  -->

  [ OracleInit(~challKey),

    OracleChallCanBeCalled(~challKey)

   ]

rule OracleEnc:

  [ OracleInit(~challKey),

    In(m) ]

  -->

  [ Out(senc(~challKey,m)) ]

rule OracleDec1:

  [ OracleInit(~challKey),

    In(senc(~challKey,m)) ]

  -->

  [ Out(m) ]

//can only be called once

rule OracleChall:

  [ OracleInit(~challKey),

    Fr(~challMsg),

    OracleChallCanBeCalled(~challKey) ]

  -->

  [ OracleChall(~challMsg),

    Out(senc(~challKey,~challMsg))]

// if OracleChall was called before, outputs nothing

rule OracleDec2_no_output:

  [ OracleInit(~challKey),

    OracleChall(~challMsg),

    In(senc(~challKey, ~challMsg)) ]

  -->  

  [ ]

//else

rule OracleDec2_output_m:

  [ OracleInit(~challKey),

    OracleChall(~challMsg),

    In(senc(~challKey, m)),

    Neq(~challMsg, m) ]

  -->  

  [ Out(m) ]

//it is impossible to obtain challMsg

lemma UnobtainableChallMsg:

  " not( Ex #k . K(~challMsg) @ #k) "

end

Is this approach correct?

In UI i get partial deconstruction. Could you please explain me why? 

Thanks in advance

[Simon BOUGET]

Hi,

I note a few issues in your code. Not sure that's really what's creating your problems, but worth looking into it.

- "Neq" sounds like a restriction, and if that's the case it should be in the Trace (the middle part of the rule), not the Conditions (the first part)

- The two rules OracleDec2_... have the same Conditions (apart from the "Neq" fact mentioned above), that's probably not what you want.

- To make sure that rule "OracleChall" can be called only once, again, you should use a restriction in the Trace, not in the condition. Check for "OnlyOnce" and/or "OnlyOnceV" in the manual, depending on what you want to do exactly.

- "OracleInit" is consumed in several conditions, so it probably should be a persistent fact (marked with a "!" at the beginning of its name)

Hope that helps,

Simon

--
You received this message because you are subscribed to the Google Groups "tamarin-prover" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tamarin-prove...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tamarin-prover/dc57c4ff-00fc-4248-9d73-0db1ac120b74n%40googlegroups.com.

[Choro Ulan uulu]

Hi Simon,

thank you for your response!

 "The two rules OracleDec2_... have the same Conditions (apart from the "Neq" fact mentioned above), that's probably not what you want." 

the difference is that we get "m" or "~challMsg" in In()

I have changed the code according to your response:

theory symmEncOracles

begin

/* senc and sdec take 2 inputs, resp. */

functions: senc/2, sdec/2

/* decryption of encryption of m is m */

equations: sdec(k,senc(k,m))=m

/* ORACLES */

rule OracleInit:

  [

    Fr(~challKey) ]

  --[OnlyOnce()]->

  [ !OracleInit(~challKey),

    PreChall()

   ]

rule OracleEnc:

  [ !OracleInit(~challKey),

    In(m) ]

  -->

  [ Out(senc(~challKey,m)) ]

rule OracleDec1:

  [ !OracleInit(~challKey),

    PreChall(),

    In(senc(~challKey,m)) ]

  -->

  [ PreChall(),

    Out(m) ]

//can only be called once

rule OracleChall:

  [ !OracleInit(~challKey),

    PreChall(),

    Fr(~challMsg)]

  -->

  [ OracleChall(senc(~challKey,~challMsg)),

    Out(senc(~challKey,~challMsg))]

// if OracleChall was called before, outputs nothing

rule OracleDec2_no_output:

  [ !OracleInit(~challKey),

    OracleChall(senc(~challKey,~challMsg)),

    In(senc(~challKey, ~challMsg)) ]

  -->  

  [ ]

//else

rule OracleDec2_output_m:

  [ !OracleInit(~challKey),

    OracleChall(senc(~challKey,~challMsg)),

    In(senc(~challKey, m))

     ]

  --[Neq(senc(~challKey,~challMsg),senc(~challKey,m))]->

  [ Out(m) ]

rule OracleFin:

  [ OracleChall(senc(~challKey,~challMsg)),

    In(m) ]

  --[ Eq(m,~challMsg),

      !AdvWins() ]->

  [ ]

//it is impossible to obtain challMsg

lemma oneWaySecurity:

  " not( Ex #i. !AdvWins() @ #i ) "

restriction OnlyOnce:

  "All #i #j. OnlyOnce()@#i & OnlyOnce()@#j ==> #i = #j"

restriction Inequality:

  "All x #i. Neq(x,x) @ #i ==> F"

restriction Equality:

  "All x y #i. Eq(x,y) @#i ==> x = y"

end

when i'm trying to autoprove this in tamarin prover after some time it gets "Killed".

What could be the Problem? 

Kind regards,

Choro