26 views

Skip to first unread message

May 15, 2023, 1:42:43 PM5/15/23

to tamarin-prover

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

May 16, 2023, 5:35:57 AM5/16/23

to tamarin...@googlegroups.com

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.

May 16, 2023, 10:01:38 AM5/16/23

to tamarin-prover

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

Reply all

Reply to author

Forward

0 new messages

Search

Clear search

Close search

Google apps

Main menu