Email Gateway (Aug 22 2022 at 18:37): Email Gateway (Aug 22 2022 at 18:37):From: Lawrence Paulson <lp15@cam.ac.uk>
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
Email Gateway (Aug 22 2022 at 18:37):From: Felipe Rodopoulos <rodopoulos@aluno.unb.br>
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
Grad. student @ University of Brasília, Brazil
Email Gateway (Aug 22 2022 at 18:38):From: Lawrence Paulson <lp15@cam.ac.uk>
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
Email Gateway (Aug 22 2022 at 18:38):From: Jean Martina <jean.martina@cl.cam.ac.uk>
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
signature.asc
Last updated: Nov 21 2024 at 12:39 UTC