| Variable Current_Msg, which is mentioned in the error message (and which is the only variable that does not appear in the subscript of the next-state relation).
Stephan On 8 May 2023, at 17:24, Sara Zain <sara.zain@xxxxxxxxxxxxx> wrote:
Hi Stephan, may I know which variable you are referring to? thank you!
Regards, Sara
--------------- Dr. Sara Zain Postdoctoral Research Associate
Technische Universität Dresden,
Dept. of Computer Science, Systems Engineering Group.
Office: APB 3077 Phone: +49 351 463-42358
From: tlaplus@xxxxxxxxxxxxxxxx <tlaplus@xxxxxxxxxxxxxxxx> on behalf of Stephan Merz <stephan.merz@xxxxxxxxx>
Sent: 08 May 2023 17:10:03
To: tlaplus@xxxxxxxxxxxxxxxx
Subject: Re: [tlaplus] Parser Error Do you have any specific reason to exclude that variable from the subscript?
I also notice that that variable is not constrained by the initial condition and that the typing invariant asserts
Len(Current_Msg) = 2
whereas action Handshake requires it to be of length 1??
Stephan On 8 May 2023, at 16:52, Sara Zain <sara.zain@xxxxxxxxxxxxx> wrote:
<Screenshot from 2023-05-08 16-48-43.png>Hi all, I am getting this TLC error for the following code. Any idea please? Thank you.
Regards, Sara
_________________________________________________________ EXTENDS
\*Crypto,
Integers, FiniteSets, TLC, Sequences
CONSTANTS
Client, Server, Msg,
SK_c, SK_s, \* private keys
N, \* nonce
Certificate, \* certificate
Sig \* signature
VARIABLES
State, \* current state
Current_Msg, \* current message
Current_State \* current state of the secure channel
Init ==
/\ State = "Init"
/\ Current_State = << SK_c, SK_s, N, Certificate, Sig >>
Handshake ==
/\ State = "Handshake"
/\ Current_Msg = << "Hello" >>
/\ Current_State[6] = <<Certificate, Sig>> \* send certificate and signature
/\ State' = "Finished"
/\ UNCHANGED << Current_State, Current_Msg >>
DataTransfer ==
/\ State = "Finished"
/\ Current_Msg = << "Data", "Secret message" >>
(*/\ S[6] = Encrypt(S[2], S[5], M[2], S[6])*) \* encrypt message with server's key
/\ State' = "Closed"
/\ UNCHANGED << Current_State, Current_Msg >>
Next == Handshake \/ DataTransfer
InitStates == << Init >>
NextStates == Next
SecureChannelInvariant ==
/\ Current_State[1] # Current_State[2] \* private keys are different
/\ Current_State[3] # N \* nonce is different each time
/\ Len(Current_State[4]) > 0 \* certificate is not empty
/\ Len(Current_State[5]) > 0 \* signature is not empty
/\ Len(Current_State[6]) > 0 \* IV is not empty
TypeOK ==
/\ State \in {"Init", "Handshake", "Finished", "Closed"}
/\ Len(Current_Msg) = 2
/\ Current_Msg[1] \in {"Hello", "Data"}
SecureChannel ==
/\ State = "Handshake" => Len(Current_State) = 6
/\ State = "Finished" => Len(Current_State) = 7
/\ State = "Closed" => Len(Current_State) = 7
/\ SecureChannelInvariant
NextStep == Next /\ TypeOK
Spec == Init /\ [][NextStep]_<<State, Current_State>>
On Monday, May 1, 2023 at 8:38:27 PM UTC+2 hwa...@ gmail.com wrote: Parser really needs to show line numbers :/
H
On Friday, April 28, 2023 at 4:59:12 AM UTC-5 Stephan Merz wrote:
Typo “Intergers”
Stephan Hi! I just downloaded the TLA toolbox. However, I am getting this error "Parser error" notification. Can anyone help me, please? Also, I don't see a TLA module and directory path compare to what I see in the video tutorial. <Screenshot from 2023-04-28 11-31-09.png>
-- You received this message because you are subscribed to the Google Groups "tlaplus" group. To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx. To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/f247500f-7679-4f68-8d62-920b5f2f945bn%40googlegroups.com. <Screenshot from 2023-04-28 11-31-09.png>
-- You received this message because you are subscribed to the Google Groups "tlaplus" group.To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/d60e90ec-1339-4d45-9260-4f7cb183028cn%40googlegroups.com.<Screenshot from 2023-05-08 16-48-43.png>
-- You received this message because you are subscribed to the Google Groups "tlaplus" group. To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx. To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/C0478BD4-0471-4F7F-8BFB-545A746CDEBA%40gmail.com.
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/4426543A-87C0-4669-8F13-BA14F4668BDF%40gmail.com.
|