Email Gateway (Aug 22 2022 at 18:02): Email Gateway (Aug 22 2022 at 18:02):From: Felipe Rodopoulos <rodopoulos@aluno.unb.br>
Hello everyone,
I am using the Isabelle HOL/Auth framework and the Inductive Method
theory in
order to formalize and verify a banking authorization protocol called
DAP. The
specification employs the user's smartphone as a trusted entity for
holding
secrets (similar as the strategy adopted with smartcards in Shoup-Rubin
protocol).
Along some protocol steps, consistency checks are necessary for the
protocol
proceed, e.g, checksum verification. Therefore, for modelling this
concept, I
used basic conditional comparison between messages. The following
example rule
contains such strategy, in the last premise:
Rule: "[ evs \in model; legalUse(Smartphone A); A != Server;
Gets_s (Smartphone A) A {Transaction, r', Checksum} \in set
evs;
Checksum == Hash {Transaction, r'} ]
==> Outputs (Smartphone A) A Transaction # evs \in model"
The model specification phase went well. However, I am struggling with
some
lemmas at the verification phase, where subgoals frequently came up,
pointing to
rules with the structure presented above. In view of such situation, I
am
suspecting that the consistency premise is not suitable for what I am
trying to
achieve, which is an equality check between messages.
I checked other protocol formalizations in Isabelle HOL/Auth library,
but didn't
find anything useful. Does someone know how to properly tackle this
problem?
Another issue I am having is deciphering messages. In the rule above,
message r'
is a cipher, generated at the Server, with the following structure:
Crypt (shrK
A) (Nonce r). At one of the latter steps of the protocol, agent A's
Smartphone
needs to decipher r' in order to obtain the plaintext and send it to the
server
again, for further comparison. It posses A's private key, but I'm not
sure how
can I properly obtain Nonce r from cipher r'. That said, how can I
properly
decipher r' at the Smartphone, given that it has A's private key?
I hope I made myself clear. Thanks in advance.
Email Gateway (Aug 22 2022 at 18:07):From: Lawrence Paulson <lp15@cam.ac.uk>
I don't understand the role of checksum verification here. You write Hash{Transaction,r'}, but it looks like the data being hashed is publicly visible on the network, so the hash has no security value. It's conceivable that the protocol provides this checksum to strengthen data integrity (i.e., guarding against transmission errors), but this hash cannot guard against cryptanalytic attacks unless it involves some sort of secret. It would be reasonable at this level of abstraction to assume that there will be no transmission errors and to eliminate the hash altogether.
I wonder however whether communication between a user and their smart phone is regarded as secure from interception. (This would be similar to the smartcard case.) Make sure that your model recognises that.
Larry
Email Gateway (Aug 22 2022 at 18:07):From: Lawrence Paulson <lp15@cam.ac.uk>
You express decryption in the rules themselves. In the case of an agent A receiving a message encrypted with its own key, write the message in the rule as Crypt (shrK A) (Nonce r). In this case the contents of the message is visible. In the case of a message containing fields encrypted with other keys, write them as X, X', et cetera, to indicate that they are opaque. You will see this if you examine the existing formalisation of, for example, the Otway-Rees Protocol.
Larry
Last updated: Apr 23 2024 at 08:19 UTC