[isabelle] Confirming protocol messages in Inductive Method

Discussion:

Felipe Rodopoulos

2018-10-17 02:15:58 UTC

Hello everyone,

I am formalizing a banking authorization protocol, using the Inductive
Method
theory from the Isabelle/HOL library.

At a given protocol stage, the user must confirm the issued transaction.
She
receives the transaction details through her smartphone screen and, if
it
matches what she first issued, she confirms the operation by clicking a
button
at the screen.

The protocol document does not specify this "confirmation message"
format, so I
defined one myself. Basically, it is a restatement of the transaction,
followed
by an acknowledgement bit. Therefore, given the transaction is defined
by its
originator name and a number (representing the transaction itself), the
events go like this, where some preconditions are omitted:

(* This rule refers to smartphone *)
| DT4: "[evs4 \in sdaptrans; legalUse(Smartphone A); A != Server; ...]
==> Shows (Smartphone A) A {Agent A, Number T} # evs4 \in sdaptrans"

(* This rule refers to the user *)
| DT5: "[evs5 ∈ sdaptrans; legalUse(Smartphone A);
Says A Server {Agent A, Number T} \in set evs5;
...
Shows (Smartphone A) A {Agent A, Number T} \in set evs5]
==> Inputs A (Smartphone A) {Agent A, Number T, Confirmation} # evs5
\in sdaptrans"

The Confirmation message is defined as follows:

abbreviation
Confirmation :: msg where "Confirmation ≡ (Number 1)"

I am not pretty sure if this is a good approach. At some lemmas, I got
some
subgoals trying to replace the confirmation number by the transaction
number, as
if the Spy was faking the message. For me, the ideal approach would be
that the
Confirmation part would be an immutable bit, not relying in a value, but
I do
not know how to properly do that. I looked at some other protocols
formalization, but I couldn't find some valuable hint.

I am open to any ideas. Thanks in advance.

Ps: I'd like to thanks Larry Paulson for answering my previous
questions. The
replies were quite useful.

-
Felipe Rodopoulos
Grad. student @ University of Brasília, Brazil

Lawrence Paulson

2018-10-17 14:00:32 UTC

Permalink

Thanks for your email.

The main issue may be whether the inductive method is a good fit to what you are working on. The network model embodied in the inductive method is an insecure network lacking confidentiality and authentication and where all traffic is visible to the Spy, who can also send spoof messages using any material at his disposal. But if you send a message to a cell phone over the cellular network, the network provides some security guarantees, confidentiality for sure as well as authentication for the device itself, and arguably (through the pass code mechanism) of the user as well. It's not clear what an external attacker can do in this context.

Larry Paulson

Post by Felipe Rodopoulos
Hello everyone,
I am formalizing a banking authorization protocol, using the Inductive Method
theory from the Isabelle/HOL library.
At a given protocol stage, the user must confirm the issued transaction. She
receives the transaction details through her smartphone screen and, if it
matches what she first issued, she confirms the operation by clicking a button
at the screen.
The protocol document does not specify this "confirmation message" format, so I
defined one myself. Basically, it is a restatement of the transaction, followed
by an acknowledgement bit. Therefore, given the transaction is defined by its
originator name and a number (representing the transaction itself), the
(* This rule refers to smartphone *)
| DT4: "[evs4 \in sdaptrans; legalUse(Smartphone A); A != Server; ...]
==> Shows (Smartphone A) A {Agent A, Number T} # evs4 \in sdaptrans"
(* This rule refers to the user *)
| DT5: "[evs5 ∈ sdaptrans; legalUse(Smartphone A);
Says A Server {Agent A, Number T} \in set evs5;
...
Shows (Smartphone A) A {Agent A, Number T} \in set evs5]
==> Inputs A (Smartphone A) {Agent A, Number T, Confirmation} # evs5 \in sdaptrans"
abbreviation
Confirmation :: msg where "Confirmation ≡ (Number 1)"
I am not pretty sure if this is a good approach. At some lemmas, I got some
subgoals trying to replace the confirmation number by the transaction number, as
if the Spy was faking the message. For me, the ideal approach would be that the
Confirmation part would be an immutable bit, not relying in a value, but I do
not know how to properly do that. I looked at some other protocols
formalization, but I couldn't find some valuable hint.
I am open to any ideas. Thanks in advance.
Ps: I'd like to thanks Larry Paulson for answering my previous questions. The
replies were quite useful.
-
Felipe Rodopoulos

Felipe Rodopoulos

2018-10-18 01:36:57 UTC

Permalink

