Email Gateway (Aug 22 2022 at 18:37): Email Gateway (Aug 22 2022 at 18:37):From: Felipe Rodopoulos <rodopoulos@aluno.unb.br>
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
Last updated: Nov 21 2024 at 12:39 UTC