WEBVTT

1
00:00:00.000 --> 00:00:05.260
CHECK→RELEASE 是合法轉移，但故障改掉了選路條件。

2
00:00:05.260 --> 00:00:09.180
另一個請求拿交易 1 的 token，來放行交易 2。

3
00:00:09.180 --> 00:00:12.380
兩種請求都可能看起來合乎結構。

4
00:00:12.380 --> 00:00:15.000
本課追每次接受事件應具備的證據。

5
00:00:15.417 --> 00:00:18.477
轉移關係列出允許的狀態配對。

6
00:00:18.477 --> 00:00:24.957
WAIT 能進 CHECK；CHECK 依成功或失敗，選 RELEASE 或 ERROR。

7
00:00:24.957 --> 00:00:30.337
這張表能拒絕 WAIT 直接跳 RELEASE，卻不能證明 success 輸入本身可信。

8
00:00:31.137 --> 00:00:33.937
條件實驗的目前映像未授權。

9
00:00:33.937 --> 00:00:37.497
一次錯誤成功判斷讓 CHECK 選 RELEASE。

10
00:00:37.497 --> 00:00:41.077
轉移檢查器仍認得 CHECK→RELEASE。

11
00:00:41.077 --> 00:00:44.917
只查狀態或弧的接收端，在 edge 3 便接受。

12
00:00:44.917 --> 00:00:47.397
接收端還需要這次授權條件。

13
00:00:47.957 --> 00:00:49.857
狀態跳躍另測。

14
00:00:49.857 --> 00:00:54.357
一次事件在 edge 0 後把狀態設為 RELEASE，而不是 CHECK。

15
00:00:54.357 --> 00:00:58.017
Arc 政策在 edge 3 請求前送它進 ERROR。

16
00:00:58.017 --> 00:01:02.157
這條軌跡顯示弧檢查有用，但沒有消除偽造條件的反例。

17
00:01:02.500 --> 00:01:07.400
本課 token 包含 valid、交易 id 與已使用旗標。

18
00:01:07.400 --> 00:01:09.420
目前交易 id 為二。

19
00:01:09.420 --> 00:01:14.320
上一筆 id＝一的 token，即使 valid 為 true，仍已過期。

20
00:01:14.320 --> 00:01:17.800
有效許可要求 valid、id 相符且未使用。

21
00:01:17.800 --> 00:01:20.080
這些只是邏輯欄位，沒有密碼認證。

22
00:01:20.840 --> 00:01:25.180
合法目前交易在 edge 1 後，由可信驗證產生 token。

23
00:01:25.180 --> 00:01:27.420
請求可在 edge 3 commit。

24
00:01:27.420 --> 00:01:29.460
該緣之後標為已使用。

25
00:01:29.460 --> 00:01:33.680
Edge 4 再來一筆，接受前可見的 consumed 狀態就必須拒絕。

26
00:01:34.400 --> 00:01:39.560
獨立 monitor 也記錄一次交付是否已發生，不複製 DUT 的 consumed。

27
00:01:39.560 --> 00:01:43.460
重複請求情境若只看狀態，會接受兩次。

28
00:01:43.460 --> 00:01:46.480
依本課只准一次交付的契約，第二次便越權。

29
00:01:46.875 --> 00:01:49.075
每條軌跡從 WAIT 到 edge 4。

30
00:01:49.075 --> 00:01:52.555
各自只有一種命名故障效果，或重複工作負載。

31
00:01:52.555 --> 00:01:56.215
Condition 與 stale 在 CHECK 後選 RELEASE；state

32
00:01:56.215 --> 00:01:59.875
在 edge 0 後跳態；repeat 保留 RELEASE 給第二筆。

33
00:01:59.875 --> 00:02:01.495
它們沒有同時注入。

34
00:02:01.495 --> 00:02:06.255
Stale 實驗帶入 valid、id＝一的舊 token，目前 id＝二。

35
00:02:06.255 --> 00:02:09.955
情境包含保留舊證據及信任它的寬鬆判斷。

36
00:02:09.955 --> 00:02:14.335
這是協定邊界情境，不能叫單一儲存 bit XOR。

37
00:02:14.335 --> 00:02:18.315
Bound 測試中，token 欄位、可信驗證及最終 grant 不受擾。

38
00:02:18.795 --> 00:02:23.815
SCFI 在強化的下一態函數中納入控制訊號與執行歷史。

39
00:02:23.815 --> 00:02:29.235
本課普通 token 示範這個區別，沒有實作 SCFI，也不能沿用它的機率性保證。

40
00:02:29.475 --> 00:02:31.915
選 condition、arc 政策及未授權。

41
00:02:31.915 --> 00:02:36.515
Edge 3 的 RELEASE 與 commit 成立，獨立 reference 卻是 false。

42
00:02:36.515 --> 00:02:39.635
改 bound，因沒有目前有效 token，便不 commit。

43
00:02:39.635 --> 00:02:43.375
再選 stale，把 tokenId＝1 與 id＝2 一起看。

44
00:02:43.375 --> 00:02:46.035
重複請求設授權 true。

45
00:02:46.035 --> 00:02:50.215
State 在 edge 3、4 都接受，bound 只接受 edge 3。

46
00:02:50.215 --> 00:02:53.275
Bound 查授權歷史，沒有合併轉移合法性。

47
00:02:53.275 --> 00:02:58.515
因此已授權的 state jump 在 bound 下提交，arc 則拒絕。

48
00:02:58.515 --> 00:03:03.355
Arc 流跡的 edge 1 可先看到 grant，更新後才進 ERROR；請求從

49
00:03:03.355 --> 00:03:06.715
edge 3 開始，先前 grant 不代表接受。

50
00:03:06.715 --> 00:03:08.755
這些案例都有分開執行的斷言。

51
00:03:09.275 --> 00:03:14.235
正常正向交易依序經 WAIT、CHECK、RELEASE，接受一次。

52
00:03:14.235 --> 00:03:17.715
故障復原不必走一條完全沒有故障的歷史。

53
00:03:17.715 --> 00:03:23.915
產品可以在錯誤後合法復原，但後續敏感接受前，復原政策仍須建立新的授權。

54
00:03:24.235 --> 00:03:25.535
草稿尚未編譯。

55
00:03:25.535 --> 00:03:31.135
Token 儲存完整性、id 回繞、abort、reset 與並行交易，先排除。

56
00:03:31.135 --> 00:03:35.895
真正綁定方案須有足夠身分空間，避免保留窗口內碰撞。

57
00:03:35.895 --> 00:03:38.255
復原與活性也要另寫性質。

58
00:03:38.255 --> 00:03:41.095
第九課會把協定推理用於組態寫入。

59
00:03:41.402 --> 00:03:47.502
Edge 0～4；條件強制、狀態替換、舊 token 與重複工作負載分開。

60
00:03:47.502 --> 00:03:51.502
Bound 情境信任 token、驗證器及最終 grant。

61
00:03:51.502 --> 00:03:59.902
Node 已跑十組 bound 控制，另重現假條件、舊 token 與重複接受；正常授權流程接受一次。

62
00:04:00.422 --> 00:04:05.142
沒有建立 SCFI、id 回繞、多交易或實體保證。

63
00:04:05.142 --> 00:04:07.242
Token 欄位仍保持可信。