equal
deleted
inserted
replaced
3 Authors: Giampaolo Bella, Fabio Massacci, Lawrence C Paulson |
3 Authors: Giampaolo Bella, Fabio Massacci, Lawrence C Paulson |
4 *) |
4 *) |
5 |
5 |
6 header{*Purchase Phase of SET*} |
6 header{*Purchase Phase of SET*} |
7 |
7 |
8 theory Purchase = PublicSET: |
8 theory Purchase imports PublicSET begin |
9 |
9 |
10 text{* |
10 text{* |
11 Note: nonces seem to consist of 20 bytes. That includes both freshness |
11 Note: nonces seem to consist of 20 bytes. That includes both freshness |
12 challenges (Chall-EE, etc.) and important secrets (CardSecret, PANsecret) |
12 challenges (Chall-EE, etc.) and important secrets (CardSecret, PANsecret) |
13 |
13 |