Sorry, I should be more clear on the communication method. The
smartphones
do not use the cellular network. The communication between users and
their
phones are made through physical means instead. Agents input data
through the
smartphone camera, using QR Code and the confirmation action is the only
one
done through touch. Smartphones output data thought its screen, showing
it
to agents (who should input it to a personal computer).

My strategy was pretty similar to what G. Bella does with smartcards,
but the
difference is that the means are always secure. The protocol which I am
analyzing assumes that the Smartphones are always secure, but I am also
verifying the case where they are not. Thus, the Spy can compromise some
phones, obtaining their data and showing spoofed messages to the agents.

With this approach, I could devise the corresponding events and build a
suitable model for Smartphones, where proofs resemble the ones in the
Smartcard
theory.

The problem with the confirmation step is whether there is a message
type or
value that would reliably express this immutable acknowledgement for the
message confirmation.

I hope that the question is more clear now. Thanks in advance,

-
Felipe Rodopoulos

Post by Lawrence Paulson
Thanks for your email.
The main issue may be whether the inductive method is a good fit to
what you are working on. The network model embodied in the inductive
method is an insecure network lacking confidentiality and
authentication and where all traffic is visible to the Spy, who can
also send spoof messages using any material at his disposal. But if you
send a message to a cell phone over the cellular network, the network
provides some security guarantees, confidentiality for sure as well as
authentication for the device itself, and arguably (through the pass
code mechanism) of the user as well. It's not clear what an external
attacker can do in this context.
Larry Paulson

Post by Felipe Rodopoulos
Hello everyone,
I am formalizing a banking authorization protocol, using the Inductive Method
theory from the Isabelle/HOL library.
At a given protocol stage, the user must confirm the issued
transaction. She
receives the transaction details through her smartphone screen and, if it
matches what she first issued, she confirms the operation by clicking a button
at the screen.
The protocol document does not specify this "confirmation message" format, so I
defined one myself. Basically, it is a restatement of the transaction, followed
by an acknowledgement bit. Therefore, given the transaction is defined by its
originator name and a number (representing the transaction itself), the
(* This rule refers to smartphone *)
| DT4: "[evs4 \in sdaptrans; legalUse(Smartphone A); A != Server; ...]
==> Shows (Smartphone A) A {Agent A, Number T} # evs4 \in sdaptrans"
(* This rule refers to the user *)
| DT5: "[evs5 ∈ sdaptrans; legalUse(Smartphone A);
Says A Server {Agent A, Number T} \in set evs5;
...
Shows (Smartphone A) A {Agent A, Number T} \in set evs5]
==> Inputs A (Smartphone A) {Agent A, Number T, Confirmation} # evs5 \in sdaptrans"
abbreviation
Confirmation :: msg where "Confirmation ≡ (Number 1)"
I am not pretty sure if this is a good approach. At some lemmas, I got some
subgoals trying to replace the confirmation number by the transaction number, as
if the Spy was faking the message. For me, the ideal approach would be that the
Confirmation part would be an immutable bit, not relying in a value, but I do
not know how to properly do that. I looked at some other protocols
formalization, but I couldn't find some valuable hint.
I am open to any ideas. Thanks in advance.
Ps: I'd like to thanks Larry Paulson for answering my previous questions. The
replies were quite useful.
-
Felipe Rodopoulos

Lawrence Paulson

2018-10-18 15:55:20 UTC

Permalink

It sounds like you want to investigate the case in which some of the smartphones have been compromised by malware. Is there a reason to believe the protocol will still work? For if not, obviously, you can't hope to prove it, and if you are looking for an attack you don't need Isabelle for that.

But the model still isn't clear to me. Are you trying to verify the protocol even in the case that the current user's phone has been compromised? But in that case it's not clear what the user's acknowledgement would signify.

But in general: you can represent an event that is outside the Spy's control by using something like Notes, which the Spy has no access to in the model.

Larry Paulson

Sorry, I should be more clear on the communication method. The smartphones
do not use the cellular network. The communication between users and their
phones are made through physical means instead. Agents input data through the
smartphone camera, using QR Code and the confirmation action is the only one
done through touch. Smartphones output data thought its screen, showing it
to agents (who should input it to a personal computer).
My strategy was pretty similar to what G. Bella does with smartcards, but the
difference is that the means are always secure. The protocol which I am
analyzing assumes that the Smartphones are always secure, but I am also
verifying the case where they are not. Thus, the Spy can compromise some
phones, obtaining their data and showing spoofed messages to the agents.
With this approach, I could devise the corresponding events and build a
suitable model for Smartphones, where proofs resemble the ones in the Smartcard
theory.
The problem with the confirmation step is whether there is a message type or
value that would reliably express this immutable acknowledgement for the
message confirmation.
I hope that the question is more clear now. Thanks in advance,
-
Felipe Rodopoulos

