Why can proverif not find value that I just created?

Grazosi

2/11/23, 5:01 PM

I have a really simple ProVerif problem. My current proverif code looks like this:

(* communication channel *)
free c:channel.

(* trying to create a mac scheme *)
type mkey.
fun mac (bitstring , mkey): bitstring.

(* Symmetric encryption *)

type skey.
type coins.

fun internal_senc(bitstring , skey , coins): bitstring.

reduc forall m:bitstring , k:skey , r:coins;
   sdec(internal_senc(m,k,r),k) = m.


let ED(AppKey :skey, NwkKey :mkey, JoinEUI :bitstring,DevEUI :bitstring, DevNonce : bitstring) =
    out(c, (JoinEUI,DevEUI,DevNonce, mac((JoinEUI , DevEUI , DevNonce), NwkKey) )).

let JS(AppKey :skey, NwkKey :mkey,DevEUI :bitstring, JoinEUI :bitstring, DevAddr : bitstring) =
    in(c,x: bitstring);
    let(=JoinEUI, =DevEUI,new DevNonce: bitstring, =mac((JoinEUI,DevEUI,DevNonce), NwkKey)) = x in
    new JoinNonce : bitstring;
    new Home_NetID : bitstring;
    let MIC2 : bitstring = mac(NwkKey, (JoinNonce,Home_NetID, DevAddr)) in
    out(c,JoinEUI).

So, in luine 25, that looks like this:

let(=JoinEUI, =DevEUI, DevNonce: bitstring, =mac((JoinEUI,DevEUI,DevNonce), NwkKey)) = x in

It fails on the DevNonce part, which I don't get at all, just look at page 71 of the manual a new variable is creaetd fine that way.

How do I actually declare this value in the JS proces?

0 + 0

protocol-design

proverif

DannyNiu

2/12/23, 6:24 AM

For those voted close, I propose reconsidering reconsidering your vote as "ProVerif" seem to be a "formal verification" tool that may be on-topic as discussed [here](https://crypto.meta.stackexchange.com/q/1550/36960)

Geoffroy Couteau

2/12/23, 7:37 AM

I agree that questions on formal verifications tools specifically designed for cryptography, even technical questions about how to use their underlying language, should be on topic here. There is no other place to ask about that and the use of these tools is an important part of cryptographic research.

kelalaka

2/12/23, 8:08 AM

@GeoffroyCouteau and DannyNiu You are right about it. Write a small Meta Question so that we can vote and make it a permanent agreement. A tag proposal will be also good.

kelalaka

2/12/23, 7:35 PM