Post by Lawrence Paulson
Thanks for your email.
The main issue may be whether the inductive method is a good fit to what you are working on. The network model embodied in the inductive method is an insecure network lacking confidentiality and authentication and where all traffic is visible to the Spy, who can also send spoof messages using any material at his disposal. But if you send a message to a cell phone over the cellular network, the network provides some security guarantees, confidentiality for sure as well as authentication for the device itself, and arguably (through the pass code mechanism) of the user as well. It's not clear what an external attacker can do in this context.
Larry Paulson

Jean Martina

2018-10-19 00:05:53 UTC

Permalink

I believe that what you want is to model this protocol as a security
ceremony by having different communication media, that is actually under
different threat models, with or without knowledge sharing between the
layers.

With that you will be able to model two different threat models for the
protocol executing on the PC and the software running on the smart-phone.

I worked with that in the past with Isabelle trying to come with a
generic modelling for human-device and human-human medium, so that you
could specify things as you explained bellow. You would only have to
place each one of the devices in a different layer. These will make the
attacks available for the phone separated from the PC for example.

Giampaolo also did some work on that, that I believe has a much more
comprehensive formalisation than mine. Instead on only having three
channels, he came up with 5 different layers (he called security
ceremony concertina) and he did some experiments with two factor
authentication.

Regards,

Jean Martina

Post by Lawrence Paulson
It sounds like you want to investigate the case in which some of the smartphones have been compromised by malware. Is there a reason to believe the protocol will still work? For if not, obviously, you can't hope to prove it, and if you are looking for an attack you don't need Isabelle for that.
But the model still isn't clear to me. Are you trying to verify the protocol even in the case that the current user's phone has been compromised? But in that case it's not clear what the user's acknowledgement would signify.
But in general: you can represent an event that is outside the Spy's control by using something like Notes, which the Spy has no access to in the model.
Larry Paulson

Sorry, I should be more clear on the communication method. The smartphones
do not use the cellular network. The communication between users and their
phones are made through physical means instead. Agents input data through the
smartphone camera, using QR Code and the confirmation action is the only one
done through touch. Smartphones output data thought its screen, showing it
to agents (who should input it to a personal computer).
My strategy was pretty similar to what G. Bella does with smartcards, but the
difference is that the means are always secure. The protocol which I am
analyzing assumes that the Smartphones are always secure, but I am also
verifying the case where they are not. Thus, the Spy can compromise some
phones, obtaining their data and showing spoofed messages to the agents.
With this approach, I could devise the corresponding events and build a
suitable model for Smartphones, where proofs resemble the ones in the Smartcard
theory.
The problem with the confirmation step is whether there is a message type or
value that would reliably express this immutable acknowledgement for the
message confirmation.
I hope that the question is more clear now. Thanks in advance,
-
Felipe Rodopoulos

Post by Lawrence Paulson
Thanks for your email.
The main issue may be whether the inductive method is a good fit to what you are working on. The network model embodied in the inductive method is an insecure network lacking confidentiality and authentication and where all traffic is visible to the Spy, who can also send spoof messages using any material at his disposal. But if you send a message to a cell phone over the cellular network, the network provides some security guarantees, confidentiality for sure as well as authentication for the device itself, and arguably (through the pass code mechanism) of the user as well. It's not clear what an external attacker can do in this context.
Larry Paulson

Post by Felipe Rodopoulos
Hello everyone,
I am formalizing a banking authorization protocol, using the Inductive Method
theory from the Isabelle/HOL library.
At a given protocol stage, the user must confirm the issued transaction. She
receives the transaction details through her smartphone screen and, if it
matches what she first issued, she confirms the operation by clicking a button
at the screen.
The protocol document does not specify this "confirmation message" format, so I
defined one myself. Basically, it is a restatement of the transaction, followed
by an acknowledgement bit. Therefore, given the transaction is defined by its
originator name and a number (representing the transaction itself), the
(* This rule refers to smartphone *)
| DT4: "[evs4 \in sdaptrans; legalUse(Smartphone A); A != Server; ...]
==> Shows (Smartphone A) A {Agent A, Number T} # evs4 \in sdaptrans"
(* This rule refers to the user *)
| DT5: "[evs5 â sdaptrans; legalUse(Smartphone A);
Says A Server {Agent A, Number T} \in set evs5;
...
Shows (Smartphone A) A {Agent A, Number T} \in set evs5]
==> Inputs A (Smartphone A) {Agent A, Number T, Confirmation} # evs5 \in sdaptrans"
abbreviation
Confirmation :: msg where "Confirmation â¡ (Number 1)"
I am not pretty sure if this is a good approach. At some lemmas, I got some
subgoals trying to replace the confirmation number by the transaction number, as
if the Spy was faking the message. For me, the ideal approach would be that the
Confirmation part would be an immutable bit, not relying in a value, but I do
not know how to properly do that. I looked at some other protocols
formalization, but I couldn't find some valuable hint.
I am open to any ideas. Thanks in advance.
Ps: I'd like to thanks Larry Paulson for answering my previous questions. The
replies were quite useful.
-
Felipe Rodopoulos

It sounds like you want to investigate the case in which some of the smartphones have been compromised by malware. Is there a reason to believe the protocol will still work? For if not, obviously, you can't hope to prove it, and if you are looking for an attack you don't need Isabelle for that.
But the model still isn't clear to me. Are you trying to verify the protocol even in the case that the current user's phone has been compromised? But in that case it's not clear what the user's acknowledgement would signify.
But in general: you can represent an event that is outside the Spy's control by using something like Notes, which the Spy has no access to in the model.
Larry Paulson

Sorry, I should be more clear on the communication method. The smartphones
do not use the cellular network. The communication between users and their
phones are made through physical means instead. Agents input data through the
smartphone camera, using QR Code and the confirmation action is the only one
done through touch. Smartphones output data thought its screen, showing it
to agents (who should input it to a personal computer).
My strategy was pretty similar to what G. Bella does with smartcards, but the
difference is that the means are always secure. The protocol which I am
analyzing assumes that the Smartphones are always secure, but I am also
verifying the case where they are not. Thus, the Spy can compromise some
phones, obtaining their data and showing spoofed messages to the agents.
With this approach, I could devise the corresponding events and build a
suitable model for Smartphones, where proofs resemble the ones in the Smartcard
theory.
The problem with the confirmation step is whether there is a message type or
value that would reliably express this immutable acknowledgement for the
message confirmation.
I hope that the question is more clear now. Thanks in advance,
-
Felipe Rodopoulos

Post by Lawrence Paulson
Thanks for your email.
The main issue may be whether the inductive method is a good fit to what you are working on. The network model embodied in the inductive method is an insecure network lacking confidentiality and authentication and where all traffic is visible to the Spy, who can also send spoof messages using any material at his disposal. But if you send a message to a cell phone over the cellular network, the network provides some security guarantees, confidentiality for sure as well as authentication for the device itself, and arguably (through the pass code mechanism) of the user as well. It's not clear what an external attacker can do in this context.
Larry Paulson

Post by Felipe Rodopoulos
Hello everyone,
I am formalizing a banking authorization protocol, using the Inductive Method
theory from the Isabelle/HOL library.
At a given protocol stage, the user must confirm the issued transaction. She
receives the transaction details through her smartphone screen and, if it
matches what she first issued, she confirms the operation by clicking a button
at the screen.
The protocol document does not specify this "confirmation message" format, so I
defined one myself. Basically, it is a restatement of the transaction, followed
by an acknowledgement bit. Therefore, given the transaction is defined by its
originator name and a number (representing the transaction itself), the
(* This rule refers to smartphone *)
| DT4: "[evs4 \in sdaptrans; legalUse(Smartphone A); A != Server; ...]
==> Shows (Smartphone A) A {Agent A, Number T} # evs4 \in sdaptrans"
(* This rule refers to the user *)
| DT5: "[evs5 â sdaptrans; legalUse(Smartphone A);
Says A Server {Agent A, Number T} \in set evs5;
...
Shows (Smartphone A) A {Agent A, Number T} \in set evs5]
==> Inputs A (Smartphone A) {Agent A, Number T, Confirmation} # evs5 \in sdaptrans"
abbreviation
Confirmation :: msg where "Confirmation â¡ (Number 1)"
I am not pretty sure if this is a good approach. At some lemmas, I got some
subgoals trying to replace the confirmation number by the transaction number, as
if the Spy was faking the message. For me, the ideal approach would be that the
Confirmation part would be an immutable bit, not relying in a value, but I do
not know how to properly do that. I looked at some other protocols
formalization, but I couldn't find some valuable hint.
I am open to any ideas. Thanks in advance.
Ps: I'd like to thanks Larry Paulson for answering my previous questions. The
replies were quite useful.
-
Felipe Rodopoulos